Email Gateway (Feb 18 2023 at 19:22): Email Gateway (Feb 18 2023 at 19:22):From: David Fuenmayor <davfuenmayor@gmail.com>
Metis shows some puzzling behaviour with equality (which blast/auto
doesn't).
In the example below, the goal is in the first two lines exactly the same,
yet metis succeeds in the first but fails in the second (in the third it
works again).
lemma "(λa b. b = a) = (λa b. a = b)" by metis (* works *)
lemma "(λa b. b = a) = (=)" by metis (* does not work. Why? *)
lemma "(=) = (λa b. b = a)" by metis (* works again. Why? *)
On an unrelated note: why cannot simp solve any of the above? nor meson,
smt, etc.?
Thanks for the help!
David
Last updated: Apr 20 2024 at 08:16 UTC