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