diff options
Diffstat (limited to 'theories/Relations')
| -rw-r--r-- | theories/Relations/Operators_Properties.v | 33 | ||||
| -rw-r--r-- | theories/Relations/Relation_Definitions.v | 2 | ||||
| -rw-r--r-- | theories/Relations/Relation_Operators.v | 18 | ||||
| -rw-r--r-- | theories/Relations/Relations.v | 2 |
4 files changed, 49 insertions, 6 deletions
diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v index 4efc528e..95d9cfa9 100644 --- a/theories/Relations/Operators_Properties.v +++ b/theories/Relations/Operators_Properties.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -17,6 +17,7 @@ Require Import Relation_Operators. Section Properties. + Arguments clos_refl [A] R x _. Arguments clos_refl_trans [A] R x _. Arguments clos_refl_trans_1n [A] R x _. Arguments clos_refl_trans_n1 [A] R x _. @@ -34,7 +35,8 @@ Section Properties. Section Clos_Refl_Trans. - Local Notation "R *" := (clos_refl_trans R) (at level 8, left associativity). + Local Notation "R *" := (clos_refl_trans R) + (at level 8, left associativity, format "R *"). (** Correctness of the reflexive-transitive closure operator *) @@ -71,6 +73,26 @@ Section Properties. apply rst_trans with y; auto with sets. Qed. + (** Reflexive closure is included in the + reflexive-transitive closure *) + + Lemma clos_r_clos_rt : + inclusion (clos_refl R) (clos_refl_trans R). + Proof. + induction 1 as [? ?| ]. + constructor; auto. + constructor 2. + Qed. + + Lemma clos_rt_t : forall x y z, + clos_refl_trans R x y -> clos_trans R y z -> + clos_trans R x z. + Proof. + induction 1 as [b d H1|b|a b d H1 H2 IH1 IH2]; auto. + intro H. apply t_trans with (y:=d); auto. + constructor. auto. + Qed. + (** Correctness of the reflexive-symmetric-transitive closure *) Lemma clos_rst_is_equiv : equivalence A (clos_refl_sym_trans R). @@ -382,6 +404,13 @@ Section Properties. End Equivalences. + Lemma clos_trans_transp_permute : forall x y, + transp _ (clos_trans R) x y <-> clos_trans (transp _ R) x y. + Proof. + split; induction 1; + (apply t_step; assumption) || eapply t_trans; eassumption. + Qed. + End Properties. (* begin hide *) diff --git a/theories/Relations/Relation_Definitions.v b/theories/Relations/Relation_Definitions.v index 390d38b5..a187f955 100644 --- a/theories/Relations/Relation_Definitions.v +++ b/theories/Relations/Relation_Definitions.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v index 701bc073..4e52017e 100644 --- a/theories/Relations/Relation_Operators.v +++ b/theories/Relations/Relation_Operators.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -46,6 +46,20 @@ Section Transitive_Closure. End Transitive_Closure. +(** ** Reflexive closure *) + +Section Reflexive_Closure. + Variable A : Type. + Variable R : relation A. + + (** Definition by direct transitive closure *) + + Inductive clos_refl (x: A) : A -> Prop := + | r_step (y:A) : R x y -> clos_refl x y + | r_refl : clos_refl x x. + +End Reflexive_Closure. + (** ** Reflexive-transitive closure *) Section Reflexive_Transitive_Closure. @@ -204,7 +218,7 @@ Section Lexicographic_Exponentiation. | d_nil : Desc Nil | d_one (x:A) : Desc (x :: Nil) | d_conc (x y:A) (l:List) : - leA x y -> Desc (l ++ y :: Nil) -> Desc ((l ++ y :: Nil) ++ x :: Nil). + clos_refl A leA x y -> Desc (l ++ y :: Nil) -> Desc ((l ++ y :: Nil) ++ x :: Nil). Definition Pow : Set := sig Desc. diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v index 6e634db3..ce849a16 100644 --- a/theories/Relations/Relations.v +++ b/theories/Relations/Relations.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |