Robert Soeldner (May 05 2022 at 16:36): Robert Soeldner (May 05 2022 at 16:36):Why is the simplifier not able to discharge the following goal:
⟦(λxa. if xa ∈ V⇘K⇙ then ⇘x⇙⇩V (⇘r⇙⇩V xa) else undefined) = (λx. if x ∈ V⇘K⇙ then ⇘y⇙⇩V (⇘d⇙⇩V x) else undefined); v ∈ V⇘K⇙⟧ ⟹ ⇘x⇙⇩V (⇘r⇙⇩V v) = ⇘y⇙⇩V (⇘d⇙⇩V v)
It follows directly from the fact that v ∈ V⇘K⇙.
Thank you for a hint
Mathias Fleury (May 05 2022 at 17:00):Because of the lambdas. Maybe (simp add: fun_eq_iff) works. But in general forall is better than lambdas.
Maximilian Schaeffeler (May 05 2022 at 17:01):metis and meson solve the goal.
To solve it using simp, add both fun_eq_iff and if_split to the simpset.
Mathias Fleury (May 05 2022 at 17:03):Don't add if_split to the simpset, usesimp add: fun_eq_iff split: if_splits
Maximilian Schaeffeler (May 05 2022 at 17:10):Yes, that's much better :)
Notification Bot (May 05 2022 at 17:37):Robert Soeldner has marked this topic as resolved.
Last updated: Dec 21 2024 at 16:20 UTC