diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /theories/Relations/Operators_Properties.v | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
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 *) |