diff options
24 files changed, 252 insertions, 125 deletions
diff --git a/doc/changelog/02-specification-language/10996-refine-instance-returns.rst b/doc/changelog/02-specification-language/10996-refine-instance-returns.rst new file mode 100644 index 0000000000..cd1a692f54 --- /dev/null +++ b/doc/changelog/02-specification-language/10996-refine-instance-returns.rst @@ -0,0 +1,4 @@ +- Added ``#[refine]`` attribute for :cmd:`Instance`, a more + predictable version of the old ``Refine Instance Mode`` which + unconditionally opens a proof (`#10996 + <https://github.com/coq/coq/pull/10996>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/04-tactics/10998-zify-complements.rst b/doc/changelog/04-tactics/10998-zify-complements.rst new file mode 100644 index 0000000000..3ec526f0a9 --- /dev/null +++ b/doc/changelog/04-tactics/10998-zify-complements.rst @@ -0,0 +1,7 @@ +- The :tacn:`zify` tactic is now aware of `Pos.pred_double`, `Pos.pred_N`, + `Pos.of_nat`, `Pos.add_carry`, `Pos.pow`, `Pos.square`, `Z.pow`, `Z.double`, + `Z.pred_double`, `Z.succ_double`, `Z.square`, `Z.div2`, and `Z.quot2`. + Injections for internal definitions in module `ZifyBool` (`isZero` and `isLeZero`) + are also added to help users to declare new :tacn:`zify` class instances using + Micromega tactics. + (`#10998 <https://github.com/coq/coq/pull/10998>`_, by Kazuhiko Sakaguchi). diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index 9f92fc4c56..0754145b39 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -530,7 +530,7 @@ A detailed example: Euclidean division ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The file ``Euclid`` contains the proof of Euclidean division. -The natural numbers used here are unary, represented by the type``nat``, +The natural numbers used here are unary, represented by the type ``nat``, which is defined by two constructors ``O`` and ``S``. This module contains a theorem ``eucl_dev``, whose type is:: diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index 93a1be027c..4feda5e875 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -117,7 +117,7 @@ parameters is any term :math:`f \, t_1 \ldots t_n`. .. example:: Morphisms Continuing the previous example, let ``union: forall (A : Type), list A -> list A -> list A`` - perform the union of two sets by appending one list to the other. ``union` is a binary + perform the union of two sets by appending one list to the other. ``union`` is a binary morphism parametric over ``A`` that respects the relation instance ``(set_eq A)``. The latter condition is proved by showing: diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 1bbf988505..57a2254100 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -47,9 +47,22 @@ Leibniz equality on some type. An example implementation is: | tt, tt => eq_refl tt end }. -Using :cmd:`Program Instance`, if one does not give all the members in -the Instance declaration, Coq generates obligations for the remaining -fields, e.g.: +Using the attribute ``refine``, if the term is not sufficient to +finish the definition (e.g. due to a missing field or non-inferable +hole) it must be finished in proof mode. If it is sufficient a trivial +proof mode with no open goals is started. + +.. coqtop:: in + + #[refine] Instance unit_EqDec' : EqDec unit := { eqb x y := true }. + Proof. intros [] [];reflexivity. Defined. + +Note that if you finish the proof with :cmd:`Qed` the entire instance +will be opaque, including the fields given in the initial term. + +Alternatively, in :flag:`Program Mode` if one does not give all the +members in the Instance declaration, Coq generates obligations for the +remaining fields, e.g.: .. coqtop:: in diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib index db089df395..3d73f9bd6e 100644 --- a/doc/sphinx/biblio.bib +++ b/doc/sphinx/biblio.bib @@ -192,7 +192,7 @@ s}, @InProceedings{Del00, author = {Delahaye, D.}, - title = {A {T}actic {L}anguage for the {S}ystem {{\sf Coq}}}, + title = {A {T}actic {L}anguage for the {S}ystem {Coq}}, booktitle = {Proceedings of Logic for Programming and Automated Reasoning (LPAR), Reunion Island}, publisher = SV, diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 54aeed428f..4beaff70f5 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -1200,7 +1200,8 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or at level :math:`\Type` (without annotations or hiding it behind a definition) template polymorphic if possible. - This can be prevented using the ``notemplate`` attribute. + This can be prevented using the ``universes(notemplate)`` + attribute. .. warn:: Automatically declaring @ident as template polymorphic. @@ -1208,9 +1209,9 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or implicitly declared template polymorphic by :flag:`Auto Template Polymorphism`. - An inductive type can be forced to be template polymorphic using the - ``template`` attribute: it should then fulfill the criterion to - be template polymorphic or an error is raised. + An inductive type can be forced to be template polymorphic using + the ``universes(template)`` attribute: it should then fulfill the + criterion to be template polymorphic or an error is raised. .. exn:: Inductive @ident cannot be made template polymorphic. @@ -1221,7 +1222,7 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or Template polymorphism and universe polymorphism (see Chapter :ref:`polymorphicuniverses`) are incompatible, so if the later is enabled it will prevail over automatic template polymorphism and - cause an error when using the ``template`` attribute. + cause an error when using the ``universes(template)`` attribute. .. flag:: Template Check diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index f667dd94b0..94e9ccf0d4 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -1503,19 +1503,20 @@ Each attribute has a name (an identifier) and may have a value. A value is either a :token:`string` (in which case it is specified with an equal ``=`` sign), or a list of attributes, enclosed within brackets. -Currently, -the following attributes names are recognized: +Some attributes are specific to a command, and so are described with +that command. Currently, the following attributes are recognized by a +variety of commands: -``monomorphic``, ``polymorphic`` - Take no value, analogous to the ``Monomorphic`` and ``Polymorphic`` flags - (see :ref:`polymorphicuniverses`). +``universes(monomorphic)``, ``universes(polymorphic)`` + Equivalent to the ``Monomorphic`` and + ``Polymorphic`` flags (see :ref:`polymorphicuniverses`). ``program`` - Takes no value, analogous to the ``Program`` flag + Takes no value, equivalent to the ``Program`` flag (see :ref:`programs`). ``global``, ``local`` - Take no value, analogous to the ``Global`` and ``Local`` flags + Take no value, equivalent to the ``Global`` and ``Local`` flags (see :ref:`controlling-locality-of-commands`). ``deprecated`` diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 4c697be963..853ddfd6dc 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1513,7 +1513,7 @@ In a goal like the following:: ============= m < 5 + n -The tactic ``abstract: abs n`` first generalizes the goal with respect ton +The tactic :g:`abstract: abs n` first generalizes the goal with respect to :g:`n` (that is not visible to the abstract constant abs) and then assigns abs. The resulting goal is:: @@ -4071,6 +4071,7 @@ which the function is supplied: :name: congr This tactic: + + checks that the goal is a Leibniz equality; + matches both sides of this equality with “term applied to some arguments”, inferring the right number of arguments from the goal and the type of term. This may expand some definitions or fixpoints; + generates the subgoals corresponding to pairwise equalities of the arguments present in the goal. @@ -4218,7 +4219,7 @@ in the second column. ``ident`` in all the occurrences of ``term2`` * - ``term1 as ident in term2`` - ``term 1`` - - in all the subterms identified by ``ident` + - in all the subterms identified by ``ident`` in all the occurrences of ``term2[term 1 /ident]`` The rewrite tactic supports two more patterns obtained prefixing the @@ -5023,7 +5024,7 @@ mechanism: Coercion is_true (b : bool) := b = true. This allows any boolean formula ``b`` to be used in a context where |Coq| -would expect a proposition, e.g., after ``Lemma … : ``. It is then +would expect a proposition, e.g., after ``Lemma … :``. It is then interpreted as ``(is_true b)``, i.e., the proposition ``b = true``. Coercions are elided by the pretty-printer, so they are essentially transparent to the user. diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index d377bd8561..b1d530438d 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -244,17 +244,17 @@ GRAMMAR EXTEND Gram ] ] ; record_declaration: - [ [ fs = record_fields -> { CAst.make ~loc @@ CRecord fs } ] ] + [ [ fs = record_fields_instance -> { CAst.make ~loc @@ CRecord fs } ] ] ; - record_fields: - [ [ f = record_field_declaration; ";"; fs = record_fields -> { f :: fs } - | f = record_field_declaration -> { [f] } + record_fields_instance: + [ [ f = record_field_instance; ";"; fs = record_fields_instance -> { f :: fs } + | f = record_field_instance -> { [f] } | -> { [] } ] ] ; - record_field_declaration: + record_field_instance: [ [ id = global; bl = binders; ":="; c = lconstr -> { (id, mkLambdaCN ~loc bl c) } ] ] ; diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 1b00a93834..eb282d1f83 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -439,7 +439,7 @@ GRAMMAR EXTEND Gram [ [ "in"; id = id_or_meta; ipat = as_ipat -> { Some (id,ipat) } | -> { None } ] ] ; - orient: + orient_rw: [ [ "->" -> { true } | "<-" -> { false } | -> { true } ] ] @@ -451,10 +451,10 @@ GRAMMAR EXTEND Gram ] ] ; fixdecl: - [ [ "("; id = ident; bl=LIST0 simple_binder; ann=fixannot; + [ [ "("; id = ident; bl=LIST0 simple_binder; ann=struct_annot; ":"; ty=lconstr; ")" -> { (loc, id, bl, ann, ty) } ] ] ; - fixannot: + struct_annot: [ [ "{"; IDENT "struct"; id=name; "}" -> { Some id } | -> { None } ] ] ; @@ -506,7 +506,7 @@ GRAMMAR EXTEND Gram ] ] ; oriented_rewriter : - [ [ b = orient; p = rewriter -> { let (m,c) = p in (b,m,c) } ] ] + [ [ b = orient_rw; p = rewriter -> { let (m,c) = p in (b,m,c) } ] ] ; induction_clause: [ [ c = destruction_arg; pat = as_or_and_ipat; eq = eqn_ipat; diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 1493092f2f..6be358be21 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -2023,7 +2023,8 @@ let add_morphism atts binders m s n = let _id, lemma = Classes.new_instance_interactive ~global:atts.global ~poly:atts.polymorphic instance_name binders instance_t - ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info + ~generalize:false ~tac ~hook:(declare_projection n instance_id) + Hints.empty_hint_info None in lemma (* no instance body -> always open proof *) diff --git a/plugins/micromega/ZifyBool.v b/plugins/micromega/ZifyBool.v index b94b74097b..4060478363 100644 --- a/plugins/micromega/ZifyBool.v +++ b/plugins/micromega/ZifyBool.v @@ -74,6 +74,14 @@ Definition isZero (z : Z) := Z_of_bool (Z.eqb z 0). Definition isLeZero (x : Z) := Z_of_bool (Z.leb x 0). +Instance Op_isZero : UnOp isZero := + { TUOp := isZero; TUOpInj := ltac: (reflexivity) }. +Add UnOp Op_isZero. + +Instance Op_isLeZero : UnOp isLeZero := + { TUOp := isLeZero; TUOpInj := ltac: (reflexivity) }. +Add UnOp Op_isLeZero. + (* Some intermediate lemma *) Lemma Z_eqb_isZero : forall n m, diff --git a/plugins/micromega/ZifyInst.v b/plugins/micromega/ZifyInst.v index afd7101667..97f6fe0613 100644 --- a/plugins/micromega/ZifyInst.v +++ b/plugins/micromega/ZifyInst.v @@ -169,7 +169,7 @@ Add BinRel Op_eq_pos. (* zify_positive_op *) -Program Instance Op_Z_of_N : UnOp Z.of_N := +Instance Op_Z_of_N : UnOp Z.of_N := { TUOp := (fun x => x) ; TUOpInj := fun x => eq_refl (Z.of_N x) }. Add UnOp Op_Z_of_N. @@ -189,6 +189,10 @@ Instance Op_pos_succ : UnOp Pos.succ := { TUOp := fun x => x + 1; TUOpInj := Pos2Z.inj_succ }. Add UnOp Op_pos_succ. +Instance Op_pos_pred_double : UnOp Pos.pred_double := + { TUOp := fun x => 2 * x - 1; TUOpInj := ltac:(reflexivity) }. +Add UnOp Op_pos_pred_double. + Instance Op_pos_pred : UnOp Pos.pred := { TUOp := fun x => Z.max 1 (x - 1) ; TUOpInj := ltac : @@ -197,14 +201,30 @@ Instance Op_pos_pred : UnOp Pos.pred := apply Pos2Z.inj_sub_max) }. Add UnOp Op_pos_pred. +Instance Op_pos_predN : UnOp Pos.pred_N := + { TUOp := fun x => x - 1 ; + TUOpInj := ltac: (now destruct x; rewrite N.pos_pred_spec) }. +Add UnOp Op_pos_predN. + Instance Op_pos_of_succ_nat : UnOp Pos.of_succ_nat := { TUOp := fun x => x + 1 ; TUOpInj := Zpos_P_of_succ_nat }. Add UnOp Op_pos_of_succ_nat. -Program Instance Op_pos_add : BinOp Pos.add := +Instance Op_pos_of_nat : UnOp Pos.of_nat := + { TUOp := fun x => Z.max 1 x ; + TUOpInj := ltac: (now destruct x; + [|rewrite <- Pos.of_nat_succ, <- (Nat2Z.inj_max 1)]) }. +Add UnOp Op_pos_of_nat. + +Instance Op_pos_add : BinOp Pos.add := { TBOp := Z.add ; TBOpInj := ltac: (reflexivity) }. Add BinOp Op_pos_add. +Instance Op_pos_add_carry : BinOp Pos.add_carry := + { TBOp := fun x y => x + y + 1 ; + TBOpInj := ltac:(now intros; rewrite Pos.add_carry_spec, Pos2Z.inj_succ) }. +Add BinOp Op_pos_add_carry. + Instance Op_pos_sub : BinOp Pos.sub := { TBOp := fun n m => Z.max 1 (n - m) ;TBOpInj := Pos2Z.inj_sub_max }. Add BinOp Op_pos_sub. @@ -221,6 +241,14 @@ Instance Op_pos_max : BinOp Pos.max := { TBOp := Z.max ; TBOpInj := Pos2Z.inj_max }. Add BinOp Op_pos_max. +Instance Op_pos_pow : BinOp Pos.pow := + { TBOp := Z.pow ; TBOpInj := Pos2Z.inj_pow }. +Add BinOp Op_pos_pow. + +Instance Op_pos_square : UnOp Pos.square := + { TUOp := Z.square ; TUOpInj := Pos2Z.inj_square }. +Add UnOp Op_pos_square. + Instance Op_xO : UnOp xO := { TUOp := fun x => 2 * x ; TUOpInj := ltac: (reflexivity) }. Add UnOp Op_xO. @@ -295,8 +323,6 @@ Instance Op_N_div : BinOp N.div := {| TBOp := Z.div ; TBOpInj := N2Z.inj_div|}. Add BinOp Op_N_div. - - Instance Op_N_mod : BinOp N.modulo := {| TBOp := Z.rem ; TBOpInj := N2Z.inj_rem|}. Add BinOp Op_N_mod. @@ -390,10 +416,38 @@ Instance Op_Z_sgn : UnOp Z.sgn := { TUOp := Z.sgn ; TUOpInj := ltac:(reflexivity) }. Add UnOp Op_Z_sgn. +Instance Op_Z_pow : BinOp Z.pow := + { TBOp := Z.pow ; TBOpInj := ltac:(reflexivity) }. +Add BinOp Op_Z_pow. + Instance Op_Z_pow_pos : BinOp Z.pow_pos := { TBOp := Z.pow ; TBOpInj := ltac:(reflexivity) }. Add BinOp Op_Z_pow_pos. +Instance Op_Z_double : UnOp Z.double := + { TUOp := Z.mul 2 ; TUOpInj := Z.double_spec }. +Add UnOp Op_Z_double. + +Instance Op_Z_pred_double : UnOp Z.pred_double := + { TUOp := fun x => 2 * x - 1 ; TUOpInj := Z.pred_double_spec }. +Add UnOp Op_Z_pred_double. + +Instance Op_Z_succ_double : UnOp Z.succ_double := + { TUOp := fun x => 2 * x + 1 ; TUOpInj := Z.succ_double_spec }. +Add UnOp Op_Z_succ_double. + +Instance Op_Z_square : UnOp Z.square := + { TUOp := fun x => x * x ; TUOpInj := Z.square_spec }. +Add UnOp Op_Z_square. + +Instance Op_Z_div2 : UnOp Z.div2 := + { TUOp := fun x => x / 2 ; TUOpInj := Z.div2_div }. +Add UnOp Op_Z_div2. + +Instance Op_Z_quot2 : UnOp Z.quot2 := + { TUOp := fun x => Z.quot x 2 ; TUOpInj := Zeven.Zquot2_quot }. +Add UnOp Op_Z_quot2. + Lemma of_nat_to_nat_eq : forall x, Z.of_nat (Z.to_nat x) = Z.max 0 x. Proof. destruct x. @@ -435,7 +489,7 @@ Proof. Qed. -Program Instance ZminSpec : BinOpSpec Z.min := +Instance ZminSpec : BinOpSpec Z.min := {| BPred := fun n m r => n < m /\ r = n \/ m <= n /\ r = m ; BSpec := Z.min_spec |}. Add Spec ZminSpec. diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 24976d8c1f..ff0bf0ac2a 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -183,12 +183,16 @@ let classify_vernac e = | VernacDeclareMLModule _ | VernacContext _ (* TASSI: unsure *) -> VtSideff ([], VtNow) | VernacProofMode pm -> VtProofMode pm - | VernacInstance ((name,_),_,_,None,_) when not (Attributes.parse_drop_extra Attributes.program atts) -> - let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in - let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in - VtStartProof (guarantee, idents_of_name name.CAst.v) - | VernacInstance ((name,_),_,_,_,_) -> - VtSideff (idents_of_name name.CAst.v, VtLater) + | VernacInstance ((name,_),_,_,props,_) -> + let program, refine = + Attributes.(parse_drop_extra Notations.(program ++ Classes.refine_att) atts) + in + if program || (props <> None && not refine) then + VtSideff (idents_of_name name.CAst.v, VtLater) + else + let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in + let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in + VtStartProof (guarantee, idents_of_name name.CAst.v) (* Stm will install a new classifier to handle these *) | VernacBack _ | VernacAbortAll | VernacUndoTo _ | VernacUndo _ diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 2ce32b309a..ef2402489e 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -86,16 +86,13 @@ let rec prolog l n gl = let prol = (prolog l (n-1)) in (tclFIRST (List.map (fun t -> (tclTHEN t prol)) (one_step l gl))) gl -let out_term env = function - | IsConstr (c, _) -> c - | IsGlobRef gr -> EConstr.of_constr (fst (UnivGen.fresh_global_instance env gr)) - let prolog_tac l n = Proofview.V82.tactic begin fun gl -> let map c = let (sigma, c) = c (pf_env gl) (project gl) in - let c = pf_apply (prepare_hint false (false,true)) gl (sigma, c) in - out_term (pf_env gl) c + (* Dropping the universe context is probably wrong *) + let (c, _) = pf_apply (prepare_hint false) gl (sigma, c) in + c in let l = List.map map l in try (prolog l n gl) diff --git a/tactics/hints.ml b/tactics/hints.ml index 131832be89..ac18d5ce97 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1258,7 +1258,7 @@ let default_prepare_hint_ident = Id.of_string "H" exception Found of constr * types -let prepare_hint check (poly,local) env init (sigma,c) = +let prepare_hint check env init (sigma,c) = let sigma = Typeclasses.resolve_typeclasses ~fail:false env sigma in (* We re-abstract over uninstantiated evars and universes. It is actually a bit stupid to generalize over evars since the first @@ -1292,10 +1292,7 @@ let prepare_hint check (poly,local) env init (sigma,c) = let empty_sigma = Evd.from_env env in if check then Pretyping.check_evars env empty_sigma sigma c'; let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in - if poly then IsConstr (c', diff) - else if local then IsConstr (c', diff) - else (Declare.declare_universe_context ~poly:false diff; - IsConstr (c', Univ.ContextSet.empty)) + (c', diff) let project_hint ~poly pri l2r r = let open EConstr in @@ -1338,7 +1335,12 @@ let interp_hints ~poly = let evd,c = Constrintern.interp_open_constr env sigma c in let env = Global.env () in let sigma = Evd.from_env env in - prepare_hint true (poly,false) env sigma (evd,c) in + let (c, diff) = prepare_hint true env sigma (evd,c) in + if poly then IsConstr (c, diff) + else + let () = Declare.declare_universe_context ~poly:false diff in + IsConstr (c, Univ.ContextSet.empty) + in let fref r = let gr = global_with_alias r in Dumpglob.add_glob ?loc:r.CAst.loc gr; @@ -1419,10 +1421,8 @@ let expand_constructor_hints env sigma lems = not (Univ.ContextSet.is_empty ctx), IsConstr (mkConstructU ((ind,i+1),u),ctx)) | _ -> - [match prepare_hint false (false,true) env sigma (evd,lem) with - | IsConstr (c, ctx) -> - not (Univ.ContextSet.is_empty ctx), IsConstr (c, ctx) - | IsGlobRef _ -> assert false (* Impossible return value *) ]) lems + let (c, ctx) = prepare_hint false env sigma (evd,lem) in + [not (Univ.ContextSet.is_empty ctx), IsConstr (c, ctx)]) lems (* builds a hint database from a constr signature *) (* typically used with (lid, ltyp) = pf_hyps_types <some goal> *) diff --git a/tactics/hints.mli b/tactics/hints.mli index 4c82a068b1..5b89f8b381 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -212,8 +212,7 @@ val interp_hints : poly:bool -> hints_expr -> hints_entry val add_hints : local:bool -> hint_db_name list -> hints_entry -> unit val prepare_hint : bool (* Check no remaining evars *) -> - (bool * bool) (* polymorphic or monomorphic, local or global *) -> - env -> evar_map -> evar_map * constr -> hint_term + env -> evar_map -> evar_map * constr -> (constr * Univ.ContextSet.t) (** [make_exact_entry info (c, ctyp, ctx)]. [c] is the term given as an exact proof to solve the goal; diff --git a/test-suite/success/RefineInstance.v b/test-suite/success/RefineInstance.v new file mode 100644 index 0000000000..f4d2f07db5 --- /dev/null +++ b/test-suite/success/RefineInstance.v @@ -0,0 +1,23 @@ + + +Class Foo := foo { a : nat; b : bool }. + +Fail Instance bla : Foo := { b:= true }. + +#[refine] Instance bla : Foo := { b:= true }. +Proof. +exact 0. +Defined. + +Instance bli : Foo := { a:=1; b := false}. +Check bli. + +Fail #[program, refine] Instance bla : Foo := {b := true}. + +#[program] Instance blo : Foo := {b := true}. +Next Obligation. exact 2. Qed. +Check blo. + +#[refine] Instance xbar : Foo := {a:=4; b:=true}. +Proof. Qed. +Check xbar. diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg index cc3a7c0f79..c1bd585f3f 100644 --- a/user-contrib/Ltac2/g_ltac2.mlg +++ b/user-contrib/Ltac2/g_ltac2.mlg @@ -643,7 +643,7 @@ GRAMMAR EXTEND Gram q_conversion: [ [ c = conversion -> { c } ] ] ; - orient: + ltac2_orient: [ [ "->" -> { CAst.make ~loc (Some true) } | "<-" -> { CAst.make ~loc (Some false) } | -> { CAst.make ~loc None } @@ -665,7 +665,7 @@ GRAMMAR EXTEND Gram ] ] ; oriented_rewriter: - [ [ b = orient; r = rewriter -> + [ [ b = ltac2_orient; r = rewriter -> { let (m, c) = r in CAst.make ~loc @@ { rew_orient = b; diff --git a/vernac/classes.ml b/vernac/classes.ml index e9a0ed7c34..0333b73ffe 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -401,7 +401,7 @@ let do_instance_subst_constructor_and_ty subst k u ctx = let term = it_mkLambda_or_LetIn (Option.get app) ctx in term, termtype -let do_instance_resolve_TC term termtype sigma env = +let do_instance_resolve_TC termtype sigma env = let sigma = Evarutil.nf_evar_map sigma in let sigma = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals_or_obligations ~fail:true env sigma in (* Try resolving fields that are typeclasses automatically. *) @@ -447,15 +447,37 @@ let do_instance_type_ctx_instance props k env' ctx' sigma ~program_mode subst = (push_rel_context ctx' env') sigma kcl_props props subst in res, sigma -let do_instance_interactive env sigma ?hook ~tac ~global ~poly cty k u ctx ctx' pri decl imps subst id = - let term, termtype = - if List.is_empty k.cl_props then +let interp_props ~program_mode env' cty k u ctx ctx' subst sigma = function + | (true, { CAst.v = CRecord fs; loc }) -> + check_duplicate ?loc fs; + let subst, sigma = do_instance_type_ctx_instance fs k env' ctx' sigma ~program_mode subst in + let term, termtype = + do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in + term, termtype, sigma + | (_, term) -> + let sigma, def = + interp_casted_constr_evars ~program_mode env' sigma term cty in + let termtype = it_mkProd_or_LetIn cty ctx in + let term = it_mkLambda_or_LetIn def ctx in + term, termtype, sigma + +let do_instance_interactive env env' sigma ?hook ~tac ~global ~poly cty k u ctx ctx' pri decl imps subst id opt_props = + let term, termtype, sigma = match opt_props with + | Some props -> + on_pi1 (fun x -> Some x) + (interp_props ~program_mode:false env' cty k u ctx ctx' subst sigma props) + | None -> let term, termtype = - do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in - Some term, termtype - else - None, it_mkProd_or_LetIn cty ctx in - let termtype, sigma = do_instance_resolve_TC term termtype sigma env in + if List.is_empty k.cl_props then + let term, termtype = + do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in + Some term, termtype + else + None, it_mkProd_or_LetIn cty ctx + in + let termtype, sigma = do_instance_resolve_TC termtype sigma env in + term, termtype, sigma + in Flags.silently (fun () -> declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps decl (List.map RelDecl.get_name ctx) term termtype) @@ -463,20 +485,9 @@ let do_instance_interactive env sigma ?hook ~tac ~global ~poly cty k u ctx ctx' let do_instance env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imps subst id props = let term, termtype, sigma = - match props with - | (true, { CAst.v = CRecord fs; loc }) -> - check_duplicate ?loc fs; - let subst, sigma = do_instance_type_ctx_instance fs k env' ctx' sigma ~program_mode:false subst in - let term, termtype = - do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in - term, termtype, sigma - | (_, term) -> - let sigma, def = - interp_casted_constr_evars ~program_mode:false env' sigma term cty in - let termtype = it_mkProd_or_LetIn cty ctx in - let term = it_mkLambda_or_LetIn def ctx in - term, termtype, sigma in - let termtype, sigma = do_instance_resolve_TC (Some term) termtype sigma env in + interp_props ~program_mode:false env' cty k u ctx ctx' subst sigma props + in + let termtype, sigma = do_instance_resolve_TC termtype sigma env in if Evd.has_undefined sigma then CErrors.user_err Pp.(str "Unsolved obligations remaining.") else @@ -485,26 +496,15 @@ let do_instance env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imp let do_instance_program env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imps subst id opt_props = let term, termtype, sigma = match opt_props with - | Some (true, { CAst.v = CRecord fs; loc }) -> - check_duplicate ?loc fs; - let subst, sigma = - do_instance_type_ctx_instance fs k env' ctx' sigma ~program_mode:true subst in - let term, termtype = - do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in - term, termtype, sigma - | Some (_, term) -> - let sigma, def = - interp_casted_constr_evars ~program_mode:true env' sigma term cty in - let termtype = it_mkProd_or_LetIn cty ctx in - let term = it_mkLambda_or_LetIn def ctx in - term, termtype, sigma + | Some props -> + interp_props ~program_mode:true env' cty k u ctx ctx' subst sigma props | None -> let subst, sigma = do_instance_type_ctx_instance [] k env' ctx' sigma ~program_mode:true subst in let term, termtype = do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in term, termtype, sigma in - let termtype, sigma = do_instance_resolve_TC term termtype sigma env in + let termtype, sigma = do_instance_resolve_TC termtype sigma env in if not (Evd.has_undefined sigma) && not (Option.is_empty opt_props) then declare_instance_constant pri global imps ?hook id decl poly sigma term termtype else @@ -555,12 +555,13 @@ let new_instance_common ~program_mode ~generalize env instid ctx cl = let new_instance_interactive ?(global=false) ~poly instid ctx cl - ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri = + ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook + pri opt_props = let env = Global.env() in let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl = new_instance_common ~program_mode:false ~generalize env instid ctx cl in - id, do_instance_interactive env sigma ?hook ~tac ~global ~poly - cty k u ctx ctx' pri decl imps subst id + id, do_instance_interactive env env' sigma ?hook ~tac ~global ~poly + cty k u ctx ctx' pri decl imps subst id opt_props let new_instance_program ?(global=false) ~poly instid ctx cl opt_props @@ -589,3 +590,10 @@ let declare_new_instance ?(global=false) ~program_mode ~poly instid ctx cl pri = interp_instance_context ~program_mode ~generalize:false env ctx pl cl in do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst instid + +let refine_att = + let open Attributes in + let open Notations in + attribute_of_list ["refine",single_key_parser ~name:"refine" ~key:"refine" ()] >>= function + | None -> return false + | Some () -> return true diff --git a/vernac/classes.mli b/vernac/classes.mli index 1247fdc8c1..594df52c70 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -35,6 +35,7 @@ val new_instance_interactive -> ?tac:unit Proofview.tactic -> ?hook:(GlobRef.t -> unit) -> Hints.hint_info_expr + -> (bool * constr_expr) option -> Id.t * Lemmas.t val new_instance @@ -84,3 +85,5 @@ val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> u (** For generation on names based on classes only *) val id_of_class : typeclass -> Id.t + +val refine_att : bool Attributes.attribute diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 4243d0c911..a78f4645c2 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -51,6 +51,7 @@ let decl_notation = Entry.create "vernac:decl_notation" let record_field = Entry.create "vernac:record_field" let of_type_with_opt_coercion = Entry.create "vernac:of_type_with_opt_coercion" let section_subset_expr = Entry.create "vernac:section_subset_expr" +let scope_delimiter = Entry.create "vernac:scope_delimiter" let make_bullet s = let open Proof_bullet in @@ -717,7 +718,7 @@ END (* Extensions: implicits, coercions, etc. *) GRAMMAR EXTEND Gram - GLOBAL: gallina_ext hint_info; + GLOBAL: gallina_ext hint_info scope_delimiter; gallina_ext: [ [ (* Transparent and Opaque *) @@ -835,11 +836,11 @@ GRAMMAR EXTEND Gram { [`ClearImplicits; `ClearScopes] } ] ] ; - scope: + scope_delimiter: [ [ "%"; key = IDENT -> { key } ] ] ; argument_spec: [ - [ b = OPT "!"; id = name ; s = OPT scope -> + [ b = OPT "!"; id = name ; s = OPT scope_delimiter -> { id.CAst.v, not (Option.is_empty b), Option.map (fun x -> CAst.make ~loc x) s } ] ]; @@ -852,7 +853,7 @@ GRAMMAR EXTEND Gram implicit_status = NotImplicit}] } | "/" -> { [`Slash] } | "&" -> { [`Ampersand] } - | "("; items = LIST1 argument_spec; ")"; sc = OPT scope -> + | "("; items = LIST1 argument_spec; ")"; sc = OPT scope_delimiter -> { let f x = match sc, x with | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x | Some _, Some _ -> user_err Pp.(str "scope declared twice") in @@ -860,7 +861,7 @@ GRAMMAR EXTEND Gram `Id { name=name; recarg_like=recarg_like; notation_scope=f notation_scope; implicit_status = NotImplicit}) items } - | "["; items = LIST1 argument_spec; "]"; sc = OPT scope -> + | "["; items = LIST1 argument_spec; "]"; sc = OPT scope_delimiter -> { let f x = match sc, x with | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x | Some _, Some _ -> user_err Pp.(str "scope declared twice") in @@ -868,7 +869,7 @@ GRAMMAR EXTEND Gram `Id { name=name; recarg_like=recarg_like; notation_scope=f notation_scope; implicit_status = Implicit}) items } - | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope -> + | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope_delimiter -> { let f x = match sc, x with | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x | Some _, Some _ -> user_err Pp.(str "scope declared twice") in @@ -1136,11 +1137,8 @@ GRAMMAR EXTEND Gram positive_search_mark: [ [ "-" -> { false } | -> { true } ] ] ; - scope: - [ [ "%"; key = IDENT -> { key } ] ] - ; searchabout_query: - [ [ b = positive_search_mark; s = ne_string; sc = OPT scope -> + [ [ b = positive_search_mark; s = ne_string; sc = OPT scope_delimiter -> { (b, SearchString (s,sc)) } | b = positive_search_mark; p = constr_pattern -> { (b, SearchSubPattern p) } diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 6dfba02ae9..128c30908b 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1048,27 +1048,27 @@ let vernac_identity_coercion ~atts id qids qidt = let vernac_instance_program ~atts name bl t props info = Dumpglob.dump_constraint (fst name) false "inst"; - let (program, locality), poly = - Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts + let locality, poly = + Attributes.(parse (Notations.(locality ++ polymorphic))) atts in let global = not (make_section_locality locality) in let _id : Id.t = Classes.new_instance_program ~global ~poly name bl t props info in () -let vernac_instance_interactive ~atts name bl t info = +let vernac_instance_interactive ~atts name bl t info props = Dumpglob.dump_constraint (fst name) false "inst"; - let (program, locality), poly = - Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts + let locality, poly = + Attributes.(parse (Notations.(locality ++ polymorphic))) atts in let global = not (make_section_locality locality) in let _id, pstate = - Classes.new_instance_interactive ~global ~poly name bl t info in + Classes.new_instance_interactive ~global ~poly name bl t info props in pstate let vernac_instance ~atts name bl t props info = Dumpglob.dump_constraint (fst name) false "inst"; - let (program, locality), poly = - Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts + let locality, poly = + Attributes.(parse (Notations.(locality ++ polymorphic))) atts in let global = not (make_section_locality locality) in let _id : Id.t = @@ -2094,16 +2094,21 @@ let translate_vernac ~atts v = let open Vernacextend in match v with (* Type classes *) | VernacInstance (name, bl, t, props, info) -> - let { DefAttributes.program } = DefAttributes.parse atts in + let atts, program = Attributes.(parse_with_extra program) atts in if program then VtDefault (fun () -> vernac_instance_program ~atts name bl t props info) else begin match props with | None -> - VtOpenProof(fun () -> - vernac_instance_interactive ~atts name bl t info) + VtOpenProof (fun () -> + vernac_instance_interactive ~atts name bl t info None) | Some props -> - VtDefault(fun () -> - vernac_instance ~atts name bl t props info) + let atts, refine = Attributes.parse_with_extra Classes.refine_att atts in + if refine then + VtOpenProof (fun () -> + vernac_instance_interactive ~atts name bl t info (Some props)) + else + VtDefault (fun () -> + vernac_instance ~atts name bl t props info) end | VernacDeclareInstance (id, bl, inst, info) -> |