diff options
Diffstat (limited to 'theories7/Relations')
| -rwxr-xr-x | theories7/Relations/Newman.v | 115 | ||||
| -rwxr-xr-x | theories7/Relations/Operators_Properties.v | 98 | ||||
| -rwxr-xr-x | theories7/Relations/Relation_Definitions.v | 83 | ||||
| -rwxr-xr-x | theories7/Relations/Relation_Operators.v | 157 | ||||
| -rwxr-xr-x | theories7/Relations/Relations.v | 28 | ||||
| -rwxr-xr-x | theories7/Relations/Rstar.v | 78 |
6 files changed, 559 insertions, 0 deletions
diff --git a/theories7/Relations/Newman.v b/theories7/Relations/Newman.v new file mode 100755 index 00000000..c53db971 --- /dev/null +++ b/theories7/Relations/Newman.v @@ -0,0 +1,115 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Newman.v,v 1.1.2.1 2004/07/16 19:31:37 herbelin Exp $ i*) + +Require Rstar. + +Section Newman. + +Variable A: Type. +Variable R: A->A->Prop. + +Local Rstar := (Rstar A R). +Local Rstar_reflexive := (Rstar_reflexive A R). +Local Rstar_transitive := (Rstar_transitive A R). +Local Rstar_Rstar' := (Rstar_Rstar' A R). + +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)) (*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 ([u:A][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 : (x:A)(confluence x). +Proof [x:A](Hyp1 x confluence Ind_proof). + +End Newman_section. + + +End Newman. + diff --git a/theories7/Relations/Operators_Properties.v b/theories7/Relations/Operators_Properties.v new file mode 100755 index 00000000..4f1818bc --- /dev/null +++ b/theories7/Relations/Operators_Properties.v @@ -0,0 +1,98 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Operators_Properties.v,v 1.1.2.1 2004/07/16 19:31:37 herbelin Exp $ i*) + +(****************************************************************************) +(* 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). +Qed. + + + +Lemma clos_rt_idempotent: + (incl (clos_refl_trans A (clos_refl_trans A R)) + (clos_refl_trans A R)). +Red. +NewInduction 1; Auto with sets. +Intros. +Apply rt_trans with y; Auto with sets. +Qed. + + 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. +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. +NewInduction 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. +NewInduction 1; Auto with sets. +Apply rst_trans with y; Auto with sets. +Qed. + +End Clos_Refl_Sym_Trans. + +End Properties. diff --git a/theories7/Relations/Relation_Definitions.v b/theories7/Relations/Relation_Definitions.v new file mode 100755 index 00000000..1e38e753 --- /dev/null +++ b/theories7/Relations/Relation_Definitions.v @@ -0,0 +1,83 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Relation_Definitions.v,v 1.1.2.1 2004/07/16 19:31:38 herbelin Exp $ i*) + +Section Relation_Definition. + + Variable A: Type. + + 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/theories7/Relations/Relation_Operators.v b/theories7/Relations/Relation_Operators.v new file mode 100755 index 00000000..14c2ae30 --- /dev/null +++ b/theories7/Relations/Relation_Operators.v @@ -0,0 +1,157 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Relation_Operators.v,v 1.1.2.1 2004/07/16 19:31:38 herbelin Exp $ i*) + +(****************************************************************************) +(* 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/theories7/Relations/Relations.v b/theories7/Relations/Relations.v new file mode 100755 index 00000000..694d0eec --- /dev/null +++ b/theories7/Relations/Relations.v @@ -0,0 +1,28 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Relations.v,v 1.1.2.1 2004/07/16 19:31:38 herbelin Exp $ i*) + +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 _ equiv_trans _ x y z H0 H1; Apply equiv_trans with (f y); Assumption. +Qed. + +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 +]. +Qed. diff --git a/theories7/Relations/Rstar.v b/theories7/Relations/Rstar.v new file mode 100755 index 00000000..3747b45e --- /dev/null +++ b/theories7/Relations/Rstar.v @@ -0,0 +1,78 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Rstar.v,v 1.1.2.1 2004/07/16 19:31:38 herbelin Exp $ i*) + +(** Properties of a binary relation [R] on type [A] *) + +Section Rstar. + +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](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')). + + +End Rstar. + |