I am in a situation where I need to show that my SAT solver finds a solution when it exists. This should follow from the fact that this (very bad) solver simply searches through all possible assignments. However, it seems that I constantly get stuck when proving lemmas that should be possible. My proof depending on these lemmas goes as follows:

```
Theorem solver_complete (p: form): satisfiable p -> solver p = true.
Proof.
intros [V H]. unfold solver.
destruct (find_valuation p) eqn:e.
- reflexivity.
- apply find_none with (x:=clip p V) in e.
* rewrite <- e. apply valid_iff. apply clip_correct. apply H.
* apply clip_in_combinations.
Qed.
```

Where

```
(* Proved *)
Lemma find_none {X: Type} (f: X -> bool) (x: X) (l: list X):
find f l = None ->
In x l ->
f x = false.
Definition clip (p: form) (V: valuation) (sym: string): bool :=
if existsb (eqb sym) (find_vars p) then V sym
else false.
(* Get stuck on conjunction, disjunction, etc. *)
Lemma clip_correct (p: form) (V: valuation): valid V p -> valid (clip p V) p.
(* Stuck also *)
Lemma clip_in_combinations (p: form) (V: valuation):
In (clip p V) (combinations (find_vars p)).
```

I have tried different strategies to no avail, such as destructing everything, induction on the formula and induction on the length of the found variables in the formula. Do you think any of these strategies will work, or is another approach required than the ones I've tried?

For example, when trying induction on the formula `p`

you can get stuck with the goal

```
valid (fun sym : string => if existsb (eqb sym) (find_vars <{ p1 /\ p2 }>) then V sym else false) p1
```

but this should follow from the hypothesis

```
valid (fun sym : string => if existsb (eqb sym) (find_vars <{ p1 }>) then V sym else false) p1
```

If anything we have just added extra symbols to the assignment that were not necessary.

It may be that my definition of `find_vars`

is not written well enough to be used for this proof.

```
Fixpoint find_vars_aux (p: form) (seen: list string): list string :=
match p with
| FVar sym => if existsb (eqb sym) seen then seen else sym :: seen
| <{ true }> | <{ false }> => seen
| <{ p /\ q }> | <{ p \/ q }> | <{ p -> q }> => find_vars_aux p (find_vars_aux q seen)
| <{ ~p }> => find_vars_aux p seen
end.
Definition find_vars (p: form): list string := find_vars_aux p [].
```

how are `satisfiable`

`solver`

`find_valuation`

defined?

Gaëtan Gilbert said:

how are

`satisfiable`

`solver`

`find_valuation`

defined?

```
Definition satisfiable (p: form): Prop := exists (V : valuation), valid V p.
Definition find_valuation (p: form): option valuation :=
find (fun V => valid' V p) (combinations (find_vars p)).
Definition solver (p: form): bool :=
match find_valuation p with
| Some _ => true
| None => false
end.
```

can you post the whole code?

I do think the `destruct (find_valuation p) eqn:e.`

is probably the wrong approach

you have a valuation from the `satisfiable`

hypothesis so there should be a direct proof that solver = true

instead of saying "if it's true then Qed otherwise we somehow get a contradiction"

Gaëtan Gilbert said:

can you post the whole code?

It's a bit long so I made a gist. https://gist.github.com/Vlamonster/00eabe9aa8df8c9133f629d0462bf700.

Gaëtan Gilbert said:

instead of saying "if it's true then Qed otherwise we somehow get a contradiction"

The idea was that we do not know yet whether the solution provided by the hypothesis is one that is found by the solver. If it is not, then we show that it can be made into one by clipping it.

Last updated: Jun 13 2024 at 21:01 UTC