fix(library/tactic/change_tactic): use id_locked in the change tactic to create checkpoint

closes #1260

library/init/default.lean

@@ -14,20 +14,3 @@ def debugger.attr : user_attribute :=
   descr := "breakpoint for debugger" }
 
 run_command attribute.register `debugger.attr
-
-open tactic
-/-
-  Define id_locked using meta-programming because we don't have
-  syntax for setting reducibility_hints.
-
-  See module init.meta.declaration.
--/
-run_command do
- l  ← return $ level.param `l,
- Ty ← return $ expr.sort l,
- type ← to_expr `(Π {α : %%Ty}, α → α),
- val  ← to_expr `(λ {α : %%Ty} (a : α), a),
- add_decl (declaration.defn `id_locked [`l] type val reducibility_hints.opaque tt)
-
-lemma {u} id_locked_eq {α : Type u} (a : α) : id_locked a = a :=
-rfl

library/init/meta/tactic.lean

@@ -753,3 +753,22 @@ meta def name.to_expr : name → tactic expr
 | (name.mk_numeral i n) := do is ← i^.to_expr, en ← name.to_expr n, to_expr `(name.mk_string %%is %%en)
 
 notation `command`:max := tactic unit
+
+open tactic
+/-
+  Define id_locked using meta-programming because we don't have
+  syntax for setting reducibility_hints.
+
+  See module init.meta.declaration.
+
+  Remark: id_locked is used in the builtin implementation of tactic.change
+-/
+run_command do
+ l  ← return $ level.param `l,
+ Ty ← return $ expr.sort l,
+ type ← to_expr `(Π {α : %%Ty}, α → α),
+ val  ← to_expr `(λ {α : %%Ty} (a : α), a),
+ add_decl (declaration.defn `id_locked [`l] type val reducibility_hints.opaque tt)
+
+lemma id_locked_eq {α : Type u} (a : α) : id_locked a = a :=
+rfl

src/frontends/lean/builtin_cmds.cpp

