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).

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?

`do 2 (unshelve eexists;[constructor|]);reflexivity.`

works

`constructor`

is a backtracking tactic, basically equivalent to `constructor 1 || constructor 2 || ...`

(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`

)

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.

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.

Okay, so as Karl told you `itauto`

would provide you full automation for this kind of goals, you can also use `SMTCoq`

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