summaryrefslogtreecommitdiff
path: root/theories/Classes/Morphisms.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Classes/Morphisms.v')
-rw-r--r--theories/Classes/Morphisms.v140
1 files changed, 77 insertions, 63 deletions
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index c2ae026d..86097a56 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -13,16 +13,15 @@
Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
91405 Orsay, France *)
-(* $Id: Morphisms.v 11282 2008-07-28 11:51:53Z msozeau $ *)
+(* $Id: Morphisms.v 11709 2008-12-20 11:42:15Z msozeau $ *)
+
+Set Manual Implicit Arguments.
Require Import Coq.Program.Basics.
Require Import Coq.Program.Tactics.
Require Import Coq.Relations.Relation_Definitions.
Require Export Coq.Classes.RelationClasses.
-Set Implicit Arguments.
-Unset Strict Implicit.
-
(** * Morphisms.
We now turn to the definition of [Morphism] and declare standard instances.
@@ -32,13 +31,9 @@ Unset Strict Implicit.
The relation [R] will be instantiated by [respectful] and [A] by an arrow type
for usual morphisms. *)
-Class Morphism A (R : relation A) (m : A) : Prop :=
+Class Morphism {A} (R : relation A) (m : A) : Prop :=
respect : R m m.
-(** We make the type implicit, it can be infered from the relations. *)
-
-Implicit Arguments Morphism [A].
-
(** Respectful morphisms. *)
(** The fully dependent version, not used yet. *)
@@ -53,7 +48,7 @@ Definition respectful_hetero
(** The non-dependent version is an instance where we forget dependencies. *)
-Definition respectful (A B : Type)
+Definition respectful {A B : Type}
(R : relation A) (R' : relation B) : relation (A -> B) :=
Eval compute in @respectful_hetero A A (fun _ => B) (fun _ => B) R (fun _ _ => R').
@@ -75,13 +70,20 @@ Arguments Scope respectful [type_scope type_scope signature_scope signature_scop
Open Local Scope signature_scope.
-(** Pointwise lifting is just respect with leibniz equality on the left. *)
+(** Dependent pointwise lifting of a relation on the range. *)
+
+Definition forall_relation {A : Type} {B : A -> Type} (sig : Π a : A, relation (B a)) : relation (Π x : A, B x) :=
+ λ f g, Π a : A, sig a (f a) (g a).
+
+Arguments Scope forall_relation [type_scope type_scope signature_scope].
-Definition pointwise_relation {A B : Type} (R : relation B) : relation (A -> B) :=
- fun f g => forall x : A, R (f x) (g x).
+(** Non-dependent pointwise lifting *)
+
+Definition pointwise_relation (A : Type) {B : Type} (R : relation B) : relation (A -> B) :=
+ Eval compute in forall_relation (B:=λ _, B) (λ _, R).
Lemma pointwise_pointwise A B (R : relation B) :
- relation_equivalence (pointwise_relation R) (@eq A ==> R).
+ relation_equivalence (pointwise_relation A R) (@eq A ==> R).
Proof. intros. split. simpl_relation. firstorder. Qed.
(** We can build a PER on the Coq function space if we have PERs on the domain and
@@ -91,24 +93,26 @@ Hint Unfold Reflexive : core.
Hint Unfold Symmetric : core.
Hint Unfold Transitive : core.
-Program Instance respectful_per [ PER A (R : relation A), PER B (R' : relation B) ] :
- PER (A -> B) (R ==> R').
+Typeclasses Opaque respectful pointwise_relation forall_relation.
+
+Program Instance respectful_per `(PER A (R : relation A), PER B (R' : relation B)) :
+ PER (R ==> R').
Next Obligation.
Proof with auto.
- assert(R x0 x0).
+ assert(R x0 x0).
transitivity y0... symmetry...
transitivity (y x0)...
Qed.
(** Subrelations induce a morphism on the identity. *)
-Instance subrelation_id_morphism [ subrelation A R₁ R₂ ] : Morphism (R₁ ==> R₂) id.
+Instance subrelation_id_morphism `(subrelation A R₁ R₂) : Morphism (R₁ ==> R₂) id.
Proof. firstorder. Qed.
(** The subrelation property goes through products as usual. *)
-Instance morphisms_subrelation_respectful [ subl : subrelation A R₂ R₁, subr : subrelation B S₁ S₂ ] :
+Instance morphisms_subrelation_respectful `(subl : subrelation A R₂ R₁, subr : subrelation B S₁ S₂) :
subrelation (R₁ ==> S₁) (R₂ ==> S₂).
Proof. simpl_relation. apply subr. apply H. apply subl. apply H0. Qed.
@@ -119,8 +123,8 @@ Proof. simpl_relation. Qed.
(** [Morphism] is itself a covariant morphism for [subrelation]. *)
-Lemma subrelation_morphism [ mor : Morphism A R₁ m, unc : Unconvertible (relation A) R₁ R₂,
- sub : subrelation A R₁ R₂ ] : Morphism R₂ m.
+Lemma subrelation_morphism `(mor : Morphism A R₁ m, unc : Unconvertible (relation A) R₁ R₂,
+ sub : subrelation A R₁ R₂) : Morphism R₂ m.
Proof.
intros. apply sub. apply mor.
Qed.
@@ -153,14 +157,14 @@ Proof. firstorder. Qed.
Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl).
Proof. firstorder. Qed.
-Instance pointwise_subrelation [ sub : subrelation A R R' ] :
- subrelation (pointwise_relation (A:=B) R) (pointwise_relation R') | 4.
+Instance pointwise_subrelation {A} `(sub : subrelation B R R') :
+ subrelation (pointwise_relation A R) (pointwise_relation A R') | 4.
Proof. reduce. unfold pointwise_relation in *. apply sub. apply H. Qed.
(** The complement of a relation conserves its morphisms. *)
Program Instance complement_morphism
- [ mR : Morphism (A -> A -> Prop) (RA ==> RA ==> iff) R ] :
+ `(mR : Morphism (A -> A -> Prop) (RA ==> RA ==> iff) R) :
Morphism (RA ==> RA ==> iff) (complement R).
Next Obligation.
@@ -173,7 +177,7 @@ Program Instance complement_morphism
(** The [inverse] too, actually the [flip] instance is a bit more general. *)
Program Instance flip_morphism
- [ mor : Morphism (A -> B -> C) (RA ==> RB ==> RC) f ] :
+ `(mor : Morphism (A -> B -> C) (RA ==> RB ==> RC) f) :
Morphism (RB ==> RA ==> RC) (flip f).
Next Obligation.
@@ -185,7 +189,7 @@ Program Instance flip_morphism
contravariant in the first argument, covariant in the second. *)
Program Instance trans_contra_co_morphism
- [ Transitive A R ] : Morphism (R --> R ++> impl) R.
+ `(Transitive A R) : Morphism (R --> R ++> impl) R.
Next Obligation.
Proof with auto.
@@ -196,7 +200,7 @@ Program Instance trans_contra_co_morphism
(** Morphism declarations for partial applications. *)
Program Instance trans_contra_inv_impl_morphism
- [ Transitive A R ] : Morphism (R --> inverse impl) (R x) | 3.
+ `(Transitive A R) : Morphism (R --> inverse impl) (R x) | 3.
Next Obligation.
Proof with auto.
@@ -204,7 +208,7 @@ Program Instance trans_contra_inv_impl_morphism
Qed.
Program Instance trans_co_impl_morphism
- [ Transitive A R ] : Morphism (R ==> impl) (R x) | 3.
+ `(Transitive A R) : Morphism (R ==> impl) (R x) | 3.
Next Obligation.
Proof with auto.
@@ -212,7 +216,7 @@ Program Instance trans_co_impl_morphism
Qed.
Program Instance trans_sym_co_inv_impl_morphism
- [ PER A R ] : Morphism (R ==> inverse impl) (R x) | 2.
+ `(PER A R) : Morphism (R ==> inverse impl) (R x) | 2.
Next Obligation.
Proof with auto.
@@ -220,7 +224,7 @@ Program Instance trans_sym_co_inv_impl_morphism
Qed.
Program Instance trans_sym_contra_impl_morphism
- [ PER A R ] : Morphism (R --> impl) (R x) | 2.
+ `(PER A R) : Morphism (R --> impl) (R x) | 2.
Next Obligation.
Proof with auto.
@@ -228,7 +232,7 @@ Program Instance trans_sym_contra_impl_morphism
Qed.
Program Instance per_partial_app_morphism
- [ PER A R ] : Morphism (R ==> iff) (R x) | 1.
+ `(PER A R) : Morphism (R ==> iff) (R x) | 1.
Next Obligation.
Proof with auto.
@@ -242,7 +246,7 @@ Program Instance per_partial_app_morphism
to get an [R y z] goal. *)
Program Instance trans_co_eq_inv_impl_morphism
- [ Transitive A R ] : Morphism (R ==> (@eq A) ==> inverse impl) R | 2.
+ `(Transitive A R) : Morphism (R ==> (@eq A) ==> inverse impl) R | 2.
Next Obligation.
Proof with auto.
@@ -251,7 +255,7 @@ Program Instance trans_co_eq_inv_impl_morphism
(** Every Symmetric and Transitive relation gives rise to an equivariant morphism. *)
-Program Instance PER_morphism [ PER A R ] : Morphism (R ==> R ==> iff) R | 1.
+Program Instance PER_morphism `(PER A R) : Morphism (R ==> R ==> iff) R | 1.
Next Obligation.
Proof with auto.
@@ -261,7 +265,7 @@ Program Instance PER_morphism [ PER A R ] : Morphism (R ==> R ==> iff) R | 1.
transitivity y... transitivity y0... symmetry...
Qed.
-Lemma symmetric_equiv_inverse [ Symmetric A R ] : relation_equivalence R (flip R).
+Lemma symmetric_equiv_inverse `(Symmetric A R) : relation_equivalence R (flip R).
Proof. firstorder. Qed.
Program Instance compose_morphism A B C R₀ R₁ R₂ :
@@ -276,7 +280,7 @@ Program Instance compose_morphism A B C R₀ R₁ R₂ :
(** Coq functions are morphisms for leibniz equality,
applied only if really needed. *)
-Instance reflexive_eq_dom_reflexive (A : Type) [ Reflexive B R' ] :
+Instance reflexive_eq_dom_reflexive (A : Type) `(Reflexive B R') :
Reflexive (@Logic.eq A ==> R').
Proof. simpl_relation. Qed.
@@ -307,20 +311,20 @@ Qed.
to set different priorities in different hint bases and select a particular hint database for
resolution of a type class constraint.*)
-Class MorphismProxy A (R : relation A) (m : A) : Prop :=
+Class MorphismProxy {A} (R : relation A) (m : A) : Prop :=
respect_proxy : R m m.
Instance reflexive_morphism_proxy
- [ Reflexive A R ] (x : A) : MorphismProxy R x | 1.
+ `(Reflexive A R) (x : A) : MorphismProxy R x | 1.
Proof. firstorder. Qed.
Instance morphism_morphism_proxy
- [ Morphism A R x ] : MorphismProxy R x | 2.
+ `(Morphism A R x) : MorphismProxy R x | 2.
Proof. firstorder. Qed.
(** [R] is Reflexive, hence we can build the needed proof. *)
-Lemma Reflexive_partial_app_morphism [ Morphism (A -> B) (R ==> R') m, MorphismProxy A R x ] :
+Lemma Reflexive_partial_app_morphism `(Morphism (A -> B) (R ==> R') m, MorphismProxy A R x) :
Morphism R' (m x).
Proof. simpl_relation. Qed.
@@ -399,38 +403,48 @@ Qed.
(** Special-purpose class to do normalization of signatures w.r.t. inverse. *)
-Class (A : Type) => Normalizes (m : relation A) (m' : relation A) : Prop :=
+Class Normalizes (A : Type) (m : relation A) (m' : relation A) : Prop :=
normalizes : relation_equivalence m m'.
-Instance inverse_respectful_norm :
- ! Normalizes (A -> B) (inverse R ==> inverse R') (inverse (R ==> R')) .
-Proof. firstorder. Qed.
+(** Current strategy: add [inverse] everywhere and reduce using [subrelation]
+ afterwards. *)
+
+Lemma inverse_atom A R : Normalizes A R (inverse (inverse R)).
+Proof.
+ firstorder.
+Qed.
-(* If not an inverse on the left, do a double inverse. *)
+Lemma inverse_arrow `(NA : Normalizes A R (inverse R'''), NB : Normalizes B R' (inverse R'')) :
+ Normalizes (A -> B) (R ==> R') (inverse (R''' ==> R'')%signature).
+Proof. unfold Normalizes. intros.
+ rewrite NA, NB. firstorder.
+Qed.
+
+Ltac inverse :=
+ match goal with
+ | [ |- Normalizes _ (respectful _ _) _ ] => eapply @inverse_arrow
+ | _ => eapply @inverse_atom
+ end.
+
+Hint Extern 1 (Normalizes _ _ _) => inverse : typeclass_instances.
+
+(** Treating inverse: can't make them direct instances as we
+ need at least a [flip] present in the goal. *)
-Instance not_inverse_respectful_norm :
- ! Normalizes (A -> B) (R ==> inverse R') (inverse (inverse R ==> R')) | 4.
+Lemma inverse1 `(subrelation A R' R) : subrelation (inverse (inverse R')) R.
Proof. firstorder. Qed.
-Instance inverse_respectful_rec_norm [ Normalizes B R' (inverse R'') ] :
- ! Normalizes (A -> B) (inverse R ==> R') (inverse (R ==> R'')).
-Proof. red ; intros.
- assert(r:=normalizes).
- setoid_rewrite r.
- setoid_rewrite inverse_respectful.
- reflexivity.
-Qed.
+Lemma inverse2 `(subrelation A R R') : subrelation R (inverse (inverse R')).
+Proof. firstorder. Qed.
-(** Once we have normalized, we will apply this instance to simplify the problem. *)
+Hint Extern 1 (subrelation (flip _) _) => eapply @inverse1 : typeclass_instances.
+Hint Extern 1 (subrelation _ (flip _)) => eapply @inverse2 : typeclass_instances.
-Definition morphism_inverse_morphism [ mor : Morphism A R m ] : Morphism (inverse R) m := mor.
+(** Once we have normalized, we will apply this instance to simplify the problem. *)
-Ltac morphism_inverse :=
- match goal with
- [ |- @Morphism _ (flip _) _ ] => eapply @morphism_inverse_morphism
- end.
+Definition morphism_inverse_morphism `(mor : Morphism A R m) : Morphism (inverse R) m := mor.
-Hint Extern 2 (@Morphism _ _ _) => morphism_inverse : typeclass_instances.
+Hint Extern 2 (@Morphism _ (flip _) _) => eapply @morphism_inverse_morphism : typeclass_instances.
(** Bootstrap !!! *)
@@ -445,7 +459,7 @@ Proof.
apply H0.
Qed.
-Lemma morphism_releq_morphism [ Normalizes A R R', Morphism _ R' m ] : Morphism R m.
+Lemma morphism_releq_morphism `(Normalizes A R R', Morphism _ R' m) : Morphism R m.
Proof.
intros.
@@ -467,7 +481,7 @@ Hint Extern 6 (@Morphism _ _ _) => morphism_normalization : typeclass_instances.
(** Every reflexive relation gives rise to a morphism, only for immediately solving goals without variables. *)
-Lemma reflexive_morphism [ Reflexive A R ] (x : A)
+Lemma reflexive_morphism `{Reflexive A R} (x : A)
: Morphism R x.
Proof. firstorder. Qed.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 02:40:29 +0000