DM 3 : Accessibility, induction in HA again, pigeons, division.

The Acc accessiblity predicate

In previous sessions, we used well-foundedness to prove properties and to define recursive functions. Let us now take a closer look at what it means: Print well_founded. returns
      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 _]

which means that a relation R : A -> A -> Prop is well founded if all its elements are accessible: forall a : A, Acc R a.

Being accessible is in turn defined by
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

saying that if all predecessors of x by R are accessible, then x is accessible too.

5) How does the accessibility property start off?

When we want to prove Acc for an element x, we usually start by inspecting the shape of x (especially if A is inductive). With the shape of x, we know if R y x can hold or not.

Keep in mind that Acc is an inductive predicate, so you can always use induction on a proof of Acc x to prove another property.

First example: lt and its lexicographic product.

Require Import Relations.
Require Import Arith.
Require Import Omega.

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.

Theorem lt_wf : well_founded lt.
Proof.
Admitted.

9) Define lt2 the lexicographic product of <.

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

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 lt2_wf : well_founded lt2.
Proof.
Admitted.

Operations on well founded relations

12) Prove the inversion lemma for Acc.

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

Sub-relation

13) Define relation inclusion.

Definition rel_incl (A : Type) (R S : relation A) := True .

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.

Inverse image

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

Lemma Acc_inverse_eq : forall y, Acc R y -> forall x, y = (f x ) -> Acc R' x.
Proof.
Admitted.

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

Lemma wf_inverse_image : well_founded R -> well_founded R'.
Proof.
Admitted.

End Inverse_image.

Transitive closure

17) Define the (non-reflexive) transitive closure operator.

Inductive trans A (R : relation A) : relation A := .

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.

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.

Lexicographic product

20) Define the lexicographic product of two relations.

Definition lexprod (A B : Type) (RA : relation A) (RB : relation B)
: 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.

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)

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

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

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

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.

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

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.

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

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.

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

Double negation of excluded middle and of the minimum principle

1) Prove the double negation of excluded middle.

Lemma NotNotEM : forall A, ~ ~ (A \/ ~ A ).
Proof.
Admitted.

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

Lemma NotNot_EM : forall P A, ((P \/ ~P) -> ~~A) -> ~~A.
Proof.
Admitted.

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.

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

Infinite pigeonhole principle

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.

Hints: you will need some lemmas. Do the proof with pen and paper before. You will use the axiom Absurd a lot, you can write a few lemmas about that, too.

Admitted.
End IPP.

Bonus : Integer division

Division using structural induction

You already know the trick using a third argument to define division:

Fixpoint divaux m n k {struct k} :=
  match n, k with
  | 0, _ | _, 0 => (0, 0)
  | S _, S k' => if le_gt_dec n m then let (q,r) := divaux (m - n) n k' in (S q , r ) else (0, m )
  end.

Definition div1 m n := divaux m n m.

Eval compute in div1 7 2.
Eval compute in div1 2 7.

3) Prove the correctness of your function.

Lemma divaux_bound : forall c, forall a b, 0 < b -> a <= c ->
  snd (divaux a b c) < b.
Proof.
  intros c; induction c; intros a b nzb ac.
    inversion ac.
    destruct b; simpl. congruence. auto with arith.

    simpl.
    destruct b. omega.
    destruct (le_gt_dec (S b) a); auto.
    specialize (IHc (a - S b) (S b) nzb).
    remember (divaux (a - S b) (S b) c) as x.
    destruct x.
    apply IHc.
    auto with *.
Qed.

Lemma divaux_correct : forall c, forall a b, 0 < b -> a <= c ->
  fst (divaux a b c) * b + snd (divaux a b c) = a.
Proof.
  intros c; induction c; intros a b nzb ac.
    inversion ac.
    destruct b; simpl. congruence. auto with arith.

    simpl.
    destruct b. inversion nzb.
    destruct (le_gt_dec (S b) a); auto.
    specialize (IHc (a - S b) (S b) nzb).
    remember (divaux (a - S b) (S b) c) as x.
    destruct x.
    simpl in *.
    auto with *.
Qed.

Theorem div1_correct : forall a b, 0 < b ->
  let (q, r) := div1 a b in q * b + r = a /\ r < b.
Proof.
  intros a b nzb; unfold div1.
  pose proof divaux_correct a a b nzb.
  pose proof divaux_bound a a b nzb.
  remember (divaux a b a) as x; destruct x as (q, r).
  simpl in *.
  auto.
Qed.

Division using well-founded induction

Instead of using the structural induction we can use more sophisticated methods.

You can use the well-foundedness proof of the standard library instead of your "lt_wf" first that the computation works more easily. (You can modify your proof and definition of lt_wf so that the last question works with it, too.)

Check Coq.Arith.Wf_nat.lt_wf.

Since we will have to deal with well-founded induction, instead of defining only div as a function from nat to nat, we might as well define it together with its full specification. In practice, this means that the return type of the division function will not be a pair of integers but the set of pairs of integers such that the (in)equations we want to the correctness hold.

Locate "{ _ | _ }".
Print sig.
Example pos_elt : {x | 3 < x < 5}.
Proof. exists 4. auto with arith. Qed.

Define the richest (ie most accurate) type for integer division. The division a/b will be defined by induction on a, so we define div_t with only one argument a.

Definition div_t (a : nat) := True
.

In order to use well-founded induction, we need to prove that if we know how to compute division for all numbers smaller than n, then we know how to do it for n as well:
∀n, (∀m, m < n → div_type m) → div_type n

6) Define such a function (in tactic mode). Wrap up everything to define division.

Check lt_minus.
Check le_plus_minus.

Definition div_t_ind : True .
Proof.
Admitted.

Definition div2 : forall n, div_t n := fun _ => I .

The Program library

The last solution to define a non structural fixpoint is to use the Program library.

Read the page about the Program library.

Require Import Program.

Using Program, define division.

Print div_t.

Program Fixpoint div3 m {measure m} : div_t m := I.

Let us now try to compute with our division functions. First, prove the lemma lt_0_3 : 0 < 3.

Lemma lt_0_3 : 0 < 3. Proof. Admitted.

What happens when you do the following?

Eval compute in (div1 5 3). Eval compute in (` (div2 5 3 lt_0_3)). Eval compute in (` (div3 5 3 lt_0_3)).

This page has been generated by coqdoc