(** * TP 6 : Accessibility, induction in HA again, pigeons. *)
(* To build an html version of the TD sheet, use the command
   "coqdoc -utf8 --no-lib-name --no-index --lib-subtitles file.v" *)

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

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

(** 9) Define [lt2] the lexicographic product of [<]. **)
Definition lt2 : relation (nat*nat) := fun _ _ => True (* un peu facile non ? *).

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.
Admitted.

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

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

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

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

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

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

End Inverse_image.

(** *** Transitive closure **)

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

Inductive trans A (R : relation A) : relation A := (* tiens bah *).

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

(** 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 W x; apply Acc_trans, W.
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) := fun _ _ => True (* décidément *).


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


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





(************************************)
(** *  On Induction in Arithmetic  **)
(************************************)

(** The idea of this part is to prove some results about Heyting arithmetic.
    Since we want to prove everything without relying on the standard library,
    we define our set of natural numbers [Nat]. **)

(** ** Axiomatisation of (some part of) Heyting arithmetic **)
Parameter Nat : Set.

(** Function and relation symbols **)
Parameter Succ : Nat -> Nat.
Parameter Zero : Nat.
Parameter Lt : Nat -> Nat -> Prop.
Notation "x < y" := (Lt x y).

(** Axioms **)
Axiom Induction : forall P : Nat -> Prop,
  P Zero -> (forall x, P x -> P (Succ x)) -> forall x, P x.

Axiom NonConf : forall x, ~ Succ x = Zero.
Axiom SuccInj : forall x y, Succ x = Succ y -> x = y.

Axiom Not_Lt_Zero : forall x, ~ (x < Zero).
Axiom Lt_Succ_disj : forall x y, y < Succ x -> y < x \/ y = x.
Axiom Lt_Succ : forall x, x < Succ x.
Axiom Lt_trans : forall x y z, x < y -> y < z -> x < z.

(** Our goal is to prove:
    - decidability of equality
    - well-founded induction
    - equivalence of excluded middle and the minimum principle **)

(** *** Some basic results about [Succ]  and [<] **)

(** As a warm-up, prove the following lemmata. **)
Lemma Zero_or_Succ : forall x, x = Zero \/ exists y, x = Succ y.
Proof.
  (* preuves gratuites que vous avez déjà faites *)
  apply Induction.
    left; auto.
    
    intros x uselessIH.
    clear uselessIH.
    right; exists x; auto.
Qed.

Lemma Succ_Not_Idempotent : forall x, ~ Succ x = x.
Proof.
  apply Induction.
    apply NonConf.
    
    intros x Dx Dsx.
    apply Dx.
    apply SuccInj.
    auto.
Qed.

Lemma Lt_Zero_Succ : forall x, Zero < Succ x.
Proof.
  apply Induction.
    apply Lt_Succ.
    
    intros x H; eapply Lt_trans.
      apply H.
      
      apply Lt_Succ.
Qed.


(** **  Decidability of equality  **)

(** Find the statement expressing that equality in Heyting arithmetic is
    decidable (Remember: we are in intuitionistic logic).
    Prove it. **)

Theorem EqDec : forall a b : Nat, a = b \/ ~ a = b.
Proof.
  (* pareil, la preuve ci-dessous vous est offerte *)
  pose (P := fun a  => forall b : Nat, a = b \/ ~ a = b).
  assert (NonConf2 : forall x, ~ Zero = Succ x)
      by (intros ? ?; eapply NonConf; symmetry; eassumption).
  pose proof Succ_Not_Idempotent.
  apply (Induction P); unfold P.
    apply Induction.
      auto.
      intros x _. auto.
    
    intros a IH.
    apply Induction.
      right; now auto.
      intros b _.
      destruct (IH b) as [ E | D ]; [ left | right ].
        subst; auto.
        intros E; apply SuccInj in E; auto.
Qed.

(** ** Well founded induction **)

(** Let us start with the most obvious proof sketch. **)
Theorem WF_Induction : forall P : Nat -> Prop,
  (forall x, (forall y, y < x -> P y) -> P x) -> forall x, P x.
Proof.
(* The following direct induction seems to be deemed to fail *)
  intros P HP.
  apply Induction.
    apply HP. intros y ?. exfalso. apply (Not_Lt_Zero _ H).
    
    intros x Hx.
    (* ?? *)
Abort.

(** 1) Where does the problem comes from? How can we strenghten the induction
       hypothesis to avoid it?
       Prove the lemma with the strengthened hypothesis. **)
