Patrick Nicodemus (Apr 16 2023 at 15:56): Patrick Nicodemus (Apr 16 2023 at 15:56):I tried to prove this with Coqhammer:
Theorem abc2 : exists k : nat * nat, fst k = 0 /\ snd k = 3
and it failed. I am wondering what the problem is here, is it with the use of product types?
Notification Bot (Apr 16 2023 at 17:28):This topic was moved here from #Miscellaneous > Coqhammer by Karl Palmskog.
Karl Palmskog (Apr 16 2023 at 17:29):moving since this is about using Coq, albeit with a plugin.
Did you try it directly with sauto and telling it to unfold fst/snd?
Patrick Nicodemus (Apr 16 2023 at 17:33):Ok, I tried sauto unfold: fst, snd. This was unsuccessful.
Karl Palmskog (Apr 16 2023 at 17:39):how about adding cases: prod?
Patrick Nicodemus (Apr 16 2023 at 17:46):I tried
Goal exists k : nat * nat, fst k = 0 /\ snd k = 3.
Proof.
sauto cases: prod unfold: fst, snd.
and this was unsuccessful
Karl Palmskog (Apr 16 2023 at 17:54):as I suspected, this was needed:
sauto use: surjective_pairing, pair_equal_spec.
I think the right frame of mind for sauto is that one needs to reference the minimal possible theory on top of FOL that can solve the problem
Notification Bot (Apr 16 2023 at 18:04):Patrick Nicodemus has marked this topic as resolved.
Last updated: Apr 20 2024 at 04:02 UTC