1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* Typeclass-based morphism definition and standard, minimal instances.
11
Author: Matthieu Sozeau
12
Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
13
91405 Orsay, France *)
15
(* $Id: Morphisms.v 12189 2009-06-15 05:08:44Z msozeau $ *)
17
Require Import Coq.Program.Basics.
18
Require Import Coq.Program.Tactics.
19
Require Import Coq.Relations.Relation_Definitions.
20
Require Export Coq.Classes.RelationClasses.
24
We now turn to the definition of [Morphism] and declare standard instances.
25
These will be used by the [setoid_rewrite] tactic later. *)
27
(** A morphism on a relation [R] is an object respecting the relation (in its kernel).
28
The relation [R] will be instantiated by [respectful] and [A] by an arrow type
29
for usual morphisms. *)
31
Class Morphism {A} (R : relation A) (m : A) : Prop :=
34
(** Respectful morphisms. *)
36
(** The fully dependent version, not used yet. *)
38
Definition respectful_hetero
40
(C : A -> Type) (D : B -> Type)
42
(R' : forall (x : A) (y : B), C x -> D y -> Prop) :
43
(forall x : A, C x) -> (forall x : B, D x) -> Prop :=
44
fun f g => forall x y, R x y -> R' x y (f x) (g y).
46
(** The non-dependent version is an instance where we forget dependencies. *)
48
Definition respectful {A B : Type}
49
(R : relation A) (R' : relation B) : relation (A -> B) :=
50
Eval compute in @respectful_hetero A A (fun _ => B) (fun _ => B) R (fun _ _ => R').
52
(** Notations reminiscent of the old syntax for declaring morphisms. *)
54
Delimit Scope signature_scope with signature.
56
Arguments Scope Morphism [type_scope signature_scope].
57
Arguments Scope respectful [type_scope type_scope signature_scope signature_scope].
59
Module MorphismNotations.
61
Notation " R ++> R' " := (@respectful _ _ (R%signature) (R'%signature))
62
(right associativity, at level 55) : signature_scope.
64
Notation " R ==> R' " := (@respectful _ _ (R%signature) (R'%signature))
65
(right associativity, at level 55) : signature_scope.
67
Notation " R --> R' " := (@respectful _ _ (inverse (R%signature)) (R'%signature))
68
(right associativity, at level 55) : signature_scope.
70
End MorphismNotations.
72
Export MorphismNotations.
74
Open Local Scope signature_scope.
76
(** Dependent pointwise lifting of a relation on the range. *)
78
Definition forall_relation {A : Type} {B : A -> Type} (sig : Π a : A, relation (B a)) : relation (Π x : A, B x) :=
79
λ f g, Π a : A, sig a (f a) (g a).
81
Arguments Scope forall_relation [type_scope type_scope signature_scope].
83
(** Non-dependent pointwise lifting *)
85
Definition pointwise_relation (A : Type) {B : Type} (R : relation B) : relation (A -> B) :=
86
Eval compute in forall_relation (B:=λ _, B) (λ _, R).
88
Lemma pointwise_pointwise A B (R : relation B) :
89
relation_equivalence (pointwise_relation A R) (@eq A ==> R).
90
Proof. intros. split. simpl_relation. firstorder. Qed.
92
(** We can build a PER on the Coq function space if we have PERs on the domain and
95
Hint Unfold Reflexive : core.
96
Hint Unfold Symmetric : core.
97
Hint Unfold Transitive : core.
99
Typeclasses Opaque respectful pointwise_relation forall_relation.
101
Program Instance respectful_per `(PER A (R : relation A), PER B (R' : relation B)) :
107
transitivity y0... symmetry...
108
transitivity (y x0)...
111
(** Subrelations induce a morphism on the identity. *)
113
Instance subrelation_id_morphism `(subrelation A R₁ R₂) : Morphism (R₁ ==> R₂) id.
114
Proof. firstorder. Qed.
116
(** The subrelation property goes through products as usual. *)
118
Instance morphisms_subrelation_respectful `(subl : subrelation A R₂ R₁, subr : subrelation B S₁ S₂) :
119
subrelation (R₁ ==> S₁) (R₂ ==> S₂).
120
Proof. simpl_relation. apply subr. apply H. apply subl. apply H0. Qed.
122
(** And of course it is reflexive. *)
124
Instance morphisms_subrelation_refl : ! subrelation A R R.
125
Proof. simpl_relation. Qed.
127
(** [Morphism] is itself a covariant morphism for [subrelation]. *)
129
Lemma subrelation_morphism `(mor : Morphism A R₁ m, unc : Unconvertible (relation A) R₁ R₂,
130
sub : subrelation A R₁ R₂) : Morphism R₂ m.
132
intros. apply sub. apply mor.
135
Instance morphism_subrelation_morphism :
136
Morphism (subrelation ++> @eq _ ==> impl) (@Morphism A).
137
Proof. reduce. subst. firstorder. Qed.
139
(** We use an external tactic to manage the application of subrelation, which is otherwise
140
always applicable. We allow its use only once per branch. *)
142
Inductive subrelation_done : Prop := did_subrelation : subrelation_done.
144
Inductive normalization_done : Prop := did_normalization.
146
Ltac subrelation_tac :=
148
| [ _ : subrelation_done |- _ ] => fail 1
149
| [ |- @Morphism _ _ _ ] => let H := fresh "H" in
150
set(H:=did_subrelation) ; eapply @subrelation_morphism
153
Hint Extern 5 (@Morphism _ _ _) => subrelation_tac : typeclass_instances.
155
(** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *)
157
Instance iff_impl_subrelation : subrelation iff impl | 2.
158
Proof. firstorder. Qed.
160
Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl) | 2.
161
Proof. firstorder. Qed.
163
Instance pointwise_subrelation {A} `(sub : subrelation B R R') :
164
subrelation (pointwise_relation A R) (pointwise_relation A R') | 4.
165
Proof. reduce. unfold pointwise_relation in *. apply sub. apply H. Qed.
167
(** The complement of a relation conserves its morphisms. *)
169
Program Instance complement_morphism
170
`(mR : Morphism (A -> A -> Prop) (RA ==> RA ==> iff) R) :
171
Morphism (RA ==> RA ==> iff) (complement R).
176
pose (mR x y H x0 y0 H0).
180
(** The [inverse] too, actually the [flip] instance is a bit more general. *)
182
Program Instance flip_morphism
183
`(mor : Morphism (A -> B -> C) (RA ==> RB ==> RC) f) :
184
Morphism (RB ==> RA ==> RC) (flip f).
191
(** Every Transitive relation gives rise to a binary morphism on [impl],
192
contravariant in the first argument, covariant in the second. *)
194
Program Instance trans_contra_co_morphism
195
`(Transitive A R) : Morphism (R --> R ++> impl) R.
203
(** Morphism declarations for partial applications. *)
205
Program Instance trans_contra_inv_impl_morphism
206
`(Transitive A R) : Morphism (R --> inverse impl) (R x) | 3.
213
Program Instance trans_co_impl_morphism
214
`(Transitive A R) : Morphism (R ==> impl) (R x) | 3.
221
Program Instance trans_sym_co_inv_impl_morphism
222
`(PER A R) : Morphism (R ==> inverse impl) (R x) | 2.
226
transitivity y... symmetry...
229
Program Instance trans_sym_contra_impl_morphism
230
`(PER A R) : Morphism (R --> impl) (R x) | 2.
234
transitivity x0... symmetry...
237
Program Instance per_partial_app_morphism
238
`(PER A R) : Morphism (R ==> iff) (R x) | 1.
242
split. intros ; transitivity x0...
248
(** Every Transitive relation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof
249
to get an [R y z] goal. *)
251
Program Instance trans_co_eq_inv_impl_morphism
252
`(Transitive A R) : Morphism (R ==> (@eq A) ==> inverse impl) R | 2.
259
(** Every Symmetric and Transitive relation gives rise to an equivariant morphism. *)
261
Program Instance PER_morphism `(PER A R) : Morphism (R ==> R ==> iff) R | 1.
266
transitivity x0... transitivity x... symmetry...
268
transitivity y... transitivity y0... symmetry...
271
Lemma symmetric_equiv_inverse `(Symmetric A R) : relation_equivalence R (flip R).
272
Proof. firstorder. Qed.
274
Program Instance compose_morphism A B C R₀ R₁ R₂ :
275
Morphism ((R₁ ==> R₂) ==> (R₀ ==> R₁) ==> (R₀ ==> R₂)) (@compose A B C).
280
unfold compose. apply H. apply H0. apply H1.
283
(** Coq functions are morphisms for leibniz equality,
284
applied only if really needed. *)
286
Instance reflexive_eq_dom_reflexive (A : Type) `(Reflexive B R') :
287
Reflexive (@Logic.eq A ==> R').
288
Proof. simpl_relation. Qed.
290
(** [respectful] is a morphism for relation equivalence. *)
292
Instance respectful_morphism :
293
Morphism (relation_equivalence ++> relation_equivalence ++> relation_equivalence) (@respectful A B).
296
unfold respectful, relation_equivalence, predicate_equivalence in * ; simpl in *.
310
(** Every element in the carrier of a reflexive relation is a morphism for this relation.
311
We use a proxy class for this case which is used internally to discharge reflexivity constraints.
312
The [Reflexive] instance will almost always be used, but it won't apply in general to any kind of
313
[Morphism (A -> B) _ _] goal, making proof-search much slower. A cleaner solution would be to be able
314
to set different priorities in different hint bases and select a particular hint database for
315
resolution of a type class constraint.*)
317
Class MorphismProxy {A} (R : relation A) (m : A) : Prop :=
318
respect_proxy : R m m.
320
Instance reflexive_morphism_proxy
321
`(Reflexive A R) (x : A) : MorphismProxy R x | 1.
322
Proof. firstorder. Qed.
324
Instance morphism_morphism_proxy
325
`(Morphism A R x) : MorphismProxy R x | 2.
326
Proof. firstorder. Qed.
328
(** [R] is Reflexive, hence we can build the needed proof. *)
330
Lemma Reflexive_partial_app_morphism `(Morphism (A -> B) (R ==> R') m, MorphismProxy A R x) :
332
Proof. simpl_relation. Qed.
334
Class Params {A : Type} (of : A) (arity : nat).
336
Class PartialApplication.
338
Ltac partial_application_tactic :=
339
let rec do_partial_apps H m :=
341
| ?m' ?x => eapply @Reflexive_partial_app_morphism ; [do_partial_apps H m'|clear H]
345
let rec do_partial H ar m :=
347
| 0 => do_partial_apps H m
350
?m' ?x => do_partial H n' m'
355
let m' := fresh in head_of_constr m' m ;
356
let n := fresh in evar (n:nat) ;
357
let v := eval compute in n in clear n ;
359
assert(H:Params m' v) by typeclasses eauto ;
360
let v' := eval compute in v in
364
| [ _ : subrelation_done |- _ ] => fail 1
365
| [ _ : normalization_done |- _ ] => fail 1
366
| [ _ : @Params _ _ _ |- _ ] => fail 1
367
| [ |- @Morphism ?T _ (?m ?x) ] =>
369
| [ _ : PartialApplication |- _ ] =>
370
eapply @Reflexive_partial_app_morphism
373
(eapply @Reflexive_partial_app_morphism ;
374
[ pose Build_PartialApplication | idtac ])
378
Hint Extern 4 (@Morphism _ _ _) => partial_application_tactic : typeclass_instances.
380
Lemma inverse_respectful : forall (A : Type) (R : relation A) (B : Type) (R' : relation B),
381
relation_equivalence (inverse (R ==> R')) (inverse R ==> inverse R').
384
unfold flip, respectful.
385
split ; intros ; intuition.
388
(** Special-purpose class to do normalization of signatures w.r.t. inverse. *)
390
Class Normalizes (A : Type) (m : relation A) (m' : relation A) : Prop :=
391
normalizes : relation_equivalence m m'.
393
(** Current strategy: add [inverse] everywhere and reduce using [subrelation]
396
Lemma inverse_atom A R : Normalizes A R (inverse (inverse R)).
401
Lemma inverse_arrow `(NA : Normalizes A R (inverse R'''), NB : Normalizes B R' (inverse R'')) :
402
Normalizes (A -> B) (R ==> R') (inverse (R''' ==> R'')%signature).
403
Proof. unfold Normalizes. intros.
404
rewrite NA, NB. firstorder.
409
| [ |- Normalizes _ (respectful _ _) _ ] => eapply @inverse_arrow
410
| _ => eapply @inverse_atom
413
Hint Extern 1 (Normalizes _ _ _) => inverse : typeclass_instances.
415
(** Treating inverse: can't make them direct instances as we
416
need at least a [flip] present in the goal. *)
418
Lemma inverse1 `(subrelation A R' R) : subrelation (inverse (inverse R')) R.
419
Proof. firstorder. Qed.
421
Lemma inverse2 `(subrelation A R R') : subrelation R (inverse (inverse R')).
422
Proof. firstorder. Qed.
424
Hint Extern 1 (subrelation (flip _) _) => eapply @inverse1 : typeclass_instances.
425
Hint Extern 1 (subrelation _ (flip _)) => eapply @inverse2 : typeclass_instances.
427
(** Once we have normalized, we will apply this instance to simplify the problem. *)
429
Definition morphism_inverse_morphism `(mor : Morphism A R m) : Morphism (inverse R) m := mor.
431
Hint Extern 2 (@Morphism _ (flip _) _) => eapply @morphism_inverse_morphism : typeclass_instances.
435
Instance morphism_morphism : Morphism (relation_equivalence ==> @eq _ ==> iff) (@Morphism A).
439
split ; red ; intros.
446
Lemma morphism_releq_morphism `(Normalizes A R R', Morphism _ R' m) : Morphism R m.
451
pose normalizes as norm.
456
Ltac morphism_normalization :=
458
| [ _ : subrelation_done |- _ ] => fail 1
459
| [ _ : normalization_done |- _ ] => fail 1
460
| [ |- @Morphism _ _ _ ] => let H := fresh "H" in
461
set(H:=did_normalization) ; eapply @morphism_releq_morphism
464
Hint Extern 6 (@Morphism _ _ _) => morphism_normalization : typeclass_instances.
466
(** Every reflexive relation gives rise to a morphism, only for immediately solving goals without variables. *)
468
Lemma reflexive_morphism `{Reflexive A R} (x : A)
470
Proof. firstorder. Qed.
472
Ltac morphism_reflexive :=
474
| [ _ : normalization_done |- _ ] => fail 1
475
| [ _ : subrelation_done |- _ ] => fail 1
476
| [ |- @Morphism _ _ _ ] => eapply @reflexive_morphism
479
Hint Extern 7 (@Morphism _ _ _) => morphism_reflexive : typeclass_instances.
added
removed
theories/Classes/Morphisms.v
