From ea8ecfd3907e5b1f5949fcd4254ef881e0981725 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 5 Jun 2017 15:06:44 -0700 Subject: [PATCH] fix(library/init/meta/interactive): use replace_target at simp_goal MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit replace_target uses id_locked. The id_locked solution is more robust because simp may build a proof using refl lemmas, but type_context may not be able to establish that the previous and new target are definitionally equal. @Armael This commit fixes the issue in the KreMLin proof you showed me. Now, the following tactic succeeds (as expected) ``` simp [lowstar_semantics.apply_ectx], ``` and the resulting goal is ``` ... |- exp.subbuf (exp.loc (b, n, list.nil field)) a_1 = exp.subbuf ↑?m_1 ?m_2 ``` --- library/init/data/nat/lemmas.lean | 2 +- library/init/meta/interactive.lean | 6 ++---- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/library/init/data/nat/lemmas.lean b/library/init/data/nat/lemmas.lean index a0879ff78a..c342598938 100644 --- a/library/init/data/nat/lemmas.lean +++ b/library/init/data/nat/lemmas.lean @@ -38,7 +38,7 @@ protected lemma add_comm : ∀ n m : ℕ, n + m = m + n protected lemma add_assoc : ∀ n m k : ℕ, (n + m) + k = n + (m + k) | n m 0 := rfl -| n m (succ k) := by simp [add_succ, add_assoc n m k] +| n m (succ k) := by rw [add_succ, add_succ, add_assoc] protected lemma add_left_comm : ∀ (n m k : ℕ), n + (m + k) = m + (n + k) := left_comm nat.add nat.add_comm nat.add_assoc diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index dba6d6cc39..105cb05ba1 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -677,10 +677,8 @@ open interactive interactive.types expr private meta def simp_goal (cfg : simp_config) : simp_lemmas → tactic unit | s := do - (new_target, Heq) ← target >>= simplify_core cfg s `eq, - tactic.assert `Htarget new_target, swap, - Ht ← get_local `Htarget, - mk_eq_mpr Heq Ht >>= tactic.exact + (new_target, pr) ← target >>= simplify_core cfg s `eq, + replace_target new_target pr private meta def simp_hyp (cfg : simp_config) (s : simp_lemmas) (h_name : name) : tactic unit := do h ← get_local h_name,