## Stream: Coq users

### Topic: Exists in proof

#### Julin Shaji (Dec 08 2023 at 07:07):

Hi.

I was trying to prove this SAT-solver style formula in coq.

``````Goal
exists a b:bool,
andb a b = true.
Proof.
``````

How would we go about this?

I guess we should somehow do ~exists false~ and then backtrack and try
with ~exists true~.

But how can something similar be achieved?

(I might have asked something similar here before, but I couldn't
find it now).

#### Louise Dubois de Prisque (Dec 08 2023 at 07:45):

Hi Julin, when you write Coq proofs manually, it's rather rare to use backtracking. Usually, you provide directly the correct proof term. Here, you'll do:

``````Goal
exists a b:bool,
andb a b = true.
Proof.
exists true.
exists true.
reflexivity.
Qed.
``````

But maybe your question was more about how to automate the proof of an arbitrary SAT-solver style formula?

#### Gaëtan Gilbert (Dec 08 2023 at 09:32):

`do 2 (unshelve eexists;[constructor|]);reflexivity.` works
`constructor` is a backtracking tactic, basically equivalent to `constructor 1 || constructor 2 || ...`

#### Gaëtan Gilbert (Dec 08 2023 at 09:34):

(although in this case the backtracking isn't used because `true` is the first constructor of `bool`, but it also works for `exists a b, andb a b = false`)

#### Karl Palmskog (Dec 08 2023 at 09:38):

Itauto recently got full support for boolean reasoning (`btauto` replacement). That's probably the closest one can get in Coq to solve this kind of goal as a SAT solver does.

#### Julin Shaji (Dec 08 2023 at 17:24):

Louise Dubois de Prisque said:

But maybe your question was more about how to automate the proof of an arbitrary SAT-solver style formula?

Yeah, I was trying to see if Coq can be used for what SAT solvers do. Even if we have to show the way manually if needed.

#### Louise Dubois de Prisque (Dec 10 2023 at 09:34):

Okay, so as Karl told you `itauto` would provide you full automation for this kind of goals, you can also use `SMTCoq`

#### Julio Di Egidio (Dec 10 2023 at 11:21):

I was trying to prove this SAT-solver style formula in coq.

Here is a little experiment, where `multimatch goal` provides the backtracking, though I don't think this would really be the way for a proper SAT solver:

``````From Coq Require Import Bool.

Open Scope bool.

Ltac solve_sat :=
repeat multimatch goal with
| [|- exists _ : bool, _] => exists true
| [|- exists _ : bool, _] => exists false
end; reflexivity.

Lemma ex_01 : exists x y z : bool, x && y || negb z = true.
Proof. solve_sat. Qed.

Lemma ex_02 : exists x y : bool, x && negb y = true.
Proof. solve_sat. Qed.

Lemma ex_03 : exists x y : bool, x || negb y = true.
Proof. solve_sat. Qed.

Lemma ex_04 : exists x : bool, negb x = true.
Proof. solve_sat. Qed.

Lemma ex_05 : exists x : bool, x && negb x = true.
Proof. Fail solve_sat. Abort.

Print ex_04.
(*
ex_04 =
ex_intro (fun x : bool => negb x = true) false eq_refl
: exists x : bool, negb x = true
*)
``````

Last updated: Jun 22 2024 at 16:02 UTC