feat: ppOrigin to use MessageData.ofConst (#4362)
so that the pretty-printed origin is clickable, and avoid the unnecessary `@`. Particularly nice is this fix: ```diff /-- -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 -/ ```
This commit is contained in:
Joachim Breitner
GitHub
parent
42f12967a6
commit
e33c32fb00
10 changed files with 55 additions and 54 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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):
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue