Julia Dijkstra has marked this topic as resolved.

instead of `clip_correct_step`

I would prove a `Lemma clip_correct_aux p V V' : (forall x, In x (find_vars p) -> V x = V' x) -> valid V p <-> valid V' p.`

(you will need lemmas like

```
Lemma find_vars_and p1 p2 x :
In x (find_vars p1) \/ In x (find_vars p2) ->
In x (find_vars <{ p1 /\ p2 }>).
```

for each connector)

(clip_correct_aux needs an equivalence `<->`

to deal with the `->`

connector)

then clip_correct is just

```
Lemma clip_correct (p: form) (V: valuation): valid V p -> valid (clip p V) p.
Proof.
apply clip_correct_aux.
intros x H.
unfold clip.
replace (existsb _ _) with true;[reflexivity|].
symmetry;apply existsb_exists.
exists x;split;[assumption|].
apply eqb_refl.
Qed.
```

However I think `clip_correct_aux`

is probably the lemma you want instead of `clip_correct`

:

I don't think `clip_in_combinations`

is true because of lack of function extensionality (combinations will contain functions that look like `fun x => if x =? a then true else if x =? b then false else ... else false`

but `clip`

looks like `fun x => if existsb (eqb sym) (find_vars _) then ... else false`

, without funext they're not equal).

so instead of `clip_in_combinations`

you should prove a lemma like `Lemma exhaustive_combinations p V : exists V', In V' (combinations (find_vars p)) /\ forall x, In x (find_vars p) -> V x = V' x.`

then you can do

```
Theorem solver_complete (p: form): satisfiable p -> solver p = true.
Proof.
intros [V H]. unfold solver.
unfold find_valuation.
destruct (exhaustive_combinations p V) as [V' [H' sameV]].
apply (clip_correct_aux _ _ _ sameV) in H.
clear V sameV.
destruct (find _ _) eqn:e.
- reflexivity.
- apply find_none with (x:=V') in e;[|assumption].
apply valid_iff in H;congruence.
Qed.
```

(I guess in the end there's no need for a direct proof)

I have managed to rewrite some of my definitions to use MSets, and was able to prove the correctness of clipping. Just have to prove the clip is actually in the combinations now :sweat_smile: !

Gaëtan Gilbert said:

so instead of

`clip_in_combinations`

you should prove a lemma like`Lemma exhaustive_combinations p V : exists V', In V' (combinations (find_vars p)) /\ forall x, In x (find_vars p) -> V x = V' x.`

I am not sure how you manage to proof this without functional extensionality. I get very stuck at least.

actually you can define the exact `V'`

which is found in `combinations`

so let's call it `clip`

(it's not the `clip`

you defined though):

```
Fixpoint clip (V:valuation) vars :=
match vars with
| [] => fun _ => false
| head :: tail =>
if V head then
fun sym => if eqb sym head then true else clip V tail sym
else clip V tail
end.
Lemma clip_notin V vars x : ~ In x vars -> clip V vars x = false.
Proof.
induction vars as [|y tl IH];simpl;intros Hin.
- reflexivity.
- destruct (V y).
+ replace (x =? y)%string with false.
2:{ symmetry;apply eqb_neq. intro e;apply Hin;auto. }
apply IH;auto.
+ apply IH;auto.
Qed.
Lemma clip_same V vars x : NoDup vars -> In x vars -> clip V vars x = V x.
Proof.
Print NoDup.
induction 1 as [|y tl Hnin Hdup IH];intros Hin.
- destruct Hin.
- simpl. destruct Hin.
+ subst.
destruct (V x);simpl.
* rewrite eqb_refl;reflexivity.
* apply clip_notin;assumption.
+ destruct (V y) eqn:e;simpl.
* destruct (eqb x _) eqn:e'.
-- apply eqb_eq in e';congruence.
-- auto.
* auto.
Qed.
Lemma clip_in_combinations V vars : NoDup vars ->
In (clip V vars) (combinations vars).
Proof.
intros Hdup;revert V;induction Hdup as [|x tl Hnin Hdup IH];intros V;simpl.
- left;reflexivity.
- apply in_or_app.
destruct (V x) eqn:e.
+ left;apply in_map_iff.
exists (clip V tl).
auto.
+ right. auto.
Qed.
```

Proving `forall p, NoDup (find_vars p)`

should be easy

Last updated: Oct 13 2024 at 01:02 UTC