aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Relations
diff options
context:
space:
mode:
authorGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-06-21 01:12:20 +0000
committerGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-06-21 01:12:20 +0000
commit639af2938c15202b12f709eb84790d0b5c627a9f (patch)
tree264517f1b305a703117e2b518a8088cbeed09524 /theories/Relations
parent71f380cb047a98d95b743edf98fe03bd041ea7bc (diff)
theories/Relations
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@510 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Relations')
-rwxr-xr-xtheories/Relations/Newman.v94
-rwxr-xr-xtheories/Relations/Operators_Properties.v93
-rwxr-xr-xtheories/Relations/Relation_Definitions.v76
-rwxr-xr-xtheories/Relations/Relation_Operators.v150
-rwxr-xr-xtheories/Relations/Relations.v21
-rwxr-xr-xtheories/Relations/Rstar.v66
6 files changed, 500 insertions, 0 deletions
diff --git a/theories/Relations/Newman.v b/theories/Relations/Newman.v
new file mode 100755
index 000000000..4f07dad8d
--- /dev/null
+++ b/theories/Relations/Newman.v
@@ -0,0 +1,94 @@
+
+(* $Id$ *)
+
+Require Rstar.
+
+Definition coherence := [x:A][y:A] (exT2 ? (Rstar x) (Rstar y)).
+
+Theorem coherence_intro : (x:A)(y:A)(z:A)(Rstar x z)->(Rstar y z)->(coherence x y).
+Proof [x:A][y:A][z:A][h1:(Rstar x z)][h2:(Rstar y z)]
+ (exT_intro2 A (Rstar x) (Rstar y) z h1 h2).
+
+(* A very simple case of coherence : *)
+
+Lemma Rstar_coherence : (x:A)(y:A)(Rstar x y)->(coherence x y).
+ Proof [x:A][y:A][h:(Rstar x y)](coherence_intro x y y h (Rstar_reflexive y)).
+
+(* coherence is symmetric *)
+Lemma coherence_sym: (x:A)(y:A)(coherence x y)->(coherence y x).
+ Proof [x:A][y:A][h:(coherence x y)]
+ (exT2_ind A (Rstar x) (Rstar y) (coherence y x)
+ [w:A][h1:(Rstar x w)][h2:(Rstar y w)]
+ (coherence_intro y x w h2 h1) h).
+
+Definition confluence :=
+ [x:A](y:A)(z:A)(Rstar x y)->(Rstar x z)->(coherence y z).
+
+Definition local_confluence :=
+ [x:A](y:A)(z:A)(R x y)->(R x z)->(coherence y z).
+
+Definition noetherian :=
+ (x:A)(P:A->Prop)((y:A)((z:A)(R y z)->(P z))->(P y))->(P x).
+
+Section Newman_section.
+
+(* The general hypotheses of the theorem *)
+
+Hypothesis Hyp1:noetherian.
+Hypothesis Hyp2:(x:A)(local_confluence x).
+
+(* The induction hypothesis *)
+
+Section Induct.
+ Variable x:A.
+ Hypothesis hyp_ind:(u:A)(R x u)->(confluence u).
+
+(* Confluence in x *)
+
+ 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).
+
+(* In the usual diagram, we assume also x->v and v->*z *)
+
+Theorem Diagram : (v:A)(u1:(R x v))(u2:(Rstar v z))(coherence y z).
+
+Proof (* We draw the diagram ! *)
+ [v:A][u1:(R x v)][u2:(Rstar v z)]
+ (exT2_ind A (Rstar u) (Rstar v) (* local confluence in x for u,v *)
+ (coherence y z) (* gives w, u->*w and v->*w *)
+ ([w:A][s1:(Rstar u w)][s2:(Rstar v w)]
+ (exT2_ind A (Rstar y) (Rstar w) (* confluence in u => coherence(y,w) *)
+ (coherence y z) (* gives a, y->*a and z->*a *)
+ ([a:A][v1:(Rstar y a)][v2:(Rstar w a)]
+ (exT2_ind A (Rstar a) (Rstar z) (* confluence in v => coherence(a,z) *)
+ (coherence y z) (* gives b, a->*b and z->*b *)
+ ([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
+ ([v:A][w:A](coherence y w))
+ (coherence_sym x y (Rstar_coherence x y h1)) (* case x=z *)
+ Diagram). (* case x->v->*z *)
+End Newman_.
+
+Theorem Ind_proof : (coherence y z).
+Proof (Rstar_Rstar' x y h1 ([u:A][v:A](coherence v z))
+ (Rstar_coherence x z h2) (* case x=y*)
+ caseRxy). (* case x->u->*z *)
+End Induct.
+
+Theorem Newman : (x:A)(confluence x).
+Proof [x:A](Hyp1 x confluence Ind_proof).
+
+End Newman_section.
diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v
new file mode 100755
index 000000000..99b9eb715
--- /dev/null
+++ b/theories/Relations/Operators_Properties.v
@@ -0,0 +1,93 @@
+
+(* $Id$ *)
+
+(****************************************************************************)
+(* Bruno Barras *)
+(****************************************************************************)
+
+Require Relation_Definitions.
+Require Relation_Operators.
+
+
+Section Properties.
+
+ Variable A: Set.
+ Variable R: (relation A).
+
+ Local incl : (relation A)->(relation A)->Prop :=
+ [R1,R2: (relation A)] (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).
+Save.
+
+
+
+Lemma clos_rt_idempotent:
+ (incl (clos_refl_trans A (clos_refl_trans A R))
+ (clos_refl_trans A R)).
+Red.
+Induction 1; Auto with sets.
+Intros.
+Apply rt_trans with y0; Auto with sets.
+Save.
+
+ Lemma clos_refl_trans_ind_left: (A:Set)(R:A->A->Prop)(M:A)(P:A->Prop)
+ (P M)
+ ->((P0,N:A)
+ (clos_refl_trans A R M P0)->(P P0)->(R P0 N)->(P N))
+ ->(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).
+Save.
+
+
+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.
+(Induction 1; Auto with sets).
+Intros.
+(Apply rst_trans with y0; Auto with sets).
+Save.
+
+ 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).
+Save.
+
+ Lemma clos_rst_idempotent:
+ (incl (clos_refl_sym_trans A (clos_refl_sym_trans A R))
+ (clos_refl_sym_trans A R)).
+Red.
+(Induction 1; Auto with sets).
+Intros.
+(Apply rst_trans with y0; Auto with sets).
+Save.
+
+End Clos_Refl_Sym_Trans.
+
+End Properties.
diff --git a/theories/Relations/Relation_Definitions.v b/theories/Relations/Relation_Definitions.v
new file mode 100755
index 000000000..9d32ae9be
--- /dev/null
+++ b/theories/Relations/Relation_Definitions.v
@@ -0,0 +1,76 @@
+
+(* $Id$ *)
+
+Section Relation_Definition.
+
+ Variable A: Set.
+
+ Definition relation := A -> A -> Prop.
+
+ Variable R: relation.
+
+
+Section General_Properties_of_Relations.
+
+ Definition reflexive : Prop := (x: A) (R x x).
+ Definition transitive : Prop := (x,y,z: A) (R x y) -> (R y z) -> (R x z).
+ Definition symmetric : Prop := (x,y: A) (R x y) -> (R y x).
+ Definition antisymmetric : Prop := (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 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.
+
+ Definition inclusion : relation -> relation -> Prop :=
+ [R1,R2: relation] (x,y:A) (R1 x y) -> (R2 x y).
+
+ Definition same_relation : relation -> relation -> Prop :=
+ [R1,R2: relation] (inclusion R1 R2) /\ (inclusion R2 R1).
+
+ Definition commut : relation -> relation -> Prop :=
+ [R1,R2:relation] (x,y:A) (R1 y x) -> (z:A) (R2 z y)
+ -> (EX y':A |(R2 y' x) & (R1 z y')).
+
+End Relations_of_Relations.
+
+
+End Relation_Definition.
+
+Hints Unfold reflexive transitive antisymmetric symmetric : sets v62.
+
+Hints 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.
+
+Hints Unfold inclusion same_relation commut : sets v62.
diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v
new file mode 100755
index 000000000..1944b60cd
--- /dev/null
+++ b/theories/Relations/Relation_Operators.v
@@ -0,0 +1,150 @@
+
+(* $Id$ *)
+
+(****************************************************************************)
+(* Bruno Barras Cristina Cornes *)
+(* *)
+(* Some of these definitons were taken from : *)
+(* Constructing Recursion Operators in Type Theory *)
+(* L. Paulson JSC (1986) 2, 325-355 *)
+(****************************************************************************)
+
+Require Relation_Definitions.
+Require PolyList.
+Require PolyListSyntax.
+
+(* Some operators to build relations *)
+
+Section Transitive_Closure.
+ Variable A: Set.
+ Variable R: (relation A).
+
+ Inductive clos_trans : A->A->Prop :=
+ t_step: (x,y:A)(R x y)->(clos_trans x y)
+ | t_trans: (x,y,z:A)(clos_trans x y)->(clos_trans y z)->(clos_trans x z).
+End Transitive_Closure.
+
+
+Section Reflexive_Transitive_Closure.
+ Variable A: Set.
+ Variable R: (relation A).
+
+ Inductive clos_refl_trans: (relation A) :=
+ rt_step: (x,y:A)(R x y)->(clos_refl_trans x y)
+ | rt_refl: (x:A)(clos_refl_trans x x)
+ | rt_trans: (x,y,z: A)(clos_refl_trans x y)->(clos_refl_trans y z)
+ ->(clos_refl_trans x z).
+End Reflexive_Transitive_Closure.
+
+
+Section Reflexive_Symetric_Transitive_Closure.
+ Variable A: Set.
+ Variable R: (relation A).
+
+ Inductive clos_refl_sym_trans: (relation A) :=
+ rst_step: (x,y:A)(R x y)->(clos_refl_sym_trans x y)
+ | rst_refl: (x:A)(clos_refl_sym_trans x x)
+ | rst_sym: (x,y:A)(clos_refl_sym_trans x y)->(clos_refl_sym_trans y x)
+ | rst_trans: (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.
+
+
+Section Transposee.
+ Variable A: Set.
+ Variable R: (relation A).
+
+ Definition transp := [x,y:A](R y x).
+End Transposee.
+
+
+Section Union.
+ Variable A: Set.
+ Variable R1,R2: (relation A).
+
+ Definition union := [x,y:A](R1 x y)\/(R2 x y).
+End Union.
+
+
+Section Disjoint_Union.
+Variable A,B:Set.
+Variable leA: A->A->Prop.
+Variable leB: B->B->Prop.
+
+Inductive le_AsB : A+B->A+B->Prop :=
+ le_aa: (x,y:A) (leA x y) -> (le_AsB (inl A B x) (inl A B y))
+| le_ab: (x:A)(y:B) (le_AsB (inl A B x) (inr A B y))
+| le_bb: (x,y:B) (leB x y) -> (le_AsB (inr A B x) (inr A B y)).
+
+End Disjoint_Union.
+
+
+
+Section Lexicographic_Product.
+(* Lexicographic order on dependent pairs *)
+
+Variable A:Set.
+Variable B:A->Set.
+Variable leA: A->A->Prop.
+Variable leB: (x:A)(B x)->(B x)->Prop.
+
+Inductive lexprod : (sigS A B) -> (sigS A B) ->Prop :=
+ left_lex : (x,x':A)(y:(B x)) (y':(B x'))
+ (leA x x') ->(lexprod (existS A B x y) (existS A B x' y'))
+| right_lex : (x:A) (y,y':(B x))
+ (leB x y y') -> (lexprod (existS A B x y) (existS A B x y')).
+End Lexicographic_Product.
+
+
+Section Symmetric_Product.
+ Variable A:Set.
+ Variable B:Set.
+ Variable leA: A->A->Prop.
+ Variable leB: B->B->Prop.
+
+ Inductive symprod : (A*B) -> (A*B) ->Prop :=
+ left_sym : (x,x':A)(leA x x')->(y:B)(symprod (x,y) (x',y))
+ | right_sym : (y,y':B)(leB y y')->(x:A)(symprod (x,y) (x,y')).
+
+End Symmetric_Product.
+
+
+Section Swap.
+ Variable A:Set.
+ Variable R:A->A->Prop.
+
+ Inductive swapprod: (A*A)->(A*A)->Prop :=
+ sp_noswap: (x,x':A*A)(symprod A A R R x x')->(swapprod x x')
+ | sp_swap: (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.
+Local Nil := (nil A).
+Local List := (list A).
+
+Inductive Ltl : List->List->Prop :=
+ Lt_nil: (a:A)(x:List)(Ltl Nil (cons a x))
+| Lt_hd : (a,b:A) (leA a b)-> (x,y:(list A))(Ltl (cons a x) (cons b y))
+| Lt_tl : (a:A)(x,y:List)(Ltl x y) -> (Ltl (cons a x) (cons a y)).
+
+
+Inductive Desc : List->Prop :=
+ d_nil : (Desc Nil)
+| d_one : (x:A)(Desc (cons x Nil))
+| d_conc : (x,y:A)(l:List)(leA x y)
+ -> (Desc l^(cons y Nil))->(Desc (l^(cons y Nil))^(cons x Nil)).
+
+Definition Pow :Set := (sig List Desc).
+
+Definition lex_exp : Pow -> Pow ->Prop :=
+ [a,b:Pow](Ltl (proj1_sig List Desc a) (proj1_sig List Desc b)).
+
+End Lexicographic_Exponentiation.
+
+Hints Unfold transp union : sets v62.
+Hints Resolve t_step rt_step rt_refl rst_step rst_refl : sets v62.
+Hints Immediate rst_sym : sets v62.
diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v
new file mode 100755
index 000000000..f11537a6e
--- /dev/null
+++ b/theories/Relations/Relations.v
@@ -0,0 +1,21 @@
+
+(* $Id$ *)
+
+Require Export Relation_Definitions.
+Require Export Relation_Operators.
+Require Export Operators_Properties.
+
+Lemma inverse_image_of_equivalence : (A,B:Set)(f:A->B)
+ (r:(relation B))(equivalence B r)->(equivalence A [x,y:A](r (f x) (f y))).
+Intros; Split; Elim H; Red; Auto.
+Intros; Apply equiv_trans with (f y); Assumption.
+Save.
+
+Lemma inverse_image_of_eq : (A,B:Set)(f:A->B)
+ (equivalence A [x,y:A](f x)=(f y)).
+Split; Red;
+[ (* reflexivity *) Reflexivity
+| (* transitivity *) Intros; Transitivity (f y); Assumption
+| (* symmetry *) Intros; Symmetry; Assumption
+].
+Save.
diff --git a/theories/Relations/Rstar.v b/theories/Relations/Rstar.v
new file mode 100755
index 000000000..fb503386c
--- /dev/null
+++ b/theories/Relations/Rstar.v
@@ -0,0 +1,66 @@
+
+(* $Id$ *)
+
+(* Properties of a binary relation R on type A *)
+
+ Parameter A : Type.
+ Parameter 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](P:A->A->Prop)
+ ((u:A)(P u u))->((u:A)(v:A)(w:A)(R u v)->(P v w)->(P u w)) -> (P x y).
+
+Theorem Rstar_reflexive: (x:A)(Rstar x x).
+ Proof [x:A][P:A->A->Prop]
+ [h1:(u:A)(P u u)][h2:(u:A)(v:A)(w:A)(R u v)->(P v w)->(P u w)]
+ (h1 x).
+
+Theorem Rstar_R: (x:A)(y:A)(z:A)(R x y)->(Rstar y z)->(Rstar x z).
+ Proof [x:A][y:A][z:A][t1:(R x y)][t2:(Rstar y z)]
+ [P:A->A->Prop]
+ [h1:(u:A)(P u u)][h2:(u:A)(v:A)(w:A)(R u v)->(P v w)->(P u w)]
+ (h2 x y z t1 (t2 P h1 h2)).
+
+(* We conclude with transitivity of Rstar : *)
+
+Theorem Rstar_transitive: (x:A)(y:A)(z:A)(Rstar x y)->(Rstar y z)->(Rstar x z).
+ Proof [x:A][y:A][z:A][h:(Rstar x y)]
+ (h ([u:A][v:A](Rstar v z)->(Rstar u z))
+ ([u:A][t:(Rstar u z)]t)
+ ([u:A][v:A][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:A][y:A](P:A->A->Prop)
+ ((P x x))->((u:A)(R x u)->(Rstar u y)->(P x y)) -> (P x y).
+
+Theorem Rstar'_reflexive: (x:A)(Rstar' x x).
+ Proof [x:A][P:A->A->Prop][h:(P x x)][h':(u:A)(R x u)->(Rstar u x)->(P x x)]h.
+
+Theorem Rstar'_R: (x:A)(y:A)(z:A)(R x z)->(Rstar z y)->(Rstar' x y).
+ Proof [x:A][y:A][z:A][t1:(R x z)][t2:(Rstar z y)]
+ [P:A->A->Prop][h1:(P x x)]
+ [h2:(u:A)(R x u)->(Rstar u y)->(P x y)](h2 z t1 t2).
+
+(* Equivalence of the two definitions: *)
+
+Theorem Rstar'_Rstar: (x:A)(y:A)(Rstar' x y)->(Rstar x y).
+ Proof [x:A][y:A][h:(Rstar' x y)]
+ (h Rstar (Rstar_reflexive x) ([u:A](Rstar_R x u y))).
+
+Theorem Rstar_Rstar': (x:A)(y:A)(Rstar x y)->(Rstar' x y).
+ Proof [x:A][y:A][h:(Rstar x y)](h Rstar' ([u:A](Rstar'_reflexive u))
+ ([u:A][v:A][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]
+ (x,y:A)(R1 y x)->(z:A)(R2 z y)
+ ->(EX y':A |(R2 y' x) & (R1 z y')).