SAT Solver

Require Import Base.

SAT solver

Definition Var := nat.
Inductive Exp := top | bot | var (x: Var) | cond (s t u: Exp).
Definition Assn := Var -> bool.

Implicit Types (a b c: bool) (x y: Var) (s t u v: Exp)
         (alpha beta: Assn) (A B: list Var).

Fixpoint eva alpha s : bool :=
  match s with
  | top => true
  | bot => false
  | var x => alpha x
  | cond s t u => if eva alpha s then eva alpha t else eva alpha u
  end.

Notation sat s := (exists alpha, eva alpha s = true).

Fixpoint vars s : list nat :=
  match s with
  | var x => [x]
  | cond s t u => vars s ++ vars t ++ vars u
  | top => nil
  | bot => nil
  end.

Fixpoint subst s x t : Exp :=
  match s with
  | top => top
  | bot => bot
  | var y => if Dec (x =y) then t else var y
  | cond s u v => cond (subst s x t) (subst u x t) (subst v x t)
  end.

Definition update alpha x b : Assn :=
  fun y => if Dec (x =y) then b else alpha y.

Definition tau : Assn := fun x => true.

Fixpoint solve A s : option Assn :=
  match A with
  | nil => if eva tau s then Some tau else None
  | x::A' => match solve A' (subst s x bot), solve A' (subst s x top) with
            | Some alpha, _ => Some (update alpha x false)
            | _, Some alpha => Some (update alpha x true)
            | None, None => None
            end
  end.

Notation ground s := (vars s = nil).

Theorem coincidence alpha beta s :
  (forall x, x el vars s -> alpha x = beta x ) -> eva alpha s = eva beta s.
Proof.
  induction s as [ | |x |s IHs t IHt u IHu]; cbn; intros A.
  - reflexivity.
  - reflexivity.
  - apply A. auto.
  - rewrite IHs, IHt, IHu.
    + reflexivity.
    + intros x B. apply A. auto.
    + intros x B. apply A. auto.
    + intros x B. apply A. auto.
Qed.

Lemma shift alpha s x t :
  eva alpha (subst s x t) = eva (update alpha x (eva alpha t)) s.
Proof.
  induction s as [| |y|s IHs u IHu v IHv]; cbn.
  - reflexivity.
  - reflexivity.
  - unfold update. now decide (x=y).
  - now rewrite <-IHs, <-IHu, <-IHv.
Qed.

Lemma update_id alpha x b z :
  alpha x = b -> update alpha x b z = alpha z.
Proof.
  unfold update. decide (x=z) as [<-|H]; congruence.
Qed.

Theorem expansion x s alpha :
  eva alpha s = if alpha x
            then eva alpha (subst s x top)
            else eva alpha (subst s x bot).
Proof.
  rewrite !shift; cbn.
  destruct (alpha x) eqn:E;
    apply coincidence;
    intros z _; symmetry; apply update_id, E.
Qed.

Lemma subst_vars_ground s x A t :
  ground t -> vars s <<= x ::A -> vars (subst s x t) <<= A.
Proof.
  intros H1 H2.
  induction s as [| |y|s IHs u IHu v IHv]; cbn in *.
  - auto.
  - auto.
  - decide (x=y) as [<-|H3];cbn.
    + rewrite H1. auto.
    + assert (y el x::A) as H4 by auto. cbn in *; intuition.
  - apply incl_app_left in H2 as [H2 [H3 H4] % incl_app_left].
    auto.
Qed.

Lemma solve_correct s A :
  vars s <<= A ->
  match solve A s with
  | Some alpha => eva alpha s = true
  | None => ~ sat s
  end.
Proof.
  revert s. induction A as [|x A IH]; cbn; intros s H.
  - destruct (eva tau s) as [alpha|] eqn:E.
    + exact E.
    + intros [alpha H1].
      enough (eva tau s = eva alpha s) by congruence.
      apply coincidence. intros x [] % H.
  - destruct (solve A (subst s x bot)) as [alpha|] eqn:E.
    + specialize (IH (subst s x bot)).
      rewrite E, shift in IH. apply IH.
      apply subst_vars_ground; cbn; auto.
    + destruct (solve A (subst s x top)) as [alpha|] eqn:E'.
      * specialize (IH (subst s x top)).
        rewrite E', shift in IH. apply IH.
        apply subst_vars_ground; cbn; auto.
      * intros [alpha H1]. rewrite (expansion x) in H1.
        destruct (alpha x).
        -- specialize (IH (subst s x top)).
           rewrite E' in IH. apply IH.
           ++ apply subst_vars_ground; cbn; auto.
           ++ now exists alpha.
         -- specialize (IH (subst s x bot)).
           rewrite E in IH. apply IH.
           ++ apply subst_vars_ground; cbn; auto.
           ++ now exists alpha.
Qed.

