(** * 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.