diff options
Diffstat (limited to 'theories/Relations/Operators_Properties.v')
| -rw-r--r-- | theories/Relations/Operators_Properties.v | 33 |
1 files changed, 31 insertions, 2 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 *) |