The equivalence of iff and entailment

Stream: new members

[edmund]

semantics.lean
can anybody help me with proving this: v v_atoms (p_iff ϕ ψ) = v v_atoms (p_and (p_imp ϕ ψ) (p_imp ψ ϕ))

[Kim Morrison]

If you can prepare a #mwe, that works in the sandbox, you're much more likely to get helpful answers. (But you may still!)

[edmund]

I'm stuck! :smiling_face_with_tear:

[Johan Commelin]

Sure. And Kim is suggesting that following the instructions on #mwe is a good first step to get unstuck.

[Notification Bot]

This topic was moved here from #maths > The equivalence of iff and entailment by Yury G. Kudryashov.

[Yury G. Kudryashov]

@edmund I moved your topic to a more appropriate channel (judging by your account's registration date).

[Robin Arnez]

This works:

example : v v_atoms (p_iff ϕ ψ) = v v_atoms (p_and (p_imp ϕ ψ) (p_imp ψ ϕ)) := by
  simp [v]
  cases v v_atoms ϕ <;> cases v v_atoms ψ <;> simp