diff options
Diffstat (limited to 'theories/Relations/Operators_Properties.v')
| -rwxr-xr-x | theories/Relations/Operators_Properties.v | 100 |
1 files changed, 49 insertions, 51 deletions
diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v index 0ca819b84..9534f707f 100755 --- a/theories/Relations/Operators_Properties.v +++ b/theories/Relations/Operators_Properties.v @@ -12,55 +12,53 @@ (* Bruno Barras *) (****************************************************************************) -Require Relation_Definitions. -Require Relation_Operators. +Require Import Relation_Definitions. +Require Import Relation_Operators. Section Properties. - Variable A: Set. - Variable R: (relation A). + Variable A : Set. + Variable R : relation A. - Local incl : (relation A)->(relation A)->Prop := - [R1,R2: (relation A)] (x,y:A) (R1 x y) -> (R2 x y). + 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). + 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). +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. -NewInduction 1; Auto with sets. -Intros. -Apply rt_trans with y; Auto with sets. +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: (A:Set)(R:A->A->Prop)(M:A)(P:A->Prop) - (P M) - ->((P0,N:A) - (clos_refl_trans A R M P0)->(P P0)->(R P0 N)->(P N)) - ->(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. + 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. @@ -69,30 +67,30 @@ 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. -NewInduction 1; Auto with sets. -Apply rst_trans with y; Auto with sets. + 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). + 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_trans A R). -Exact (rst_sym 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. -NewInduction 1; Auto with sets. -Apply rst_trans with y; Auto with sets. + 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. +End Properties.
\ No newline at end of file |