(** * 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? **) (** It starts off with minimal elements or [R]: the argument of Acc_intro, of type [∀ y : A, R y x -> Acc R y], can be proven because [R y x] cannot hold ([x] begin minimal exactly means there is no [y] such that [R y x]. **) (** 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, thus 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]. **) Lemma Acc_0 : Acc lt 0. Proof. apply Acc_intro. intros y Hy. inversion Hy. Qed. Lemma Acc_1 : Acc lt 1. Proof. apply Acc_intro. intros n Hn. replace n with 0 by omega. apply Acc_0. Qed. Lemma Acc_2 : Acc lt 2. Proof. apply Acc_intro. intros n Hn. unfold lt in Hn. apply le_S_n in Hn. destruct n. now apply Acc_0. replace n with 0 by omega. apply Acc_1. Qed. (** 3) What is the structure of a proof of [Acc lt n]? **) (** Because [Acc] is an inductive type, any proof of this predicate starts with an application of its only constructor [Acc_intro]. The argument of this constructor is a function returning of proof of [Acc], which again will start by [Acc_intro] and so on. Note: Defining a function by well-founded induction means defining it by structural induction on the proof of [∀x, Acc R x]. **) (** 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. intros n. induction n. apply Acc_intro. intros y Hy. now inversion Hy. apply Acc_intro. intros y Hy. destruct (eq_nat_dec y n). subst. now apply IHn. destruct IHn as [Hn]. apply Hn. omega. Qed. (** 5) Define [lt2] the lexicographic product of [<]. **) Definition lt2 : relation (nat*nat) := fun x y => fst x < fst y \/ fst x = fst y /\ snd x < snd y. 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]. **) Lemma lt2_irrefl : forall x, ~x << x. Proof. intros [x y] [Habs | [Heq Habs]]; elim (lt_irrefl _ Habs). Qed. Lemma lt2_trans : forall x y z, x << y -> y << z -> x << z. Proof. intros [x₁ x₂] [y₁ y₂] [z₁ z₂] [Hlt₁ | [Heq₁ Hlt₁]] [Hlt₂ | [Heq₂ Hlt₂]]; simpl in *. left. now apply lt_trans with y₁. left. subst. now apply lt_le_trans with z₁. left. subst. now apply le_lt_trans with y₁. right. subst. split. easy. now apply lt_trans with y₂. Qed. (** 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. intros [x y]. revert y. induction x. induction y. (* x = 0, y = 0 *) apply Acc_intro. intros [x' y'] [Habs | [Heq Habs]]; now inversion Habs. (* x > 0, y > 0 *) apply Acc_intro. intros [x' y'] [Habs | [Heq Hlt]]. now inversion Habs. simpl in *. subst. destruct (eq_nat_dec y' y). subst y'. easy. destruct IHy as [Hy]. apply Hy. right. split. easy. simpl. omega. induction y. (* x > 0, y = 0 *) apply Acc_intro. intros [x' y'] [Hlt | [Heq Habs]]; simpl in *. destruct (eq_nat_dec x' x). subst. now apply IHx. destruct (IHx y') as [Hx]. apply Hx. left. simpl. omega. now inversion Habs. (* x > 0, y > 0 *) apply Acc_intro. intros [x' y'] [Hlt | [Heq Hlt]]; simpl in *. destruct IHy as [Hy]. apply Hy. now left. subst. destruct (eq_nat_dec y' y). subst. exact IHy. destruct IHy as [Hy]. apply Hy. right. split; simpl; omega. 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. intros A R x y Hxy Hy. destruct Hy as [Hy]. now apply Hy. Qed. (** *** Sub-relation **) (** 9) Define relation inclusion. **) Definition rel_incl (A : Type) (R S : relation A) := forall x y, R x y -> S x y. (** 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. intros incl wfS x. induction (wfS x). apply Acc_intro. auto. 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. intros y Hy. induction Hy as [y _ IHy]. intros x eq. apply Acc_intro. intros x' Hxx'. apply (IHy (f x')). subst y. unfold R' in Hxx'. easy. reflexivity. 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. intros wfR x. now apply Acc_inverse_eq with (f x). Qed. End Inverse_image. (** *** Transitive closure **) (** 13) Define the (non-reflexive) transitive closure operator. **) Inductive trans (A : Type) (R : relation A) x y : Prop := | Tstep : R x y -> trans R x y | Ttrans : forall z, trans R x z -> R z y -> trans R x y. (** 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. intros x Hx. induction Hx as [x _ IHx]. apply Acc_intro. intros y Hy. induction Hy as [| x' y' Hy']. now apply IHx. apply IHHy'. intros z Hz. apply Acc_inv with y'. now constructor. now apply IHx. 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) := fun x y => RA (fst x) (fst y) \/ fst x = fst y /\ RB (snd x) (snd y). (** 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. intros wfRA wfRB [x y]. revert y. induction (wfRA x) as [x _ IHx]. intros y. induction (wfRB y) as [y _ IHy]. apply Acc_intro. intros [x' y'] Hxy'. induction Hxy' as [Hlt | [Heq Hlt]]; simpl in *. now apply IHx. subst. now apply IHy. 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) **)