Stream: Coq users

Topic: ✔ Coqhammer


view this post on Zulip 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?

view this post on Zulip Notification Bot (Apr 16 2023 at 17:28):

This topic was moved here from #Miscellaneous > Coqhammer by Karl Palmskog.

view this post on Zulip 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?

view this post on Zulip Patrick Nicodemus (Apr 16 2023 at 17:33):

Ok, I tried sauto unfold: fst, snd. This was unsuccessful.

view this post on Zulip Karl Palmskog (Apr 16 2023 at 17:39):

how about adding cases: prod?

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Apr 16 2023 at 17:54):

as I suspected, this was needed:

sauto use: surjective_pairing, pair_equal_spec.

view this post on Zulip 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

view this post on Zulip Notification Bot (Apr 16 2023 at 18:04):

Patrick Nicodemus has marked this topic as resolved.


Last updated: Jun 20 2024 at 11:02 UTC