Stream: Coq users

Topic: Showing Completeness


view this post on Zulip Julia Dijkstra (Jan 09 2024 at 12:19):

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?

view this post on Zulip Julia Dijkstra (Jan 09 2024 at 12:33):

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.

view this post on Zulip Julia Dijkstra (Jan 09 2024 at 12:36):

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 [].

view this post on Zulip Gaëtan Gilbert (Jan 09 2024 at 12:36):

how are satisfiable solver find_valuation defined?

view this post on Zulip Julia Dijkstra (Jan 09 2024 at 12:37):

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.

view this post on Zulip Gaëtan Gilbert (Jan 09 2024 at 12:43):

can you post the whole code?

view this post on Zulip Gaëtan Gilbert (Jan 09 2024 at 12:45):

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

view this post on Zulip Gaëtan Gilbert (Jan 09 2024 at 12:46):

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

view this post on Zulip Julia Dijkstra (Jan 09 2024 at 12:48):

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.

view this post on Zulip Julia Dijkstra (Jan 09 2024 at 12:56):

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