diff --git a/library/init/default.lean b/library/init/default.lean index 7fcb420a1e..91c19edff5 100644 --- a/library/init/default.lean +++ b/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 diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index 3f4f1a9441..94adcc62e9 100644 --- a/library/init/meta/tactic.lean +++ b/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 diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 773c29219a..e00ba7ad93 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/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); diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 040c82ef81..f1e44adf16 100644 --- a/src/library/constants.cpp +++ b/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; } diff --git a/src/library/constants.h b/src/library/constants.h index cdb85970a6..453da34501 100644 --- a/src/library/constants.h +++ b/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(); diff --git a/src/library/constants.txt b/src/library/constants.txt index 8ef0d24782..d660a5a80c 100644 --- a/src/library/constants.txt +++ b/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 diff --git a/src/library/tactic/change_tactic.cpp b/src/library/tactic/change_tactic.cpp index 188c023242..d75c5b302d 100644 --- a/src/library/tactic/change_tactic.cpp +++ b/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 new_gs(new_M, tail(s.goals())); return mk_tactic_success(set_mctx_goals(s, mctx, new_gs)); } else { diff --git a/tests/lean/anc1.lean.expected.out b/tests/lean/anc1.lean.expected.out index 0fe8cd86dc..8a83dd85a2 100644 --- a/tests/lean/anc1.lean.expected.out +++ b/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), diff --git a/tests/lean/run/1260.lean b/tests/lean/run/1260.lean new file mode 100644 index 0000000000..b5d4be6508 --- /dev/null +++ b/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