diff --git a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean index cd933ce793..6b7b9e3578 100644 --- a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean +++ b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean @@ -11,6 +11,7 @@ import Lean.Meta.AppBuilder import Lean.Meta.Eqns import Lean.Meta.Tactic.AuxLemma import Lean.DocString +import Lean.PrettyPrinter namespace Lean.Meta /-- @@ -164,7 +165,7 @@ instance : ToFormat SimpTheorem where def ppOrigin [Monad m] [MonadEnv m] [MonadError m] : Origin → m MessageData | .decl n post inv => do - let r ← mkConstWithLevelParams n; + let r := MessageData.ofConst (← mkConstWithLevelParams n) match post, inv with | true, true => return m!"← {r}" | true, false => return r diff --git a/tests/lean/1079.lean.expected.out b/tests/lean/1079.lean.expected.out index 375bb67af3..2b1c5e8436 100644 --- a/tests/lean/1079.lean.expected.out +++ b/tests/lean/1079.lean.expected.out @@ -1,8 +1,8 @@ 1079.lean:4:2-6:12: error: alternative 'isFalse' has not been provided [Meta.Tactic.simp.rewrite] h:1000, m ==> n -[Meta.Tactic.simp.rewrite] @eq_self:1000, n = n ==> True -[Meta.Tactic.simp.unify] @eq_self:1000, failed to unify +[Meta.Tactic.simp.rewrite] eq_self:1000, n = n ==> True +[Meta.Tactic.simp.unify] eq_self:1000, failed to unify ?a = ?a with Ordering.eq = Ordering.lt -[Meta.Tactic.simp.rewrite] @imp_self:10000, False → False ==> True +[Meta.Tactic.simp.rewrite] imp_self:10000, False → False ==> True diff --git a/tests/lean/973b.lean.expected.out b/tests/lean/973b.lean.expected.out index 8f6ba145e0..f68dd13270 100644 --- a/tests/lean/973b.lean.expected.out +++ b/tests/lean/973b.lean.expected.out @@ -1,5 +1,5 @@ 973b.lean:5:8-5:10: warning: declaration uses 'sorry' 973b.lean:9:8-9:11: warning: declaration uses 'sorry' -[Meta.Tactic.simp.discharge] @ex discharge ❌ +[Meta.Tactic.simp.discharge] ex discharge ❌ ?p x -[Meta.Tactic.simp.discharge] @ex discharge ❌ ?p (f x) +[Meta.Tactic.simp.discharge] ex discharge ❌ ?p (f x) diff --git a/tests/lean/discrTreeIota.lean.expected.out b/tests/lean/discrTreeIota.lean.expected.out index 6b265322d5..5675a15566 100644 --- a/tests/lean/discrTreeIota.lean.expected.out +++ b/tests/lean/discrTreeIota.lean.expected.out @@ -1,2 +1,2 @@ [Meta.Tactic.simp.rewrite] PUnit.default_eq_unit:1000, default ==> PUnit.unit -[Meta.Tactic.simp.rewrite] @eq_self:1000, PUnit.unit = x ==> True +[Meta.Tactic.simp.rewrite] eq_self:1000, PUnit.unit = x ==> True diff --git a/tests/lean/run/1234.lean b/tests/lean/run/1234.lean index ad84cca23f..e026411a36 100644 --- a/tests/lean/run/1234.lean +++ b/tests/lean/run/1234.lean @@ -10,12 +10,12 @@ set_option trace.Meta.Tactic.simp true warning: declaration uses 'sorry' --- info: [Meta.Tactic.simp.rewrite] h₁:1000, k ≤ v - 1 ==> True -[Meta.Tactic.simp.discharge] @succ_pred_eq_of_pos discharge ✅ +[Meta.Tactic.simp.discharge] succ_pred_eq_of_pos discharge ✅ 0 < v [Meta.Tactic.simp.rewrite] h₂:1000, 0 < v ==> True -[Meta.Tactic.simp.rewrite] @succ_pred_eq_of_pos:1000, v - 1 + 1 ==> v -[Meta.Tactic.simp.rewrite] @ite_true:1000, if True then ⟨v, ⋯⟩ else ⟨v - 1, ⋯⟩ ==> ⟨v, ⋯⟩ -[Meta.Tactic.simp.rewrite] @eq_self:1000, ⟨v, ⋯⟩ = ⟨v, ⋯⟩ ==> True +[Meta.Tactic.simp.rewrite] succ_pred_eq_of_pos:1000, v - 1 + 1 ==> v +[Meta.Tactic.simp.rewrite] ite_true:1000, if True then ⟨v, ⋯⟩ else ⟨v - 1, ⋯⟩ ==> ⟨v, ⋯⟩ +[Meta.Tactic.simp.rewrite] eq_self:1000, ⟨v, ⋯⟩ = ⟨v, ⋯⟩ ==> True -/ #guard_msgs in example (h₁: k ≤ v - 1) (h₂: 0 < v): @@ -35,12 +35,12 @@ example (h₁: k ≤ v - 1) (h₂: 0 < v): warning: declaration uses 'sorry' --- info: [Meta.Tactic.simp.rewrite] h₁:1000, k ≤ v - 1 ==> True -[Meta.Tactic.simp.discharge] @succ_pred_eq_of_pos discharge ✅ +[Meta.Tactic.simp.discharge] succ_pred_eq_of_pos discharge ✅ 0 < v [Meta.Tactic.simp.rewrite] h₂:1000, 0 < v ==> True -[Meta.Tactic.simp.rewrite] @succ_pred_eq_of_pos:1000, v - 1 + 1 ==> v -[Meta.Tactic.simp.rewrite] @ite_true:1000, if True then ⟨v, ⋯⟩ else ⟨v - 1, ⋯⟩ ==> ⟨v, ⋯⟩ -[Meta.Tactic.simp.rewrite] @eq_self:1000, ⟨v, ⋯⟩ = ⟨v, ⋯⟩ ==> True +[Meta.Tactic.simp.rewrite] succ_pred_eq_of_pos:1000, v - 1 + 1 ==> v +[Meta.Tactic.simp.rewrite] ite_true:1000, if True then ⟨v, ⋯⟩ else ⟨v - 1, ⋯⟩ ==> ⟨v, ⋯⟩ +[Meta.Tactic.simp.rewrite] eq_self:1000, ⟨v, ⋯⟩ = ⟨v, ⋯⟩ ==> True -/ #guard_msgs in example (h₁: k ≤ v - 1) (h₂: 0 < v): @@ -58,12 +58,12 @@ example (h₁: k ≤ v - 1) (h₂: 0 < v): warning: declaration uses 'sorry' --- info: [Meta.Tactic.simp.rewrite] h₁:1000, k ≤ v - 1 ==> True -[Meta.Tactic.simp.discharge] @succ_pred_eq_of_pos discharge ✅ +[Meta.Tactic.simp.discharge] succ_pred_eq_of_pos discharge ✅ 0 < v [Meta.Tactic.simp.rewrite] h₂:1000, 0 < v ==> True -[Meta.Tactic.simp.rewrite] @succ_pred_eq_of_pos:1000, v - 1 + 1 ==> v -[Meta.Tactic.simp.rewrite] @ite_true:1000, if True then ⟨v, ⋯⟩ else ⟨v - 1, ⋯⟩ ==> ⟨v, ⋯⟩ -[Meta.Tactic.simp.rewrite] @eq_self:1000, ⟨v, ⋯⟩ = ⟨v, ⋯⟩ ==> True +[Meta.Tactic.simp.rewrite] succ_pred_eq_of_pos:1000, v - 1 + 1 ==> v +[Meta.Tactic.simp.rewrite] ite_true:1000, if True then ⟨v, ⋯⟩ else ⟨v - 1, ⋯⟩ ==> ⟨v, ⋯⟩ +[Meta.Tactic.simp.rewrite] eq_self:1000, ⟨v, ⋯⟩ = ⟨v, ⋯⟩ ==> True -/ #guard_msgs in example (h₁: k ≤ v - 1) (h₂: 0 < v): diff --git a/tests/lean/run/1380.lean b/tests/lean/run/1380.lean index 828c344526..23fea60c85 100644 --- a/tests/lean/run/1380.lean +++ b/tests/lean/run/1380.lean @@ -3,19 +3,19 @@ variable (n v₁ v₂) (hv₁: v₁ < n + 1) (hv₂: v₂ < n + 1) theorem foo (_: ¬ Fin.mk v₂ hv₂ = Fin.mk v₁ hv₁ ): True := trivial /-- -info: [Meta.Tactic.simp.unify] @eq_self:1000, failed to unify +info: [Meta.Tactic.simp.unify] eq_self:1000, failed to unify ?a = ?a with ⟨v₂, hv₂⟩ = ⟨v₁, hv₁⟩ -[Meta.Tactic.simp.rewrite] @Fin.mk.injEq:1000, ⟨v₂, hv₂⟩ = ⟨v₁, hv₁⟩ ==> v₂ = v₁ -[Meta.Tactic.simp.unify] @eq_self:1000, failed to unify +[Meta.Tactic.simp.rewrite] Fin.mk.injEq:1000, ⟨v₂, hv₂⟩ = ⟨v₁, hv₁⟩ ==> v₂ = v₁ +[Meta.Tactic.simp.unify] eq_self:1000, failed to unify ?a = ?a with v₂ = v₁ -[Meta.Tactic.simp.discharge] @Nat.ne_of_gt discharge ✅ +[Meta.Tactic.simp.discharge] Nat.ne_of_gt discharge ✅ v₁ < v₂ [Meta.Tactic.simp.rewrite] hv:1000, v₁ < v₂ ==> True -[Meta.Tactic.simp.rewrite] @Nat.ne_of_gt:1000, v₂ = v₁ ==> False +[Meta.Tactic.simp.rewrite] Nat.ne_of_gt:1000, v₂ = v₁ ==> False -/ #guard_msgs in set_option trace.Meta.Tactic.simp true in diff --git a/tests/lean/run/1815.lean b/tests/lean/run/1815.lean index 6987a45f17..5aa7df320f 100644 --- a/tests/lean/run/1815.lean +++ b/tests/lean/run/1815.lean @@ -7,10 +7,10 @@ theorem mul_comm (a b : α) : a * b = b * a := sorry set_option trace.Meta.Tactic.simp true /-- -info: [Meta.Tactic.simp.rewrite] @mul_comm:1000:perm, perm rejected Left a ==> default * a -[Meta.Tactic.simp.rewrite] @mul_comm:1000:perm, Right a ==> a * default -[Meta.Tactic.simp.rewrite] @mul_comm:1000:perm, perm rejected a * default ==> default * a -[Meta.Tactic.simp.rewrite] @eq_self:1000, Left a = a * default ==> True +info: [Meta.Tactic.simp.rewrite] mul_comm:1000:perm, perm rejected Left a ==> default * a +[Meta.Tactic.simp.rewrite] mul_comm:1000:perm, Right a ==> a * default +[Meta.Tactic.simp.rewrite] mul_comm:1000:perm, perm rejected a * default ==> default * a +[Meta.Tactic.simp.rewrite] eq_self:1000, Left a = a * default ==> True -/ #guard_msgs in example (a : α) : Left a = Right a := by diff --git a/tests/lean/run/3257.lean b/tests/lean/run/3257.lean index e16c29bc37..e56a7dc79a 100644 --- a/tests/lean/run/3257.lean +++ b/tests/lean/run/3257.lean @@ -14,10 +14,10 @@ example : U := by simp [foo, T.mk] /-- -info: [Meta.Tactic.simp.discharge] @bar discharge ✅ +info: [Meta.Tactic.simp.discharge] bar discharge ✅ autoParam T _auto✝ - [Meta.Tactic.simp.rewrite] { }:1000, T ==> True -[Meta.Tactic.simp.rewrite] @bar:1000, U ==> True + [Meta.Tactic.simp.rewrite] T.mk:1000, T ==> True +[Meta.Tactic.simp.rewrite] bar:1000, U ==> True -/ #guard_msgs in example : U := by diff --git a/tests/lean/run/790.lean b/tests/lean/run/790.lean index 37a390d634..c08c8c17a4 100644 --- a/tests/lean/run/790.lean +++ b/tests/lean/run/790.lean @@ -16,8 +16,8 @@ instance : Vec' Nat := ⟨⟩ set_option trace.Meta.Tactic.simp true /-- -info: [Meta.Tactic.simp.rewrite] @differential_of_linear:1000, differential f x dx ==> f dx -[Meta.Tactic.simp.rewrite] @eq_self:1000, f dx = f dx ==> True +info: [Meta.Tactic.simp.rewrite] differential_of_linear:1000, differential f x dx ==> f dx +[Meta.Tactic.simp.rewrite] eq_self:1000, f dx = f dx ==> True -/ #guard_msgs in example {Y : Type} [Vec Y] (f : Nat → Y) (x dx : Nat) diff --git a/tests/lean/simp_trace.lean.expected.out b/tests/lean/simp_trace.lean.expected.out index 7905221a93..714d70454c 100644 --- a/tests/lean/simp_trace.lean.expected.out +++ b/tests/lean/simp_trace.lean.expected.out @@ -1,23 +1,23 @@ Try this: simp only [f] [Meta.Tactic.simp.rewrite] unfold f, f (a :: b = []) ==> a :: b = [] -[Meta.Tactic.simp.rewrite] @eq_self:1000, False = False ==> True +[Meta.Tactic.simp.rewrite] eq_self:1000, False = False ==> True Try this: simp only [length, gt_iff_lt] [Meta.Tactic.simp.rewrite] unfold length, length (a :: b :: as) ==> length (b :: as) + 1 [Meta.Tactic.simp.rewrite] unfold length, length (b :: as) ==> length as + 1 -[Meta.Tactic.simp.rewrite] @gt_iff_lt:1000, length as + 1 + 1 > length as ==> length as < length as + 1 + 1 +[Meta.Tactic.simp.rewrite] gt_iff_lt:1000, length as + 1 + 1 > length as ==> length as < length as + 1 + 1 Try this: simp only [fact, gt_iff_lt, Nat.zero_lt_succ, Nat.mul_pos_iff_of_pos_left] [Meta.Tactic.simp.rewrite] unfold fact, fact (x + 1) ==> (x + 1) * fact x -[Meta.Tactic.simp.rewrite] @gt_iff_lt:1000, (x + 1) * fact x > 0 ==> 0 < (x + 1) * fact x +[Meta.Tactic.simp.rewrite] gt_iff_lt:1000, (x + 1) * fact x > 0 ==> 0 < (x + 1) * fact x [Meta.Tactic.simp.rewrite] Nat.zero_lt_succ:1000, 0 < x + 1 ==> True -[Meta.Tactic.simp.rewrite] @Nat.mul_pos_iff_of_pos_left:1000, 0 < (x + 1) * fact x ==> 0 < fact x +[Meta.Tactic.simp.rewrite] Nat.mul_pos_iff_of_pos_left:1000, 0 < (x + 1) * fact x ==> 0 < fact x Try this: simp only [head] [Meta.Tactic.simp.rewrite] unfold head, head (a :: as) ==> match a :: as with | [] => default | a :: tail => a -[Meta.Tactic.simp.rewrite] @eq_self:1000, a = a ==> True +[Meta.Tactic.simp.rewrite] eq_self:1000, a = a ==> True Try this: simp only [foo] [Meta.Tactic.simp.rewrite] unfold foo, foo ==> 10 -[Meta.Tactic.simp.rewrite] @eq_self:1000, 10 + x = 10 + x ==> True +[Meta.Tactic.simp.rewrite] eq_self:1000, 10 + x = 10 + x ==> True Try this: simp only [g, pure] [Meta.Tactic.simp.rewrite] unfold g, g x ==> (let x := x; pure x).run @@ -37,33 +37,33 @@ Try this: simp (config := { unfoldPartialApp := true }) only [f1, modify, modify [Meta.Tactic.simp.rewrite] unfold getThe, getThe Nat s ==> MonadStateOf.get s [Meta.Tactic.simp.rewrite] unfold StateT.get, StateT.get s ==> pure (s, s) [Meta.Tactic.simp.rewrite] unfold StateT.set, StateT.set (g s) s ==> pure (PUnit.unit, g s) -[Meta.Tactic.simp.rewrite] @eq_self:1000, (fun s => (PUnit.unit, g s)) = fun s => (PUnit.unit, g s) ==> True +[Meta.Tactic.simp.rewrite] eq_self:1000, (fun s => (PUnit.unit, g s)) = fun s => (PUnit.unit, g s) ==> True Try this: simp only [bla, h] [Meta.Tactic.simp.rewrite] unfold bla, bla x ==> match h x with | Sum.inl (y, z) => y + z | Sum.inr val => 0 [Meta.Tactic.simp.rewrite] unfold h, h x ==> Sum.inl (x, x) -[Meta.Tactic.simp.rewrite] @eq_self:1000, x + x = x + x ==> True +[Meta.Tactic.simp.rewrite] eq_self:1000, x + x = x + x ==> True Try this: simp only [h, Nat.sub_add_cancel] [Meta.Tactic.simp.rewrite] h:1000, 1 ≤ x ==> True -[Meta.Tactic.simp.rewrite] @Nat.sub_add_cancel:1000, x - 1 + 1 ==> x -[Meta.Tactic.simp.rewrite] @eq_self:1000, x + 2 = x + 2 ==> True +[Meta.Tactic.simp.rewrite] Nat.sub_add_cancel:1000, x - 1 + 1 ==> x +[Meta.Tactic.simp.rewrite] eq_self:1000, x + 2 = x + 2 ==> True Try this: simp (config := { contextual := true }) only [Nat.sub_add_cancel, dite_eq_ite] [Meta.Tactic.simp.rewrite] h:1000, 1 ≤ x ==> True -[Meta.Tactic.simp.rewrite] @Nat.sub_add_cancel:1000, x - 1 + 1 ==> x -[Meta.Tactic.simp.rewrite] @dite_eq_ite:1000, if h : 1 ≤ x then x else 0 ==> if 1 ≤ x then x else 0 -[Meta.Tactic.simp.rewrite] @dite_eq_ite:1000, if _h : 1 ≤ x then x else 0 ==> if 1 ≤ x then x else 0 -[Meta.Tactic.simp.rewrite] @eq_self:1000, (if 1 ≤ x then x else 0) = if 1 ≤ x then x else 0 ==> True +[Meta.Tactic.simp.rewrite] Nat.sub_add_cancel:1000, x - 1 + 1 ==> x +[Meta.Tactic.simp.rewrite] dite_eq_ite:1000, if h : 1 ≤ x then x else 0 ==> if 1 ≤ x then x else 0 +[Meta.Tactic.simp.rewrite] dite_eq_ite:1000, if _h : 1 ≤ x then x else 0 ==> if 1 ≤ x then x else 0 +[Meta.Tactic.simp.rewrite] eq_self:1000, (if 1 ≤ x then x else 0) = if 1 ≤ x then x else 0 ==> True Try this: simp only [and_self] [Meta.Tactic.simp.rewrite] and_self:1000, b ∧ b ==> b [Meta.Tactic.simp.rewrite] iff_self:1000, a ∧ b ↔ a ∧ b ==> True Try this: simp only [my_thm] -[Meta.Tactic.simp.rewrite] @my_thm:1000, b ∧ b ==> b -[Meta.Tactic.simp.rewrite] @eq_self:1000, (a ∧ b) = (a ∧ b) ==> True +[Meta.Tactic.simp.rewrite] my_thm:1000, b ∧ b ==> b +[Meta.Tactic.simp.rewrite] eq_self:1000, (a ∧ b) = (a ∧ b) ==> True Try this: simp (discharger := sorry) only [Nat.sub_add_cancel] simp_trace.lean:83:0-83:7: warning: declaration uses 'sorry' -[Meta.Tactic.simp.rewrite] @Nat.sub_add_cancel:1000, x - 1 + 1 ==> x -[Meta.Tactic.simp.rewrite] @eq_self:1000, x = x ==> True +[Meta.Tactic.simp.rewrite] Nat.sub_add_cancel:1000, x - 1 + 1 ==> x +[Meta.Tactic.simp.rewrite] eq_self:1000, x = x ==> True Try this: simp only [bla, h] at * [Meta.Tactic.simp.rewrite] unfold bla, bla x ==> match h x with | Sum.inl (y, z) => y + z @@ -86,7 +86,7 @@ h₂ : xs.length + ys.length = y | Sum.inl (y, z) => y + z | Sum.inr val => 0 [Meta.Tactic.simp.rewrite] unfold h, h x ==> Sum.inl (x, x) -[Meta.Tactic.simp.rewrite] @List.length_append:1000, (xs ++ ys).length ==> xs.length + ys.length +[Meta.Tactic.simp.rewrite] List.length_append:1000, (xs ++ ys).length ==> xs.length + ys.length Try this: simp only [bla, h, List.length_append] at * simp_trace.lean:103:101-104:53: error: unsolved goals x y : Nat @@ -99,7 +99,7 @@ h₂ : xs.length + ys.length = y | Sum.inl (y, z) => y + z | Sum.inr val => 0 [Meta.Tactic.simp.rewrite] unfold h, h x ==> Sum.inl (x, x) -[Meta.Tactic.simp.rewrite] @List.length_append:1000, (xs ++ ys).length ==> xs.length + ys.length +[Meta.Tactic.simp.rewrite] List.length_append:1000, (xs ++ ys).length ==> xs.length + ys.length Try this: simp only [bla, h] at * [Meta.Tactic.simp.rewrite] unfold bla, bla x ==> match h x with | Sum.inl (y, z) => y + z @@ -122,7 +122,7 @@ Try this: simp only [HasProp.toProp] Try this: simp only [← h] [Meta.Tactic.simp.rewrite] ← h:1000, Q ==> P Try this: simp only [← my_thm'] -[Meta.Tactic.simp.rewrite] ← @my_thm':1000, P ∧ P ==> P +[Meta.Tactic.simp.rewrite] ← my_thm':1000, P ∧ P ==> P [Meta.Tactic.simp.rewrite] iff_self:1000, P ↔ P ==> True Try this: simp only [h] [Meta.Tactic.simp.rewrite] h:1000, P ==> True