Stream: Beginner Questions

Topic: Simplifier problem


view this post on Zulip Robert Soeldner (May 05 2022 at 16:36):

Why is the simplifier not able to discharge the following goal:

(λxa. if xa  VK then x⇙⇩V (r⇙⇩V xa) else undefined) = (λx. if x  VK then y⇙⇩V (d⇙⇩V x) else undefined); v  VK⇙⟧  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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mathias Fleury (May 05 2022 at 17:03):

Don't add if_split to the simpset, usesimp add: fun_eq_iff split: if_splits

view this post on Zulip Maximilian Schaeffeler (May 05 2022 at 17:10):

Yes, that's much better :)


Last updated: Jul 15 2022 at 23:21 UTC