blob: 7dc1f95ef54567d3ecfdae231ebe017924491b4e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
|
(* -*- coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms") -*- *)
(************************************************************************)
(* 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 *)
(************************************************************************)
(* Morphism instances for propositional connectives.
Author: Matthieu Sozeau
Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
91405 Orsay, France *)
Require Import Coq.Classes.Morphisms.
Require Import Coq.Program.Basics.
Require Import Coq.Program.Tactics.
(** Standard instances for [not], [iff] and [impl]. *)
(** Logical negation. *)
Program Instance not_impl_morphism :
Morphism (impl --> impl) not.
Program Instance not_iff_morphism :
Morphism (iff ++> iff) not.
(** Logical conjunction. *)
Program Instance and_impl_iff_morphism :
Morphism (impl ==> impl ==> impl) and.
(* Program Instance and_impl_iff_morphism : *)
(* Morphism (impl ==> iff ==> impl) and. *)
(* Program Instance and_iff_impl_morphism : *)
(* Morphism (iff ==> impl ==> impl) and. *)
(* Program Instance and_inverse_impl_iff_morphism : *)
(* Morphism (inverse impl ==> iff ==> inverse impl) and. *)
(* Program Instance and_iff_inverse_impl_morphism : *)
(* Morphism (iff ==> inverse impl ==> inverse impl) and. *)
Program Instance and_iff_morphism :
Morphism (iff ==> iff ==> iff) and.
(** Logical disjunction. *)
Program Instance or_impl_iff_morphism :
Morphism (impl ==> impl ==> impl) or.
(* Program Instance or_impl_iff_morphism : *)
(* Morphism (impl ==> iff ==> impl) or. *)
(* Program Instance or_iff_impl_morphism : *)
(* Morphism (iff ==> impl ==> impl) or. *)
(* Program Instance or_inverse_impl_iff_morphism : *)
(* Morphism (inverse impl ==> iff ==> inverse impl) or. *)
(* Program Instance or_iff_inverse_impl_morphism : *)
(* Morphism (iff ==> inverse impl ==> inverse impl) or. *)
Program Instance or_iff_morphism :
Morphism (iff ==> iff ==> iff) or.
(** Logical implication [impl] is a morphism for logical equivalence. *)
Program Instance iff_iff_iff_impl_morphism : Morphism (iff ==> iff ==> iff) impl.
(** Morphisms for quantifiers *)
Program Instance ex_iff_morphism {A : Type} : Morphism (pointwise_relation iff ==> iff) (@ex A).
Next Obligation.
Proof.
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.
Program Instance ex_impl_morphism {A : Type} :
Morphism (pointwise_relation impl ==> impl) (@ex A).
Next Obligation.
Proof.
unfold pointwise_relation in H.
exists H0. apply H. assumption.
Qed.
Program Instance ex_inverse_impl_morphism {A : Type} :
Morphism (pointwise_relation (inverse impl) ==> inverse impl) (@ex A).
Next Obligation.
Proof.
unfold pointwise_relation in H.
exists H0. apply H. assumption.
Qed.
Program Instance all_iff_morphism {A : Type} :
Morphism (pointwise_relation 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} :
Morphism (pointwise_relation impl ==> impl) (@all A).
Next Obligation.
Proof.
unfold pointwise_relation, all in *.
intuition ; specialize (H x0) ; intuition.
Qed.
Program Instance all_inverse_impl_morphism {A : Type} :
Morphism (pointwise_relation (inverse impl) ==> inverse impl) (@all A).
Next Obligation.
Proof.
unfold pointwise_relation, all in *.
intuition ; specialize (H x0) ; intuition.
Qed.
|
