## Stream: Beginner Questions

### Topic: ✔ Simplifier problem

#### 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, use`simp 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: Aug 13 2022 at 06:26 UTC