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?

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

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`

?

Ok, I tried ` sauto unfold: fst, snd.`

This was unsuccessful.

how about adding `cases: prod`

?

I tried

```
Goal exists k : nat * nat, fst k = 0 /\ snd k = 3.
Proof.
sauto cases: prod unfold: fst, snd.
```

and this was unsuccessful

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

Patrick Nicodemus has marked this topic as resolved.

Last updated: Oct 04 2023 at 22:01 UTC