(** * TD03 : Curry-Howard & induction in HA *)
(* To build an html version of this exercise sheet, use the command
   "coqdoc -utf8 --no-lib-name --no-index --lib-subtitles TD03.v" *)


(************************)
(** *  From last week  **)
(************************)

(** Using the Curry-Howard isomorphism, find λ-terms proving
    the following formulæ.
    - [P ∧ (Q ∨ R) → (P ∧ Q) ∨ (P ∧ R)]
    - [((P ∨ Q) → R) → (P → R) ∧ (Q → R)]
    - [(P → R) ∨ (Q → R) → P ∧ Q → R] **)
Section CurryHoward.
Variables P Q R : Prop.

Definition ex1 : P /\ (Q \/ R) -> (P /\ Q) \/ (P /\ R) :=
  fun x => match proj2 x with
             | or_introl q => or_introl (conj (proj1 x) q)
             | or_intror r => or_intror (conj (proj1 x) r)
           end.

Definition ex2 : ((P \/ Q) -> R) -> (P -> R) /\ (Q -> R) :=
  fun f => conj (fun p => f (or_introl p))  (fun q => f (or_intror q)).

Definition ex3 : ((P -> R) \/ (Q -> R)) -> P /\ Q -> R :=
  fun x y => match x with
               | or_introl f => f (proj1 y)
               | or_intror g => g (proj2 y)
             end.

(** Prove the following statements in natural deduction (on paper).
    What are the corresponding λ-terms ?
    - [¬¬P → ¬¬Q → ¬¬(P ∧ Q)]
    - [(P → ¬¬Q) → ¬¬(P → Q)]
    - [(P → ¬¬Q) → ¬¬P → ¬¬Q] **)
Lemma and_weak : ~~P -> ~~Q -> ~~(P /\ Q).
Proof.
intros nnP nnQ nPQ.
(* we can switch the order *)
apply nnP. intro p. apply nnQ. intro q.
apply nPQ. split; assumption.
Qed.

(* Already defined in Coq ≥ 8.3 *)
Ltac exfalso := apply False_ind.

Lemma imp_strong : (P -> ~~Q) -> ~~(P -> Q).
Proof.
intros PnnQ nPQ. apply nPQ. intro p.
exfalso. (* here we use the ex falso quod libet *)
apply (PnnQ p). intro q. apply nPQ. intros _. exact q.
Qed.

Lemma imp_weak : (P -> ~~Q) -> ~~P -> ~~Q.
Proof.
intros PnnQ nnP nQ. apply nnP. intro p. revert nQ. now apply PnnQ. Qed.
End CurryHoward.


(************************************)
(** *  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 standrad 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,
  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.
apply Induction.
  now left.
  intros x _. right. now exists x.
Qed.

Lemma Succ_Not_Idempotent : forall x, ~ Succ x = x.
Proof.
apply Induction.
  now apply NonConf.
  intros x IH H. apply IH. now apply SuccInj.
Qed.

Lemma Lt_Zero_Succ : forall x, Zero < Succ x.
Proof.
apply Induction.
  now apply Lt_Succ.
  intros x H. apply (Lt_trans Zero _ _ 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 x y : Nat, x = y \/ ~ x = y.
Proof.
apply (Induction (fun x => forall y : Nat, x = y \/ ~ x = y)).
  (* x = 0 *)
  apply Induction.
    now left.
    intros x _. right. intro. now apply (NonConf x).
  (* x > 0 *)
  intros x IH. apply Induction.
    right. now apply NonConf.
    intros z [HxSz | HxSz].
    (* Succ x = z *)
    right. intro H. apply (Succ_Not_Idempotent z). now rewrite <- H.
    (* Succ x ≠ z *)
    destruct (IH z) as [Hxz | Hxz].
      (* x = z *)
      left. now subst.
      (* x ≠ z *)
      right. intro H. apply Hxz. now apply SuccInj.
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 y). assumption.
  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,
  (forall x, (forall y, y < x -> P y) -> P x) ->
  forall x, forall y, y < x -> P y.
Proof.
intros P H. apply (Induction (fun x => forall y, y < x -> P y)).
  intros y Hlt. elim Not_Lt_Zero with y. exact Hlt.
  intros x IH y Hlt.
  destruct (Lt_Succ_disj x y Hlt) as [Hyx | Hyx].
    apply IH. apply Hyx.
    apply H. rewrite Hyx. apply IH.
Qed.

(** 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.
intros P H x.
apply WF_Pre_ind with (Succ x).
  apply H.
  apply Lt_Succ.
Qed.


(** ** 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.
intros EM A HexA.
destruct (EM (exists x, A x /\ forall y, y < x -> ~ A y)) as [Goal | Habs].
  easy.
  assert (forall x, ~ A x) as HContr.
    apply wf_Nat_ind. intros x ? ?. apply Habs. exists x. now split.
  destruct HexA as [x HAx]. elim (HContr x HAx).
Qed.

(** 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.
intros HMinP P.
pose (Q x := x = Zero /\ P \/ x = Succ Zero /\ ~ P \/ x = Succ (Succ Zero)).
assert (HexQ : exists x, Q x). exists (Succ (Succ Zero)). now do 2 right.
destruct (HMinP Q HexQ) as [x [Hx HMin]].
destruct Hx as [[_ H] | [[_ H] | H]].
  now left.
  now right.
(* By MinP we have [~ (P \/ ~ ~P)], ie [~ P] and [~ ~ P] *)
  elim (HMin (Succ Zero)). rewrite H. now apply Lt_Succ.
  right. left. split. easy. intro HP.
  apply (HMin Zero). rewrite H. apply Lt_Zero_Succ.
  left. split. easy. apply HP.
Qed.


(** ** 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. intros ? HK. apply HK. right. intro. apply HK. now left. Qed.

(** 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. intros T A P H [x Hx]. now apply (H x). Qed.

Lemma NotNotMinP_aux : forall P : Nat -> Prop, NotNotMinP_alt P -> ~~MinP P.
Proof. intros P HP. apply imp_strong. apply forallP_exP. exact HP. Qed.

(** 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. intros P A H. cut (~~(P \/ ~P)). now apply imp_weak. apply NotNotEM. Qed.

(** 4) Now prove the alternate formulation and conclude. **)
Theorem NotNotMinP_Shift : forall P, NotNotMinP_alt P.
Proof.
intro P. unfold NotNotMinP_alt.
apply (wf_Nat_ind (fun x => P x -> ~~exists x, P x /\ forall y, y < x -> ~ P y)).
intros x IH HPx.
apply (NotNot_EM (exists y, y < x /\ P y)).
intros [[y [? ?]] | HNy].
  now apply IH with y.
(* [~ exists y, y < x /\ P y] implies [forall y, y < x -> ~ P y] *)
  intro H. apply H. exists x. split. apply HPx.
  intros y Hyx HPy. apply HNy. exists y. now split.
Qed.

Corollary NotNotMinP : forall P, ~~MinP P.
Proof. intro. apply NotNotMinP_aux. apply NotNotMinP_Shift. Qed.


(** ** 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.
intros x [z Hz]. rewrite PlusSucc in Hz. now elim NonConf with (z + x).
Qed.

Lemma PLt_Succ : forall x, x < Succ x.
Proof. intro x. exists Zero. rewrite PlusSucc. now rewrite PlusZero. Qed.

Lemma PLt_Succ_disj : forall x y, y < Succ x -> y < x \/ y = x.
Proof.
intros x y H. destruct H as [z H].
destruct (Zero_or_Succ z) as [HZ | Hlt].
  right. apply SuccInj. 
  rewrite HZ in H. rewrite PlusSucc in H. now rewrite PlusZero in H.
  left. destruct Hlt as [t Heq]. exists t. apply SuccInj.
  rewrite <- H. rewrite Heq. now rewrite <- PlusSucc.
Qed.

Axiom Plus_assoc :  forall x y z, x + (y + z) = x + y + z.
Lemma PLt_trans : forall x y z, x < y -> y < z -> x < z.
Proof.
intros x y z [a Ha] [b Hb]. exists (b + Succ a).
rewrite <- PlusSucc. rewrite <- Hb. rewrite <- Plus_assoc. now f_equal.
Qed.