Stream: Coq users

Topic: ✔ Coqhammer

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.

Karl Palmskog (Apr 16 2023 at 17:56):

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: Oct 04 2023 at 22:01 UTC