Theorem sat_solver s :
  { alpha | eva alpha s = true } + { ~sat s }.
Proof.
  assert (vars s <<= vars s) as H by auto.
  apply solve_correct in H.
  destruct (solve _ _); eauto.
Qed.

Instance sat_dec s :
  dec (sat s).
Proof.
  unfold dec.
  destruct (sat_solver s) as [[alpha H]|H]; eauto.
Qed.

Equivalence

Example Ex1 a b c :
  ifb a b c = a && b || negb a && c.
Proof.
  now destruct a, b, c.
Qed.

Fact ground_sat_dec s :
  ground s -> sat s <-> eva tau s = true.
Proof.
  intros H. split.
  - intros [alpha <-]. apply coincidence.
    intros x. rewrite H. auto.
  - intros H1. now exists tau.
Qed.

Theorem sat_var_elim s x :
  sat s <-> sat (subst s x top) \/ sat (subst s x bot).
Proof.
  split.
  - intros [alpha H]. rewrite (expansion x) in H.
    destruct (alpha x) eqn:E; eauto.
  - intros [[alpha H]|[alpha H]].
    + exists (update alpha x true). now rewrite shift in H.
    + exists (update alpha x false). now rewrite shift in H.
Qed.

Notation "s == t" := (forall alpha, eva alpha s = eva alpha t) (at level 70).

Fact ground_equiv s :
  ground s -> s == top \/ s == bot.
Proof.
  intros H. destruct (eva tau s) eqn:E.
  - left. intros alpha. cbn. rewrite <-E.
    apply coincidence. intros x. rewrite H. auto.
  - right. intros alpha. cbn. rewrite <-E.
    apply coincidence. intros x. rewrite H. auto.
Qed.

Fact cond_expansion s x :
  s == cond (var x) (subst s x top) (subst s x bot).
Proof.
  apply expansion.
Qed.

Fact cond_reduction s t :
  cond s t t == t.
Proof.
  intros alpha. cbn. now destruct (eva alpha s).
Qed.

Fact cond_compatibility s s' t t' u u' :
  s == s' -> t == t' -> u == u' -> cond s t u == cond s' t' u'.
Proof.
  intros H1 H2 H3 alpha. cbn. rewrite H1, H2, H3. reflexivity.
Qed.

Notation neg s := (cond s bot top).

Fact neg_neg s :
  neg (neg s) == s.
Proof.
  intros alpha. cbn. now destruct (eva alpha s).
Qed.

Fact neg_cond s t u :
  neg (cond s t u) == cond s (neg t) (neg u).
Proof.
  intros alpha. cbn. now destruct (eva alpha s), (eva alpha t), (eva alpha u).
Qed.

Fact sat_compatibility s s' :
  s == s' -> sat s <-> sat s'.
Proof.
  intros H; split; intros [alpha H1]; exists alpha; specialize (H alpha); congruence.
Qed.

Fact eeq_sat s t :
  s == t <-> ~ sat (cond s (neg t) t).
Proof.
  split.
  - intros H [alpha H1]. cbn in H1. destruct (eva alpha s) eqn:E.
    + destruct (eva alpha t) eqn:E'; congruence.
    + specialize (H alpha). congruence.
  - intros H alpha. contra_dec H1. contradict H.
    exists alpha. cbn. destruct (eva alpha s), (eva alpha t); congruence.
Qed.

Instance eeq_dec s t :
  dec (s == t).
Proof.
  apply dec_transfer with (P:= ~ sat (cond s (neg t) t)).
  - symmetry. apply eeq_sat.
  - auto.
Qed.

Fact sat_eeq s :
  sat s <-> ~ s == bot.
Proof.
  split.
  - intros [alpha H] H1. specialize (H1 alpha).
    cbn in H1. congruence.
  - intros H. contra_dec H1. contradict H. intros alpha. cbn.
    rewrite DM_exists in H1. specialize (H1 alpha).
    destruct (eva alpha s); congruence.
Qed.

Separability

Notation sep s t := (exists alpha, eva alpha s <> eva alpha t).

Fact sep_sat s t :
  sep s t <-> sat (cond s (neg t) t).
Proof.
  split.
  - intros [alpha H]. exists alpha. cbn.
    destruct (eva _ _), (eva _ _); congruence.
  - intros [alpha H]. exists alpha. cbn in H.
    destruct (eva _ _), (eva _ _); congruence.
Qed.

Instance sep_dec s t :
  dec (sep s t).
Proof.
  apply dec_transfer with (P:= sat (cond s (neg t) t)).
  - symmetry. apply sep_sat.
  - auto.
Qed.

Fact dec_contra_not (P Q: Prop) :
  dec P -> (~ P -> Q ) -> ~ Q -> P.
Proof.
  unfold dec. tauto.
Qed.

Fact sep_eeq s t : (* difficult, requires several lemmas *)
  sep s t <-> ~ s == t.
