# tp6

# The Acc accessiblity predicate

well_founded =

fun (A : Type) (R : A -> A -> Prop) => forall a : A, Acc R a

: forall A : Type, (A -> A -> Prop) -> Prop

Argument A is implicit

Argument scopes are [type_scope _]

Inductive Acc (A : Type) (R : A -> A -> Prop) (x : A) : Prop :=

Acc_intro : (forall y : A, R y x -> Acc R y) -> Acc R x

## First example: lt and its lexicographic product.

6) As an example, prove the lemmas Acc lt 0, Acc lt 1,
and Acc lt 2.
7) What is the structure of a proof of Acc lt n?
8) Prove (on paper) that any natural number is accessible by <.
Then (and only then), translate this proof to Coq.

9) Define lt2 the lexicographic product of <.

Definition lt2 : relation (nat*nat) := fun _ _ => True .

Notation "x << y " := (lt2 x y) (at level 70).

Notation "x << y " := (lt2 x y) (at level 70).

10) Prove that lt2 is a strict order, i.e. is irreflexive and
transitive.
You can use SearchPattern or SearchAbout to look for lemmas
you might need about lt and le.
11) Prove (on paper) that the strict lexicographic ordering on
nat*nat is well-founded.
Then (and only then) translate this proof to Coq.

Lemma Acc_inv : forall (A : Type) (R : relation A) x y, R x y -> Acc R y -> Acc R x.

Proof.

Admitted.

Proof.

Admitted.

14) Prove that if R is included in S and S is well-founded,
then R is well-founded.

Theorem rel_incl_wf (A : Type) (R S : relation A) :

rel_incl _ R S -> well_founded S -> well_founded R.

Proof.

Admitted.

rel_incl _ R S -> well_founded S -> well_founded R.

Proof.

Admitted.

Section Inverse_image.

Variables (A B : Type) (R : relation B) (f : A -> B).

Definition R' x y := R (f x) (f y).

15) Prove the following lemma relating Acc R and Acc R'.

16) Deduce from this lemma that the reverse image of a well-founded
relation by any function is a well-founded relation.

18) Prove that if x is accessible by R then x is accessible
from the transitive closure of x.
You will need the lemma Acc_inv.

Lemma Acc_trans (A : Type) (R : relation A) :

forall x, Acc R x -> Acc (trans _ R) x.

Proof.

Admitted.

forall x, Acc R x -> Acc (trans _ R) x.

Proof.

Admitted.

19) Prove that if R is well-founded, then its transitive closure
is well-founded.

Theorem wf_trans : forall (A : Type) (R : relation A),

well_founded R -> well_founded (trans _ R).

Proof.

intros A R W x; apply Acc_trans, W.

Qed.

well_founded R -> well_founded (trans _ R).

Proof.

intros A R W x; apply Acc_trans, W.

Qed.

Definition lexprod (A B : Type) (RA : relation A) (RB : relation B)

: relation (A*B) := fun _ _ => True .

: relation (A*B) := fun _ _ => True .

21) prove that the lexicographic product of two well-founded relations
is a well-founded relation.

Theorem lexprod_wf (A B : Type) (RA : relation A) (RB : relation B) :

well_founded RA -> well_founded RB -> well_founded (lexprod _ _ RA RB).

Proof.

Admitted.

well_founded RA -> well_founded RB -> well_founded (lexprod _ _ RA RB).

Proof.

Admitted.

22) Bonus: What about the dependent lexicographic product?
(i.e. when the type of the second component of the pair depends
on the value of the first component)
The idea of this part is to prove some results about Heyting arithmetic.
Since we want to prove everything without relying on the standard library,
we define our set of natural numbers Nat.

# 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 : Nat -> Prop,

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.

Proof.

apply Induction.

left; auto.

intros x uselessIH.

clear uselessIH.

right; exists x; auto.

Qed.

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

Proof.

apply Induction.

apply NonConf.

intros x Dx Dsx.

apply Dx.

apply SuccInj.

auto.

Qed.

Lemma Lt_Zero_Succ : forall x, Zero < Succ x.

Proof.

apply Induction.

apply Lt_Succ.

intros x H; eapply Lt_trans.

apply H.

apply Lt_Succ.

Qed.

Proof.

apply Induction.

left; auto.

intros x uselessIH.

clear uselessIH.

right; exists x; auto.

Qed.

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

Proof.

apply Induction.

apply NonConf.

intros x Dx Dsx.

apply Dx.

apply SuccInj.

auto.

Qed.

Lemma Lt_Zero_Succ : forall x, Zero < Succ x.

Proof.

apply Induction.

apply Lt_Succ.

intros x H; eapply Lt_trans.

apply H.

apply Lt_Succ.

Qed.

## Decidability of equality

Theorem EqDec : forall a b : Nat, a = b \/ ~ a = b.

Proof.

pose (P := fun a => forall b : Nat, a = b \/ ~ a = b).

assert (NonConf2 : forall x, ~ Zero = Succ x)

by (intros ? ?; eapply NonConf; symmetry; eassumption).

pose proof Succ_Not_Idempotent.

apply (Induction P); unfold P.

apply Induction.

auto.

intros x _. auto.

intros a IH.

apply Induction.

right; now auto.

intros b _.

destruct (IH b) as [ E | D ]; [ left | right ].

subst; auto.

intros E; apply SuccInj in E; auto.

Qed.

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

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

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.

Admitted.

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

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

Proof.

Admitted.

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.

Admitted.

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

Proof.

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.

Proof.

Admitted.

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

Proof.

Admitted.

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

Proof.

Admitted.

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

Proof.

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.

Proof.

Admitted.

Corollary NotNotMinP : forall P, ~~MinP P.

Proof.

Admitted.

Proof.

Admitted.

Corollary NotNotMinP : forall P, ~~MinP P.

Proof.

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

Proof.

Admitted.

Lemma PLt_Succ : forall x, x < Succ x.

Proof.

Admitted.

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

Proof.

Admitted.

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.

Admitted.

Proof.

Admitted.

Lemma PLt_Succ : forall x, x < Succ x.

Proof.

Admitted.

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

Proof.

Admitted.

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.

Admitted.

Require Import Omega.

Open Scope nat_scope.

Definition infinite (P : nat -> Prop) := forall x, exists y, x < y /\ P y.

Section IPP.

Hypothesis Absurd : forall A, (~ ~ A) -> A.

Variable X : nat -> Prop.

Hypothesis Xu : infinite X.

Variable A : nat -> nat -> Prop.

Variable k : nat.

Hypothesis Xcovered : forall x, X x -> exists i, i <= k /\ A i x.

Theorem IPP : exists i, i <= k /\ infinite (A i).

Proof.

Admitted.

End IPP.

This page has been generated by coqdoc