diff options
| -rw-r--r-- | CHANGES | 6 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 7 | ||||
| -rw-r--r-- | tactics/tactics.ml | 5 | ||||
| -rw-r--r-- | test-suite/success/intros.v | 24 |
4 files changed, 41 insertions, 1 deletions
@@ -19,6 +19,12 @@ Vernacular Commands - Removed deprecated commands Arguments Scope and Implicit Arguments (not the option). Use the Arguments command instead. +Tactics + +- Introduction tactics "intro"/"intros" on a goal which is an + existential variable now force a refinement of the goal into a + dependent product rather than failing. + Tactic language - Support for fix/cofix added in Ltac "match" and "lazymatch". diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index a3d06ae04..6c1b1c08c 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -634,7 +634,12 @@ puts in the local context either :g:`Hn:T` (if :g:`T` is of type :g:`Set` or ``n`` is such that ``Hn`` or ``Xn`` is a fresh identifier. In both cases, the new subgoal is :g:`U`. -If the goal is neither a product nor starting with a let definition, +If the goal is an existential variable, ``intro`` forces the resolution of the +existential variable into a dependent product :math:`\forall`:g:`x:?X, ?Y`, puts +:g:`x:?X` in the local context and leaves :g:`?Y` as a new subgoal allowed to +depend on :g:`x`. + +If the goal is neither a product, nor starting with a let definition, nor an existential variable, the tactic ``intro`` applies the tactic ``hnf`` until the tactic ``intro`` can be applied or the goal is not head-reducible. diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 3a20c3fc4..59c035e83 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -979,6 +979,11 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = | LetIn (name,b,t,u) when not dep_flag || not (noccurn sigma 1 u) -> let name = find_name false (LocalDef (name,b,t)) name_flag gl in build_intro_tac name move_flag tac + | Evar ev when force_flag -> + let sigma, t = Evardefine.define_evar_as_product sigma ev in + Tacticals.New.tclTHEN + (Proofview.Unsafe.tclEVARS sigma) + (intro_then_gen name_flag move_flag force_flag dep_flag tac) | _ -> begin if not force_flag then Proofview.tclZERO (RefinerError (env, sigma, IntroNeedsProduct)) (* Note: red_in_concl includes betaiotazeta and this was like *) diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v index a329894aa..d37ad9f52 100644 --- a/test-suite/success/intros.v +++ b/test-suite/success/intros.v @@ -127,4 +127,28 @@ induction 1 as (n,H,IH). exact Logic.I. Qed. +(* Make "intro"/"intros" progress on existential variables *) +Module Evar. + +Goal exists (A:Prop), A. +eexists. +unshelve (intro x). +- exact nat. +- exact (x=x). +- auto. +Qed. + +Goal exists (A:Prop), A. +eexists. +unshelve (intros x). +- exact nat. +- exact (x=x). +- auto. +Qed. + +Definition d := ltac:(intro x; exact (x*x)). + +Definition d' : nat -> _ := ltac:(intros;exact 0). + +End Evar. |