Stream: Coq users

Topic: ✔ Showing Completeness


view this post on Zulip Notification Bot (Jan 09 2024 at 13:25):

Julia Dijkstra has marked this topic as resolved.

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

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)

view this post on Zulip Julia Dijkstra (Jan 09 2024 at 15:41):

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: !

view this post on Zulip Julia Dijkstra (Jan 09 2024 at 21:08):

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.

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

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: Jun 23 2024 at 04:03 UTC