diff options
Diffstat (limited to 'theories/Classes/Morphisms_Prop.v')
| -rw-r--r-- | theories/Classes/Morphisms_Prop.v | 30 |
1 files changed, 15 insertions, 15 deletions
diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v index b672651b9..5b61e2c07 100644 --- a/theories/Classes/Morphisms_Prop.v +++ b/theories/Classes/Morphisms_Prop.v @@ -7,7 +7,7 @@ (************************************************************************) (* [Proper] instances for propositional connectives. - + Author: Matthieu Sozeau Institution: LRI, CNRS UMR 8623 - Université Paris Sud 91405 Orsay, France *) @@ -25,7 +25,7 @@ Obligation Tactic := simpl_relation. Program Instance not_impl_morphism : Proper (impl --> impl) not | 1. -Program Instance not_iff_morphism : +Program Instance not_iff_morphism : Proper (iff ++> iff) not. (** Logical conjunction. *) @@ -33,15 +33,15 @@ Program Instance not_iff_morphism : Program Instance and_impl_morphism : Proper (impl ==> impl ==> impl) and | 1. -Program Instance and_iff_morphism : +Program Instance and_iff_morphism : Proper (iff ==> iff ==> iff) and. (** Logical disjunction. *) -Program Instance or_impl_morphism : +Program Instance or_impl_morphism : Proper (impl ==> impl ==> impl) or | 1. -Program Instance or_iff_morphism : +Program Instance or_iff_morphism : Proper (iff ==> iff ==> iff) or. (** Logical implication [impl] is a morphism for logical equivalence. *) @@ -54,11 +54,11 @@ Program Instance ex_iff_morphism {A : Type} : Proper (pointwise_relation A iff = Next Obligation. Proof. - unfold pointwise_relation in H. + unfold pointwise_relation in H. split ; intros. destruct H0 as [x₁ H₁]. exists x₁. rewrite H in H₁. assumption. - + destruct H0 as [x₁ H₁]. exists x₁. rewrite H. assumption. Qed. @@ -68,20 +68,20 @@ Program Instance ex_impl_morphism {A : Type} : Next Obligation. Proof. - unfold pointwise_relation in H. + unfold pointwise_relation in H. exists H0. apply H. assumption. Qed. -Program Instance ex_inverse_impl_morphism {A : Type} : +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. + unfold pointwise_relation in H. exists H0. apply H. assumption. Qed. -Program Instance all_iff_morphism {A : Type} : +Program Instance all_iff_morphism {A : Type} : Proper (pointwise_relation A iff ==> iff) (@all A). Next Obligation. @@ -90,18 +90,18 @@ Program Instance all_iff_morphism {A : Type} : intuition ; specialize (H x0) ; intuition. Qed. -Program Instance all_impl_morphism {A : Type} : +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} : +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 *. |