7ca47aad7d
This PR adds `at` location syntax to the `cbv` tactic, matching the interface of `simp at`. Previously `cbv` could only reduce the goal target; now it supports `cbv at h`, `cbv at h |-`, and `cbv at *`. `cbvGoal` is rewritten to use `Sym.preprocessMVar` followed by `cbvCore` within a single `SymM` context, sharing the term table across all hypotheses and the target. The old `cbvGoalCore` (which reduced one side of an equation goal at a time) is replaced by a general approach that reduces arbitrary goal types and hypothesis types, with special handling for `True` targets and `False` hypotheses. `cbvDecideGoal` is updated to use the extracted `cbvCore` as well. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
59 lines
1.4 KiB
Text
59 lines
1.4 KiB
Text
set_option cbv.warning false
|
|
|
|
-- Case 1: p is literally True/False
|
|
theorem test1 : decide True = true := by cbv
|
|
theorem test2 : decide False = false := by cbv
|
|
|
|
/--
|
|
info: theorem test1 : decide True = true :=
|
|
of_eq_true (Eq.trans (congrFun' (congrArg Eq (decide_true instDecidableTrue)) true) (eq_self true))
|
|
-/
|
|
#guard_msgs in
|
|
#print test1
|
|
|
|
/--
|
|
info: theorem test2 : decide False = false :=
|
|
of_eq_true (Eq.trans (congrFun' (congrArg Eq (decide_false instDecidableFalse)) false) (eq_self false))
|
|
-/
|
|
#guard_msgs in
|
|
#print test2
|
|
|
|
-- Case 2: p simplifies to True/False
|
|
theorem test3 : decide (1 < 2) = true := by cbv
|
|
theorem test4 : decide (3 < 2) = false := by cbv
|
|
|
|
/--
|
|
info: theorem test3 : decide (1 < 2) = true :=
|
|
of_eq_true
|
|
(Eq.trans
|
|
(congrFun'
|
|
(congrArg Eq (Lean.Sym.decide_prop_eq_true (1 < 2) (Lean.Sym.Nat.lt_eq_true 1 2 (eagerReduce (Eq.refl true)))))
|
|
true)
|
|
(eq_self true))
|
|
-/
|
|
#guard_msgs in
|
|
#print test3
|
|
|
|
/--
|
|
info: theorem test4 : decide (3 < 2) = false :=
|
|
of_eq_true
|
|
(Eq.trans
|
|
(congrFun'
|
|
(congrArg Eq (Lean.Sym.decide_prop_eq_false (3 < 2) (Lean.Sym.Nat.lt_eq_false 3 2 (eagerReduce (Eq.refl false)))))
|
|
false)
|
|
(eq_self false))
|
|
-/
|
|
#guard_msgs in
|
|
#print test4
|
|
|
|
/--
|
|
trace: x : Nat
|
|
⊢ decide (x = 4) = true
|
|
---
|
|
warning: declaration uses `sorry`
|
|
-/
|
|
#guard_msgs in
|
|
theorem test5 : decide (x = (2 + 2)) = true := by
|
|
cbv
|
|
trace_state
|
|
sorry
|