@@ -525,8 +525,8 @@ static environment run_command_cmd(parser & p) {
     options opts         = p.get_options();
     metavar_context mctx;
     expr tactic          = p.parse_expr();
-    expr try_constructor = mk_app(mk_constant(get_tactic_try_name()), mk_constant(get_tactic_constructor_name()));
-    tactic               = mk_app(mk_constant(get_pre_monad_and_then_name()), tactic, try_constructor);
+    expr try_triv        = mk_app(mk_constant(get_tactic_try_name()), mk_constant(get_tactic_triv_name()));
+    tactic               = mk_app(mk_constant(get_pre_monad_and_then_name()), tactic, try_triv);
     expr val             = mk_typed_expr(mk_true(), mk_by(tactic));
     bool check_unassigned = false;
     elaborate(env, opts, mctx, local_context(), val, check_unassigned);

src/library/constants.cpp

@@ -109,6 +109,7 @@ name const * g_heq_refl = nullptr;
 name const * g_heq_symm = nullptr;
 name const * g_heq_trans = nullptr;
 name const * g_heq_of_eq = nullptr;
+name const * g_id_locked = nullptr;
 name const * g_if_neg = nullptr;
 name const * g_if_pos = nullptr;
 name const * g_iff = nullptr;
@@ -384,6 +385,7 @@ name const * g_tactic_step = nullptr;
 name const * g_tactic_to_expr = nullptr;
 name const * g_tactic_skip = nullptr;
 name const * g_tactic_try = nullptr;
+name const * g_tactic_triv = nullptr;
 name const * g_tactic_interactive = nullptr;
 name const * g_tactic_interactive_exact = nullptr;
 name const * g_tactic_interactive_types_ident = nullptr;
@@ -534,6 +536,7 @@ void initialize_constants() {
     g_heq_symm = new name{"heq", "symm"};
     g_heq_trans = new name{"heq", "trans"};
     g_heq_of_eq = new name{"heq_of_eq"};
+    g_id_locked = new name{"id_locked"};
     g_if_neg = new name{"if_neg"};
     g_if_pos = new name{"if_pos"};
     g_iff = new name{"iff"};
@@ -809,6 +812,7 @@ void initialize_constants() {
     g_tactic_to_expr = new name{"tactic", "to_expr"};
     g_tactic_skip = new name{"tactic", "skip"};
     g_tactic_try = new name{"tactic", "try"};
+    g_tactic_triv = new name{"tactic", "triv"};
     g_tactic_interactive = new name{"tactic", "interactive"};
     g_tactic_interactive_exact = new name{"tactic", "interactive", "exact"};
     g_tactic_interactive_types_ident = new name{"tactic", "interactive", "types", "ident"};
@@ -960,6 +964,7 @@ void finalize_constants() {
     delete g_heq_symm;
     delete g_heq_trans;
     delete g_heq_of_eq;
+    delete g_id_locked;
     delete g_if_neg;
     delete g_if_pos;
     delete g_iff;
@@ -1235,6 +1240,7 @@ void finalize_constants() {
     delete g_tactic_to_expr;
     delete g_tactic_skip;
     delete g_tactic_try;
+    delete g_tactic_triv;
     delete g_tactic_interactive;
     delete g_tactic_interactive_exact;
     delete g_tactic_interactive_types_ident;
@@ -1385,6 +1391,7 @@ name const & get_heq_refl_name() { return *g_heq_refl; }
 name const & get_heq_symm_name() { return *g_heq_symm; }
 name const & get_heq_trans_name() { return *g_heq_trans; }
 name const & get_heq_of_eq_name() { return *g_heq_of_eq; }
+name const & get_id_locked_name() { return *g_id_locked; }
 name const & get_if_neg_name() { return *g_if_neg; }
 name const & get_if_pos_name() { return *g_if_pos; }
 name const & get_iff_name() { return *g_iff; }
@@ -1660,6 +1667,7 @@ name const & get_tactic_step_name() { return *g_tactic_step; }
 name const & get_tactic_to_expr_name() { return *g_tactic_to_expr; }
 name const & get_tactic_skip_name() { return *g_tactic_skip; }
 name const & get_tactic_try_name() { return *g_tactic_try; }
+name const & get_tactic_triv_name() { return *g_tactic_triv; }
 name const & get_tactic_interactive_name() { return *g_tactic_interactive; }
 name const & get_tactic_interactive_exact_name() { return *g_tactic_interactive_exact; }
 name const & get_tactic_interactive_types_ident_name() { return *g_tactic_interactive_types_ident; }

src/library/constants.h

@@ -111,6 +111,7 @@ name const & get_heq_refl_name();
 name const & get_heq_symm_name();
 name const & get_heq_trans_name();
 name const & get_heq_of_eq_name();
+name const & get_id_locked_name();
 name const & get_if_neg_name();
 name const & get_if_pos_name();
 name const & get_iff_name();
@@ -386,6 +387,7 @@ name const & get_tactic_step_name();
 name const & get_tactic_to_expr_name();
 name const & get_tactic_skip_name();
 name const & get_tactic_try_name();
+name const & get_tactic_triv_name();
 name const & get_tactic_interactive_name();
 name const & get_tactic_interactive_exact_name();
 name const & get_tactic_interactive_types_ident_name();

src/library/constants.txt

@@ -104,6 +104,7 @@ heq.refl
 heq.symm
 heq.trans
 heq_of_eq
+id_locked
 if_neg
 if_pos
 iff
@@ -379,6 +380,7 @@ tactic.step
 tactic.to_expr
 tactic.skip
 tactic.try
+tactic.triv
 tactic.interactive
 tactic.interactive.exact
 tactic.interactive.types.ident

src/library/tactic/change_tactic.cpp

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "library/util.h"
+#include "library/constants.h"
 #include "library/vm/vm_expr.h"
 #include "library/tactic/tactic_state.h"
 
@@ -16,7 +18,16 @@ vm_obj change(expr const & e, tactic_state const & s) {
         if (ctx.is_def_eq(e, g->get_type())) {
             auto mctx    = ctx.mctx();
             expr new_M   = mctx.mk_metavar_decl(g->get_context(), e);
-            mctx.assign(head(s.goals()), new_M);
+            /*
+               We use the proof term
+
+                  (@id_locked (g->get_type()) new_M)
+
+               to create a "checkpoint". See discussion at issue #1260
+            */
+            level lvl = get_level(ctx, g->get_type());
+            expr  pr  = mk_app(mk_constant(get_id_locked_name(), {lvl}), g->get_type(), new_M);
+            mctx.assign(head(s.goals()), pr);
             list<expr> new_gs(new_M, tail(s.goals()));
             return mk_tactic_success(set_mctx_goals(s, mctx, new_gs));
         } else {

tests/lean/anc1.lean.expected.out

@@ -2,7 +2,7 @@
 and.intro trivial trivial : true ∧ true
 sigma.mk 1 sorry : Σ (x : ℕ), x > 0
 show true, from true.intro : true
-Exists.intro 1 (λ (a : 1 = 0), nat.no_confusion a) : ∃ (x : ℕ), 1 ≠ 0
+Exists.intro 1 (id_locked (λ (a : 1 = 0), nat.no_confusion a)) : ∃ (x : ℕ), 1 ≠ 0
 λ (A B C : Prop) (Ha : A) (Hb : B) (Hc : C), show B ∧ A, from and.intro Hb Ha :
   ∀ (A B C : Prop), A → B → C → B ∧ A
 λ (A B C : Prop) (Ha : A) (Hb : B) (Hc : C),

tests/lean/run/1260.lean

@@ -0,0 +1,32 @@
+inductive dvec {X : Type} (Y : X → Type) : list X → Type
+| dnil {}  : dvec []
+| dcons : Π {x : X}, Y x → Π {xs : list X}, dvec xs → dvec (x::xs)
+
+namespace dvec
+
+notation `⟦` l:(foldr `, ` (h t, dvec.dcons h t) dvec.dnil `⟧`) := l
+
+def get {X : Type} [decidable_eq X] {Y : X → Type} (x₀ : X) [inhabited (Y x₀)]
+  : Π {xs : list X}, dvec Y xs → ℕ → Y x₀
+| []      _                _      := default (Y x₀)
+| (x::xs) (dvec.dcons y ys) 0     := if H : x = x₀ then eq.rec_on H y else default (Y x₀)
+| (x::xs) (dvec.dcons y ys) (n+1) := get ys n
+
+end dvec
+
+constant tensor : list ℕ → Type
+noncomputable instance inhabited_tensor (shape : list ℕ) : inhabited (tensor shape) := sorry
+constant f {shape : list ℕ} : tensor shape → tensor shape → tensor shape
+
+noncomputable def bar {shape : list ℕ} (μσ : dvec tensor [shape, shape]) : tensor shape :=
+  let μ := dvec.get shape μσ 0, σ := dvec.get shape μσ 1 in f μ σ
+
+lemma foo {shape : list ℕ} (μ σ : tensor shape) :
+      bar ⟦μ, σ⟧ = bar ⟦μ, σ⟧ :=
+suffices H_suffices : true, from
+begin
+dunfold bar, dsimp,
+dunfold dvec.get,
+reflexivity
+end,
+trivial