(** * 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]. **)
Inductive listn (A : Type) : nat -> Type :=
| niln : listn A 0
| consn (n : nat) (x : A) (l : listn A n) : listn A (S n).
(** 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. **)
Fixpoint concat (A : Type) (n₁ n₂ : nat) (l₁ : listn A n₁) (l₂ : listn A n₂) :=
match l₁ in listn _ n return listn A (n + n₂) with
| niln => l₂
| consn k x l => consn A (k + n₂) x (concat A k n₂ l l₂)
end.
(********************************)
(** * 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 :=
match equality in eq _ y return P y with
| refl_equal => Px
end.
(** You can omit the [in eq _ y return P y] part of mattern matching
because Coq is smart enough to infer it. **)
(** 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 :=
fun H => eq_elim Two (diff True False) Zero One I H.