diff options
Diffstat (limited to 'theories/Relations/Operators_Properties.v')
| -rw-r--r-- | theories/Relations/Operators_Properties.v | 144 |
1 files changed, 73 insertions, 71 deletions
diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v index 22a08a27..40fd8f36 100644 --- a/theories/Relations/Operators_Properties.v +++ b/theories/Relations/Operators_Properties.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Operators_Properties.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Operators_Properties.v 9245 2006-10-17 12:53:34Z notin $ i*) (****************************************************************************) (* Bruno Barras *) @@ -22,75 +22,77 @@ Section Properties. 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. + + Section Clos_Refl_Trans. + + Lemma clos_rt_is_preorder : preorder A (clos_refl_trans A R). + Proof. + 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). + Proof. + 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. + Proof. + 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). + Proof. + 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). + Proof. + 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). + Proof. + 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 |