TP06: The accessiblity predicate

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.

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

The following line turn implicit all arguments that can be infered from other arguments, this removing the need to explicitely tag them with { }.

Set Implicit Arguments.

2) As an example, prove the lemmas Acc lt 0, Acc lt 1, and Acc lt 2.

3) What is the structure of a proof of Acc lt n?

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

5) Define lt2 the lexicographic product of <.

Definition lt2 : relation (nat*nat) := ...

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

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

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

Operations on well founded relations

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

Sub-relation

9) Define relation inclusion.

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

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

Inverse image

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

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

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

12) 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.
...
Qed.
End Inverse_image.

Transitive closure

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

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

15) 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 wfR x. apply Acc_trans. apply wfR. Qed.

Lexicographic product

16) Define the lexicographic product of two relations.

Definition lexprod (A B : Type) (RA : relation A) (RB : relation B)
: relation (A*B) := ...

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

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

This page has been generated by coqdoc