(** * TP06 : The accessiblity predicate *)
(* To build an html version of the TD sheet, use the command
"coqdoc -utf8 --no-lib-name --no-index --lib-subtitles TP06.v" *)
(******************************************)
(** * 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) **)