aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/subtac/subtac_classes.ml4
-rw-r--r--interp/implicit_quantifiers.ml8
-rw-r--r--parsing/g_vernac.ml45
-rw-r--r--tactics/class_tactics.ml431
-rw-r--r--theories/Classes/Equivalence.v16
-rw-r--r--theories/Classes/Functions.v14
-rw-r--r--theories/Classes/Morphisms.v53
-rw-r--r--theories/Classes/RelationClasses.v30
-rw-r--r--theories/Classes/SetoidDec.v10
-rw-r--r--toplevel/classes.ml141
-rw-r--r--toplevel/classes.mli3
-rw-r--r--toplevel/command.mli1
-rw-r--r--toplevel/vernacentries.ml2
13 files changed, 168 insertions, 150 deletions
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index 39865f1f9..0c99fe16e 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -107,7 +107,7 @@ let new_instance ctx (instid, bk, cl) props pri =
let bound, fvs = Implicit_quantifiers.free_vars_of_binders ~bound [] ctx in
let tclass =
match bk with
- | Explicit ->
+ | Implicit ->
let loc, id, par = Implicit_quantifiers.destClassAppExpl cl in
let k = class_info (Nametab.global id) in
let applen = List.fold_left (fun acc (x, y) -> if y = None then succ acc else acc) 0 par in
@@ -128,7 +128,7 @@ let new_instance ctx (instid, bk, cl) props pri =
par (List.rev k.cl_context)
in Topconstr.CAppExpl (loc, (None, id), pars)
- | Implicit -> cl
+ | Explicit -> cl
in
let ctx_bound = Idset.union bound (Implicit_quantifiers.ids_of_list fvs) in
let gen_ids = Implicit_quantifiers.free_vars_of_constr_expr ~bound:ctx_bound tclass [] in
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 3b2b5d3d4..3551746b8 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -172,7 +172,7 @@ let full_class_binders env l =
let l', avoid =
List.fold_left (fun (l', avoid) (iid, bk, cl as x) ->
match bk with
- Explicit ->
+ Implicit ->
let (loc, id, l) = destClassAppExpl cl in
let gr = Nametab.global id in
(try
@@ -180,14 +180,14 @@ let full_class_binders env l =
let args, avoid = combine_params_freevar avoid l (List.rev c.cl_context) in
(iid, bk, CAppExpl (loc, (None, id), args)) :: l', avoid
with Not_found -> not_a_class (Global.env ()) (constr_of_global gr))
- | Implicit -> (x :: l', avoid))
+ | Explicit -> (x :: l', avoid))
([], avoid) l
in List.rev l'
let constr_expr_of_constraint (kind, id) l =
match kind with
- | Explicit -> CAppExpl (fst id, (None, Ident id), l)
- | Implicit -> CApp (fst id, (None, CRef (Ident id)),
+ | Implicit -> CAppExpl (fst id, (None, Ident id), l)
+ | Explicit -> CApp (fst id, (None, CRef (Ident id)),
List.map (fun x -> x, None) l)
(* | CApp of loc * (proj_flag * constr_expr) * *)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 3b6740731..40c6180f0 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -492,6 +492,11 @@ GEXTEND Gram
| IDENT "Instance"; sup = OPT [ l = delimited_binders_let ; "=>" -> l ];
is = typeclass_constraint ; pri = OPT [ "|"; i = natural -> i ] ; props = typeclass_field_defs ->
let sup = match sup with None -> [] | Some l -> l in
+ let is = (* We reverse the default binding mode on the right *)
+ let n, bk, t = is in
+ n, (match bk with Rawterm.Implicit -> Rawterm.Explicit
+ | Rawterm.Explicit -> Rawterm.Implicit), t
+ in
VernacInstance (sup, is, props, pri)
| IDENT "Existing"; IDENT "Instance"; is = identref -> VernacDeclareInstance is
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index a3baa1abb..4f740f865 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -973,11 +973,11 @@ END
let mkappc s l = CAppExpl (dummy_loc,(None,(Libnames.Ident (dummy_loc,id_of_string s))),l)
-let declare_instance a aeq n s = ((dummy_loc,Name n),Explicit,
- CApp (dummy_loc, (None, mkRefC (Qualid (dummy_loc, qualid_of_string s))),
- [(a,None);(aeq,None)]))
+let declare_instance a aeq n s = ((dummy_loc,Name n), Explicit,
+ CAppExpl (dummy_loc, (None, Qualid (dummy_loc, qualid_of_string s)),
+ [a;aeq]))
-let anew_instance instance fields = new_instance [] instance fields None (fun _ -> ())
+let anew_instance instance fields = new_instance [] instance fields None
let require_library dirpath =
let qualid = (dummy_loc, Libnames.qualid_of_dirpath (Libnames.dirpath_of_string dirpath)) in
@@ -1104,6 +1104,7 @@ let declare_projection n instance_id r =
let c = constr_of_global r in
let term = respect_projection c ty in
let typ = Typing.type_of (Global.env ()) Evd.empty term in
+ let ctx, typ = Sign.decompose_prod_assum typ in
let typ =
let n =
let rec aux t =
@@ -1122,6 +1123,7 @@ let declare_projection n instance_id r =
let ctx,ccl = Reductionops.decomp_n_prod (Global.env()) Evd.empty (3 * n) typ
in it_mkProd_or_LetIn ccl ctx
in
+ let typ = it_mkProd_or_LetIn typ ctx in
let cst =
{ const_entry_body = term;
const_entry_type = Some typ;
@@ -1209,18 +1211,15 @@ VERNAC COMMAND EXTEND AddSetoid1
[ init_setoid ();
let instance_id = add_suffix n "_Morphism" in
let instance =
- ((dummy_loc,Name instance_id), Implicit,
- CApp (dummy_loc, (None, mkRefC
- (Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Classes.Morphisms.Morphism"))),
- [(s,None);(m,None)]))
- in
- if Lib.is_modtype () then (context ~hook:(fun r -> declare_projection n instance_id r) [ instance ])
- else (
- Flags.silently
- (fun () ->
- ignore(new_instance [] instance [] None (fun cst -> declare_projection n instance_id (ConstRef cst)));
- Pfedit.by (Tacinterp.interp <:tactic<add_morphism_tactic>>)) ();
- Flags.if_verbose (fun x -> msg (Printer.pr_open_subgoals x)) ())
+ ((dummy_loc,Name instance_id), Explicit,
+ CAppExpl (dummy_loc,
+ (None, Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Classes.Morphisms.Morphism")),
+ [cHole; s; m]))
+ in
+ let tac = Tacinterp.interp <:tactic<add_morphism_tactic>> in
+ ignore(new_instance [] instance []
+ ~tac ~hook:(fun cst -> declare_projection n instance_id (ConstRef cst))
+ None)
]
END
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 58aef9a7b..d0c999196 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -30,23 +30,23 @@ Open Local Scope signature_scope.
(** Every [Equivalence] gives a default relation, if no other is given (lowest priority). *)
-Instance [ ! Equivalence A R ] =>
+Instance [ Equivalence A R ] =>
equivalence_default : DefaultRelation A R | 4.
Definition equiv [ Equivalence A R ] : relation A := R.
(** Shortcuts to make proof search possible (unification won't unfold equiv). *)
-Program Instance [ sa : ! Equivalence A ] => equiv_refl : Reflexive equiv.
+Program Instance [ sa : Equivalence A ] => equiv_refl : Reflexive equiv.
-Program Instance [ sa : ! Equivalence A ] => equiv_sym : Symmetric equiv.
+Program Instance [ sa : Equivalence A ] => equiv_sym : Symmetric equiv.
Next Obligation.
Proof.
symmetry ; auto.
Qed.
-Program Instance [ sa : ! Equivalence A ] => equiv_trans : Transitive equiv.
+Program Instance [ sa : Equivalence A ] => equiv_trans : Transitive equiv.
Next Obligation.
Proof.
@@ -81,7 +81,7 @@ Ltac clsubst_nofail :=
Tactic Notation "clsubst" "*" := clsubst_nofail.
-Lemma nequiv_equiv_trans : forall [ ! Equivalence A ] (x y z : A), x =/= y -> y === z -> x =/= z.
+Lemma nequiv_equiv_trans : forall [ Equivalence A ] (x y z : A), x =/= y -> y === z -> x =/= z.
Proof with auto.
intros; intro.
assert(z === y) by (symmetry ; auto).
@@ -89,7 +89,7 @@ Proof with auto.
contradiction.
Qed.
-Lemma equiv_nequiv_trans : forall [ ! Equivalence A ] (x y z : A), x === y -> y =/= z -> x =/= z.
+Lemma equiv_nequiv_trans : forall [ Equivalence A ] (x y z : A), x === y -> y =/= z -> x =/= z.
Proof.
intros; intro.
assert(y === x) by (symmetry ; auto).
@@ -116,12 +116,12 @@ Ltac equivify := repeat equivify_tac.
(** Every equivalence relation gives rise to a morphism, as it is Transitive and Symmetric. *)
-Instance [ sa : ! Equivalence ] => equiv_morphism : Morphism (equiv ++> equiv ++> iff) equiv :=
+Instance [ sa : Equivalence ] => equiv_morphism : Morphism (equiv ++> equiv ++> iff) equiv :=
respect := respect.
(** The partial application too as it is Reflexive. *)
-Instance [ sa : ! Equivalence A ] (x : A) =>
+Instance [ sa : Equivalence A ] (x : A) =>
equiv_partial_app_morphism : Morphism (equiv ++> iff) (equiv x) :=
respect := respect.
diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v
index 28fa55ee1..4750df639 100644
--- a/theories/Classes/Functions.v
+++ b/theories/Classes/Functions.v
@@ -21,22 +21,22 @@ Require Import Coq.Classes.Morphisms.
Set Implicit Arguments.
Unset Strict Implicit.
-Class [ m : ! Morphism (A -> B) (RA ++> RB) f ] => Injective : Prop :=
+Class [ m : Morphism (A -> B) (RA ++> RB) f ] => Injective : Prop :=
injective : forall x y : A, RB (f x) (f y) -> RA x y.
-Class [ m : ! Morphism (A -> B) (RA ++> RB) f ] => Surjective : Prop :=
+Class [ m : Morphism (A -> B) (RA ++> RB) f ] => Surjective : Prop :=
surjective : forall y, exists x : A, RB y (f x).
-Definition Bijective [ m : ! Morphism (A -> B) (RA ++> RB) (f : A -> B) ] :=
+Definition Bijective [ m : Morphism (A -> B) (RA ++> RB) (f : A -> B) ] :=
Injective m /\ Surjective m.
-Class [ m : ! Morphism (A -> B) (eqA ++> eqB) ] => MonoMorphism :=
+Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => MonoMorphism :=
monic :> Injective m.
-Class [ m : ! Morphism (A -> B) (eqA ++> eqB) ] => EpiMorphism :=
+Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => EpiMorphism :=
epic :> Surjective m.
-Class [ m : ! Morphism (A -> B) (eqA ++> eqB) ] => IsoMorphism :=
+Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => IsoMorphism :=
monomorphism :> MonoMorphism m ; epimorphism :> EpiMorphism m.
-Class [ m : ! Morphism (A -> A) (eqA ++> eqA), IsoMorphism m ] => AutoMorphism.
+Class [ m : Morphism (A -> A) (eqA ++> eqA), ! IsoMorphism m ] => AutoMorphism.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index f4ec50989..eda2aecaa 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -152,7 +152,7 @@ Proof.
reduce. apply* H. apply* sub. assumption.
Qed.
-Lemma subrelation_morphism [ SubRelation A R₁ R₂, Morphism R₂ m ] : Morphism R₁ m.
+Lemma subrelation_morphism [ SubRelation A R₁ R₂, ! Morphism R₂ m ] : Morphism R₁ m.
Proof.
intros. apply* H. apply H0.
Qed.
@@ -177,7 +177,7 @@ Program Instance iff_iff_iff_impl_morphism : Morphism (iff ==> iff ==> iff) impl
(* Typeclasses eauto := debug. *)
-Program Instance [ ! Symmetric A R, Morphism (R ==> impl) m ] => Reflexive_impl_iff : Morphism (R ==> iff) m.
+Program Instance [ Symmetric A R, Morphism _ (R ==> impl) m ] => Reflexive_impl_iff : Morphism (R ==> iff) m.
Next Obligation.
Proof.
@@ -186,7 +186,7 @@ Program Instance [ ! Symmetric A R, Morphism (R ==> impl) m ] => Reflexive_impl_
(** The complement of a relation conserves its morphisms. *)
-Program Instance {A} (RA : relation A) [ mR : Morphism (RA ==> RA ==> iff) R ] =>
+Program Instance [ mR : Morphism (A -> A -> Prop) (RA ==> RA ==> iff) R ] =>
complement_morphism : Morphism (RA ==> RA ==> iff) (complement R).
Next Obligation.
@@ -200,7 +200,7 @@ Program Instance {A} (RA : relation A) [ mR : Morphism (RA ==> RA ==> iff) R ] =
(** The inverse too. *)
-Program Instance {A} (RA : relation A) [ Morphism (RA ==> RA ==> iff) R ] =>
+Program Instance [ Morphism (A -> _) (RA ==> RA ==> iff) R ] =>
inverse_morphism : Morphism (RA ==> RA ==> iff) (inverse R).
Next Obligation.
@@ -208,7 +208,7 @@ Program Instance {A} (RA : relation A) [ Morphism (RA ==> RA ==> iff) R ] =>
apply respect ; auto.
Qed.
-Program Instance {A B C : Type} [ Morphism (RA ==> RB ==> RC) (f : A -> B -> C) ] =>
+Program Instance [ Morphism (A -> B -> C) (RA ==> RB ==> RC) f ] =>
flip_morphism : Morphism (RB ==> RA ==> RC) (flip f).
Next Obligation.
@@ -219,7 +219,7 @@ Program Instance {A B C : Type} [ Morphism (RA ==> RB ==> RC) (f : A -> B -> C)
(** Every Transitive relation gives rise to a binary morphism on [impl],
contravariant in the first argument, covariant in the second. *)
-Program Instance [ ! Transitive A (R : relation A) ] =>
+Program Instance [ Transitive A R ] =>
trans_contra_co_morphism : Morphism (R --> R ++> impl) R.
Next Obligation.
@@ -230,7 +230,7 @@ Program Instance [ ! Transitive A (R : relation A) ] =>
(** Dually... *)
-Program Instance [ ! Transitive A (R : relation A) ] =>
+Program Instance [ Transitive A R ] =>
trans_co_contra_inv_impl_morphism : Morphism (R ++> R --> inverse impl) R.
Next Obligation.
@@ -252,7 +252,7 @@ Program Instance [ ! Transitive A (R : relation A) ] =>
(** Morphism declarations for partial applications. *)
-Program Instance [ ! Transitive A R ] (x : A) =>
+Program Instance [ Transitive A R ] (x : A) =>
trans_contra_inv_impl_morphism : Morphism (R --> inverse impl) (R x).
Next Obligation.
@@ -260,7 +260,7 @@ Program Instance [ ! Transitive A R ] (x : A) =>
transitivity y...
Qed.
-Program Instance [ ! Transitive A R ] (x : A) =>
+Program Instance [ Transitive A R ] (x : A) =>
trans_co_impl_morphism : Morphism (R ==> impl) (R x).
Next Obligation.
@@ -268,7 +268,7 @@ Program Instance [ ! Transitive A R ] (x : A) =>
transitivity x0...
Qed.
-Program Instance [ ! Transitive A R, Symmetric R ] (x : A) =>
+Program Instance [ Transitive A R, Symmetric A R ] (x : A) =>
trans_sym_co_inv_impl_morphism : Morphism (R ==> inverse impl) (R x).
Next Obligation.
@@ -276,7 +276,7 @@ Program Instance [ ! Transitive A R, Symmetric R ] (x : A) =>
transitivity y...
Qed.
-Program Instance [ ! Transitive A R, Symmetric R ] (x : A) =>
+Program Instance [ Transitive A R, Symmetric _ R ] (x : A) =>
trans_sym_contra_impl_morphism : Morphism (R --> impl) (R x).
Next Obligation.
@@ -309,14 +309,13 @@ Program Instance [ Equivalence A R ] (x : A) =>
(** [R] is Reflexive, hence we can build the needed proof. *)
-Program Instance (A B : Type) (R : relation A) (R' : relation B)
- [ Morphism (R ==> R') m ] [ Reflexive R ] (x : A) =>
+Program Instance [ Morphism (A -> B) (R ==> R') m, Reflexive _ R ] (x : A) =>
Reflexive_partial_app_morphism : Morphism R' (m x) | 3.
(** Every Transitive relation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof
to get an [R y z] goal. *)
-Program Instance [ ! Transitive A R ] =>
+Program Instance [ Transitive A R ] =>
trans_co_eq_inv_impl_morphism : Morphism (R ==> (@eq A) ==> inverse impl) R.
Next Obligation.
@@ -324,7 +323,7 @@ Program Instance [ ! Transitive A R ] =>
transitivity y...
Qed.
-Program Instance [ ! Transitive A R ] =>
+Program Instance [ Transitive A R ] =>
trans_contra_eq_impl_morphism : Morphism (R --> (@eq A) ==> impl) R.
Next Obligation.
@@ -334,7 +333,7 @@ Program Instance [ ! Transitive A R ] =>
(** Every Symmetric and Transitive relation gives rise to an equivariant morphism. *)
-Program Instance [ ! Transitive A R, Symmetric R ] =>
+Program Instance [ Transitive A R, Symmetric _ R ] =>
trans_sym_morphism : Morphism (R ==> R ==> iff) R.
Next Obligation.
@@ -421,11 +420,11 @@ Program Instance or_iff_morphism :
(* red ; intros. subst ; split; trivial. *)
(* Qed. *)
-Instance (A B : Type) [ ! Reflexive B R ] (m : A -> B) =>
- eq_Reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3.
+Instance (A : Type) [ Reflexive B R ] (m : A -> B) =>
+ eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3.
Proof. simpl_relation. Qed.
-Instance (A B : Type) [ ! Reflexive B R' ] =>
+Instance (A : Type) [ Reflexive B R' ] =>
Reflexive (@Logic.eq A ==> R').
Proof. simpl_relation. Qed.
@@ -469,9 +468,8 @@ Proof.
symmetry ; apply inverse_respectful.
Qed.
-Instance (A : Type) (R : relation A) (B : Type) (R' R'' : relation B)
- [ Normalizes relation_equivalence R' (inverse R'') ] =>
- Normalizes relation_equivalence (inverse R ==> R') (inverse (R ==> R'')) .
+Instance [ Normalizes (relation B) relation_equivalence R' (inverse R'') ] =>
+ ! Normalizes (relation (A -> B)) relation_equivalence (inverse R ==> R') (inverse (R ==> R'')) .
Proof.
red.
pose normalizes.
@@ -480,9 +478,8 @@ Proof.
reflexivity.
Qed.
-Program Instance (A : Type) (R : relation A)
- [ Morphism R m ] => morphism_inverse_morphism :
- Morphism (inverse R) m | 2.
+Program Instance [ Morphism A R m ] =>
+ morphism_inverse_morphism : Morphism (inverse R) m | 2.
(** Bootstrap !!! *)
@@ -497,9 +494,9 @@ Proof.
apply respect.
Qed.
-Lemma morphism_releq_morphism (A : Type) (R : relation A) (R' : relation A)
- [ Normalizes relation_equivalence R R' ]
- [ Morphism R' m ] : Morphism R m.
+Lemma morphism_releq_morphism
+ [ Normalizes (relation A) relation_equivalence R R',
+ Morphism _ R' m ] : Morphism R m.
Proof.
intros.
pose respect.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 492b8498a..0ca074589 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -75,48 +75,48 @@ Hint Resolve @irreflexivity : ord.
(** We can already dualize all these properties. *)
-Program Instance [ ! Reflexive A R ] => flip_Reflexive : Reflexive (flip R) :=
+Program Instance [ Reflexive A R ] => flip_Reflexive : Reflexive (flip R) :=
reflexivity := reflexivity (R:=R).
-Program Instance [ ! Irreflexive A R ] => flip_Irreflexive : Irreflexive (flip R) :=
+Program Instance [ Irreflexive A R ] => flip_Irreflexive : Irreflexive (flip R) :=
irreflexivity := irreflexivity (R:=R).
-Program Instance [ ! Symmetric A R ] => flip_Symmetric : Symmetric (flip R).
+Program Instance [ Symmetric A R ] => flip_Symmetric : Symmetric (flip R).
Solve Obligations using unfold flip ; program_simpl ; clapply Symmetric.
-Program Instance [ ! Asymmetric A R ] => flip_Asymmetric : Asymmetric (flip R).
+Program Instance [ Asymmetric A R ] => flip_Asymmetric : Asymmetric (flip R).
Solve Obligations using program_simpl ; unfold flip in * ; intros ; clapply asymmetry.
-Program Instance [ ! Transitive A R ] => flip_Transitive : Transitive (flip R).
+Program Instance [ Transitive A R ] => flip_Transitive : Transitive (flip R).
Solve Obligations using unfold flip ; program_simpl ; clapply transitivity.
(** Have to do it again for Prop. *)
-Program Instance [ ! Reflexive A (R : relation A) ] => inverse_Reflexive : Reflexive (inverse R) :=
+Program Instance [ Reflexive A (R : relation A) ] => inverse_Reflexive : Reflexive (inverse R) :=
reflexivity := reflexivity (R:=R).
-Program Instance [ ! Irreflexive A (R : relation A) ] => inverse_Irreflexive : Irreflexive (inverse R) :=
+Program Instance [ Irreflexive A (R : relation A) ] => inverse_Irreflexive : Irreflexive (inverse R) :=
irreflexivity := irreflexivity (R:=R).
-Program Instance [ ! Symmetric A (R : relation A) ] => inverse_Symmetric : Symmetric (inverse R).
+Program Instance [ Symmetric A (R : relation A) ] => inverse_Symmetric : Symmetric (inverse R).
Solve Obligations using unfold inverse, flip ; program_simpl ; clapply Symmetric.
-Program Instance [ ! Asymmetric A (R : relation A) ] => inverse_Asymmetric : Asymmetric (inverse R).
+Program Instance [ Asymmetric A (R : relation A) ] => inverse_Asymmetric : Asymmetric (inverse R).
Solve Obligations using program_simpl ; unfold inverse, flip in * ; intros ; clapply asymmetry.
-Program Instance [ ! Transitive A (R : relation A) ] => inverse_Transitive : Transitive (inverse R).
+Program Instance [ Transitive A (R : relation A) ] => inverse_Transitive : Transitive (inverse R).
Solve Obligations using unfold inverse, flip ; program_simpl ; clapply transitivity.
-Program Instance [ ! Reflexive A (R : relation A) ] =>
+Program Instance [ Reflexive A (R : relation A) ] =>
Reflexive_complement_Irreflexive : Irreflexive (complement R).
-Program Instance [ ! Irreflexive A (R : relation A) ] =>
+Program Instance [ Irreflexive A (R : relation A) ] =>
Irreflexive_complement_Reflexive : Reflexive (complement R).
Next Obligation.
@@ -125,7 +125,7 @@ Program Instance [ ! Irreflexive A (R : relation A) ] =>
apply (irreflexivity H).
Qed.
-Program Instance [ ! Symmetric A (R : relation A) ] => complement_Symmetric : Symmetric (complement R).
+Program Instance [ Symmetric A (R : relation A) ] => complement_Symmetric : Symmetric (complement R).
Next Obligation.
Proof.
@@ -210,10 +210,10 @@ Class Equivalence (carrier : Type) (equiv : relation carrier) :=
Class [ Equivalence A eqA ] => Antisymmetric (R : relation A) :=
antisymmetry : forall x y, R x y -> R y x -> eqA x y.
-Program Instance [ eq : Equivalence A eqA, Antisymmetric eq R ] =>
+Program Instance [ eq : Equivalence A eqA, ! Antisymmetric eq R ] =>
flip_antiSymmetric : Antisymmetric eq (flip R).
-Program Instance [ eq : Equivalence A eqA, Antisymmetric eq (R : relation A) ] =>
+Program Instance [ eq : Equivalence A eqA, ! Antisymmetric eq (R : relation A) ] =>
inverse_antiSymmetric : Antisymmetric eq (inverse R).
(** Leibinz equality [eq] is an equivalence relation. *)
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 86a2bef80..26e1ab244 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -54,7 +54,7 @@ Open Local Scope program_scope.
(** Invert the branches. *)
-Program Definition nequiv_dec [ ! EqDec A ] (x y : A) : { x =/= y } + { x == y } := swap_sumbool (x == y).
+Program Definition nequiv_dec [ EqDec A ] (x y : A) : { x =/= y } + { x == y } := swap_sumbool (x == y).
(** Overloaded notation for inequality. *)
@@ -62,10 +62,10 @@ Infix "=/=" := nequiv_dec (no associativity, at level 70).
(** Define boolean versions, losing the logical information. *)
-Definition equiv_decb [ ! EqDec A ] (x y : A) : bool :=
+Definition equiv_decb [ EqDec A ] (x y : A) : bool :=
if x == y then true else false.
-Definition nequiv_decb [ ! EqDec A ] (x y : A) : bool :=
+Definition nequiv_decb [ EqDec A ] (x y : A) : bool :=
negb (equiv_decb x y).
Infix "==b" := equiv_decb (no associativity, at level 70).
@@ -97,7 +97,7 @@ Program Instance unit_eqdec : EqDec (@eq_setoid unit) :=
reflexivity.
Qed.
-Program Instance [ EqDec (@eq_setoid A), EqDec (@eq_setoid B) ] =>
+Program Instance [ ! EqDec (@eq_setoid A), ! EqDec (@eq_setoid B) ] =>
prod_eqdec : EqDec (@eq_setoid (prod A B)) :=
equiv_dec x y :=
dest x as (x1, x2) in
@@ -113,7 +113,7 @@ Program Instance [ EqDec (@eq_setoid A), EqDec (@eq_setoid B) ] =>
Require Import Coq.Program.FunctionalExtensionality.
-Program Instance [ EqDec (@eq_setoid A) ] => bool_function_eqdec : EqDec (@eq_setoid (bool -> A)) :=
+Program Instance [ ! EqDec (@eq_setoid A) ] => bool_function_eqdec : EqDec (@eq_setoid (bool -> A)) :=
equiv_dec f g :=
if f true == g true then
if f false == g false then in_left
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index cff8bce1e..9a0a0981e 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -401,14 +401,14 @@ open Pp
let ($$) g f = fun x -> g (f x)
-let new_instance ctx (instid, bk, cl) props pri hook =
+let new_instance ctx (instid, bk, cl) props ?(tac:Proof_type.tactic option) ?(hook:(Names.constant -> unit) option) pri =
let env = Global.env() in
let isevars = ref (Evd.create_evar_defs Evd.empty) in
let bound = Implicit_quantifiers.ids_of_list (Termops.ids_of_context env) in
let bound, fvs = Implicit_quantifiers.free_vars_of_binders ~bound [] ctx in
let tclass =
match bk with
- | Explicit ->
+ | Implicit ->
let loc, id, par = Implicit_quantifiers.destClassAppExpl cl in
let k = class_info (global id) in
let applen = List.fold_left (fun acc (x, y) -> if y = None then succ acc else acc) 0 par in
@@ -429,7 +429,7 @@ let new_instance ctx (instid, bk, cl) props pri hook =
par (List.rev k.cl_context)
in Topconstr.CAppExpl (loc, (None, id), pars)
- | Implicit -> cl
+ | Explicit -> cl
in
let ctx_bound = Idset.union bound (Implicit_quantifiers.ids_of_list fvs) in
let gen_ids = Implicit_quantifiers.free_vars_of_constr_expr ~bound:ctx_bound tclass [] in
@@ -461,34 +461,7 @@ let new_instance ctx (instid, bk, cl) props pri hook =
isevars := resolve_typeclasses env sigma !isevars;
let sigma = Evd.evars_of !isevars in
let substctx = Typeclasses.nf_substitution sigma subst in
- let subst, _propsctx =
- let props =
- List.map (fun (x, l, d) ->
- x, Topconstr.abstract_constr_expr d (binders_of_lidents l))
- props
- in
- if List.length props > List.length k.cl_props then
- mismatched_props env' (List.map snd props) k.cl_props;
- let props, rest =
- List.fold_left
- (fun (props, rest) (id,_,_) ->
- try
- let (_, c) = List.find (fun ((_,id'), c) -> id' = id) rest in
- let rest' = List.filter (fun ((_,id'), c) -> id' <> id) rest in
- c :: props, rest'
- with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest)
- ([], props) k.cl_props
- in
- if rest <> [] then
- unbound_method env' k.cl_impl (fst (List.hd rest))
- else
- type_ctx_instance isevars env' k.cl_props props substctx
- in
let inst_constr, ty_constr = instance_constructor k in
- let app = inst_constr (List.rev_map snd subst) in
- let term = Termops.it_mkNamedLambda_or_LetIn app ctx' in
- isevars := Evarutil.nf_evar_defs !isevars;
- let term = Evarutil.nf_isevar !isevars term in
let termtype =
let app = applistc ty_constr (List.rev_map snd substctx) in
let t = it_mkNamedProd_or_LetIn app ctx' in
@@ -499,40 +472,82 @@ let new_instance ctx (instid, bk, cl) props pri hook =
(fun i (na, b, t) -> ExplByPos (i, Some na), (true, true))
1 ctx'
in
- let hook cst =
- let inst =
- { is_class = k;
- is_pri = pri;
- is_impl = cst;
- }
- in
- Impargs.declare_manual_implicits false (ConstRef cst) false imps;
- Typeclasses.add_instance inst;
- hook cst
- in
- let evm = Evd.evars_of (undefined_evars !isevars) in
- if evm = Evd.empty then
- let cdecl =
- let kind = IsDefinition Instance in
- let entry =
- { const_entry_body = term;
- const_entry_type = Some termtype;
- const_entry_opaque = false;
- const_entry_boxed = false }
- in DefinitionEntry entry, kind
- in
- let kn = Declare.declare_constant id cdecl in
- Flags.if_verbose Command.definition_message id;
- hook kn;
- id
+ if Lib.is_modtype () then
+ begin
+ let cst = Declare.declare_internal_constant id
+ (Entries.ParameterEntry (termtype,false), Decl_kinds.IsAssumption Decl_kinds.Logical)
+ in
+ Impargs.maybe_declare_manual_implicits false (ConstRef cst) false imps;
+ Typeclasses.add_instance { is_class = k ; is_pri = None; is_impl = cst };
+ Command.assumption_message id;
+ (match hook with Some h -> h cst | None -> ()); id
+ end
else
- let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in
- Command.start_proof id kind termtype (fun _ -> function ConstRef cst -> hook cst | _ -> assert false);
- Pfedit.by (* (Refiner.tclTHEN (Refiner.tclEVARS (Evd.evars_of !isevars)) *)
- (!refine_ref (evm, term));
- Flags.if_verbose (msg $$ Printer.pr_open_subgoals) ();
- id
-
+ begin
+ let subst, _propsctx =
+ let props =
+ List.map (fun (x, l, d) ->
+ x, Topconstr.abstract_constr_expr d (binders_of_lidents l))
+ props
+ in
+ if List.length props > List.length k.cl_props then
+ mismatched_props env' (List.map snd props) k.cl_props;
+ let props, rest =
+ List.fold_left
+ (fun (props, rest) (id,_,_) ->
+ try
+ let (_, c) = List.find (fun ((_,id'), c) -> id' = id) rest in
+ let rest' = List.filter (fun ((_,id'), c) -> id' <> id) rest in
+ c :: props, rest'
+ with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest)
+ ([], props) k.cl_props
+ in
+ if rest <> [] then
+ unbound_method env' k.cl_impl (fst (List.hd rest))
+ else
+ type_ctx_instance isevars env' k.cl_props props substctx
+ in
+ let app = inst_constr (List.rev_map snd subst) in
+ let term = Termops.it_mkNamedLambda_or_LetIn app ctx' in
+ isevars := Evarutil.nf_evar_defs !isevars;
+ let term = Evarutil.nf_isevar !isevars term in
+ let hook cst =
+ let inst =
+ { is_class = k;
+ is_pri = pri;
+ is_impl = cst;
+ }
+ in
+ Impargs.maybe_declare_manual_implicits false (ConstRef cst) false imps;
+ Typeclasses.add_instance inst;
+ (match hook with Some h -> h cst | None -> ())
+ in
+ let evm = Evd.evars_of (undefined_evars !isevars) in
+ if evm = Evd.empty then
+ let cdecl =
+ let kind = IsDefinition Instance in
+ let entry =
+ { const_entry_body = term;
+ const_entry_type = Some termtype;
+ const_entry_opaque = false;
+ const_entry_boxed = false }
+ in DefinitionEntry entry, kind
+ in
+ let kn = Declare.declare_constant id cdecl in
+ Flags.if_verbose Command.definition_message id;
+ hook kn;
+ id
+ else
+ let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in
+ Flags.silently (fun () ->
+ Command.start_proof id kind termtype (fun _ -> function ConstRef cst -> hook cst | _ -> assert false);
+ Pfedit.by (* (Refiner.tclTHEN (Refiner.tclEVARS (Evd.evars_of !isevars)) *)
+ (!refine_ref (evm, term));
+ (match tac with Some tac -> Pfedit.by tac | None -> ())) ();
+ Flags.if_verbose (msg $$ Printer.pr_open_subgoals) ();
+ id
+ end
+
let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition
let solve_by_tac env evd evar evi t =
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 6671eed72..973845d9c 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -43,8 +43,9 @@ val new_instance :
local_binder list ->
typeclass_constraint ->
binder_def_list ->
+ ?tac:Proof_type.tactic ->
+ ?hook:(constant -> unit) ->
int option ->
- (constant -> unit) ->
identifier
(* For generation on names based on classes only *)
diff --git a/toplevel/command.mli b/toplevel/command.mli
index a6a403c03..31420d189 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -33,6 +33,7 @@ open Redexpr
val set_declare_definition_hook : (Entries.definition_entry -> unit) -> unit
val definition_message : identifier -> unit
+val assumption_message : identifier -> unit
val declare_definition : identifier -> definition_kind ->
local_binder list -> red_expr option -> constr_expr ->
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 4e2901319..1ea732add 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -537,7 +537,7 @@ let vernac_class id par ar sup props =
Classes.new_class id par ar sup props
let vernac_instance sup inst props pri =
- ignore(Classes.new_instance sup inst props pri (fun _ -> ()))
+ ignore(Classes.new_instance sup inst props pri)
let vernac_context l =
Classes.context l
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 22:12:40 +0000