Lemma WF_Pre_ind : forall P : Nat -> Prop,
  (* l'hypothèse renforcée vous est offerte aussi. *)
  (forall x, (forall y, y < x -> P y) -> P x) ->
    forall x, forall y, y < x -> P y.
Proof.
Admitted.

(** 2) Conclude by proving well-founded induction for [Nat]. **)
Theorem wf_Nat_ind : forall P : Nat -> Prop,
  (forall x, (forall y, y < x -> P y) -> P x) -> forall x, P x.
Proof.
Admitted.

(** ** In HA, the minimum principle is equivalent to the excluded middle **)

Definition MinP (P : Nat -> Prop) : Prop :=
  (exists x, P x) ->
  exists x, P x /\ forall y, y < x -> ~ P y.

(** 1) Prove that excluded middle implies the minimum principle. **)
Theorem EM_MinP : (forall P, P \/ ~P) -> forall A, MinP A.
Proof.
Admitted.

(** 2) For the converse implication, we will use the minimum principle on the
    following proposition:
    [[
      Q x := x = Zero ∧ P ∨ x = Succ Zero ∧ ¬P ∨ x = Succ (Succ Zero)
    ]]
    Using this trick, prove the converse implication.
    **)
(* We follow [Troelstra & van Dalen] *)
Theorem MinP_EM : (forall A, MinP A) -> forall P, P \/ ~ P.
Proof.
Admitted.


(** ** Double negation of excluded middle and of the minimum principle **)

(** 1) Prove the double negation of excluded middle. **)
Lemma NotNotEM : forall A, ~ ~ (A \/ ~ A).
Proof.
Admitted.

(** For the double negation of the minimum principle,
    we will use an alternate fomulation of ¬¬ MinP:
    [[
      ∀P (x : Nat), P x → ¬¬(∃ x, P x /\ ∀ y, y < x → ¬P y).
    ]]
    **)
Definition NotNotMinP_alt (P : Nat -> Prop) :=
  forall x, P x -> ~ ~ exists x, P x /\ forall y, y < x -> ~ P y.

(** 2) Prove the following lemma and then that the alternate formulation
       implies ¬¬MinP. **)
Definition forallP_exP : forall T (A : T -> Prop) (P : Prop),
  (forall x, A x -> P) -> (exists x, A x) -> P.
Proof.
Admitted.

Lemma NotNotMinP_aux : forall P : Nat -> Prop, NotNotMinP_alt P -> ~~MinP P.
Proof.
Admitted.

(** 3) To prove the alternate formulation, we note that
       on a doubly negated statement, we can use excluded middle. **)
Lemma NotNot_EM : forall P A, ((P \/ ~P) -> ~~A) -> ~~A.
Proof.
Admitted.

(** 4) Now prove the alternate formulation and conclude. **)
Theorem NotNotMinP_Shift : forall P, NotNotMinP_alt P.
Proof.
Admitted.

Corollary NotNotMinP : forall P, ~~MinP P.
Proof.
Admitted.


(** ** Definition of [<] by [+] **)

(** Finally, we prove that by defining
    [[
      x < y := exists z, Succ z + x = y
    ]]
    we get an order satisfying all the axioms we used do far. **)

(** Definition of [+] and its properties **)
Parameter Plus : Nat -> Nat -> Nat.
Notation "x + y" := (Plus x y).
Axiom PlusZero : forall x, Zero + x = x.
Axiom PlusSucc : forall x y, Succ x + y = Succ (x + y).
Notation "x < y" := (exists z, Succ z + x = y).

(** Prove the four lemmata. **)
Lemma Not_PLt_Zero : forall x, ~ (x < Zero).
Proof.
Admitted.

Lemma PLt_Succ : forall x, x < Succ x.
Proof.
Admitted.

Lemma PLt_Succ_disj : forall x y, y < Succ x -> y < x \/ y = x.
Proof.
Admitted.

Axiom Plus_assoc :  forall x y z, x + (y + z) = x + y + z. (* indice *)

Lemma PLt_trans : forall x y z, x < y -> y < z -> x < z.
Proof.
Admitted.



(*************************************)
(** * Infinite pigeonhole principle **)
(*************************************)

(* statement: if X is infinite and is covered by k Ai, then one Ai is infinite *)

Require Import Omega.
Open Scope nat_scope.
Definition infinite (P : nat -> Prop) := forall x, exists y, x < y /\ P y.

Section IPP.
  Hypothesis Absurd : forall A, (~ ~ A) -> A.
  Variable X : nat -> Prop.
  Hypothesis Xu : infinite X.
  Variable A : nat -> nat -> Prop.
  Variable k : nat.
  Hypothesis Xcovered : forall x, X x -> exists i, i <= k /\ A i x.
  
  Theorem IPP : exists i, i <= k /\ infinite (A i).
  Proof.
    (* vous aurez peut-être besoin de quelques lemmes. *)
  Admitted.
End IPP.