diff options
61 files changed, 509 insertions, 289 deletions
diff --git a/.travis.yml b/.travis.yml index 8d70e346ad..b71f4cc851 100644 --- a/.travis.yml +++ b/.travis.yml @@ -37,9 +37,10 @@ env: # Main test suites matrix: - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit" + - TEST_TARGET="test-suite" COMPILER="4.06.0+trunk" CAMLP5_VER="7.03" EXTRA_OPAM="num" FINDLIB_VER="1.7.3" - TEST_TARGET="validate" TW="travis_wait" - TEST_TARGET="validate" COMPILER="4.02.3+32bit" TW="travis_wait" - - TEST_TARGET="validate" COMPILER="4.05.0+flambda" CAMLP5_VER="7.01" NATIVE_COMP="no" EXTRA_CONF="-flambda-opts -O3" NATIVE_COMP="no" + - TEST_TARGET="validate" COMPILER="4.06.0+trunk+flambda" CAMLP5_VER="7.03" NATIVE_COMP="no" EXTRA_CONF="-flambda-opts -O3" EXTRA_OPAM="num" FINDLIB_VER="1.7.3" - TEST_TARGET="ci-bignums TIMED=1" - TEST_TARGET="ci-color TIMED=1" - TEST_TARGET="ci-compcert TIMED=1" @@ -95,7 +96,7 @@ matrix: - TEST_TARGET="test-suite" - COMPILER="4.05.0" - FINDLIB_VER="1.7.3" - - CAMLP5_VER="7.01" + - CAMLP5_VER="7.03" - EXTRA_CONF="-coqide opt -with-doc yes" - EXTRA_OPAM="lablgtk-extras hevea" addons: @@ -109,7 +110,7 @@ matrix: - TEST_TARGET="test-suite" - COMPILER="4.05.0+flambda" - FINDLIB_VER="1.7.3" - - CAMLP5_VER="7.01" + - CAMLP5_VER="7.03" - NATIVE_COMP="no" - EXTRA_CONF="-coqide opt -with-doc yes -flambda-opts -O3" - EXTRA_OPAM="lablgtk-extras hevea" @@ -139,7 +140,7 @@ matrix: - env: - TEST_TARGET="coqocaml" - COMPILER="4.05.0" - - CAMLP5_VER="7.01" + - CAMLP5_VER="7.03" - FINDLIB_VER="1.7.3" - EXTRA_CONF="-coqide opt -warn-error" - EXTRA_OPAM="lablgtk-extras hevea" diff --git a/API/API.ml b/API/API.ml index bf99d0febd..6e61063e4b 100644 --- a/API/API.ml +++ b/API/API.ml @@ -131,6 +131,7 @@ module Geninterp = Geninterp (******************************************************************************) (* Pretyping *) (******************************************************************************) +module Ltac_pretype = Ltac_pretype module Locusops = Locusops module Pretype_errors = Pretype_errors module Reductionops = Reductionops diff --git a/API/API.mli b/API/API.mli index a41009fa2f..e207930771 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2757,13 +2757,6 @@ sig | PFix of Term.fixpoint | PCoFix of Term.cofixpoint - type constr_under_binders = Names.Id.t list * EConstr.constr - - (** Types of substitutions with or w/o bound variables *) - - type patvar_map = EConstr.constr Names.Id.Map.t - type extended_patvar_map = constr_under_binders Names.Id.Map.t - end module Namegen : @@ -3185,34 +3178,6 @@ sig type any_glob_constr = | AnyGlobConstr : 'r glob_constr_g -> any_glob_constr - (** A globalised term together with a closure representing the value - of its free variables. Intended for use when these variables are taken - from the Ltac environment. *) - - type closure = { - idents : Names.Id.t Names.Id.Map.t; - typed : Pattern.constr_under_binders Names.Id.Map.t ; - untyped: closed_glob_constr Names.Id.Map.t } - and closed_glob_constr = { - closure: closure; - term: glob_constr } - - (** Ltac variable maps *) - type var_map = Pattern.constr_under_binders Names.Id.Map.t - type uconstr_var_map = closed_glob_constr Names.Id.Map.t - type unbound_ltac_var_map = Geninterp.Val.t Names.Id.Map.t - - type ltac_var_map = { - ltac_constrs : var_map; - (** Ltac variables bound to constrs *) - ltac_uconstrs : uconstr_var_map; - (** Ltac variables bound to untyped constrs *) - ltac_idents: Names.Id.t Names.Id.Map.t; - (** Ltac variables bound to identifiers *) - ltac_genargs : unbound_ltac_var_map; - (** Ltac variables bound to other kinds of arguments *) - } - end module Notation_term : @@ -3276,6 +3241,79 @@ end (* Modules from pretyping/ *) (************************************************************************) +module Ltac_pretype : +sig +open Names +open Glob_term + +(** {5 Maps of pattern variables} *) + +(** Type [constr_under_binders] is for representing the term resulting + of a matching. Matching can return terms defined in a some context + of named binders; in the context, variable names are ordered by + (<) and referred to by index in the term Thanks to the canonical + ordering, a matching problem like + + [match ... with [(fun x y => ?p,fun y x => ?p)] => [forall x y => p]] + + will be accepted. Thanks to the reference by index, a matching + problem like + + [match ... with [(fun x => ?p)] => [forall x => p]] + + will work even if [x] is also the name of an existing goal + variable. + + Note: we do not keep types in the signature. Besides simplicity, + the main reason is that it would force to close the signature over + binders that occur only in the types of effective binders but not + in the term itself (e.g. for a term [f x] with [f:A -> True] and + [x:A]). + + On the opposite side, by not keeping the types, we loose + opportunity to propagate type informations which otherwise would + not be inferable, as e.g. when matching [forall x, x = 0] with + pattern [forall x, ?h = 0] and using the solution "x|-h:=x" in + expression [forall x, h = x] where nothing tells how the type of x + could be inferred. We also loose the ability of typing ltac + variables before calling the right-hand-side of ltac matching clauses. *) + +type constr_under_binders = Id.t list * EConstr.constr + +(** Types of substitutions with or w/o bound variables *) + +type patvar_map = EConstr.constr Id.Map.t +type extended_patvar_map = constr_under_binders Id.Map.t + +(** A globalised term together with a closure representing the value + of its free variables. Intended for use when these variables are taken + from the Ltac environment. *) +type closure = { + idents:Id.t Id.Map.t; + typed: constr_under_binders Id.Map.t ; + untyped:closed_glob_constr Id.Map.t } +and closed_glob_constr = { + closure: closure; + term: glob_constr } + +(** Ltac variable maps *) +type var_map = constr_under_binders Id.Map.t +type uconstr_var_map = closed_glob_constr Id.Map.t +type unbound_ltac_var_map = Geninterp.Val.t Id.Map.t + +type ltac_var_map = { + ltac_constrs : var_map; + (** Ltac variables bound to constrs *) + ltac_uconstrs : uconstr_var_map; + (** Ltac variables bound to untyped constrs *) + ltac_idents: Id.t Id.Map.t; + (** Ltac variables bound to identifiers *) + ltac_genargs : unbound_ltac_var_map; + (** Ltac variables bound to other kinds of arguments *) +} + +end + module Locusops : sig val clause_with_generic_occurrences : 'a Locus.clause_expr -> bool @@ -3513,7 +3551,7 @@ sig val map_glob_constr : (Glob_term.glob_constr -> Glob_term.glob_constr) -> Glob_term.glob_constr -> Glob_term.glob_constr - val empty_lvar : Glob_term.ltac_var_map + val empty_lvar : Ltac_pretype.ltac_var_map end @@ -3529,7 +3567,7 @@ sig val subst_pattern : Mod_subst.substitution -> Pattern.constr_pattern -> Pattern.constr_pattern val pattern_of_constr : Environ.env -> Evd.evar_map -> Constr.t -> Pattern.constr_pattern val instantiate_pattern : Environ.env -> - Evd.evar_map -> Pattern.extended_patvar_map -> + Evd.evar_map -> Ltac_pretype.extended_patvar_map -> Pattern.constr_pattern -> Pattern.constr_pattern end @@ -3542,16 +3580,16 @@ sig val is_matching : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> EConstr.constr -> bool val extended_matches : Environ.env -> Evd.evar_map -> binding_bound_vars * Pattern.constr_pattern -> - EConstr.constr -> bound_ident_map * Pattern.extended_patvar_map + EConstr.constr -> bound_ident_map * Ltac_pretype.extended_patvar_map exception PatternMatchingFailure type matching_result = - { m_sub : bound_ident_map * Pattern.patvar_map; + { m_sub : bound_ident_map * Ltac_pretype.patvar_map; m_ctx : EConstr.constr } val match_subterm_gen : Environ.env -> Evd.evar_map -> bool -> binding_bound_vars * Pattern.constr_pattern -> EConstr.constr -> matching_result IStream.t - val matches : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> EConstr.constr -> Pattern.patvar_map + val matches : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> EConstr.constr -> Ltac_pretype.patvar_map end module Tacred : @@ -4082,7 +4120,7 @@ sig } val understand_ltac : inference_flags -> - Environ.env -> Evd.evar_map -> Glob_term.ltac_var_map -> + Environ.env -> Evd.evar_map -> Ltac_pretype.ltac_var_map -> typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.t val understand_tcc : ?flags:inference_flags -> Environ.env -> Evd.evar_map -> ?expected_type:typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr @@ -4091,11 +4129,11 @@ sig val check_evars : Environ.env -> Evd.evar_map -> Evd.evar_map -> EConstr.constr -> unit val register_constr_interp0 : ('r, 'g, 't) Genarg.genarg_type -> - (Glob_term.unbound_ltac_var_map -> Environ.env -> Evd.evar_map -> EConstr.types -> 'g -> EConstr.constr * Evd.evar_map) -> unit + (Ltac_pretype.unbound_ltac_var_map -> Environ.env -> Evd.evar_map -> EConstr.types -> 'g -> EConstr.constr * Evd.evar_map) -> unit val all_and_fail_flags : inference_flags val ise_pretype_gen : inference_flags -> Environ.env -> Evd.evar_map -> - Glob_term.ltac_var_map -> typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr + Ltac_pretype.ltac_var_map -> typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr end module Unification : @@ -4203,7 +4241,7 @@ sig val wit_int_or_var : (int Misctypes.or_var, int Misctypes.or_var, int) Genarg.genarg_type val wit_ref : (Libnames.reference, Globnames.global_reference Loc.located Misctypes.or_var, Globnames.global_reference) Genarg.genarg_type val wit_clause_dft_concl : (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) Genarg.genarg_type - val wit_uconstr : (Constrexpr.constr_expr , Tactypes.glob_constr_and_expr, Glob_term.closed_glob_constr) Genarg.genarg_type + val wit_uconstr : (Constrexpr.constr_expr , Tactypes.glob_constr_and_expr, Ltac_pretype.closed_glob_constr) Genarg.genarg_type val wit_red_expr : ((Constrexpr.constr_expr,Libnames.reference Misctypes.or_by_notation,Constrexpr.constr_expr) Genredexpr.red_expr_gen, (Tactypes.glob_constr_and_expr,Names.evaluable_global_reference Misctypes.and_short_name Misctypes.or_var,Tactypes.glob_constr_pattern_and_expr) Genredexpr.red_expr_gen, @@ -4456,7 +4494,7 @@ end module Evar_refiner : sig - type glob_constr_ltac_closure = Glob_term.ltac_var_map * Glob_term.glob_constr + type glob_constr_ltac_closure = Ltac_pretype.ltac_var_map * Glob_term.glob_constr val w_refine : Evar.t * Evd.evar_info -> glob_constr_ltac_closure -> Evd.evar_map -> Evd.evar_map @@ -4994,16 +5032,16 @@ sig val pr_econstr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t val pr_constr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.t val pr_lconstr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.t - val pr_closed_glob : Glob_term.closed_glob_constr -> Pp.t + val pr_closed_glob : Ltac_pretype.closed_glob_constr -> Pp.t val pr_lglob_constr : Glob_term.glob_constr -> Pp.t val pr_leconstr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t val pr_leconstr : EConstr.constr -> Pp.t val pr_global : Globnames.global_reference -> Pp.t - val pr_lconstr_under_binders : Pattern.constr_under_binders -> Pp.t - val pr_lconstr_under_binders_env : Environ.env -> Evd.evar_map -> Pattern.constr_under_binders -> Pp.t + val pr_lconstr_under_binders : Ltac_pretype.constr_under_binders -> Pp.t + val pr_lconstr_under_binders_env : Environ.env -> Evd.evar_map -> Ltac_pretype.constr_under_binders -> Pp.t - val pr_constr_under_binders_env : Environ.env -> Evd.evar_map -> Pattern.constr_under_binders -> Pp.t - val pr_closed_glob_env : Environ.env -> Evd.evar_map -> Glob_term.closed_glob_constr -> Pp.t + val pr_constr_under_binders_env : Environ.env -> Evd.evar_map -> Ltac_pretype.constr_under_binders -> Pp.t + val pr_closed_glob_env : Environ.env -> Evd.evar_map -> Ltac_pretype.closed_glob_constr -> Pp.t val pr_rel_context_of : Environ.env -> Evd.evar_map -> Pp.t val pr_named_context_of : Environ.env -> Evd.evar_map -> Pp.t val pr_ltype : Term.types -> Pp.t @@ -5158,7 +5196,7 @@ module Tactics : sig open Proofview - type change_arg = Pattern.patvar_map -> Evd.evar_map -> Evd.evar_map * EConstr.constr + type change_arg = Ltac_pretype.patvar_map -> Evd.evar_map -> Evd.evar_map * EConstr.constr type tactic_reduction = Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr type elim_scheme = @@ -5337,6 +5375,11 @@ sig | Naive | FirstSolved | AllMatches + type inj_flags = { + keep_proof_equalities : bool; (* One may want it or not *) + injection_in_context : bool; (* For regularity; one may want it from ML code but not interactively *) + injection_pattern_l2r_order : bool; (* Compatibility option: no reason not to want it *) + } val build_selector : Environ.env -> Evd.evar_map -> int -> EConstr.constr -> EConstr.types -> @@ -5345,20 +5388,20 @@ sig val general_rewrite : orientation -> Locus.occurrences -> freeze_evars_flag -> dep_proof_flag -> ?tac:(unit Proofview.tactic * conditions) -> EConstr.constr -> unit Proofview.tactic - val inj : Tactypes.intro_patterns option -> Misctypes.evars_flag -> + val inj : inj_flags option -> Tactypes.intro_patterns option -> Misctypes.evars_flag -> Misctypes.clear_flag -> EConstr.constr Misctypes.with_bindings -> unit Proofview.tactic val general_multi_rewrite : Misctypes.evars_flag -> (bool * Misctypes.multi * Misctypes.clear_flag * Tactypes.delayed_open_constr_with_bindings) list -> Locus.clause -> (unit Proofview.tactic * conditions) option -> unit Proofview.tactic val replace_in_clause_maybe_by : EConstr.constr -> EConstr.constr -> Locus.clause -> unit Proofview.tactic option -> unit Proofview.tactic val replace_term : bool option -> EConstr.constr -> Locus.clause -> unit Proofview.tactic - val dEq : Misctypes.evars_flag -> EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option -> unit Proofview.tactic + val dEq : keep_proofs:bool option -> Misctypes.evars_flag -> EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option -> unit Proofview.tactic val discr_tac : Misctypes.evars_flag -> EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option -> unit Proofview.tactic - val injClause : Tactypes.intro_patterns option -> Misctypes.evars_flag -> + val injClause : inj_flags option -> Tactypes.intro_patterns option -> Misctypes.evars_flag -> EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option -> unit Proofview.tactic - val simpleInjClause : Misctypes.evars_flag -> + val simpleInjClause : inj_flags option -> Misctypes.evars_flag -> EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option -> unit Proofview.tactic val rewriteInConcl : bool -> EConstr.constr -> unit Proofview.tactic @@ -5392,8 +5435,8 @@ sig ?tac:(unit Proofview.tactic * conditions) -> EConstr.constr Misctypes.with_bindings -> Misctypes.evars_flag -> unit Proofview.tactic val discriminable : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool val discrHyp : Names.Id.t -> unit Proofview.tactic - val injectable : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool - val injHyp : Misctypes.clear_flag -> Names.Id.t -> unit Proofview.tactic + val injectable : Environ.env -> Evd.evar_map -> keep_proofs:(bool option) -> EConstr.constr -> EConstr.constr -> bool + val injHyp : inj_flags option -> Misctypes.clear_flag -> Names.Id.t -> unit Proofview.tactic val subst_gen : bool -> Names.Id.t list -> unit Proofview.tactic end @@ -18,6 +18,8 @@ Tactics such as "x := 5 : Z" (see BZ#148). This could be disabled via Unset Omega UseLocalDefs. - The tactic "romega" is also aware now of the bodies of context variables. +- Tactic "decide equality" now able to manage constructors which + contain proofs. Changes from 8.7+beta2 to 8.7.0 =============================== diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 82fd41199e..699ee6b840 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -44,6 +44,12 @@ We renamed the following datatypes: - `Pp.std_ppcmds` -> `Pp.t` +Some tactics and related functions now support static configurability, e.g.: + +- injectable, dEq, etc. takes an argument ~keep_proofs which, + - if None, tells to behave as told with the flag Keep Proof Equalities + - if Some b, tells to keep proof equalities iff b is true + ## Changes between Coq 8.6 and Coq 8.7 ### Ocaml diff --git a/dev/doc/versions-history.tex b/dev/doc/versions-history.tex index 492e75a7bb..3867d4af90 100644 --- a/dev/doc/versions-history.tex +++ b/dev/doc/versions-history.tex @@ -376,9 +376,27 @@ Coq V8.5 beta1 & released 21 January 2015 & \feature{computation via compilation && \feature{new proof engine deployed} [2-11-2013]\\ && \feature{universe polymorphism} [6-5-2014]\\ && \feature{primitive projections} [6-5-2014]\\ +&& \feature{miscellaneous optimizations}\\ Coq V8.5 beta2 & released 22 April 2015 & \feature{MMaps library} [4-3-2015]\\ +Coq V8.5 & released 22 January 2016 & \\ + +Coq V8.6 beta 1 & released 19 November 2016 & \feature{irrefutable patterns} [15-2-2016]\\ +&& \feature{Ltac profiling} [14-6-2016]\\ +&& \feature{warning system} [29-6-2016]\\ +&& \feature{miscellaneous optimizations}\\ + +Coq V8.6 & released 14 December 2016 & \\ + +Coq V8.7 beta 1 & released 6 September 2017 & \feature{bundled with Ssreflect plugin} [6-6-2017]\\ +&& \feature{cumulative polymorphic inductive types} [19-6-2017]\\ +&& \feature{further optimizations}\\ + +Coq V8.7 beta 2 & released 6 October 2017 & \\ + +Coq V8.7 & released 18 October 2016 & \\ + \end{tabular} \medskip diff --git a/dev/top_printers.ml b/dev/top_printers.ml index ffa8fffdf5..70f7c4283f 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -108,8 +108,7 @@ let ppconstrunderbindersidmap l = pp (prconstrunderbindersidmap l) let ppunbound_ltac_var_map l = ppidmap (fun _ arg -> str"<genarg:" ++ pr_argument_type(genarg_tag arg) ++ str">") -open Glob_term - +open Ltac_pretype let rec pr_closure {idents=idents;typed=typed;untyped=untyped} = hov 1 (str"{idents=" ++ prididmap idents ++ str";" ++ spc() ++ str"typed=" ++ prconstrunderbindersidmap typed ++ str";" ++ spc() ++ diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 0dbfe05d48..2695c5eee4 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -883,56 +883,60 @@ the type $V$ satisfies the nested positivity condition for $X$ \settowidth\framecharacterwidth{\hh} \newcommand\ws{\hbox{}\hskip\the\framecharacterwidth} \newcommand\ruleref[1]{\hskip.25em\dots\hskip.2em{\em (bullet #1)}} +\newcommand{\NatTree}{\mbox{\textsf{nattree}}} +\newcommand{\NatTreeA}{\mbox{\textsf{nattree}}~\ensuremath{A}} +\newcommand{\cnode}{\mbox{\textsf{node}}} +\newcommand{\cleaf}{\mbox{\textsf{leaf}}} -\noindent For instance, if one considers the type +\noindent For instance, if one considers the following variant of a tree type branching over the natural numbers \begin{verbatim} -Inductive tree (A:Type) : Type := - | leaf : list A - | node : A -> (nat -> tree A) -> tree A +Inductive nattree (A:Type) : Type := + | leaf : nattree A + | node : A -> (nat -> nattree A) -> nattree A \end{verbatim} \begin{latexonly} -\noindent Then every instantiated constructor of $\ListA$ satisfies the nested positivity condition for $\List$\\ +\noindent Then every instantiated constructor of $\NatTreeA$ satisfies the nested positivity condition for $\NatTree$\\ \noindent \ws\ws\vv\\ -\ws\ws\vh\hh\ws concerning type $\ListA$ of constructor $\Nil$:\\ -\ws\ws\vv\ws\ws\ws\ws Type $\ListA$ of constructor $\Nil$ satisfies the positivity condition for $\List$\\ -\ws\ws\vv\ws\ws\ws\ws because $\List$ does not appear in any (real) arguments of the type of that constructor\\ -\ws\ws\vv\ws\ws\ws\ws (primarily because $\List$ does not have any (real) arguments)\ruleref1\\ +\ws\ws\vh\hh\ws concerning type $\NatTreeA$ of constructor $\cleaf$:\\ +\ws\ws\vv\ws\ws\ws\ws Type $\NatTreeA$ of constructor $\cleaf$ satisfies the positivity condition for $\NatTree$\\ +\ws\ws\vv\ws\ws\ws\ws because $\NatTree$ does not appear in any (real) arguments of the type of that constructor\\ +\ws\ws\vv\ws\ws\ws\ws (primarily because $\NatTree$ does not have any (real) arguments)\ruleref1\\ \ws\ws\vv\\ -\ws\ws\hv\hh\ws concerning type $\forall~A\ra\ListA\ra\ListA$ of constructor $\cons$:\\ -\ws\ws\ws\ws\ws\ws\ws Type $\forall~A:\Type,A\ra\ListA\ra\ListA$ of constructor $\cons$\\ -\ws\ws\ws\ws\ws\ws\ws satisfies the positivity condition for $\List$ because:\\ +\ws\ws\hv\hh\ws concerning type $\forall~A\ra(\NN\ra\NatTreeA)\ra\NatTreeA$ of constructor $\cnode$:\\ + \ws\ws\ws\ws\ws\ws\ws Type $\forall~A:\Type,A\ra(\NN\ra\NatTreeA)\ra\NatTreeA$ of constructor $\cnode$\\ +\ws\ws\ws\ws\ws\ws\ws satisfies the positivity condition for $\NatTree$ because:\\ \ws\ws\ws\ws\ws\ws\ws\vv\\ -\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $\Type$\ruleref3\\ +\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\NatTree$ occurs only strictly positively in $\Type$\ruleref1\\ \ws\ws\ws\ws\ws\ws\ws\vv\\ -\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $A$\ruleref3\\ +\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\NatTree$ occurs only strictly positively in $A$\ruleref1\\ \ws\ws\ws\ws\ws\ws\ws\vv\\ -\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $\ListA$\ruleref4\\ + \ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\NatTree$ occurs only strictly positively in $\NN\ra\NatTreeA$\ruleref{3+2}\\ \ws\ws\ws\ws\ws\ws\ws\vv\\ -\ws\ws\ws\ws\ws\ws\ws\hv\hh\ws $\List$ satisfies the positivity condition for $\ListA$\ruleref1 +\ws\ws\ws\ws\ws\ws\ws\hv\hh\ws $\NatTree$ satisfies the positivity condition for $\NatTreeA$\ruleref1 \end{latexonly} \begin{rawhtml} <pre> -<span style="font-family:serif">Then every instantiated constructor of <span style="font-family:monospace">list A</span> satisfies the nested positivity condition for <span style="font-family:monospace">list</span></span> +<span style="font-family:serif">Then every instantiated constructor of <span style="font-family:monospace">nattree A</span> satisfies the nested positivity condition for <span style="font-family:monospace">nattree</span></span> │ - ├─ <span style="font-family:serif">concerning type <span style="font-family:monospace">list A</span> of constructor <span style="font-family:monospace">nil</span>:</span> - │ <span style="font-family:serif">Type <span style="font-family:monospace">list A</span> of constructor <span style="font-family:monospace">nil</span> satisfies the positivity condition for <span style="font-family:monospace">list</span></span> - │ <span style="font-family:serif">because <span style="font-family:monospace">list</span> does not appear in any (real) arguments of the type of that constructor</span> - │ <span style="font-family:serif">(primarily because list does not have any (real) arguments) ... <span style="font-style:italic">(bullet 1)</span></span> + ├─ <span style="font-family:serif">concerning type <span style="font-family:monospace">nattree A</span> of constructor <span style="font-family:monospace">nil</span>:</span> + │ <span style="font-family:serif">Type <span style="font-family:monospace">nattree A</span> of constructor <span style="font-family:monospace">nil</span> satisfies the positivity condition for <span style="font-family:monospace">nattree</span></span> + │ <span style="font-family:serif">because <span style="font-family:monospace">nattree</span> does not appear in any (real) arguments of the type of that constructor</span> + │ <span style="font-family:serif">(primarily because nattree does not have any (real) arguments) ... <span style="font-style:italic">(bullet 1)</span></span> │ - ╰─ <span style="font-family:serif">concerning type <span style="font-family:monospace">∀ A → list A → list A</span> of constructor <span style="font-family:monospace">cons</span>:</span> - <span style="font-family:serif">Type <span style="font-family:monospace">∀ A : Type, A → list A → list A</span> of constructor <span style="font-family:monospace">cons</span></span> - <span style="font-family:serif">satisfies the positivity condition for <span style="font-family:monospace">list</span> because:</span> + ╰─ <span style="font-family:serif">concerning type <span style="font-family:monospace">∀ A → (nat → nattree A) → nattree A</span> of constructor <span style="font-family:monospace">cons</span>:</span> + <span style="font-family:serif">Type <span style="font-family:monospace">∀ A : Type, A → (nat → nattree A) → nattree A</span> of constructor <span style="font-family:monospace">cons</span></span> + <span style="font-family:serif">satisfies the positivity condition for <span style="font-family:monospace">nattree</span> because:</span> │ - ├─ <span style="font-family:serif"><span style="font-family:monospace">list</span> occurs only strictly positively in <span style="font-family:monospace">Type</span> ... <span style="font-style:italic">(bullet 3)</span></span> + ├─ <span style="font-family:serif"><span style="font-family:monospace">nattree</span> occurs only strictly positively in <span style="font-family:monospace">Type</span> ... <span style="font-style:italic">(bullet 1)</span></span> │ - ├─ <span style="font-family:serif"><span style="font-family:monospace">list</span> occurs only strictly positively in <span style="font-family:monospace">A</span> ... <span style="font-style:italic">(bullet 3)</span></span> + ├─ <span style="font-family:serif"><span style="font-family:monospace">nattree</span> occurs only strictly positively in <span style="font-family:monospace">A</span> ... <span style="font-style:italic">(bullet 1)</span></span> │ - ├─ <span style="font-family:serif"><span style="font-family:monospace">list</span> occurs only strictly positively in <span style="font-family:monospace">list A</span> ... <span style="font-style:italic">(bullet 4)</span></span> + ├─ <span style="font-family:serif"><span style="font-family:monospace">nattree</span> occurs only strictly positively in <span style="font-family:monospace">nat → nattree A</span> ... <span style="font-style:italic">(bullet 3+2)</span></span> │ - ╰─ <span style="font-family:serif"><span style="font-family:monospace">list</span> satisfies the positivity condition for <span style="font-family:monospace">list A</span> ... <span style="font-style:italic">(bullet 1)</span></span> + ╰─ <span style="font-family:serif"><span style="font-family:monospace">nattree</span> satisfies the positivity condition for <span style="font-family:monospace">nattree A</span> ... <span style="font-style:italic">(bullet 1)</span></span> </pre> \end{rawhtml} diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index b27a4dc943..5c519e46e3 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -1840,6 +1840,9 @@ This is useful for declaring the implicit type of a single variable. \subsection{Implicit generalization \label{implicit-generalization} \comindex{Generalizable Variables}} +% \textquoteleft since \` doesn't do what we want +\index{0genimpl@{\textquoteleft\{\ldots\}}} +\index{0genexpl@{\textquoteleft(\ldots)}} Implicit generalization is an automatic elaboration of a statement with free variables into a closed statement where these variables are diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index df0cd2b825..41ea0a5dcd 100644 --- a/doc/refman/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex @@ -434,6 +434,7 @@ be shortened in {\tt fun~x~y~z~:~A~=>~t}). \subsection{Abstractions \label{abstractions} \index{abstractions}} +\index{fun@{{\tt fun \ldots => \ldots}}} The expression ``{\tt fun} {\ident} {\tt :} {\type} {\tt =>}~{\term}'' defines the {\em abstraction} of the variable {\ident}, of type @@ -455,6 +456,7 @@ occurs in the list of binders, it is expanded to a let-in definition \subsection{Products \label{products} \index{products}} +\index{forall@{{\tt forall \ldots, \ldots}}} The expression ``{\tt forall}~{\ident}~{\tt :}~{\type}{\tt ,}~{\term}'' denotes the {\em product} of the variable {\ident} of @@ -495,6 +497,7 @@ arguments is used for making explicit the value of implicit arguments \subsection{Type cast \label{typecast} \index{Cast}} +\index{cast@{{\tt(\ldots: \ldots)}}} The expression ``{\term}~{\tt :}~{\type}'' is a type cast expression. It enforces the type of {\term} to be {\type}. @@ -514,6 +517,7 @@ symbol ``\_'' and {\Coq} will guess the missing piece of information. \label{let-in} \index{Let-in definitions} \index{let-in}} +\index{let@{{\tt let \ldots := \ldots in \ldots}}} {\tt let}~{\ident}~{\tt :=}~{\term$_1$}~{\tt in}~{\term$_2$} denotes diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index a2d45046b0..675c2bf174 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3523,8 +3523,13 @@ with its $\beta\iota$-normal form. \end{ErrMsgs} \begin{Variants} +\item {\tt unfold {\qualid} in {\ident}} + \tacindex{unfold \dots in} + + Replaces {\qualid} in hypothesis {\ident} with its definition + and replaces the hypothesis with its $\beta\iota$ normal form. + \item {\tt unfold {\qualid}$_1$, \dots, \qualid$_n$} - \tacindex{unfold \dots\ in} Replaces {\em simultaneously} {\qualid}$_1$, \dots, {\qualid}$_n$ with their definitions and replaces the current goal with its @@ -3836,6 +3841,26 @@ this tactic. % En attente d'un moyen de valoriser les fichiers de demos %\SeeAlso file \texttt{contrib/Rocq/DEMOS/Demo\_AutoRewrite.v} +\subsection{\tt easy} +\tacindex{easy} +\label{easy} + +This tactic tries to solve the current goal by a number of standard closing steps. +In particular, it tries to close the current goal using the closing tactics +{\tt trivial}, reflexivity, symmetry, contradiction and inversion of hypothesis. +If this fails, it tries introducing variables and splitting and-hypotheses, +using the closing tactics afterwards, and splitting the goal using {\tt split} and recursing. + +This tactic solves goals that belong to many common classes; in particular, many cases of +unsatisfiable hypotheses, and simple equality goals are usually solved by this tactic. + +\begin{Variant} +\item {\tt now \tac} + \tacindex{now} + + Run \tac\/ followed by easy. This is a notation for {\tt \tac; easy}. +\end{Variant} + \section{Controlling automation} \subsection{The hints databases for {\tt auto} and {\tt eauto}} diff --git a/ide/tags.ml b/ide/tags.ml index 08ca47a842..4020271798 100644 --- a/ide/tags.ml +++ b/ide/tags.ml @@ -15,33 +15,22 @@ let make_tag (tt:GText.tag_table) ~name prop = module Script = struct + (* More recently defined tags have highest priority in case of overlapping *) let table = GText.tag_table () - let comment = make_tag table ~name:"comment" [] - let error = make_tag table ~name:"error" [`UNDERLINE `SINGLE] let warning = make_tag table ~name:"warning" [`UNDERLINE `SINGLE; `FOREGROUND "blue"] + let error = make_tag table ~name:"error" [`UNDERLINE `SINGLE] let error_bg = make_tag table ~name:"error_bg" [] let to_process = make_tag table ~name:"to_process" [] let processed = make_tag table ~name:"processed" [] - let incomplete = make_tag table ~name:"incomplete" [ - `BACKGROUND_STIPPLE_SET true; - ] + let incomplete = make_tag table ~name:"incomplete" [`BACKGROUND_STIPPLE_SET true] let unjustified = make_tag table ~name:"unjustified" [`BACKGROUND "gold"] - let found = make_tag table ~name:"found" [`BACKGROUND "blue"; `FOREGROUND "white"] - let sentence = make_tag table ~name:"sentence" [] let tooltip = make_tag table ~name:"tooltip" [] (* debug:`BACKGROUND "blue" *) - let ephemere = [error; warning; error_bg; tooltip; processed; to_process; incomplete; unjustified] - - let all = - comment :: found :: sentence :: ephemere - - let edit_zone = - let t = make_tag table ~name:"edit_zone" [`UNDERLINE `SINGLE] in - t#set_priority (List.length all); - t - let all = edit_zone :: all - + let comment = make_tag table ~name:"comment" [] + let sentence = make_tag table ~name:"sentence" [] + let edit_zone = make_tag table ~name:"edit_zone" [`UNDERLINE `SINGLE] (* for debugging *) + let all = edit_zone :: comment :: sentence :: ephemere end module Proof = struct diff --git a/ide/tags.mli b/ide/tags.mli index 265dfe46e3..15a35185df 100644 --- a/ide/tags.mli +++ b/ide/tags.mli @@ -17,7 +17,6 @@ sig val processed : GText.tag val incomplete : GText.tag val unjustified : GText.tag - val found : GText.tag val sentence : GText.tag val tooltip : GText.tag val edit_zone : GText.tag (* for debugging *) diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 593580fb7e..b2df449c59 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -19,6 +19,7 @@ open Constrexpr open Notation_term open Notation open Misctypes +open Ltac_pretype (** Translation of pattern, cases pattern, glob_constr and term into syntax trees for printing *) diff --git a/interp/stdarg.mli b/interp/stdarg.mli index dffbd6659f..ed00fe2967 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -51,7 +51,7 @@ val wit_sort_family : (Sorts.family, unit, unit) genarg_type val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type -val wit_uconstr : (constr_expr , glob_constr_and_expr, Glob_term.closed_glob_constr) genarg_type +val wit_uconstr : (constr_expr , glob_constr_and_expr, Ltac_pretype.closed_glob_constr) genarg_type val wit_open_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type diff --git a/intf/glob_term.ml b/intf/glob_term.ml index 757ba57868..508990a580 100644 --- a/intf/glob_term.ml +++ b/intf/glob_term.ml @@ -100,30 +100,3 @@ type 'a extended_glob_local_binder_r = and 'a extended_glob_local_binder_g = ('a extended_glob_local_binder_r, 'a) DAst.t type extended_glob_local_binder = [ `any ] extended_glob_local_binder_g - -(** A globalised term together with a closure representing the value - of its free variables. Intended for use when these variables are taken - from the Ltac environment. *) -type closure = { - idents:Id.t Id.Map.t; - typed: Pattern.constr_under_binders Id.Map.t ; - untyped:closed_glob_constr Id.Map.t } -and closed_glob_constr = { - closure: closure; - term: glob_constr } - -(** Ltac variable maps *) -type var_map = Pattern.constr_under_binders Id.Map.t -type uconstr_var_map = closed_glob_constr Id.Map.t -type unbound_ltac_var_map = Geninterp.Val.t Id.Map.t - -type ltac_var_map = { - ltac_constrs : var_map; - (** Ltac variables bound to constrs *) - ltac_uconstrs : uconstr_var_map; - (** Ltac variables bound to untyped constrs *) - ltac_idents: Id.t Id.Map.t; - (** Ltac variables bound to identifiers *) - ltac_genargs : unbound_ltac_var_map; - (** Ltac variables bound to other kinds of arguments *) -} diff --git a/intf/pattern.ml b/intf/pattern.ml index 2ab526984a..16c4807355 100644 --- a/intf/pattern.ml +++ b/intf/pattern.ml @@ -11,45 +11,6 @@ open Globnames open Term open Misctypes -(** {5 Maps of pattern variables} *) - -(** Type [constr_under_binders] is for representing the term resulting - of a matching. Matching can return terms defined in a some context - of named binders; in the context, variable names are ordered by - (<) and referred to by index in the term Thanks to the canonical - ordering, a matching problem like - - [match ... with [(fun x y => ?p,fun y x => ?p)] => [forall x y => p]] - - will be accepted. Thanks to the reference by index, a matching - problem like - - [match ... with [(fun x => ?p)] => [forall x => p]] - - will work even if [x] is also the name of an existing goal - variable. - - Note: we do not keep types in the signature. Besides simplicity, - the main reason is that it would force to close the signature over - binders that occur only in the types of effective binders but not - in the term itself (e.g. for a term [f x] with [f:A -> True] and - [x:A]). - - On the opposite side, by not keeping the types, we loose - opportunity to propagate type informations which otherwise would - not be inferable, as e.g. when matching [forall x, x = 0] with - pattern [forall x, ?h = 0] and using the solution "x|-h:=x" in - expression [forall x, h = x] where nothing tells how the type of x - could be inferred. We also loose the ability of typing ltac - variables before calling the right-hand-side of ltac matching clauses. *) - -type constr_under_binders = Id.t list * EConstr.constr - -(** Types of substitutions with or w/o bound variables *) - -type patvar_map = EConstr.constr Id.Map.t -type extended_patvar_map = constr_under_binders Id.Map.t - (** {5 Patterns} *) type case_info_pattern = diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 9cb2a0a3f5..93317fce1b 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -570,6 +570,11 @@ let rec reflexivity_with_destruct_cases g = with e when CErrors.noncritical e -> Proofview.V82.of_tactic reflexivity in let eq_ind = make_eq () in + let my_inj_flags = Some { + Equality.keep_proof_equalities = false; + injection_in_context = false; (* for compatibility, necessary *) + injection_pattern_l2r_order = false; (* probably does not matter; except maybe with dependent hyps *) + } in let discr_inject = Tacticals.onAllHypsAndConcl ( fun sc g -> @@ -580,8 +585,8 @@ let rec reflexivity_with_destruct_cases g = | App(eq,[|_;t1;t2|]) when EConstr.eq_constr (project g) eq eq_ind -> if Equality.discriminable (pf_env g) (project g) t1 t2 then Proofview.V82.of_tactic (Equality.discrHyp id) g - else if Equality.injectable (pf_env g) (project g) t1 t2 - then tclTHENLIST [Proofview.V82.of_tactic (Equality.injHyp None id);thin [id];intros_with_rewrite] g + else if Equality.injectable (pf_env g) (project g) ~keep_proofs:None t1 t2 + then tclTHENLIST [Proofview.V82.of_tactic (Equality.injHyp my_inj_flags None id);thin [id];intros_with_rewrite] g else tclIDTAC g | _ -> tclIDTAC g ) diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index d9150a7bbd..1f628803a3 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -17,6 +17,7 @@ open Refiner open Evd open Locus open Context.Named.Declaration +open Ltac_pretype module NamedDecl = Context.Named.Declaration @@ -27,7 +28,7 @@ let instantiate_evar evk (ist,rawc) sigma = let filtered = Evd.evar_filtered_env evi in let constrvars = Tacinterp.extract_ltac_constr_values ist filtered in let lvar = { - Glob_term.ltac_constrs = constrvars; + ltac_constrs = constrvars; ltac_uconstrs = Names.Id.Map.empty; ltac_idents = Names.Id.Map.empty; ltac_genargs = ist.Geninterp.lfun; diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index a7aebf9e15..65c186a419 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -91,12 +91,12 @@ let elimOnConstrWithHoles tac with_evars c = (fun c -> tac with_evars (Some (None,ElimOnConstr c))) TACTIC EXTEND simplify_eq - [ "simplify_eq" ] -> [ dEq false None ] -| [ "simplify_eq" destruction_arg(c) ] -> [ mytclWithHoles dEq false c ] + [ "simplify_eq" ] -> [ dEq ~keep_proofs:None false None ] +| [ "simplify_eq" destruction_arg(c) ] -> [ mytclWithHoles (dEq ~keep_proofs:None) false c ] END TACTIC EXTEND esimplify_eq -| [ "esimplify_eq" ] -> [ dEq true None ] -| [ "esimplify_eq" destruction_arg(c) ] -> [ mytclWithHoles dEq true c ] +| [ "esimplify_eq" ] -> [ dEq ~keep_proofs:None true None ] +| [ "esimplify_eq" destruction_arg(c) ] -> [ mytclWithHoles (dEq ~keep_proofs:None) true c ] END let discr_main c = elimOnConstrWithHoles discr_tac false c @@ -117,31 +117,31 @@ let discrHyp id = discr_main (fun env sigma -> (sigma, (EConstr.mkVar id, NoBindings))) let injection_main with_evars c = - elimOnConstrWithHoles (injClause None) with_evars c + elimOnConstrWithHoles (injClause None None) with_evars c TACTIC EXTEND injection -| [ "injection" ] -> [ injClause None false None ] -| [ "injection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None) false c ] +| [ "injection" ] -> [ injClause None None false None ] +| [ "injection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None None) false c ] END TACTIC EXTEND einjection -| [ "einjection" ] -> [ injClause None true None ] -| [ "einjection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None) true c ] +| [ "einjection" ] -> [ injClause None None true None ] +| [ "einjection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None None) true c ] END TACTIC EXTEND injection_as | [ "injection" "as" intropattern_list(ipat)] -> - [ injClause (Some ipat) false None ] + [ injClause None (Some ipat) false None ] | [ "injection" destruction_arg(c) "as" intropattern_list(ipat)] -> - [ mytclWithHoles (injClause (Some ipat)) false c ] + [ mytclWithHoles (injClause None (Some ipat)) false c ] END TACTIC EXTEND einjection_as | [ "einjection" "as" intropattern_list(ipat)] -> - [ injClause (Some ipat) true None ] + [ injClause None (Some ipat) true None ] | [ "einjection" destruction_arg(c) "as" intropattern_list(ipat)] -> - [ mytclWithHoles (injClause (Some ipat)) true c ] + [ mytclWithHoles (injClause None (Some ipat)) true c ] END TACTIC EXTEND simple_injection -| [ "simple" "injection" ] -> [ simpleInjClause false None ] -| [ "simple" "injection" destruction_arg(c) ] -> [ mytclWithHoles simpleInjClause false c ] +| [ "simple" "injection" ] -> [ simpleInjClause None false None ] +| [ "simple" "injection" destruction_arg(c) ] -> [ mytclWithHoles (simpleInjClause None) false c ] END let injHyp id = diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 9e3a54cc86..a79a92a661 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -10,7 +10,6 @@ open Util open Names open Term open EConstr -open Pattern open Misctypes open Genarg open Stdarg @@ -24,7 +23,7 @@ let (wit_constr_context : (Empty.t, Empty.t, EConstr.constr) Genarg.genarg_type) wit (* includes idents known to be bound and references *) -let (wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) Genarg.genarg_type) = +let (wit_constr_under_binders : (Empty.t, Empty.t, Ltac_pretype.constr_under_binders) Genarg.genarg_type) = let wit = Genarg.create_arg "constr_under_binders" in let () = register_val0 wit None in wit diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index 1a67f6f888..d7b253a687 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -10,7 +10,6 @@ open Util open Names open EConstr open Misctypes -open Pattern open Genarg open Geninterp @@ -37,8 +36,8 @@ sig val of_constr : constr -> t val to_constr : t -> constr option - val of_uconstr : Glob_term.closed_glob_constr -> t - val to_uconstr : t -> Glob_term.closed_glob_constr option + val of_uconstr : Ltac_pretype.closed_glob_constr -> t + val to_uconstr : t -> Ltac_pretype.closed_glob_constr option val of_int : int -> t val to_int : t -> int option val to_list : t -> t list option @@ -63,9 +62,9 @@ val coerce_to_hint_base : Value.t -> string val coerce_to_int : Value.t -> int -val coerce_to_constr : Environ.env -> Value.t -> constr_under_binders +val coerce_to_constr : Environ.env -> Value.t -> Ltac_pretype.constr_under_binders -val coerce_to_uconstr : Environ.env -> Value.t -> Glob_term.closed_glob_constr +val coerce_to_uconstr : Environ.env -> Value.t -> Ltac_pretype.closed_glob_constr val coerce_to_closed_constr : Environ.env -> Value.t -> constr @@ -93,4 +92,4 @@ val coerce_to_int_or_var_list : Value.t -> int or_var list val wit_constr_context : (Empty.t, Empty.t, EConstr.constr) genarg_type -val wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) genarg_type +val wit_constr_under_binders : (Empty.t, Empty.t, Ltac_pretype.constr_under_binders) genarg_type diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 2c36faeff4..1639736883 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -386,7 +386,7 @@ type ltac_call_kind = | LtacNameCall of ltac_constant | LtacAtomCall of glob_atomic_tactic_expr | LtacVarCall of Id.t * glob_tactic_expr - | LtacConstrInterp of Glob_term.glob_constr * Glob_term.ltac_var_map + | LtacConstrInterp of Glob_term.glob_constr * Ltac_pretype.ltac_var_map type ltac_trace = ltac_call_kind Loc.located list diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 99d7684d36..f171fd07d7 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -322,13 +322,23 @@ let intern_constr_pattern ist ~as_type ~ltacvars pc = let dummy_pat = PRel 0 -let intern_typed_pattern ist p = +let intern_typed_pattern ist ~as_type ~ltacvars p = (* we cannot ensure in non strict mode that the pattern is closed *) (* keeping a constr_expr copy is too complicated and we want anyway to *) (* type it, so we remember the pattern as a glob_constr only *) + let metas,pat = + if !strict_check then + let ltacvars = { + Constrintern.ltac_vars = ltacvars; + ltac_bound = Id.Set.empty; + ltac_extra = ist.extra; + } in + Constrintern.intern_constr_pattern ist.genv ~as_type ~ltacvars p + else + [], dummy_pat in let (glob,_ as c) = intern_constr_gen true false ist p in let bound_names = Glob_ops.bound_glob_vars glob in - (bound_names,c,dummy_pat) + metas,(bound_names,c,pat) let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = let interp_ref r = @@ -364,7 +374,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = (* We interpret similarly @ref and ref *) interp_ref (AN r) | Inr c -> - Inr (intern_typed_pattern ist c)) + Inr (snd (intern_typed_pattern ist ~as_type:false ~ltacvars:ist.ltacvars c))) (* This seems fairly hacky, but it's the first way I've found to get proper globalization of [unfold]. --adamc *) @@ -529,7 +539,12 @@ let rec intern_atomic lf ist x = then intern_type ist c else intern_constr ist c), clause_app (intern_hyp_location ist) cl) | TacChange (Some p,c,cl) -> - TacChange (Some (intern_typed_pattern ist p),intern_constr ist c, + let { ltacvars } = ist in + let metas,pat = intern_typed_pattern ist ~as_type:false ~ltacvars p in + let fold accu x = Id.Set.add x accu in + let ltacvars = List.fold_left fold ltacvars metas in + let ist' = { ist with ltacvars } in + TacChange (Some pat,intern_constr ist' c, clause_app (intern_hyp_location ist) cl) (* Equality and inversion *) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 20f117ff4f..66f124d2d1 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -38,6 +38,7 @@ open Tacintern open Taccoerce open Proofview.Notations open Context.Named.Declaration +open Ltac_pretype let ltac_trace_info = Tactic_debug.ltac_trace_info @@ -551,7 +552,6 @@ let interp_fresh_id ist env sigma l = (* Extract the uconstr list from lfun *) let extract_ltac_constr_context ist env sigma = - let open Glob_term in let add_uconstr id v map = try Id.Map.add id (coerce_to_uconstr env v) map with CannotCoerceTo _ -> map @@ -602,10 +602,10 @@ let interp_gen kind ist pattern_mode flags env sigma c = let { closure = constrvars ; term } = interp_glob_closure ist env sigma ~kind:kind_for_intern ~pattern_mode c in let vars = { - Glob_term.ltac_constrs = constrvars.typed; - Glob_term.ltac_uconstrs = constrvars.untyped; - Glob_term.ltac_idents = constrvars.idents; - Glob_term.ltac_genargs = ist.lfun; + ltac_constrs = constrvars.typed; + ltac_uconstrs = constrvars.untyped; + ltac_idents = constrvars.idents; + ltac_genargs = ist.lfun; } in (* Jason Gross: To avoid unnecessary modifications to tacinterp, as suggested by Arnaud Spiwack, we run push_trace immediately. We do diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index d0a0a81d4c..5f2723a1e3 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -44,7 +44,7 @@ val f_avoid_ids : Id.Set.t TacStore.field val f_debug : debug_info TacStore.field val extract_ltac_constr_values : interp_sign -> Environ.env -> - Pattern.constr_under_binders Id.Map.t + Ltac_pretype.constr_under_binders Id.Map.t (** Given an interpretation signature, extract all values which are coercible to a [constr]. *) @@ -57,7 +57,7 @@ val get_debug : unit -> debug_info val type_uconstr : ?flags:Pretyping.inference_flags -> ?expected_type:Pretyping.typing_constraint -> - Geninterp.interp_sign -> Glob_term.closed_glob_constr -> constr Tactypes.delayed_open + Geninterp.interp_sign -> Ltac_pretype.closed_glob_constr -> constr Tactypes.delayed_open (** Adds an interpretation function for extra generic arguments *) @@ -79,10 +79,10 @@ val interp_hyp : interp_sign -> Environ.env -> Evd.evar_map -> val interp_glob_closure : interp_sign -> Environ.env -> Evd.evar_map -> ?kind:Pretyping.typing_constraint -> ?pattern_mode:bool -> glob_constr_and_expr -> - Glob_term.closed_glob_constr + Ltac_pretype.closed_glob_constr val interp_uconstr : interp_sign -> Environ.env -> Evd.evar_map -> - glob_constr_and_expr -> Glob_term.closed_glob_constr + glob_constr_and_expr -> Ltac_pretype.closed_glob_constr val interp_constr_gen : Pretyping.typing_constraint -> interp_sign -> Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Evd.evar_map * constr diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 5394b1e116..a669692fc9 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -363,7 +363,7 @@ let explain_ltac_call_trace last trace loc = | Tacexpr.LtacAtomCall te -> quote (Pptactic.pr_glob_tactic (Global.env()) (Tacexpr.TacAtom (Loc.tag te))) - | Tacexpr.LtacConstrInterp (c, { Glob_term.ltac_constrs = vars }) -> + | Tacexpr.LtacConstrInterp (c, { Ltac_pretype.ltac_constrs = vars }) -> quote (Printer.pr_glob_constr_env (Global.env()) c) ++ (if not (Id.Map.is_empty vars) then strbrk " (with " ++ diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index 18bb7d2dbd..89b78e5907 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -22,7 +22,7 @@ module NamedDecl = Context.Named.Declaration those of {!Matching.matching_result}), and a {!Term.constr} substitution mapping corresponding to matched hypotheses. *) type 'a t = { - subst : Constr_matching.bound_ident_map * Pattern.extended_patvar_map ; + subst : Constr_matching.bound_ident_map * Ltac_pretype.extended_patvar_map ; context : EConstr.constr Id.Map.t; terms : EConstr.constr Id.Map.t; lhs : 'a; @@ -36,8 +36,8 @@ type 'a t = { (** Some of the functions of {!Matching} return the substitution with a [patvar_map] instead of an [extended_patvar_map]. [adjust] coerces substitution of the former type to the latter. *) -let adjust : Constr_matching.bound_ident_map * Pattern.patvar_map -> - Constr_matching.bound_ident_map * Pattern.extended_patvar_map = +let adjust : Constr_matching.bound_ident_map * Ltac_pretype.patvar_map -> + Constr_matching.bound_ident_map * Ltac_pretype.extended_patvar_map = fun (l, lc) -> (l, Id.Map.map (fun c -> [], c) lc) diff --git a/plugins/ltac/tactic_matching.mli b/plugins/ltac/tactic_matching.mli index 01334d36c9..955f8105fb 100644 --- a/plugins/ltac/tactic_matching.mli +++ b/plugins/ltac/tactic_matching.mli @@ -18,7 +18,7 @@ those of {!Matching.matching_result}), and a {!Term.constr} substitution mapping corresponding to matched hypotheses. *) type 'a t = { - subst : Constr_matching.bound_ident_map * Pattern.extended_patvar_map ; + subst : Constr_matching.bound_ident_map * Ltac_pretype.extended_patvar_map ; context : EConstr.constr Names.Id.Map.t; terms : EConstr.constr Names.Id.Map.t; lhs : 'a; diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index d37c676e38..1f2d02093d 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -227,7 +227,7 @@ let isAppInd gl c = let interp_refine ist gl rc = let constrvars = Tacinterp.extract_ltac_constr_values ist (pf_env gl) in let vars = { Glob_ops.empty_lvar with - Glob_term.ltac_constrs = constrvars; ltac_genargs = ist.Tacinterp.lfun + Ltac_pretype.ltac_constrs = constrvars; ltac_genargs = ist.Tacinterp.lfun } in let kind = Pretyping.OfType (pf_concl gl) in let flags = { diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 832044909c..26b5c57675 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -396,7 +396,7 @@ let revtoptac n0 gl = let equality_inj l b id c gl = let msg = ref "" in - try Proofview.V82.of_tactic (Equality.inj l b None c) gl + try Proofview.V82.of_tactic (Equality.inj None l b None c) gl with | Ploc.Exc(_,CErrors.UserError (_,s)) | CErrors.UserError (_,s) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 08ce72932a..aefa09dbe6 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -33,6 +33,7 @@ open Evarsolve open Evarconv open Evd open Context.Rel.Declaration +open Ltac_pretype module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration @@ -245,7 +246,7 @@ let push_history_pattern n pci cont = type 'a pattern_matching_problem = { env : env; - lvar : Glob_term.ltac_var_map; + lvar : Ltac_pretype.ltac_var_map; evdref : evar_map ref; pred : constr; tomatch : tomatch_stack; diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 7bdc604b88..cbf5788e48 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -14,6 +14,7 @@ open EConstr open Inductiveops open Glob_term open Evarutil +open Ltac_pretype (** {5 Compilation of pattern-matching } *) @@ -101,7 +102,7 @@ and pattern_continuation = type 'a pattern_matching_problem = { env : env; - lvar : Glob_term.ltac_var_map; + lvar : Ltac_pretype.ltac_var_map; evdref : evar_map ref; pred : constr; tomatch : tomatch_stack; @@ -119,11 +120,11 @@ val prepare_predicate : ?loc:Loc.t -> Environ.env -> Evd.evar_map ref -> ltac_var_map -> glob_constr -> unsafe_judgment) -> Environ.env -> Evd.evar_map -> - Glob_term.ltac_var_map -> + Ltac_pretype.ltac_var_map -> (types * tomatch_type) list -> (rel_context * rel_context) list -> constr option -> glob_constr option -> (Evd.evar_map * Names.name list * constr) list val make_return_predicate_ltac_lvar : Evd.evar_map -> Names.name -> - Glob_term.glob_constr -> constr -> Glob_term.ltac_var_map -> Glob_term.ltac_var_map + Glob_term.glob_constr -> constr -> Ltac_pretype.ltac_var_map -> ltac_var_map diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 0973d73ee0..9128d4042b 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -22,6 +22,7 @@ open Pattern open Patternops open Misctypes open Context.Rel.Declaration +open Ltac_pretype (*i*) (* Given a term with second-order variables in it, diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli index 1d7019d09f..34c62043ef 100644 --- a/pretyping/constr_matching.mli +++ b/pretyping/constr_matching.mli @@ -13,6 +13,7 @@ open Term open EConstr open Environ open Pattern +open Ltac_pretype type binding_bound_vars = Id.Set.t diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index f3e8e72bb7..c02fc5aafd 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -27,6 +27,7 @@ open Mod_subst open Misctypes open Decl_kinds open Context.Named.Declaration +open Ltac_pretype type _ delay = | Now : 'a delay diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index b70bfd83c1..f03bde68ec 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -15,6 +15,7 @@ open Termops open Mod_subst open Misctypes open Evd +open Ltac_pretype type _ delay = | Now : 'a delay diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index ad1409f5b1..7f81d1aa34 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -842,6 +842,15 @@ let rec find_solution_type evarenv = function | (id,ProjectEvar _)::l -> find_solution_type evarenv l | [] -> assert false +let find_most_recent_projection evi sols = + let sign = List.map get_id (evar_filtered_context evi) in + match sols with + | y::l -> + List.fold_right (fun (id,p as x) (id',_ as y) -> + if List.index Id.equal id sign < List.index Id.equal id' sign then x else y) + l y + | _ -> assert false + (* In case the solution to a projection problem requires the instantiation of * subsidiary evars, [do_projection_effects] performs them; it * also try to instantiate the type of those subsidiary evars if their @@ -1429,7 +1438,8 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = let c, p = match sols with | [] -> raise Not_found | [id,p] -> (mkVar id, p) - | (id,p)::_::_ -> + | _ -> + let (id,p) = find_most_recent_projection evi sols in if choose then (mkVar id, p) else raise (NotUniqueInType sols) in let ty = lazy (Retyping.get_type_of env !evdref (of_alias t)) in diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 7804cc6796..055fd68f6c 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -13,6 +13,7 @@ open Globnames open Misctypes open Glob_term open Evar_kinds +open Ltac_pretype (* Untyped intermediate terms, after ASTs and before constr. *) diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 49ea9727c6..f27928662e 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -84,5 +84,5 @@ val glob_constr_of_closed_cases_pattern : 'a cases_pattern_g -> Name.t * 'a glob val add_patterns_for_params_remove_local_defs : constructor -> 'a cases_pattern_g list -> 'a cases_pattern_g list -val ltac_interp_name : Glob_term.ltac_var_map -> Names.name -> Names.name -val empty_lvar : Glob_term.ltac_var_map +val ltac_interp_name : Ltac_pretype.ltac_var_map -> Names.name -> Names.name +val empty_lvar : Ltac_pretype.ltac_var_map diff --git a/pretyping/ltac_pretype.ml b/pretyping/ltac_pretype.ml new file mode 100644 index 0000000000..be8579c2e5 --- /dev/null +++ b/pretyping/ltac_pretype.ml @@ -0,0 +1,68 @@ +open Names +open Glob_term + +(** {5 Maps of pattern variables} *) + +(** Type [constr_under_binders] is for representing the term resulting + of a matching. Matching can return terms defined in a some context + of named binders; in the context, variable names are ordered by + (<) and referred to by index in the term Thanks to the canonical + ordering, a matching problem like + + [match ... with [(fun x y => ?p,fun y x => ?p)] => [forall x y => p]] + + will be accepted. Thanks to the reference by index, a matching + problem like + + [match ... with [(fun x => ?p)] => [forall x => p]] + + will work even if [x] is also the name of an existing goal + variable. + + Note: we do not keep types in the signature. Besides simplicity, + the main reason is that it would force to close the signature over + binders that occur only in the types of effective binders but not + in the term itself (e.g. for a term [f x] with [f:A -> True] and + [x:A]). + + On the opposite side, by not keeping the types, we loose + opportunity to propagate type informations which otherwise would + not be inferable, as e.g. when matching [forall x, x = 0] with + pattern [forall x, ?h = 0] and using the solution "x|-h:=x" in + expression [forall x, h = x] where nothing tells how the type of x + could be inferred. We also loose the ability of typing ltac + variables before calling the right-hand-side of ltac matching clauses. *) + +type constr_under_binders = Id.t list * EConstr.constr + +(** Types of substitutions with or w/o bound variables *) + +type patvar_map = EConstr.constr Id.Map.t +type extended_patvar_map = constr_under_binders Id.Map.t + +(** A globalised term together with a closure representing the value + of its free variables. Intended for use when these variables are taken + from the Ltac environment. *) +type closure = { + idents:Id.t Id.Map.t; + typed: constr_under_binders Id.Map.t ; + untyped:closed_glob_constr Id.Map.t } +and closed_glob_constr = { + closure: closure; + term: glob_constr } + +(** Ltac variable maps *) +type var_map = constr_under_binders Id.Map.t +type uconstr_var_map = closed_glob_constr Id.Map.t +type unbound_ltac_var_map = Geninterp.Val.t Id.Map.t + +type ltac_var_map = { + ltac_constrs : var_map; + (** Ltac variables bound to constrs *) + ltac_uconstrs : uconstr_var_map; + (** Ltac variables bound to untyped constrs *) + ltac_idents: Id.t Id.Map.t; + (** Ltac variables bound to identifiers *) + ltac_genargs : unbound_ltac_var_map; + (** Ltac variables bound to other kinds of arguments *) +} diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index 3a1faf1c77..ffe0186af0 100644 --- a/pretyping/patternops.mli +++ b/pretyping/patternops.mli @@ -12,6 +12,7 @@ open Glob_term open Mod_subst open Misctypes open Pattern +open Ltac_pretype (** {5 Functions on patterns} *) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index ea1f2de539..30783bfad5 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -43,6 +43,7 @@ open Glob_term open Glob_ops open Evarconv open Misctypes +open Ltac_pretype module NamedDecl = Context.Named.Declaration diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 5822f5add5..6537d1ecf7 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -18,6 +18,7 @@ open Evd open EConstr open Glob_term open Evarutil +open Ltac_pretype (** An auxiliary function for searching for fixpoint guard indexes *) diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index d04dcb8e3b..9904b73540 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -1,3 +1,4 @@ +Ltac_pretype Locusops Pretype_errors Reductionops diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 91726e8c6d..a6b8262f7f 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -15,6 +15,7 @@ open Pattern open Globnames open Locus open Univ +open Ltac_pretype type reduction_tactic_error = InvalidAbstraction of env * evar_map * constr * (env * Type_errors.type_error) diff --git a/printing/printer.mli b/printing/printer.mli index 2c9a4d70e6..ba849bee6a 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -14,6 +14,7 @@ open Pattern open Evd open Proof_type open Glob_term +open Ltac_pretype (** These are the entry points for printing terms, context, tac, ... *) diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 48fa2202ee..d38ff7512f 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -14,6 +14,7 @@ open Evarutil open Evarsolve open Pp open Glob_term +open Ltac_pretype (******************************************) (* Instantiation of existential variables *) diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index 5d69715967..a0e3b718a2 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -8,6 +8,7 @@ open Evd open Glob_term +open Ltac_pretype (** Refinement of existential variables. *) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 7e6d83b10f..d4e9555f34 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -15,6 +15,7 @@ open Proof_type open Redexpr open Pattern open Locus +open Ltac_pretype (** Operations for handling terms under a local typing context. *) diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index d912decff4..8764ef085d 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -89,6 +89,12 @@ let mkBranches (eqonleft,mk,c1,c2,typ) = clear_last; intros] +let inj_flags = Some { + Equality.keep_proof_equalities = true; (* necessary *) + Equality.injection_in_context = true; (* does not matter here *) + Equality.injection_pattern_l2r_order = true; (* does not matter here *) + } + let discrHyp id = let c env sigma = (sigma, (mkVar id, NoBindings)) in let tac c = Equality.discr_tac false (Some (None, ElimOnConstr c)) in @@ -136,7 +142,7 @@ let eqCase tac = let injHyp id = let c env sigma = (sigma, (mkVar id, NoBindings)) in - let tac c = Equality.injClause None false (Some (None, ElimOnConstr c)) in + let tac c = Equality.injClause inj_flags None false (Some (None, ElimOnConstr c)) in Tacticals.New.tclDELAYEDWITHHOLES false c tac let diseqCase hyps eqonleft = diff --git a/tactics/equality.ml b/tactics/equality.ml index e33dd2e5ed..7c03a3ba6a 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -48,6 +48,12 @@ module NamedDecl = Context.Named.Declaration (* Options *) +type inj_flags = { + keep_proof_equalities : bool; + injection_in_context : bool; + injection_pattern_l2r_order : bool; + } + let discriminate_introduction = ref true let discr_do_intro () = !discriminate_introduction @@ -63,7 +69,9 @@ let _ = let injection_pattern_l2r_order = ref true -let use_injection_pattern_l2r_order () = !injection_pattern_l2r_order +let use_injection_pattern_l2r_order = function + | None -> !injection_pattern_l2r_order + | Some flags -> flags.injection_pattern_l2r_order let _ = declare_bool_option @@ -75,9 +83,9 @@ let _ = let injection_in_context = ref false -let use_injection_in_context () = - !injection_in_context - && Flags.version_strictly_greater Flags.V8_5 +let use_injection_in_context = function + | None -> !injection_in_context && Flags.version_strictly_greater Flags.V8_5 + | Some flags -> flags.injection_in_context let _ = declare_bool_option @@ -721,7 +729,14 @@ let _ = optread = (fun () -> !keep_proof_equalities_for_injection) ; optwrite = (fun b -> keep_proof_equalities_for_injection := b) } -let find_positions env sigma ~no_discr t1 t2 = +let keep_proof_equalities = function + | None -> !keep_proof_equalities_for_injection + | Some flags -> flags.keep_proof_equalities + +(* [keep_proofs] is relevant for types in Prop with elimination in Type *) +(* In particular, it is relevant for injection but not for discriminate *) + +let find_positions env sigma ~keep_proofs ~no_discr t1 t2 = let project env sorts posn t1 t2 = let ty1 = get_type_of env sigma t1 in let s = get_sort_family_of env sigma ty1 in @@ -768,20 +783,22 @@ let find_positions env sigma ~no_discr t1 t2 = project env sorts posn t1_0 t2_0 in try - let sorts = if !keep_proof_equalities_for_injection then [InSet;InType;InProp] - else [InSet;InType] - in + let sorts = if keep_proofs then [InSet;InType;InProp] else [InSet;InType] in Inr (findrec sorts [] t1 t2) with DiscrFound (path,c1,c2) -> Inl (path,c1,c2) +let use_keep_proofs = function + | None -> !keep_proof_equalities_for_injection + | Some b -> b + let discriminable env sigma t1 t2 = - match find_positions env sigma ~no_discr:false t1 t2 with + match find_positions env sigma ~keep_proofs:false ~no_discr:false t1 t2 with | Inl _ -> true | _ -> false -let injectable env sigma t1 t2 = - match find_positions env sigma ~no_discr:true t1 t2 with +let injectable env sigma ~keep_proofs t1 t2 = + match find_positions env sigma ~keep_proofs:(use_keep_proofs keep_proofs) ~no_discr:true t1 t2 with | Inl _ -> assert false | Inr [] | Inr [([],_,_)] -> false | Inr _ -> true @@ -1024,7 +1041,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let sigma = eq_clause.evd in Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in - match find_positions env sigma ~no_discr:false t1 t2 with + match find_positions env sigma ~keep_proofs:false ~no_discr:false t1 t2 with | Inr _ -> tclZEROMSG (str"Not a discriminable equality.") | Inl (cpath, (_,dirn), _) -> @@ -1069,9 +1086,8 @@ let discr with_evars = onEquality with_evars discrEq let discrClause with_evars = onClause (discrSimpleClause with_evars) let discrEverywhere with_evars = -(* - tclORELSE -*) + tclTHEN (Proofview.tclUNIT ()) + (* Delay the interpretation of side-effect *) (if discr_do_intro () then (tclTHEN (tclREPEAT introf) @@ -1079,9 +1095,7 @@ let discrEverywhere with_evars = (fun id -> tclCOMPLETE (discr with_evars (mkVar id,NoBindings))))) else (* <= 8.2 compat *) tryAllHypsAndConcl (discrSimpleClause with_evars)) -(* (fun gls -> - user_err ~hdr:"DiscrEverywhere" (str"No discriminable equalities.")) -*) + let discr_tac with_evars = function | None -> discrEverywhere with_evars | Some c -> onInductionArg (fun clear_flag -> discr with_evars) c @@ -1403,15 +1417,15 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = (if l2r then List.rev injectors else injectors))) (tac (List.length injectors))) -let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause = +let injEqThen keep_proofs tac l2r (eq,_,(t,t1,t2) as u) eq_clause = let sigma = eq_clause.evd in let env = eq_clause.env in - match find_positions env sigma ~no_discr:true t1 t2 with + match find_positions env sigma ~keep_proofs ~no_discr:true t1 t2 with | Inl _ -> assert false | Inr [] -> let suggestion = - if !keep_proof_equalities_for_injection then + if keep_proofs then "" else " You can try to use option Set Keep Proof Equalities." in tclZEROMSG (strbrk("No information can be deduced from this equality and the injectivity of constructors. This may be because the terms are convertible, or due to pattern matching restrictions in the sort Prop." ^ suggestion)) @@ -1430,13 +1444,13 @@ let get_previous_hyp_position id gl = in aux MoveLast (Proofview.Goal.hyps (Proofview.Goal.assume gl)) -let injEq ?(old=false) with_evars clear_flag ipats = +let injEq flags ?(old=false) with_evars clear_flag ipats = (* Decide which compatibility mode to use *) let ipats_style, l2r, dft_clear_flag, bounded_intro = match ipats with - | None when not old && use_injection_in_context () -> + | None when not old && use_injection_in_context flags -> Some [], true, true, true | None -> None, false, false, false - | _ -> let b = use_injection_pattern_l2r_order () in ipats, b, b, b in + | _ -> let b = use_injection_pattern_l2r_order flags in ipats, b, b, b in (* Built the post tactic depending on compatibility mode *) let post_tac c n = match ipats_style with @@ -1456,26 +1470,26 @@ let injEq ?(old=false) with_evars clear_flag ipats = tclTHEN clear_tac intro_tac end | None -> tclIDTAC in - injEqThen post_tac l2r + injEqThen (keep_proof_equalities flags) post_tac l2r -let inj ipats with_evars clear_flag = onEquality with_evars (injEq with_evars clear_flag ipats) +let inj flags ipats with_evars clear_flag = onEquality with_evars (injEq flags with_evars clear_flag ipats) -let injClause ipats with_evars = function - | None -> onNegatedEquality with_evars (injEq with_evars None ipats) - | Some c -> onInductionArg (inj ipats with_evars) c +let injClause flags ipats with_evars = function + | None -> onNegatedEquality with_evars (injEq flags with_evars None ipats) + | Some c -> onInductionArg (inj flags ipats with_evars) c -let simpleInjClause with_evars = function - | None -> onNegatedEquality with_evars (injEq ~old:true with_evars None None) - | Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (injEq ~old:true with_evars clear_flag None)) c +let simpleInjClause flags with_evars = function + | None -> onNegatedEquality with_evars (injEq flags ~old:true with_evars None None) + | Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (injEq flags ~old:true with_evars clear_flag None)) c -let injConcl = injClause None false None -let injHyp clear_flag id = injClause None false (Some (clear_flag,ElimOnIdent (Loc.tag id))) +let injConcl flags = injClause flags None false None +let injHyp flags clear_flag id = injClause flags None false (Some (clear_flag,ElimOnIdent (Loc.tag id))) -let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause = +let decompEqThen keep_proofs ntac (lbeq,_,(t,t1,t2) as u) clause = Proofview.Goal.enter begin fun gl -> let sigma = clause.evd in let env = Proofview.Goal.env gl in - match find_positions env sigma ~no_discr:false t1 t2 with + match find_positions env sigma ~keep_proofs ~no_discr:false t1 t2 with | Inl (cpath, (_,dirn), _) -> discr_positions env sigma u clause cpath dirn | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *) @@ -1485,18 +1499,18 @@ let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause = (ntac (clenv_value clause)) end -let dEqThen with_evars ntac = function - | None -> onNegatedEquality with_evars (decompEqThen (ntac None)) - | Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (decompEqThen (ntac clear_flag))) c +let dEqThen ~keep_proofs with_evars ntac = function + | None -> onNegatedEquality with_evars (decompEqThen (use_keep_proofs keep_proofs) (ntac None)) + | Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (decompEqThen (use_keep_proofs keep_proofs) (ntac clear_flag))) c -let dEq with_evars = - dEqThen with_evars (fun clear_flag c x -> +let dEq ~keep_proofs with_evars = + dEqThen ~keep_proofs with_evars (fun clear_flag c x -> (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c)) let intro_decomp_eq tac data (c, t) = Proofview.Goal.enter begin fun gl -> let cl = pf_apply make_clenv_binding gl (c, t) NoBindings in - decompEqThen (fun _ -> tac) data cl + decompEqThen !keep_proof_equalities_for_injection (fun _ -> tac) data cl end let _ = declare_intro_decomp_eq intro_decomp_eq diff --git a/tactics/equality.mli b/tactics/equality.mli index a4d1c0f9bd..65da2e7dc0 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -67,23 +67,31 @@ val replace_in_clause_maybe_by : constr -> constr -> clause -> unit Proofview.ta val replace : constr -> constr -> unit Proofview.tactic val replace_by : constr -> constr -> unit Proofview.tactic -> unit Proofview.tactic +type inj_flags = { + keep_proof_equalities : bool; (* One may want it or not *) + injection_in_context : bool; (* For regularity; one may want it from ML code but not interactively *) + injection_pattern_l2r_order : bool; (* Compatibility option: no reason not to want it *) + } + val discr : evars_flag -> constr with_bindings -> unit Proofview.tactic val discrConcl : unit Proofview.tactic val discrHyp : Id.t -> unit Proofview.tactic val discrEverywhere : evars_flag -> unit Proofview.tactic val discr_tac : evars_flag -> constr with_bindings destruction_arg option -> unit Proofview.tactic -val inj : intro_patterns option -> evars_flag -> + +(* Below, if flag is [None], it takes the value from the dynamic value of the option *) +val inj : inj_flags option -> intro_patterns option -> evars_flag -> clear_flag -> constr with_bindings -> unit Proofview.tactic -val injClause : intro_patterns option -> evars_flag -> +val injClause : inj_flags option -> intro_patterns option -> evars_flag -> constr with_bindings destruction_arg option -> unit Proofview.tactic -val injHyp : clear_flag -> Id.t -> unit Proofview.tactic -val injConcl : unit Proofview.tactic -val simpleInjClause : evars_flag -> +val injHyp : inj_flags option -> clear_flag -> Id.t -> unit Proofview.tactic +val injConcl : inj_flags option -> unit Proofview.tactic +val simpleInjClause : inj_flags option -> evars_flag -> constr with_bindings destruction_arg option -> unit Proofview.tactic -val dEq : evars_flag -> constr with_bindings destruction_arg option -> unit Proofview.tactic -val dEqThen : evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> constr with_bindings destruction_arg option -> unit Proofview.tactic +val dEq : keep_proofs:(bool option) -> evars_flag -> constr with_bindings destruction_arg option -> unit Proofview.tactic +val dEqThen : keep_proofs:(bool option) -> evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> constr with_bindings destruction_arg option -> unit Proofview.tactic val make_iterated_tuple : env -> evar_map -> constr -> (constr * types) -> evar_map * (constr * constr * constr) @@ -100,7 +108,7 @@ val rewriteInConcl : bool -> constr -> unit Proofview.tactic val discriminable : env -> evar_map -> constr -> constr -> bool (* Tells if tactic "injection" is applicable *) -val injectable : env -> evar_map -> constr -> constr -> bool +val injectable : env -> evar_map -> keep_proofs:(bool option) -> constr -> constr -> bool (* Subst *) diff --git a/tactics/inv.ml b/tactics/inv.ml index f391382bfc..c5aa74ba5c 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -371,7 +371,7 @@ let projectAndApply as_mode thin avoid id eqname names depids = (* If no immediate variable in the equation, try to decompose it *) (* and apply a trailer which again try to substitute *) (fun id -> - dEqThen false (deq_trailer id) + dEqThen ~keep_proofs:None false (deq_trailer id) (Some (None,ElimOnConstr (EConstr.mkVar id,NoBindings)))) id diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e8a78d72d6..6ab6432394 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -839,7 +839,7 @@ let e_change_in_hyp redfun (id,where) = (convert_hyp c) end -type change_arg = Pattern.patvar_map -> evar_map -> evar_map * EConstr.constr +type change_arg = Ltac_pretype.patvar_map -> evar_map -> evar_map * EConstr.constr let make_change_arg c pats sigma = (sigma, replace_vars (Id.Map.bindings pats) c) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index e07d514cd0..32923ea811 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -21,6 +21,7 @@ open Unification open Misctypes open Tactypes open Locus +open Ltac_pretype (** Main tactics defined in ML. This file is huge and should probably be split in more reasonable units at some point. Because of its size and age, the diff --git a/test-suite/bugs/closed/2881.v b/test-suite/bugs/closed/2881.v new file mode 100644 index 0000000000..b4f09305b4 --- /dev/null +++ b/test-suite/bugs/closed/2881.v @@ -0,0 +1,7 @@ +(* About scoping of pattern variables in strict/non-strict mode *) + +Ltac eta_red := change (fun a => ?f0 a) with f0. +Goal forall T1 T2 (f : T1 -> T2), (fun x => f x) = f. +intros. +eta_red. +Abort. diff --git a/test-suite/bugs/closed/5281.v b/test-suite/bugs/closed/5281.v new file mode 100644 index 0000000000..03bafdc9ae --- /dev/null +++ b/test-suite/bugs/closed/5281.v @@ -0,0 +1,6 @@ +Inductive A (T : Prop) := B (_ : T). +Scheme Equality for A. + +Goal forall (T:Prop), (forall x y : T, {x=y}+{x<>y}) -> forall x y : A T, {x=y}+{x<>y}. +decide equality. +Qed. diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index a19f9f9025..5996d30f25 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -171,6 +171,26 @@ Proof. auto with qarith. Qed. +Lemma Qeq_bool_comm x y: Qeq_bool x y = Qeq_bool y x. +Proof. + apply eq_true_iff_eq. rewrite !Qeq_bool_iff. now symmetry. +Qed. + +Lemma Qeq_bool_refl x: Qeq_bool x x = true. +Proof. + rewrite Qeq_bool_iff. now reflexivity. +Qed. + +Lemma Qeq_bool_sym x y: Qeq_bool x y = true -> Qeq_bool y x = true. +Proof. + rewrite !Qeq_bool_iff. now symmetry. +Qed. + +Lemma Qeq_bool_trans x y z: Qeq_bool x y = true -> Qeq_bool y z = true -> Qeq_bool x z = true. +Proof. + rewrite !Qeq_bool_iff; apply Qeq_trans. +Qed. + Hint Resolve Qnot_eq_sym : qarith. (** * Addition, multiplication and opposite *) diff --git a/theories/QArith/Qabs.v b/theories/QArith/Qabs.v index 116aa0d429..ec2ac7832d 100644 --- a/theories/QArith/Qabs.v +++ b/theories/QArith/Qabs.v @@ -100,6 +100,13 @@ rewrite Z.abs_mul. reflexivity. Qed. +Lemma Qabs_Qinv : forall q, Qabs (/ q) == / (Qabs q). +Proof. + intros [n d]; simpl. + unfold Qinv. + case_eq n; intros; simpl in *; apply Qeq_refl. +Qed. + Lemma Qabs_Qminus x y: Qabs (x - y) = Qabs (y - x). Proof. unfold Qminus, Qopp. simpl. diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 503508fc04..7af391758d 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -91,6 +91,15 @@ let destruct_on_using c id = let destruct_on_as c l = destruct false None c (Some (Loc.tag l)) None +let inj_flags = Some { + Equality.keep_proof_equalities = true; (* necessary *) + injection_in_context = true; (* does not matter here *) + Equality.injection_pattern_l2r_order = true; (* does not matter here *) + } + +let my_discr_tac = Equality.discr_tac false None +let my_inj_tac x = Equality.inj inj_flags None false None (EConstr.mkVar x,NoBindings) + (* reconstruct the inductive with the correct de Bruijn indexes *) let mkFullInd (ind,u) n = let mib = Global.lookup_mind (fst ind) in @@ -595,7 +604,7 @@ let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec = intro_using freshz; intros; Tacticals.New.tclTRY ( - Tacticals.New.tclORELSE reflexivity (Equality.discr_tac false None) + Tacticals.New.tclORELSE reflexivity my_discr_tac ); simpl_in_hyp (freshz,Locus.InHyp); (* @@ -739,9 +748,9 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = intro_using freshz; intros; Tacticals.New.tclTRY ( - Tacticals.New.tclORELSE reflexivity (Equality.discr_tac false None) + Tacticals.New.tclORELSE reflexivity my_discr_tac ); - Equality.inj None false None (EConstr.mkVar freshz,NoBindings); + my_inj_tac freshz; intros; simpl_in_concl; Auto.default_auto; Tacticals.New.tclREPEAT ( @@ -936,7 +945,7 @@ let compute_dec_tact ind lnamesparrec nparrec = NoBindings ) true; - Equality.discr_tac false None + my_discr_tac ] end ] |