diff options
Diffstat (limited to 'theories/Relations/Rstar.v')
| -rw-r--r-- | theories/Relations/Rstar.v | 139 |
1 files changed, 73 insertions, 66 deletions
diff --git a/theories/Relations/Rstar.v b/theories/Relations/Rstar.v index 4e62d73a..91d2aaa4 100644 --- a/theories/Relations/Rstar.v +++ b/theories/Relations/Rstar.v @@ -6,82 +6,89 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rstar.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Rstar.v 9245 2006-10-17 12:53:34Z notin $ i*) (** Properties of a binary relation [R] on type [A] *) Section Rstar. + + Variable A : Type. + Variable R : A -> A -> Prop. -Variable A : Type. -Variable R : A -> A -> Prop. - -(** Definition of the reflexive-transitive closure [R*] of [R] *) -(** Smallest reflexive [P] containing [R o P] *) - -Definition Rstar (x y:A) := - forall P:A -> A -> Prop, - (forall u:A, P u u) -> (forall u v w:A, R u v -> P v w -> P u w) -> P x y. + (** Definition of the reflexive-transitive closure [R*] of [R] *) + (** Smallest reflexive [P] containing [R o P] *) -Theorem Rstar_reflexive : forall x:A, Rstar x x. - Proof - fun (x:A) (P:A -> A -> Prop) (h1:forall u:A, P u u) - (h2:forall u v w:A, R u v -> P v w -> P u w) => - h1 x. + Definition Rstar (x y:A) := + forall P:A -> A -> Prop, + (forall u:A, P u u) -> (forall u v w:A, R u v -> P v w -> P u w) -> P x y. -Theorem Rstar_R : forall x y z:A, R x y -> Rstar y z -> Rstar x z. - Proof - fun (x y z:A) (t1:R x y) (t2:Rstar y z) (P:A -> A -> Prop) - (h1:forall u:A, P u u) (h2:forall u v w:A, R u v -> P v w -> P u w) => - h2 x y z t1 (t2 P h1 h2). + Theorem Rstar_reflexive : forall x:A, Rstar x x. + Proof. + unfold Rstar. intros x P P_refl RoP. apply P_refl. + Qed. + + Theorem Rstar_R : forall x y z:A, R x y -> Rstar y z -> Rstar x z. + Proof. + intros x y z R_xy Rstar_yz. + unfold Rstar. + intros P P_refl RoP. apply RoP with (v:=y). + assumption. + apply Rstar_yz; assumption. + Qed. + + (** We conclude with transitivity of [Rstar] : *) + + Theorem Rstar_transitive : + forall x y z:A, Rstar x y -> Rstar y z -> Rstar x z. + Proof. + intros x y z Rstar_xy; unfold Rstar in Rstar_xy. + apply Rstar_xy; trivial. + intros u v w R_uv fz Rstar_wz. + apply Rstar_R with (y:=v); auto. + Qed. + + (** Another characterization of [R*] *) + (** Smallest reflexive [P] containing [R o R*] *) + + Definition Rstar' (x y:A) := + forall P:A -> A -> Prop, + P x x -> (forall u:A, R x u -> Rstar u y -> P x y) -> P x y. + + Theorem Rstar'_reflexive : forall x:A, Rstar' x x. + Proof. + unfold Rstar'; intros; assumption. + Qed. -(** We conclude with transitivity of [Rstar] : *) - -Theorem Rstar_transitive : - forall x y z:A, Rstar x y -> Rstar y z -> Rstar x z. - Proof - fun (x y z:A) (h:Rstar x y) => - h (fun u v:A => Rstar v z -> Rstar u z) (fun (u:A) (t:Rstar u z) => t) - (fun (u v w:A) (t1:R u v) (t2:Rstar w z -> Rstar v z) - (t3:Rstar w z) => Rstar_R u v z t1 (t2 t3)). - -(** Another characterization of [R*] *) -(** Smallest reflexive [P] containing [R o R*] *) - -Definition Rstar' (x y:A) := - forall P:A -> A -> Prop, - P x x -> (forall u:A, R x u -> Rstar u y -> P x y) -> P x y. - -Theorem Rstar'_reflexive : forall x:A, Rstar' x x. - Proof - fun (x:A) (P:A -> A -> Prop) (h:P x x) - (h':forall u:A, R x u -> Rstar u x -> P x x) => h. + Theorem Rstar'_R : forall x y z:A, R x z -> Rstar z y -> Rstar' x y. + Proof. + unfold Rstar'. intros x y z Rxz Rstar_zy P Pxx RoP. + apply RoP with (u:=z); trivial. + Qed. -Theorem Rstar'_R : forall x y z:A, R x z -> Rstar z y -> Rstar' x y. - Proof - fun (x y z:A) (t1:R x z) (t2:Rstar z y) (P:A -> A -> Prop) - (h1:P x x) (h2:forall u:A, R x u -> Rstar u y -> P x y) => - h2 z t1 t2. + (** Equivalence of the two definitions: *) + + Theorem Rstar'_Rstar : forall x y:A, Rstar' x y -> Rstar x y. + Proof. + intros x z Rstar'_xz; unfold Rstar' in Rstar'_xz. + apply Rstar'_xz. + exact (Rstar_reflexive x). + intro y; generalize x y z; exact Rstar_R. + Qed. -(** Equivalence of the two definitions: *) - -Theorem Rstar'_Rstar : forall x y:A, Rstar' x y -> Rstar x y. - Proof - fun (x y:A) (h:Rstar' x y) => - h Rstar (Rstar_reflexive x) (fun u:A => Rstar_R x u y). + Theorem Rstar_Rstar' : forall x y:A, Rstar x y -> Rstar' x y. + Proof. + intros. + apply H. + exact Rstar'_reflexive. + intros u v w R_uv Rs'_vw. apply Rstar'_R with (z:=v). + assumption. + apply Rstar'_Rstar; assumption. + Qed. + + (** Property of Commutativity of two relations *) -Theorem Rstar_Rstar' : forall x y:A, Rstar x y -> Rstar' x y. - Proof - fun (x y:A) (h:Rstar x y) => - h Rstar' (fun u:A => Rstar'_reflexive u) - (fun (u v w:A) (h1:R u v) (h2:Rstar' v w) => - Rstar'_R u w v h1 (Rstar'_Rstar v w h2)). - - -(** Property of Commutativity of two relations *) - -Definition commut (A:Set) (R1 R2:A -> A -> Prop) := - forall x y:A, - R1 y x -> forall z:A, R2 z y -> exists2 y' : A, R2 y' x & R1 z y'. - + Definition commut (A:Set) (R1 R2:A -> A -> Prop) := + forall x y:A, + R1 y x -> forall z:A, R2 z y -> exists2 y' : A, R2 y' x & R1 z y'. End Rstar. |