Proof.
  split.
  - intros [alpha H] H1. apply H, H1.
  - apply dec_contra_not. now auto.
    rewrite DM_exists. intros H alpha. specialize (H alpha).
    apply dec_DN; auto.
Qed.

Fact eeq_sep s t :
  s == t <-> ~ sep s t.
Proof.
  split.
  - intros H [alpha H1]. apply H1, H.
  - rewrite DM_exists. intros H alpha.
    specialize (H alpha). apply dec_DN; auto.
Qed.

Validity

Notation val s := (forall alpha, eva alpha s = true).

Fact val_sat s :
  val s <-> ~ sat (neg s).
Proof.
  split.
  - intros H [alpha H1]. revert H1. cbn. rewrite H. congruence.
  - cbn. intros A alpha. contra_dec B.
    apply A. exists alpha. destruct (eva alpha s); congruence.
Qed.

Fact eeq_val s t :
  s == t <-> val (cond s t (neg t)).
Proof.
  split.
  - intros H alpha. specialize (H alpha). cbn.
    destruct (eva _ _), (eva _ _); congruence.
  - intros H alpha. specialize (H alpha). cbn in H.
    destruct (eva _ _), (eva _ _); congruence.
Qed.

Fact dec_contra (P Q: Prop) :
  dec Q -> P <-> ~Q -> Q <-> ~P.
Proof.
  unfold dec. tauto.
Qed.

Fact sat_val s :
  sat s <-> ~ val (neg s).
Proof.
  apply dec_contra. now auto.
  rewrite val_sat.
  rewrite (sat_compatibility (neg_neg s)).
  reflexivity.
Qed.

Exercises

Instance Exp_eq_dec :
  eq_dec Exp.
Proof.
  unfold dec. decide equality. apply nat_eq_dec.
Qed.

Lemma subst_vars s x A t :
  vars s <<= x ::A -> vars t <<= A -> vars (subst s x t) <<= A.
Proof.
  induction s as [| |y|s IHs u IHu v IHv]; cbn.
  - auto.
  - auto.
  - intros H1 H2. decide (x=y) as [<-|H3];cbn. now auto.
    assert (y el x::A) as H4 by auto. cbn in *; intuition.
  - intros [H1 [H2 H3] % incl_app_left] % incl_app_left H4.
    rewrite IHs, IHu, IHv; auto.
Qed.

Example Ex4 alpha x y :
  update alpha x (alpha x) y = alpha y.
Proof.
  unfold update. now decide (x=y) as [<-|H].
Qed.

Example Ex5 alpha x s :
  eva (update alpha x (alpha x)) s = eva alpha s.
Proof.
  apply coincidence. auto using update_id.
Qed.

Example Ex6 alpha x s b :
  eva alpha s = true -> alpha x = b -> eva (update alpha x b) s = true.
Proof.
  intros <-H. apply coincidence. auto using update_id.
Qed.

Fact if_complete2 (f: bool -> bool -> bool) a b :
  f a b = if a then if b then f true true else f true false
          else if b then f false true else f false false.
Proof.
  destruct a, b; reflexivity.
Qed.

Coercion bool2exp (b: bool) : Exp := if b then top else bot.

Fact cond_complete2 (f: bool -> bool -> bool) a b :
  (f a b : Exp ) == cond a (cond b (f true true) (f true false))
                       (cond b (f false true) (f false false)).
Proof.
  intros alpha. destruct a, b; cbn; reflexivity.
Qed.

Shallow and deep Embedding

Lemma shallow_embedding b f i :
  implb (negb b) f &&
  implb (b &&f) (negb i) &&
  implb (i || negb b) (negb f)
  =
  b && (negb f || negb i ).
Proof.
  destruct b,f,i; cbn; reflexivity.
Qed.

Module Deep_embedding.
  Notation "s '&&' t" := (cond s t bot).
  Notation "s '||' t" := (cond s top t).
  Notation imp s t := (cond s t top).
  Notation b := (var 0).
  Notation f := (var 1).
  Notation i := (var 2).

  Goal imp (neg b) f &&
       imp (b &&f) (neg i) &&
       imp (i || neg b) (neg f)
       ==
       b && neg (f &&i).
  Proof.
    intros alpha. cbn.
    destruct (alpha 0), (alpha 1), (alpha 2); cbn; reflexivity.
  Qed.

We may also use a SAT solver to prove equivalence of boolean expressions.

Definition check_sat s := if solve (vars s) s then true else false.
Definition check_equiv s t := negb (check_sat (cond s (neg t) s)).

Recall that solve uses the functions update and subst, which in turn use a decider for equality on nat. This decider is put in automatically in non-reducible form (type class inference for dec). Thus check_equiv will not reduce to a boolean. The function check_equiv can be made reducible by replacing the Qed closing the definition of nat_eq_dec in Base.v with Defined.

End Deep_embedding.