Stream: Coq users

Topic: Exists in proof


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

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

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

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

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

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

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

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