From 28dc7a05cc1d3e03ed1435b3db4340db954a59e2 Mon Sep 17 00:00:00 2001 From: notin Date: Tue, 17 Oct 2006 12:53:34 +0000 Subject: Mise en forme des theories git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Relations/Newman.v | 130 ++++++++++++++------------- theories/Relations/Operators_Properties.v | 142 +++++++++++++++--------------- theories/Relations/Relation_Definitions.v | 87 +++++++++--------- theories/Relations/Relation_Operators.v | 74 ++++++++-------- theories/Relations/Relations.v | 23 ++--- theories/Relations/Rstar.v | 137 ++++++++++++++-------------- 6 files changed, 301 insertions(+), 292 deletions(-) (limited to 'theories/Relations') diff --git a/theories/Relations/Newman.v b/theories/Relations/Newman.v index 9c53a28be..d97943280 100644 --- a/theories/Relations/Newman.v +++ b/theories/Relations/Newman.v @@ -23,24 +23,23 @@ Let Rstar_Rstar' := Rstar_Rstar' A R. Definition coherence (x y:A) := ex2 (Rstar x) (Rstar y). Theorem coherence_intro : - forall x y z:A, Rstar x z -> Rstar y z -> coherence x y. -Proof - fun (x y z:A) (h1:Rstar x z) (h2:Rstar y z) => - ex_intro2 (Rstar x) (Rstar y) z h1 h2. + forall x y z:A, Rstar x z -> Rstar y z -> coherence x y. +Proof fun (x y z:A) (h1:Rstar x z) (h2:Rstar y z) => + ex_intro2 (Rstar x) (Rstar y) z h1 h2. (** A very simple case of coherence : *) Lemma Rstar_coherence : forall x y:A, Rstar x y -> coherence x y. - Proof - fun (x y:A) (h:Rstar x y) => coherence_intro x y y h (Rstar_reflexive y). +Proof + fun (x y:A) (h:Rstar x y) => coherence_intro x y y h (Rstar_reflexive y). (** coherence is symmetric *) Lemma coherence_sym : forall x y:A, coherence x y -> coherence y x. - Proof - fun (x y:A) (h:coherence x y) => - ex2_ind - (fun (w:A) (h1:Rstar x w) (h2:Rstar y w) => - coherence_intro y x w h2 h1) h. +Proof + fun (x y:A) (h:coherence x y) => + ex2_ind + (fun (w:A) (h1:Rstar x w) (h2:Rstar y w) => + coherence_intro y x w h2 h1) h. Definition confluence (x:A) := forall y z:A, Rstar x y -> Rstar x z -> coherence y z. @@ -54,68 +53,67 @@ Definition noetherian := Section Newman_section. -(** The general hypotheses of the theorem *) + (** The general hypotheses of the theorem *) -Hypothesis Hyp1 : noetherian. -Hypothesis Hyp2 : forall x:A, local_confluence x. + Hypothesis Hyp1 : noetherian. + Hypothesis Hyp2 : forall x:A, local_confluence x. -(** The induction hypothesis *) + (** The induction hypothesis *) -Section Induct. - Variable x : A. - Hypothesis hyp_ind : forall u:A, R x u -> confluence u. + Section Induct. + Variable x : A. + Hypothesis hyp_ind : forall u:A, R x u -> confluence u. -(** Confluence in [x] *) + (** Confluence in [x] *) - Variables y z : A. - Hypothesis h1 : Rstar x y. - Hypothesis h2 : Rstar x z. + Variables y z : A. + Hypothesis h1 : Rstar x y. + Hypothesis h2 : Rstar x z. -(** particular case [x->u] and [u->*y] *) -Section Newman_. - Variable u : A. - Hypothesis t1 : R x u. - Hypothesis t2 : Rstar u y. + (** particular case [x->u] and [u->*y] *) + Section Newman_. + Variable u : A. + Hypothesis t1 : R x u. + Hypothesis t2 : Rstar u y. + + (** In the usual diagram, we assume also [x->v] and [v->*z] *) + + Theorem Diagram : forall (v:A) (u1:R x v) (u2:Rstar v z), coherence y z. + Proof + (* We draw the diagram ! *) + fun (v:A) (u1:R x v) (u2:Rstar v z) => + ex2_ind + (* local confluence in x for u,v *) + (* gives w, u->*w and v->*w *) + (fun (w:A) (s1:Rstar u w) (s2:Rstar v w) => + ex2_ind + (* confluence in u => coherence(y,w) *) + (* gives a, y->*a and z->*a *) + (fun (a:A) (v1:Rstar y a) (v2:Rstar w a) => + ex2_ind + (* confluence in v => coherence(a,z) *) + (* gives b, a->*b and z->*b *) + (fun (b:A) (w1:Rstar a b) (w2:Rstar z b) => + coherence_intro y z b (Rstar_transitive y a b v1 w1) w2) + (hyp_ind v u1 a z (Rstar_transitive v w a s2 v2) u2)) + (hyp_ind u t1 y w t2 s1)) (Hyp2 x u v t1 u1). -(** In the usual diagram, we assume also [x->v] and [v->*z] *) - -Theorem Diagram : forall (v:A) (u1:R x v) (u2:Rstar v z), coherence y z. - -Proof - (* We draw the diagram ! *) - fun (v:A) (u1:R x v) (u2:Rstar v z) => - ex2_ind - (* local confluence in x for u,v *) - (* gives w, u->*w and v->*w *) - (fun (w:A) (s1:Rstar u w) (s2:Rstar v w) => - ex2_ind - (* confluence in u => coherence(y,w) *) - (* gives a, y->*a and z->*a *) - (fun (a:A) (v1:Rstar y a) (v2:Rstar w a) => - ex2_ind - (* confluence in v => coherence(a,z) *) - (* gives b, a->*b and z->*b *) - (fun (b:A) (w1:Rstar a b) (w2:Rstar z b) => - coherence_intro y z b (Rstar_transitive y a b v1 w1) w2) - (hyp_ind v u1 a z (Rstar_transitive v w a s2 v2) u2)) - (hyp_ind u t1 y w t2 s1)) (Hyp2 x u v t1 u1). - -Theorem caseRxy : coherence y z. -Proof - Rstar_Rstar' x z h2 (fun v w:A => coherence y w) - (coherence_sym x y (Rstar_coherence x y h1)) (*i case x=z i*) - Diagram. (*i case x->v->*z i*) -End Newman_. - -Theorem Ind_proof : coherence y z. -Proof - Rstar_Rstar' x y h1 (fun u v:A => coherence v z) - (Rstar_coherence x z h2) (*i case x=y i*) - caseRxy. (*i case x->u->*z i*) -End Induct. - -Theorem Newman : forall x:A, confluence x. -Proof fun x:A => Hyp1 x confluence Ind_proof. + Theorem caseRxy : coherence y z. + Proof + Rstar_Rstar' x z h2 (fun v w:A => coherence y w) + (coherence_sym x y (Rstar_coherence x y h1)) (*i case x=z i*) + Diagram. (*i case x->v->*z i*) + End Newman_. + + Theorem Ind_proof : coherence y z. + Proof + Rstar_Rstar' x y h1 (fun u v:A => coherence v z) + (Rstar_coherence x z h2) (*i case x=y i*) + caseRxy. (*i case x->u->*z i*) + End Induct. + + Theorem Newman : forall x:A, confluence x. + Proof fun x:A => Hyp1 x confluence Ind_proof. End Newman_section. diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v index 317a5ed07..3cae9d571 100644 --- a/theories/Relations/Operators_Properties.v +++ b/theories/Relations/Operators_Properties.v @@ -22,75 +22,77 @@ Section Properties. Variable R : relation A. Let incl (R1 R2:relation A) : Prop := forall x y:A, R1 x y -> R2 x y. - -Section Clos_Refl_Trans. - - Lemma clos_rt_is_preorder : preorder A (clos_refl_trans A R). -apply Build_preorder. -exact (rt_refl A R). - -exact (rt_trans A R). -Qed. - - - -Lemma clos_rt_idempotent : - incl (clos_refl_trans A (clos_refl_trans A R)) (clos_refl_trans A R). -red in |- *. -induction 1; auto with sets. -intros. -apply rt_trans with y; auto with sets. -Qed. - - Lemma clos_refl_trans_ind_left : - forall (A:Set) (R:A -> A -> Prop) (M:A) (P:A -> Prop), - P M -> - (forall P0 N:A, clos_refl_trans A R M P0 -> P P0 -> R P0 N -> P N) -> - forall a:A, clos_refl_trans A R M a -> P a. -intros. -generalize H H0. -clear H H0. -elim H1; intros; auto with sets. -apply H2 with x; auto with sets. - -apply H3. -apply H0; auto with sets. - -intros. -apply H5 with P0; auto with sets. -apply rt_trans with y; auto with sets. -Qed. - - -End Clos_Refl_Trans. - - -Section Clos_Refl_Sym_Trans. - - Lemma clos_rt_clos_rst : - inclusion A (clos_refl_trans A R) (clos_refl_sym_trans A R). -red in |- *. -induction 1; auto with sets. -apply rst_trans with y; auto with sets. -Qed. - - Lemma clos_rst_is_equiv : equivalence A (clos_refl_sym_trans A R). -apply Build_equivalence. -exact (rst_refl A R). - -exact (rst_trans A R). - -exact (rst_sym A R). -Qed. - - Lemma clos_rst_idempotent : - incl (clos_refl_sym_trans A (clos_refl_sym_trans A R)) - (clos_refl_sym_trans A R). -red in |- *. -induction 1; auto with sets. -apply rst_trans with y; auto with sets. -Qed. - -End Clos_Refl_Sym_Trans. + + Section Clos_Refl_Trans. + + Lemma clos_rt_is_preorder : preorder A (clos_refl_trans A R). + Proof. + apply Build_preorder. + exact (rt_refl A R). + + exact (rt_trans A R). + Qed. + + Lemma clos_rt_idempotent : + incl (clos_refl_trans A (clos_refl_trans A R)) (clos_refl_trans A R). + Proof. + red in |- *. + induction 1; auto with sets. + intros. + apply rt_trans with y; auto with sets. + Qed. + + Lemma clos_refl_trans_ind_left : + forall (A:Set) (R:A -> A -> Prop) (M:A) (P:A -> Prop), + P M -> + (forall P0 N:A, clos_refl_trans A R M P0 -> P P0 -> R P0 N -> P N) -> + forall a:A, clos_refl_trans A R M a -> P a. + Proof. + intros. + generalize H H0. + clear H H0. + elim H1; intros; auto with sets. + apply H2 with x; auto with sets. + + apply H3. + apply H0; auto with sets. + + intros. + apply H5 with P0; auto with sets. + apply rt_trans with y; auto with sets. + Qed. + + + End Clos_Refl_Trans. + + + Section Clos_Refl_Sym_Trans. + + Lemma clos_rt_clos_rst : + inclusion A (clos_refl_trans A R) (clos_refl_sym_trans A R). + Proof. + red in |- *. + induction 1; auto with sets. + apply rst_trans with y; auto with sets. + Qed. + + Lemma clos_rst_is_equiv : equivalence A (clos_refl_sym_trans A R). + Proof. + apply Build_equivalence. + exact (rst_refl A R). + exact (rst_trans A R). + exact (rst_sym A R). + Qed. + + Lemma clos_rst_idempotent : + incl (clos_refl_sym_trans A (clos_refl_sym_trans A R)) + (clos_refl_sym_trans A R). + Proof. + red in |- *. + induction 1; auto with sets. + apply rst_trans with y; auto with sets. + Qed. + + End Clos_Refl_Sym_Trans. End Properties. \ No newline at end of file diff --git a/theories/Relations/Relation_Definitions.v b/theories/Relations/Relation_Definitions.v index e0f13b46e..977135fab 100644 --- a/theories/Relations/Relation_Definitions.v +++ b/theories/Relations/Relation_Definitions.v @@ -10,63 +10,62 @@ Section Relation_Definition. - Variable A : Type. - - Definition relation := A -> A -> Prop. + Variable A : Type. + + Definition relation := A -> A -> Prop. - Variable R : relation. + Variable R : relation. -Section General_Properties_of_Relations. - - Definition reflexive : Prop := forall x:A, R x x. - Definition transitive : Prop := forall x y z:A, R x y -> R y z -> R x z. - Definition symmetric : Prop := forall x y:A, R x y -> R y x. - Definition antisymmetric : Prop := forall x y:A, R x y -> R y x -> x = y. - - (* for compatibility with Equivalence in ../PROGRAMS/ALG/ *) - Definition equiv := reflexive /\ transitive /\ symmetric. - -End General_Properties_of_Relations. - + Section General_Properties_of_Relations. + + Definition reflexive : Prop := forall x:A, R x x. + Definition transitive : Prop := forall x y z:A, R x y -> R y z -> R x z. + Definition symmetric : Prop := forall x y:A, R x y -> R y x. + Definition antisymmetric : Prop := forall x y:A, R x y -> R y x -> x = y. + (* for compatibility with Equivalence in ../PROGRAMS/ALG/ *) + Definition equiv := reflexive /\ transitive /\ symmetric. -Section Sets_of_Relations. + End General_Properties_of_Relations. - Record preorder : Prop := - {preord_refl : reflexive; preord_trans : transitive}. - Record order : Prop := - {ord_refl : reflexive; - ord_trans : transitive; - ord_antisym : antisymmetric}. - Record equivalence : Prop := - {equiv_refl : reflexive; - equiv_trans : transitive; - equiv_sym : symmetric}. - - Record PER : Prop := {per_sym : symmetric; per_trans : transitive}. - -End Sets_of_Relations. + Section Sets_of_Relations. + + Record preorder : Prop := + { preord_refl : reflexive; preord_trans : transitive}. + + Record order : Prop := + { ord_refl : reflexive; + ord_trans : transitive; + ord_antisym : antisymmetric}. + + Record equivalence : Prop := + { equiv_refl : reflexive; + equiv_trans : transitive; + equiv_sym : symmetric}. + + Record PER : Prop := {per_sym : symmetric; per_trans : transitive}. + End Sets_of_Relations. -Section Relations_of_Relations. + Section Relations_of_Relations. + + Definition inclusion (R1 R2:relation) : Prop := + forall x y:A, R1 x y -> R2 x y. + + Definition same_relation (R1 R2:relation) : Prop := + inclusion R1 R2 /\ inclusion R2 R1. + + Definition commut (R1 R2:relation) : Prop := + forall x y:A, + R1 y x -> forall z:A, R2 z y -> exists2 y' : A, R2 y' x & R1 z y'. - Definition inclusion (R1 R2:relation) : Prop := - forall x y:A, R1 x y -> R2 x y. + End Relations_of_Relations. - Definition same_relation (R1 R2:relation) : Prop := - inclusion R1 R2 /\ inclusion R2 R1. - - Definition commut (R1 R2:relation) : Prop := - forall x y:A, - R1 y x -> forall z:A, R2 z y -> exists2 y' : A, R2 y' x & R1 z y'. -End Relations_of_Relations. - - End Relation_Definition. Hint Unfold reflexive transitive antisymmetric symmetric: sets v62. @@ -75,4 +74,4 @@ Hint Resolve Build_preorder Build_order Build_equivalence Build_PER preord_refl preord_trans ord_refl ord_trans ord_antisym equiv_refl equiv_trans equiv_sym per_sym per_trans: sets v62. -Hint Unfold inclusion same_relation commut: sets v62. \ No newline at end of file +Hint Unfold inclusion same_relation commut: sets v62. diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v index b538620d1..e4918d40e 100644 --- a/theories/Relations/Relation_Operators.v +++ b/theories/Relations/Relation_Operators.v @@ -24,7 +24,7 @@ Require Import List. Section Transitive_Closure. Variable A : Type. Variable R : relation A. - + Inductive clos_trans (x: A) : A -> Prop := | t_step : forall y:A, R x y -> clos_trans x y | t_trans : @@ -48,16 +48,16 @@ End Reflexive_Transitive_Closure. Section Reflexive_Symetric_Transitive_Closure. Variable A : Type. Variable R : relation A. - + Inductive clos_refl_sym_trans : relation A := | rst_step : forall x y:A, R x y -> clos_refl_sym_trans x y | rst_refl : forall x:A, clos_refl_sym_trans x x | rst_sym : - forall x y:A, clos_refl_sym_trans x y -> clos_refl_sym_trans y x + forall x y:A, clos_refl_sym_trans x y -> clos_refl_sym_trans y x | rst_trans : - forall x y z:A, - clos_refl_sym_trans x y -> - clos_refl_sym_trans y z -> clos_refl_sym_trans x z. + forall x y z:A, + clos_refl_sym_trans x y -> + clos_refl_sym_trans y z -> clos_refl_sym_trans x z. End Reflexive_Symetric_Transitive_Closure. @@ -92,18 +92,18 @@ End Disjoint_Union. Section Lexicographic_Product. -(* Lexicographic order on dependent pairs *) + (* Lexicographic order on dependent pairs *) -Variable A : Set. -Variable B : A -> Set. -Variable leA : A -> A -> Prop. -Variable leB : forall x:A, B x -> B x -> Prop. + Variable A : Set. + Variable B : A -> Set. + Variable leA : A -> A -> Prop. + Variable leB : forall x:A, B x -> B x -> Prop. -Inductive lexprod : sigS B -> sigS B -> Prop := - | left_lex : + Inductive lexprod : sigS B -> sigS B -> Prop := + | left_lex : forall (x x':A) (y:B x) (y':B x'), leA x x' -> lexprod (existS B x y) (existS B x' y') - | right_lex : + | right_lex : forall (x:A) (y y':B x), leB x y y' -> lexprod (existS B x y) (existS B x y'). End Lexicographic_Product. @@ -117,9 +117,9 @@ Section Symmetric_Product. Inductive symprod : A * B -> A * B -> Prop := | left_sym : - forall x x':A, leA x x' -> forall y:B, symprod (x, y) (x', y) + forall x x':A, leA x x' -> forall y:B, symprod (x, y) (x', y) | right_sym : - forall y y':B, leB y y' -> forall x:A, symprod (x, y) (x, y'). + forall y y':B, leB y y' -> forall x:A, symprod (x, y) (x, y'). End Symmetric_Product. @@ -131,34 +131,34 @@ Section Swap. Inductive swapprod : A * A -> A * A -> Prop := | sp_noswap : forall x x':A * A, symprod A A R R x x' -> swapprod x x' | sp_swap : - forall (x y:A) (p:A * A), - symprod A A R R (x, y) p -> swapprod (y, x) p. + forall (x y:A) (p:A * A), + symprod A A R R (x, y) p -> swapprod (y, x) p. End Swap. Section Lexicographic_Exponentiation. - -Variable A : Set. -Variable leA : A -> A -> Prop. -Let Nil := nil (A:=A). -Let List := list A. - -Inductive Ltl : List -> List -> Prop := - | Lt_nil : forall (a:A) (x:List), Ltl Nil (a :: x) - | Lt_hd : forall a b:A, leA a b -> forall x y:list A, Ltl (a :: x) (b :: y) - | Lt_tl : forall (a:A) (x y:List), Ltl x y -> Ltl (a :: x) (a :: y). - - -Inductive Desc : List -> Prop := - | d_nil : Desc Nil - | d_one : forall x:A, Desc (x :: Nil) - | d_conc : + + Variable A : Set. + Variable leA : A -> A -> Prop. + Let Nil := nil (A:=A). + Let List := list A. + + Inductive Ltl : List -> List -> Prop := + | Lt_nil : forall (a:A) (x:List), Ltl Nil (a :: x) + | Lt_hd : forall a b:A, leA a b -> forall x y:list A, Ltl (a :: x) (b :: y) + | Lt_tl : forall (a:A) (x y:List), Ltl x y -> Ltl (a :: x) (a :: y). + + + Inductive Desc : List -> Prop := + | d_nil : Desc Nil + | d_one : forall x:A, Desc (x :: Nil) + | d_conc : forall (x y:A) (l:List), leA x y -> Desc (l ++ y :: Nil) -> Desc ((l ++ y :: Nil) ++ x :: Nil). -Definition Pow : Set := sig Desc. - -Definition lex_exp (a b:Pow) : Prop := Ltl (proj1_sig a) (proj1_sig b). + Definition Pow : Set := sig Desc. + + Definition lex_exp (a b:Pow) : Prop := Ltl (proj1_sig a) (proj1_sig b). End Lexicographic_Exponentiation. diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v index 6578f6c85..938d514df 100644 --- a/theories/Relations/Relations.v +++ b/theories/Relations/Relations.v @@ -13,16 +13,19 @@ Require Export Relation_Operators. Require Export Operators_Properties. Lemma inverse_image_of_equivalence : - forall (A B:Set) (f:A -> B) (r:relation B), - equivalence B r -> equivalence A (fun x y:A => r (f x) (f y)). -intros; split; elim H; red in |- *; auto. -intros _ equiv_trans _ x y z H0 H1; apply equiv_trans with (f y); assumption. + forall (A B:Set) (f:A -> B) (r:relation B), + equivalence B r -> equivalence A (fun x y:A => r (f x) (f y)). +Proof. + intros; split; elim H; red in |- *; auto. + intros _ equiv_trans _ x y z H0 H1; apply equiv_trans with (f y); assumption. Qed. Lemma inverse_image_of_eq : - forall (A B:Set) (f:A -> B), equivalence A (fun x y:A => f x = f y). -split; red in |- *; - [ (* reflexivity *) reflexivity - | (* transitivity *) intros; transitivity (f y); assumption - | (* symmetry *) intros; symmetry in |- *; assumption ]. -Qed. \ No newline at end of file + forall (A B:Set) (f:A -> B), equivalence A (fun x y:A => f x = f y). +Proof. + split; red in |- *; + [ (* reflexivity *) reflexivity + | (* transitivity *) intros; transitivity (f y); assumption + | (* symmetry *) intros; symmetry in |- *; assumption ]. +Qed. + diff --git a/theories/Relations/Rstar.v b/theories/Relations/Rstar.v index eda581e8d..8dfacf2cf 100644 --- a/theories/Relations/Rstar.v +++ b/theories/Relations/Rstar.v @@ -11,77 +11,84 @@ (** 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. -- cgit v1.2.3