mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
54f188160c
This PR solves three distinct issues with the handling of `ite`/`dite`,`decide`. 1) We prevent the simprocs from picking up `noncomputable`, `Classical` instances, such as `Classical.propDecidable`, when simplifying the proposition in `ite`/`dite`/`decide`. 2) We fix a type mismatch occurring when the condition/proposition is unchanged but the `Decidable` instance is simplified. 3) If we rewrite the proposition from `c` to `c'` and the evaluation of the original instance `Decidable c` gets stuck we try fallback path of of obtaining `Decidable c'` instance and evaluating it. This matters when the instance is evaluated via `cbv_eval` lemmas. --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
36 lines
907 B
Lean4
36 lines
907 B
Lean4
set_option cbv.warning false
|
|
set_option trace.Meta.Tactic true
|
|
axiom P : Prop
|
|
axiom instDecidableP : Decidable P
|
|
axiom Q : Prop
|
|
|
|
axiom P_eval : P = Q
|
|
attribute [cbv_eval] P_eval
|
|
example : P = Q := by cbv
|
|
|
|
axiom hQ : Q
|
|
|
|
axiom instDecidableQ : Decidable Q
|
|
noncomputable instance : Decidable P := instDecidableP
|
|
noncomputable instance : Decidable Q := instDecidableQ
|
|
axiom dQ_eval : instDecidableQ = Decidable.isTrue hQ
|
|
attribute [cbv_eval] dQ_eval
|
|
|
|
example : (if P then true else false) = true := by cbv
|
|
|
|
example : (if P then true else false) = true := by conv => lhs; cbv
|
|
|
|
example : (if _ : P then true else false) = true := by cbv
|
|
|
|
example : P := by decide_cbv
|
|
|
|
example : decide P = true := by conv => lhs; cbv
|
|
|
|
example : Q := by decide_cbv
|
|
|
|
example : decide Q = true := by conv => lhs; cbv
|
|
|
|
example : (if Q then true else false) = true := by cbv
|
|
|
|
example : (if _ : Q then true else false) = true := by cbv
|