mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
e01cbf2b8f
This PR adds a `result? : Option TraceResult` field to `TraceData` and populates it in `withTraceNode` and `withTraceNodeBefore`, so that metaprograms walking trace trees can determine success/failure structurally instead of string-matching on emoji. `TraceResult` has three cases: `.success` (checkEmoji), `.failure` (crossEmoji), and `.error` (bombEmoji, exception thrown). An `ExceptToTraceResult` typeclass converts `Except` results to `TraceResult` directly, with instances for `Bool` and `Option`. `TraceResult.toEmoji` converts back to emoji for display. This replaces the previous `ExceptToEmoji` typeclass — `TraceResult` is now the primary representation rather than being derived from emoji strings. `withTraceNodeBefore` (used by `isDefEq`) uses `ExceptToTraceResult.toTraceResult` directly, correctly handling `Bool` (`.ok false` = failure) and `Option` (`.ok none` = failure), with `Except.error` mapping to `.error`. For `withTraceNode`, `result?` defaults to `none`. Callers can pass `mkResult?` to provide structured results; when set, the corresponding emoji is auto-prepended to the message. Motivated by mathlib's `#defeq_abuse` diagnostic tactic (https://github.com/leanprover-community/mathlib4/pull/35750) which currently string-matches on emoji to determine trace node outcomes. See https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/backward.2EisDefEq.2ErespectTransparency 🤖 Prepared with Claude Code --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
128 lines
3.1 KiB
Lean4
128 lines
3.1 KiB
Lean4
axiom testSorry : α
|
||
|
||
theorem le_of_not_lt {a b : Nat} (_: ¬ a < b): b ≤ a := testSorry
|
||
theorem lt_of_succ_lt (_: a + 1 < b): a < b := testSorry
|
||
theorem succ_pred_eq_of_pos (_: 0 < v): v - 1 + 1 = v := testSorry
|
||
|
||
set_option trace.Meta.Tactic.simp true
|
||
set_option linter.unusedSimpArgs false
|
||
--set_option trace.Debug.Meta.Tactic.simp true
|
||
|
||
set_option Elab.async false -- for stable message ordering in #guard_msgs
|
||
|
||
/--
|
||
warning: declaration uses `sorry`
|
||
---
|
||
trace: [Meta.Tactic.simp.rewrite] h₁:1000:
|
||
k ≤ v - 1
|
||
==>
|
||
True
|
||
[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
|
||
-/
|
||
#guard_msgs in
|
||
example (h₁: k ≤ v - 1) (h₂: 0 < v):
|
||
(if k ≤ v - 1 then Fin.mk (v-1+1) sorry else Fin.mk (v-1) sorry) = Fin.mk v sorry (n:=n) := by
|
||
simp only [
|
||
h₁, h₂,
|
||
ite_true,
|
||
succ_pred_eq_of_pos
|
||
----------------
|
||
, le_of_not_lt
|
||
, lt_of_succ_lt
|
||
]
|
||
|
||
-- it works
|
||
|
||
/--
|
||
warning: declaration uses `sorry`
|
||
---
|
||
trace: [Meta.Tactic.simp.rewrite] h₁:1000:
|
||
k ≤ v - 1
|
||
==>
|
||
True
|
||
[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
|
||
-/
|
||
#guard_msgs in
|
||
example (h₁: k ≤ v - 1) (h₂: 0 < v):
|
||
(if k ≤ v - 1 then Fin.mk (v-1+1) sorry else Fin.mk (v-1) sorry) = Fin.mk v sorry (n:=n) := by
|
||
simp (config := { memoize := false}) only [
|
||
h₁, h₂,
|
||
ite_true,
|
||
succ_pred_eq_of_pos
|
||
----------------
|
||
, le_of_not_lt
|
||
, lt_of_succ_lt
|
||
]
|
||
|
||
/--
|
||
warning: declaration uses `sorry`
|
||
---
|
||
trace: [Meta.Tactic.simp.rewrite] h₁:1000:
|
||
k ≤ v - 1
|
||
==>
|
||
True
|
||
[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
|
||
-/
|
||
#guard_msgs in
|
||
example (h₁: k ≤ v - 1) (h₂: 0 < v):
|
||
(if k ≤ v - 1 then Fin.mk (v-1+1) sorry else Fin.mk (v-1) sorry) = Fin.mk v sorry (n:=n) := by
|
||
simp only [
|
||
h₁, h₂,
|
||
ite_true,
|
||
succ_pred_eq_of_pos
|
||
----------------
|
||
--, le_of_not_lt
|
||
--, lt_of_succ_lt
|
||
]
|