Commit 302fe4c7 authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

solution to TD4

parent 4b679663
(** TD4 : inductive predicates *)
Require Import Relations.
Print relation.
(* To shorten the types of (binary) relations: *)
(* relation T := T -> T -> Prop *)
Parameter T : Type.
(* Reflexive-transitive closure, version 1 *)
Inductive clos1 (R : relation T) : relation T :=
| cl1_base : forall x y, R x y -> clos1 R x y
| cl1_refl : forall x, clos1 R x x
| cl1_trans : forall x y z, clos1 R x y -> clos1 R y z -> clos1 R x z.
Check clos1_ind.
(*
clos1_ind
: forall (R : relation T) (P : T -> T -> Prop),
(forall x y : T, R x y -> P x y) ->
(forall x : T, P x x) ->
(forall x y z : T, clos1 R x y -> P x y -> clos1 R y z -> P y z -> P x z) ->
forall t t0 : T, clos1 R t t0 -> P t t0
*)
(* One may rather expect the following form (note the transitivity) :
clos1_ind_manual
: forall (R : relation T) (P : T -> T -> Prop),
(forall x y : T, R x y -> P x y) ->
(forall x : T, P x x) ->
(forall x y z : T, P x y -> P y z -> P x z) ->
forall t t0 : T, clos1 R t t0 -> P t t0
This version is implied by the previous one...
*)
(*
3. Show that if `R` is symmetric, then so is `clos1 R`.
(Hint: define a predicate on relations `Symmetric : (T->T->Prop)->Prop`).
*)
Definition Symmetric (R:relation T) := forall x y, R x y -> R y x.
(* Beware, the following is false (find a counterexample !)
Lemma bad_statement (R:relation T) :
forall x y, (R x y -> R y x) -> (clos1 R x y -> clos1 R y x)
(Hint: find a R and points x, y where R x y is false
(hence R x y -> R y x is true) but where clos1 R x y is true
(and not clos1 R y x).
For instance:
Definition R x y := y = S x.
And take x = 0 and y = 2
Rather, here is a correct statement:
*)
Lemma clos1_sym R : Symmetric R -> Symmetric (clos1 R).
Proof.
(* unfold Symmetric. *)
intros symR x y Hxy.
induction Hxy.
- apply cl1_base. apply symR. assumption.
- apply cl1_refl.
- apply cl1_trans with y; assumption.
Qed.
Lemma clos1_idem R : forall x y, clos1 (clos1 R) x y -> clos1 R x y.
Proof.
intros x y H.
induction H.
- assumption.
- apply cl1_refl.
- apply cl1_trans with y; auto.
Qed.
(* Reflexive-transitive closure, Version 2 *)
Inductive clos2 (R : relation T) : relation T :=
| cl2_refl x : clos2 R x x
| cl2_next x y z : clos2 R x y -> R y z -> clos2 R x z.
Lemma clos2_clos1 R : forall x y, clos2 R x y -> clos1 R x y.
Proof.
induction 1. (* induction on the first hypothesis without name *)
(* equivalent here to intros x y H; induction H *)
- apply cl1_refl.
- apply cl1_trans with y. assumption. apply cl1_base; assumption.
Qed.
Lemma clos2_base (R:relation T) : forall x y, R x y -> clos2 R x y.
Proof.
intros x y H. apply cl2_next with x. apply cl2_refl. assumption.
Qed.
Definition Trans (R:relation T) := forall x y z, R x y -> R y z -> R x z.
Lemma clos2_trans R : Trans (clos2 R).
Proof.
intros x y z Hxy Hyz.
(* Don't do `induction Hxy` or you will soon be stuck...
Hxy Hyz
x------>y----->z
| | |
x-----t-y------z
* 1 *
No easy way to go on, the R part is just in the middle,
not on the right. Rather:
*)
induction Hyz.
(*
Hxy Hyz
x-------xO---y-z
* * 1
x------------y-z
* 1
*)
- assumption.
- apply cl2_next with y; auto.
Qed.
Lemma clos1_clos2 (R:relation T) : forall x y, clos1 R x y -> clos2 R x y.
Proof.
induction 1. (* induction on the (unamed) hypothesis clos1 R x y *)
- apply clos2_base. assumption.
- apply cl2_refl.
- apply clos2_trans with y; assumption.
Qed.
Lemma clos1_clos2_equiv R : forall x y, clos1 R x y <-> clos2 R x y.
Proof.
split.
- apply clos1_clos2.
- apply clos2_clos1.
Qed.
(* Reflexive-transitive closure, version 3 *)
Definition identity : relation T := fun x y => x=y.
(* Or
Definition identity' : relation T := eq.
*)
Definition comp (R1 R2 : relation T) : relation T :=
fun x z => exists y, R1 x y /\ R2 y z.
Fixpoint pow (R:relation T) n : relation T :=
match n with
| O => identity
| S n => comp (pow R n) R
end.
(* of course (comp R (pow R n)) above is also possible,
but way harder to prove equivalent with clos2.
See below the pow' definition. *)
Definition clos3 (R : relation T) : relation T :=
fun x y => exists n, pow R n x y.
Lemma clos3_clos2 R : forall x y, clos3 R x y -> clos2 R x y.
Proof.
intros x y (n,H).
revert x y H.
induction n; simpl in *; intros x y.
- unfold identity.
intros ->. (* just the same as intro H; rewrite H *)
apply cl2_refl.
- intros (u,(Hxu,Huy)). (* clever intros for an exists and a /\ *)
apply cl2_next with u; auto.
Qed.
Lemma clos2_clos3 R : forall x y, clos2 R x y -> clos3 R x y.
Proof.
induction 1.
- exists 0. simpl. reflexivity.
- (* here clos2 was built through cl2_next *)
destruct IHclos2 as (n,IH). exists (S n). simpl.
exists y. split; assumption.
Qed.
(* Instance of always writing "forall x y, Foo x y <-> Bar x y",
we could abstract that into an equivalence on relations : *)
Definition relequiv (R1 R2 : relation T) :=
forall x y, R1 x y <-> R2 x y.
Infix "==" := relequiv (at level 70).
Lemma clos3_clos2_equiv R : clos3 R == clos2 R.
Proof.
split. apply clos3_clos2. apply clos2_clos3.
Qed.
(* Extra question :
Define pow in the other possible way :
R^(n+1) = R.R^n instead of R^(n+1) = R^n.R
And prove equivalent the two versions. *)
Fixpoint pow' (R:relation T) n : relation T :=
match n with
| O => identity
| S n => comp R (pow' R n)
end.
(* For working comfortably on ==, and especially be able
to rewrite with it, let's first show it to be a setoid
equivalence, compatible with composition comp. *)
Require Import Setoid Morphisms.
Instance : Equivalence relequiv.
Proof.
split; try firstorder.
intros R1 R2 R3 Eq1 Eq2 x y. now transitivity (R2 x y).
Qed.
Instance : Proper (relequiv ==> relequiv ==> relequiv) comp.
Proof.
intros R1 R1' Eq1 R2 R2' Eq2.
intros x y. split.
- intros (u,(H1,H2)). exists u. now rewrite <- (Eq1 x u), <- (Eq2 u y).
- intros (u,(H1,H2)). exists u. now rewrite (Eq1 x u), (Eq2 u y).
Qed.
(* Let's also prove a few basic laws of composition *)
Lemma comp_assoc R1 R2 R3 :
comp (comp R1 R2) R3 == comp R1 (comp R2 R3).
Proof.
split.
- intros (u,((v,(H1,H2)),H3)).
exists v. split; auto. now exists u.
- intros (u,(H1, (v,(H2,H3)))).
exists v. split; auto. now exists u.
Qed.
Lemma comp_id_r R : comp R identity == R.
Proof.
intros x y. split.
- now intros (u,(H,->)).
- now exists y.
Qed.
Lemma comp_id_l R : comp identity R == R.
Proof.
intros x y. split.
- now intros (u,(->,H)).
- now exists x.
Qed.
Lemma pow_S R n : pow R (S n) == comp R (pow R n).
Proof.
induction n; simpl.
- now rewrite comp_id_l, comp_id_r.
- now rewrite <- comp_assoc, IHn.
Qed.
Lemma pow_equiv R n : pow R n == pow' R n.
Proof.
induction n; simpl in *.
- reflexivity.
- now rewrite <- IHn, <- pow_S.
Qed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment