(** * TP05 : Dependent pattern matching *)
(* To build an html version of the TD sheet, use the command
"coqdoc -utf8 --no-lib-name --no-index --lib-subtitles TP05.v" *)
(************************************)
(** * Dependent pattern-matching **)
(************************************)
(** The most general form of pattern matching in Coq is
[[
match t as n in T return P with ...
]]
where
- [t] is the term to be destructed
- [n] is a name used to refer to [t] (used when it is an application)
- [T] is the type of [t], in case it contains terms that need to be
bound for the matching branches (dependent types)
- [P] is the elimination predicate, the type of the matching branches
(necessary when it differs between branches and cannot be infered)
1) Define a type [listn T n] of lists of size [n] containing
elements of type [T].
You can draw inspiration from Coq's type [list]. **)
(** 2) Write a concatenating function for this type by directly writing
its term (i.e. without using the tactic mode).
You will need the full power of pattern matching. **)
(********************************)
(** * The "injection" tactic **)
(********************************)
(** We want to see how the "injection" tactic works.
Remember that "injection" is used to show injectivity of constructors
of an inductive type: a term of an inductive type built with a
constructor "c₁" cannot be equal to a term built with constructor
"c₂" different from "c₁". **)
(** For simplicity we take an inductive type with 2 constructors. **)
Inductive Two : Set := Zero | One.
(** 3) Define the elimination function of the equality type by directly
writing its term. This function takes proofs of [P x] and [x = y]
and returns a proof of [P y]. **)
Definition eq_elim (A : Type) (P : A -> Prop) (x y : A)
(Px : P x) (equality : x = y) : P y := ...
(** The crucial part for [diff] is "strong elimination" :
it allows building a type (here a [Prop])
by pattern matching values from a small type like [nat]. **)
Definition diff (P Q : Prop) x : Prop :=
match x with
| Zero => P
| One => Q
end.
(** 4) Give now the proof term that says [Zero <> One]. **)
Definition NonConf : Zero = One -> False := ...