diff options
Diffstat (limited to 'theories/Classes/Morphisms_Prop.v')
| -rw-r--r-- | theories/Classes/Morphisms_Prop.v | 59 |
1 files changed, 9 insertions, 50 deletions
diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v index c3737658..096c96e5 100644 --- a/theories/Classes/Morphisms_Prop.v +++ b/theories/Classes/Morphisms_Prop.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 *) @@ -16,7 +16,7 @@ Require Import Coq.Classes.Morphisms. Require Import Coq.Program.Basics. Require Import Coq.Program.Tactics. -Local Obligation Tactic := simpl_relation. +Local Obligation Tactic := try solve [simpl_relation | firstorder auto]. (** Standard instances for [not], [iff] and [impl]. *) @@ -52,61 +52,20 @@ Program Instance iff_iff_iff_impl_morphism : Proper (iff ==> iff ==> iff) impl. Program Instance ex_iff_morphism {A : Type} : Proper (pointwise_relation A iff ==> iff) (@ex A). - Next Obligation. - Proof. - unfold pointwise_relation in H. - split ; intros. - destruct H0 as [x1 H1]. - exists x1. rewrite H in H1. assumption. - - destruct H0 as [x1 H1]. - exists x1. rewrite H. assumption. - Qed. - Program Instance ex_impl_morphism {A : Type} : Proper (pointwise_relation A impl ==> impl) (@ex A) | 1. - Next Obligation. - Proof. - unfold pointwise_relation in H. - exists H0. apply H. assumption. - Qed. - -Program Instance ex_inverse_impl_morphism {A : Type} : - Proper (pointwise_relation A (inverse impl) ==> inverse impl) (@ex A) | 1. - - Next Obligation. - Proof. - unfold pointwise_relation in H. - exists H0. apply H. assumption. - Qed. +Program Instance ex_flip_impl_morphism {A : Type} : + Proper (pointwise_relation A (flip impl) ==> flip impl) (@ex A) | 1. Program Instance all_iff_morphism {A : Type} : Proper (pointwise_relation A iff ==> iff) (@all A). - Next Obligation. - Proof. - unfold pointwise_relation, all in *. - intuition ; specialize (H x0) ; intuition. - Qed. - Program Instance all_impl_morphism {A : Type} : Proper (pointwise_relation A impl ==> impl) (@all A) | 1. - Next Obligation. - Proof. - unfold pointwise_relation, all in *. - intuition ; specialize (H x0) ; intuition. - Qed. - -Program Instance all_inverse_impl_morphism {A : Type} : - Proper (pointwise_relation A (inverse impl) ==> inverse impl) (@all A) | 1. - - Next Obligation. - Proof. - unfold pointwise_relation, all in *. - intuition ; specialize (H x0) ; intuition. - Qed. +Program Instance all_flip_impl_morphism {A : Type} : + Proper (pointwise_relation A (flip impl) ==> flip impl) (@all A) | 1. (** Equivalent points are simultaneously accessible or not *) @@ -116,13 +75,13 @@ Instance Acc_pt_morphism {A:Type}(E R : A->A->Prop) Proof. apply proper_sym_impl_iff; auto with *. intros x y EQ WF. apply Acc_intro; intros z Hz. - rewrite <- EQ in Hz. now apply Acc_inv with x. +rewrite <- EQ in Hz. now apply Acc_inv with x. Qed. (** Equivalent relations have the same accessible points *) Instance Acc_rel_morphism {A:Type} : - Proper (@relation_equivalence A ==> Logic.eq ==> iff) (@Acc A). + Proper (relation_equivalence ==> Logic.eq ==> iff) (@Acc A). Proof. apply proper_sym_impl_iff_2. red; now symmetry. red; now symmetry. intros R R' EQ a a' Ha WF. subst a'. @@ -133,7 +92,7 @@ Qed. (** Equivalent relations are simultaneously well-founded or not *) Instance well_founded_morphism {A : Type} : - Proper (@relation_equivalence A ==> iff) (@well_founded A). + Proper (relation_equivalence ==> iff) (@well_founded A). Proof. unfold well_founded. solve_proper. Qed. |