# TP03: Curry-Howard & induction in HA

# From last week

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

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

## 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).

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.

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:
As a warm-up, prove the following lemmata.

- decidability of equality
- well-founded induction
- equivalence of excluded middle and the minimum principle

### Some basic results about Succ and <

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.

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

Lemma Lt_Zero_Succ : forall x, Zero < Succ x.

## Decidability of equality

Theorem EqDec : ...

Theorem WF_Induction : forall P : Nat -> Prop,

(forall x, (forall y, y < x -> P y) -> P x) -> forall x, P x.

Proof.

intros P HP. apply Induction.

apply HP. intros y ?. exfalso. apply (Not_Lt_Zero y). assumption.

intros x Hx.

Abort.

(forall x, (forall y, y < x -> P y) -> P x) -> forall x, P x.

Proof.

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.

(forall x, (forall y, y < x -> P y) -> P x) -> forall x, P x.

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.

Q x := x = Zero ∧ P ∨ x = Succ Zero ∧ ¬P ∨ x = Succ (Succ Zero)

Theorem MinP_EM : (forall A, MinP A) -> forall P, P \/ ~ P.

## Double negation of excluded middle and of the minimum principle

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

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

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.

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

Corollary NotNotMinP : forall P, ~~MinP P.

## Definition of < by +

x < y := exists z, Succ z + x = y

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

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.

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.

This page has been generated by coqdoc