# tp3

# From last week

- P ∧ (Q ∨ R) → (P ∧ Q) ∨ (P ∧ R)
- ((P ∨ Q) → R) → (P → R) ∧ (Q → R)
- (P → R) ∨ (Q → R) → P ∧ Q → R

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

# On Induction in Arithmetic

## Axiomatisation of (some part of) Heyting arithmetic

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.

Admitted.

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

Admitted.

Lemma Lt_Zero_Succ : forall x, Zero < Succ x.

Admitted.

Admitted.

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

Admitted.

Lemma Lt_Zero_Succ : forall x, Zero < Succ x.

Admitted.

## Decidability of equality

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.

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.

Admitted.

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

Admitted.

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.

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)

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

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.

Admitted.

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

Admitted.

(forall x, A x -> P) -> (exists x, A x) -> P.

Admitted.

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

Admitted.

3) To prove the alternate formulation, we note that
on a doubly negated statement, we can use excluded middle.

4) Now prove the alternate formulation and conclude.

Theorem NotNotMinP_Shift : forall P, NotNotMinP_alt P.

Admitted.

Corollary NotNotMinP : forall P, ~~MinP P.

Admitted.

Admitted.

Corollary NotNotMinP : forall P, ~~MinP P.

Admitted.

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

Admitted.

Lemma PLt_Succ : forall x, x < Succ x.

Admitted.

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

Admitted.

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

Admitted.

Admitted.

Lemma PLt_Succ : forall x, x < Succ x.

Admitted.

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

Admitted.

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

Admitted.

This page has been generated by coqdoc