(** * TP 5 : Dependent pattern matching and accessibility  *)
(* To build an html version of the TD sheet, use the command
   "coqdoc -utf8 --no-lib-name --no-index --lib-subtitles file.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 := ...


(******************************************)
(** *  The [Acc] accessiblity predicate  **)
(******************************************)

(** In previous sessions, we used well-foundedness to prove properties
    and to define recursive functions.
    Let us now take a closer look at what it means:
    [Print well_founded.] returns
    [[
      well_founded = 
      fun (A : Type) (R : A -> A -> Prop) => forall a : A, Acc R a
           : forall A : Type, (A -> A -> Prop) -> Prop
      
      Argument A is implicit
      Argument scopes are [type_scope _]
    ]]
    which means that a relation [R : A -> A -> Prop] is well founded
    if all its elements are accessible: [forall a : A, Acc R a].

    Being accessible is in turn defined by
    [[
      Inductive Acc (A : Type) (R : A -> A -> Prop) (x : A) : Prop :=
          Acc_intro : (forall y : A, R y x -> Acc R y) -> Acc R x
    ]]
    saying that if all predecessors of [x] by [R] are accessible,
    then [x] is accessible too. **)

(** 5) How does the accessibility property start off? **)

(** When we want to prove [Acc] for an element [x], we usually start
    by inspecting the shape of [x] (especially if [A] is inductive).
    With the shape of [x], we know if [R y x] can hold or not.

    Keep in mind that [Acc] is an inductive predicate, so you can always
    use induction on a proof of [Acc x] to prove another property. **)


(** ** First example: [lt] and its lexicographic product. **)

Require Import Relations.
Require Import Arith.
Require Import Omega.
(** The following line turn implicit all arguments that can be infered
    from other arguments, this removing the need to explicitely tag 
    them with [{ }]. **)
Set Implicit Arguments.

(** 6) As an example, prove the lemmas [Acc lt 0], [Acc lt 1],
       and [Acc lt 2]. **)

(** 7) What is the structure of a proof of [Acc lt n]? **)

(** 8) Prove (on paper) that any natural number is accessible by [<].
       Then (and only then), translate this proof to Coq. **)
Theorem lt_wf : well_founded lt.
Proof.
...
Qed.

(** 9) Define [lt2] the lexicographic product of [<]. **)
Definition lt2 : relation (nat*nat) := ...

Notation "x << y " := (lt2 x y) (at level 70).

(** 10) Prove that [lt2] is a strict order, i.e. is irreflexive and
       transitive.

       You can use [SearchPattern] or [SearchAbout] to look for lemmas
       you might need about [lt] and [le]. **)

(** 11) Prove (on paper) that the strict lexicographic ordering on
       [nat*nat] is well-founded.
       Then (and only then) translate this proof to Coq. **)
Lemma lt2_wf : well_founded lt2.
Proof.
...
Qed.

(** ** Operations on well founded relations **)

(** 12) Prove the inversion lemma for [Acc]. **)
Lemma Acc_inv : forall (A : Type) (R : relation A) x y, R x y -> Acc R y -> Acc R x.
Proof.
...
Qed.

(** *** Sub-relation **)

(** 13) Define relation inclusion.  **)
Definition rel_incl (A : Type) (R S : relation A) := ...

(** 14) Prove that if [R] is included in [S] and [S] is well-founded,
        then [R] is well-founded. **)
Theorem rel_incl_wf (A : Type) (R S : relation A) :
  rel_incl R S -> well_founded S -> well_founded R.
Proof.
...
Qed.

(** *** Inverse image **)

Section Inverse_image.
Variables (A B : Type) (R : relation B) (f : A -> B).

Definition R' x y := R (f x) (f y).

(** 15) Prove the following lemma relating [Acc R] and [Acc R']. **)
Lemma Acc_inverse_eq : forall y, Acc R y -> forall x, y = (f x) -> Acc R' x.
Proof.
...
Qed.

(** 16) Deduce from this lemma that the reverse image of a well-founded
        relation by any function is a well-founded relation. **)
Lemma wf_inverse_image : well_founded R -> well_founded R'.
Proof.
...
Qed.
End Inverse_image.

(** *** Transitive closure **)

(** 17) Define the (non-reflexive) transitive closure operator. **)

(** 18) Prove that if [x] is accessible by [R] then [x] is accessible
        from the transitive closure of [x].
        You will need the lemma [Acc_inv]. **)
Lemma Acc_trans (A : Type) (R : relation A) :
  forall x, Acc R x -> Acc (trans R) x.
Proof.
...
Qed.

(** 19) Prove that if [R] is well-founded, then its transitive closure
        is well-founded. **)
Theorem wf_trans : forall (A : Type) (R : relation A),
  well_founded R -> well_founded (trans R).
Proof. intros A R wfR x. apply Acc_trans. apply wfR. Qed.

(** *** Lexicographic product **)

(** 20) Define the lexicographic product of two relations. **)
Definition lexprod (A B : Type) (RA : relation A) (RB : relation B)
  : relation (A*B) := ...


(** 21) prove that the lexicographic product of two well-founded relations
        is a well-founded relation. **)
Theorem lexprod_wf  (A B : Type) (RA : relation A) (RB : relation B) :
  well_founded RA -> well_founded RB -> well_founded (lexprod RA RB).
Proof.
...
Qed.

(** 22) Bonus: What about the dependent lexicographic product?
        (i.e. when the type of the second component of the pair depends
        on the value of the first component) **)