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



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



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.

Lemma Succ_Not_Idempotent : forall x, ~ Succ x = x.

Lemma Lt_Zero_Succ : forall x, Zero < Succ x.


(** **  Decidability of equality  **)

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


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

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


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

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


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

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

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

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

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

Corollary NotNotMinP : forall P, ~~MinP P.


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

Lemma PLt_Succ : forall x, x < Succ x.

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

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