diff options
Diffstat (limited to 'theories/Relations/Operators_Properties.v')
| -rwxr-xr-x | theories/Relations/Operators_Properties.v | 96 |
1 files changed, 96 insertions, 0 deletions
diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v new file mode 100755 index 00000000..5e0e9ec8 --- /dev/null +++ b/theories/Relations/Operators_Properties.v @@ -0,0 +1,96 @@ +(************************************************************************) +(* 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.7.2.1 2004/07/16 19:31:16 herbelin Exp $ i*) + +(****************************************************************************) +(* Bruno Barras *) +(****************************************************************************) + +Require Import Relation_Definitions. +Require Import Relation_Operators. + + +Section Properties. + + Variable A : Set. + Variable R : relation A. + + Let incl (R1 R2:relation A) : Prop := forall 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 in |- *. +induction 1; auto with sets. +intros. +apply rt_trans with y; auto with sets. +Qed. + + Lemma clos_refl_trans_ind_left : + forall (A:Set) (R:A -> A -> Prop) (M:A) (P:A -> Prop), + P M -> + (forall P0 N:A, clos_refl_trans A R M P0 -> P P0 -> R P0 N -> P N) -> + forall 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 in |- *. +induction 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 in |- *. +induction 1; auto with sets. +apply rst_trans with y; auto with sets. +Qed. + +End Clos_Refl_Sym_Trans. + +End Properties.
\ No newline at end of file |