Formalising 2-Sat in Coq (source code TwoSat.v, a note TwoSat.pdf)
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq fintype finfun bigop.
Require Import path fingraph.
Section TwoSat.
(* The set of variables *)
Variable var : finType.
Implicit Type v : var.
(* A litteral is a signed variable *)
Notation lit := (bool * var)%type.
Implicit Type l : lit.
Definition flip l := (~~ l.1, l.2).
Lemma flipK : cancel flip flip.
Proof. by do 2 case. Qed.
Lemma flip_neq l : flip l != l.
Proof. by case: l => [] []. Qed.
(* A clause is a pair of litterals *)
Local Notation clause := (lit * lit)%type.
Implicit Type cl : clause.
(* Clauses are sequences of clauses *)
Local Notation clauses := (seq clause).
Implicit Type cls : clauses.
(* An assignment is a function for var to bool *)
Local Notation val := (option (bool * bool)).
Local Notation mem:= {ffun var -> val}.
Implicit Types m : mem.
(* The list of clauses *)
Variable cls : clauses.
(* Implication between literals *)
Definition imply := [rel a b | ((flip a, b) \in cls) || ((b, flip a) \in cls)].
Notation " a [->] b " := (imply a b) (at level 40).
Lemma imply_flip l1 l2 : flip l1 [->] flip l2 = l2 [->] l1.
Proof. by rewrite /imply /= flipK orbC. Qed.
Lemma path_flip l1 l2 p :
path imply (flip l1) (rcons p (flip l2)) =
path imply l2 (rcons (map flip (rev p)) l1).
Proof.
elim: p l1 l2 => [l1 l2 /=|l p IH l1 l2].
by (rewrite !andbT; exact: imply_flip).
rewrite /= -{3}(flipK l) IH rev_cons map_rcons [X in _ = X]rcons_path andbC.
by rewrite last_rcons -{3}(flipK l1) imply_flip.
Qed.
Lemma connect_flip l1 l2 :
connect imply (flip l1) (flip l2) = connect imply l2 l1.
Proof.
apply/connectP/connectP => [] [p e_p e_f].
elim/last_ind: p e_p e_f => //= [_ /(can_inj flipK)->|p l3 _ e_p e_f].
by exists [::].
exists (rcons (map flip (rev p)) l1); rewrite last_rcons in e_f.
by rewrite -path_flip e_f.
by rewrite last_rcons.
elim/last_ind: p e_p e_f => //= [_ ->|p l3 _ e_p e_f]; first by exists [::].
exists (rcons (map flip (rev p)) (flip l2)); rewrite last_rcons in e_f.
by rewrite -path_flip !flipK e_f.
by rewrite last_rcons.
Qed.
(* Flip value *)
Definition vflip (x : val) : val :=
omap (fun x => (x.1, negb x.2)) x.
Lemma vflipK : cancel vflip vflip.
Proof. by move=> [] // [] [] []. Qed.
(* Getting the value of a literal *)
Definition lit_get m l : val := if l.1 then m l.2 else vflip (m l.2).
Lemma lit_get_flip m l : lit_get m (flip l) = vflip (lit_get m l).
Proof. by case: l => [] // [] b; rewrite /lit_get /= ?vflipK. Qed.
(* Setting the value of a literal *)
Definition lit_set m l r : mem :=
[ffun x => if x == l.2 then if l.1 then r else vflip r
else m x].
Lemma lit_set_eq m l x : lit_get (lit_set m l x) l = x.
Proof.
by rewrite /lit_get /lit_set !ffunE eqxx; case: l.1; rewrite ?vflipK.
Qed.
Lemma lit_set_neq m l1 l2 x : l2 != l1 -> l2 != flip l1 ->
lit_get (lit_set m l1 x) l2 = lit_get m l2.
Proof.
by ((case: l1 => [[] v1]; case: l2 => [[] v2];
rewrite /lit_set /lit_get !ffunE //=; case: (v2 =P v1))
=> //->) => [|_|_|] /negP[].
Qed.
(* The list of literals implied by a literal *)
Definition inext : lit -> seq lit := rgraph imply.
Lemma inext_flip l1 l2 :
flip l1 \in inext (flip l2) = (l2 \in inext l1).
Proof. by rewrite  imply_flip. Qed.
Lemma inext_imply l l1 : l1 \in inext l = l [->] l1.
Proof. by rewrite [_ \in _]rgraphK. Qed.
(* The propagation algorithm *)
Fixpoint propagate n m s :=
if n is n1.+1 then
if s is (l, ls) :: s1 then
if lit_get m l is Some (b1, true) then
(* We check that l is still set to true not to propagate
wrong values. Example:
A -> {~B, E, B}, ~A -> {}, B -> {A}, ~B -> {~E, A}, E -> {B}, ~E -> {~A}
*)
if ls is l1 :: ls1 then
if lit_get m l1 is Some (b, v) then
if v then propagate n1 m ((l, ls1) :: s1)
else
if b then Some (false, n1.+1, m)
else
let m1 := lit_set m l1 (Some (true, true)) in
propagate n1 m1 [:: (l1, inext l1), (l, ls1) & s1]
else
let m1 := lit_set m l1 (Some (b1, true)) in
propagate n1 m1 [:: (l1, inext l1), (l, ls1) & s1]
else propagate n1 m s1
else propagate n1 m s1
else Some (true, n1.+1, m)
else None.
(* Check if a literal is true *)
Definition lit_is_true m l := oapp (fun x => x.2) false (lit_get m l).
Lemma lit_is_true_set_eq m x l :
lit_is_true (lit_set m l x) l = oapp (fun x => x.2) false x.
Proof. by rewrite /lit_is_true lit_set_eq. Qed.
Lemma lit_is_true_flip m l : lit_is_true m (flip l) -> ~~ lit_is_true m l.
Proof. by rewrite /lit_is_true lit_get_flip; case: lit_get => // [[[] []]]. Qed.
Lemma lit_is_true_set_eq_flip m x l :
lit_is_true (lit_set m l x) (flip l) = oapp (fun x => x.2) false (vflip x).
Proof. by rewrite /lit_is_true lit_get_flip lit_set_eq. Qed.
Lemma lit_is_true_set_neq m x l1 l2 :
l2 != l1 -> l2 != flip l1 ->
lit_is_true (lit_set m l1 x) l2 = lit_is_true m l2.
Proof. by move=> H1 H2; rewrite /lit_is_true lit_set_neq. Qed.
Lemma lit_is_true_set_neq_flip m x l1 l2 :
l2 != l1 -> l2 != flip l1 ->
lit_is_true (lit_set m l1 x) (flip l2) = lit_is_true m (flip l2).
Proof.
by move=> H1 H2; rewrite /lit_is_true lit_get_flip lit_set_neq // lit_get_flip.
Qed.
Lemma lit_is_true_set_flip m b l l1 :
lit_is_true (lit_set m l (Some (b, true))) l1 -> l1 != flip l.
Proof.
move=> H; apply/eqP => El1fl.
by move: H; rewrite El1fl lit_is_true_set_eq_flip.
Qed.
(* Check if a literal is strongly true, i.e. its value can't be changed *)
Definition lit_is_strue m l := oapp (fun x => x.2 && x.1) false (lit_get m l).
Lemma lit_is_strueW m l : lit_is_strue m l -> lit_is_true m l.
Proof.
by rewrite /lit_is_true /lit_is_strue; case: lit_get => // [] [[] []].
Qed.
Lemma lit_is_strue_set_eq m x l :
lit_is_strue (lit_set m l x) l = oapp (fun i => i.1 && i.2) false x.
Proof. by rewrite /lit_is_strue lit_set_eq; case: x => // [[[] []]]. Qed.
Lemma lit_is_strue_set_eq_flip m x l :
lit_is_strue (lit_set m l x) (flip l) = oapp (fun i => i.1 && ~~ i.2) false x.
Proof.
by rewrite /lit_is_strue lit_get_flip lit_set_eq; case: x => // [[[] []]].
Qed.
Lemma lit_is_strue_set_neq m x l1 l2 :
l2 != l1 -> l2 != flip l1 ->
lit_is_strue (lit_set m l1 x) l2 = lit_is_strue m l2.
Proof. by move=> H1 H2; rewrite /lit_is_strue lit_set_neq. Qed.
Lemma lit_is_strue_set_neq_flip m x l1 l2 :
l2 != l1 -> l2 != flip l1 ->
lit_is_strue (lit_set m l1 x) (flip l2) = lit_is_strue m (flip l2).
Proof.
by move=> H1 H2; rewrite /lit_is_strue lit_get_flip lit_set_neq // lit_get_flip.
Qed.
Lemma lit_is_strue_set_flip m b l l1 :
lit_is_strue (lit_set m l (Some (b, true))) l1 -> l1 != flip l.
Proof.
move=> H; apply/eqP => El1fl.
by move: H; rewrite El1fl lit_is_strue_set_eq_flip /= andbF.
Qed.
(* l has an implication cycle, so it must be true *)
Definition lit_cycle l := connect imply (flip l) l.
Lemma lit_cycle_inext l l1 :
l1 \in inext l -> lit_cycle l -> lit_cycle l1.
Proof.
move=> Il1 Cl.
have Coll1 : connect imply l l1 by apply: connect1; rewrite -inext_imply.
have Cofl1fl : connect imply (flip l1) (flip l).
by apply: connect1; rewrite -inext_imply inext_flip.
apply: connect_trans Coll1.
by apply: connect_trans Cofl1fl _.
Qed.
(* Stack is composed of an implication *)
Definition istack s := if rev s is l :: ls then path imply l ls else true.
Lemma istack_cons l l1 ls :
istack (l :: ls) -> l1 \in inext l -> istack [:: l1, l & ls].
Proof.
rewrite inext_imply /istack !rev_cons; case: rev => /= [|l2 ls1 H1 H2].
by rewrite andbT.
by rewrite rcons_path H1 last_rcons.
Qed.
Lemma istack_consE l ls : istack (l :: ls) -> istack ls.
Proof.
rewrite /istack rev_cons; case: rev => //= l2 ls1.
by rewrite rcons_path => /andP[].
Qed.
Lemma path_head_connect (A : finType) (r : rel A) (a b c : A) p :
path r a (rcons p b) -> c \in (a :: p) -> connect r c b.
Proof.
elim: p a c => /= [a c | d p IH a c].
by rewrite inE andbT => H /eqP->; apply: connect1.
rewrite inE => /andP[H1 H2] /orP[/eqP->|]; last by exact: IH.
apply: connect_trans (connect1 H1) _.
by apply/connectP; exists (rcons p b) => //; rewrite last_rcons.
Qed.
Lemma mem_istack l l1 ls :
istack (l :: ls) -> l1 \in l :: ls -> connect imply l1 l.
Proof.
rewrite inE => H1 /orP[/eqP->//|H2].
have : l1 \in rev ls by rewrite mem_rev.
move : H1; rewrite /istack rev_cons; case: rev => //= l2 ls1 H3 H4.
by apply: path_head_connect H4.
Qed.
(* Ordered stack, i.e. strong values are at the top of the stack *)
Definition ostack m (s : seq lit) (s1 := [seq x <- s | lit_is_true m x]) :=
s1 = [seq x <- s1 | lit_is_strue m x] ++ [seq x <- s1 | ~~ lit_is_strue m x].
Lemma ostackE m l s : ostack m (l :: s) -> ostack m s.
Proof.
rewrite /ostack /=.
case Ll : lit_is_true => //=.
case Sl : lit_is_strue => /=; first by case.
case Es : [seq _ <- [seq _ <- _ | _]| _] => /= [|l1 s1]; first by case.
case => El.
have: l1 \in l1 :: s1 by rewrite inE eqxx.
by rewrite -Es -El mem_filter Sl.
Qed.
Lemma ostack_neg_lit_is_strue m l1 l2 s :
lit_is_true m l1 -> ~~ lit_is_strue m l1 ->
ostack m (l1 :: s) -> l2 \in (l1 :: s) -> ~~ lit_is_strue m l2.
Proof.
move=> Ll1 Sl1.
rewrite /ostack inE /= Ll1 /= Sl1 (negPf Sl1) => El1s /orP[/eqP->//|l2Is].
apply/negP => Sl2; move: El1s.
set d := [seq x <- [seq x <- s | _] | _].
have: l2 \in d by rewrite !mem_filter Sl2 lit_is_strueW.
case Ed : d => [|l3 ls3] //= l2Il2 [] El1l3.
have: l1 \notin d by rewrite mem_filter negb_and Sl1.
by rewrite Ed -El1l3 inE eqxx.
Qed.
Lemma ostack_strue m l s :
lit_is_strue m l -> ostack m s -> ostack m (l :: s).
Proof.
by move=> Sl; rewrite /ostack /= (lit_is_strueW _ _ Sl) /= Sl /= => <-.
Qed.
Lemma filter_cons (T : Type) (p : pred T) (s : seq T) x:
filter p (x :: s) = if p x then x :: filter p s else filter p s.
Proof. by []. Qed.
Lemma ostack_same m l1 l2 s :
lit_get m l1 = lit_get m l2 ->
ostack m (l1 :: s) -> ostack m (l2 :: l1 :: s).
Proof.
move=> Egl1gl2; rewrite /ostack !filter_cons.
have ETl1Tl2 : lit_is_true m l1 = lit_is_true m l2.
by rewrite /lit_is_true Egl1gl2.
have ESl1Sl2 : lit_is_strue m l1 = lit_is_strue m l2.
by rewrite /lit_is_strue Egl1gl2.
rewrite -ETl1Tl2 /=.
case: lit_is_true => //=.
rewrite -ESl1Sl2.
case E : lit_is_strue => //=; first by move->.
set d := [seq x <- s | lit_is_true m x].
case E1 : [seq x <- d | lit_is_strue m x] => [|l3 d1] //=.
by case=> <-.
case=> El1l3.
have: l1 \in l1 :: d1 by rewrite inE eqxx.
by rewrite El1l3 -E1 mem_filter -El1l3 E.
Qed.
Lemma ostack_weak m1 m2 s :
(forall l, l \in s -> lit_is_true m1 l -> lit_is_true m2 l) ->
(forall l, l \in s -> lit_is_strue m1 l = lit_is_strue m2 l) ->
ostack m2 s -> ostack m1 s.
Proof.
move=> FL FSL.
rewrite /ostack => Om2.
suff {1}-> : [seq x <- s | lit_is_true m1 x] =
[seq x <- [seq x <- s | lit_is_true m1 x] | lit_is_strue m2 x] ++
[seq x <- [seq x <- s | lit_is_true m1 x] | ~~ lit_is_strue m2 x].
by congr (_ ++ _); apply: eq_in_filter=> l;
rewrite mem_filter => /andP[_ HH]; rewrite FSL.
have Hf P :
[seq x <- [seq x <- s | lit_is_true m1 x] | P x] =
[seq x <-
[seq x <- [seq x <- s | lit_is_true m2 x] | P x] | lit_is_true m1 x].
rewrite -!filter_predI.
apply: eq_in_filter=> l lIs /=.
by case: (P _); case: lit_is_true (FL _ lIs); case: lit_is_true => //=
/(_ is_true_true).
rewrite !Hf -filter_cat -Om2 -filter_predI.
apply: eq_in_filter=> l lIs /=.
by case: lit_is_true (FL _ lIs); case: lit_is_true => //= /(_ is_true_true).
Qed.
(* Main invariant *)
Definition valid m (s : seq (lit * seq lit)) :=
[/\
let s1 := [seq i.1 | i <- s] in
[/\ uniq s1, istack s1, ostack m s1 &
forall l, l \in s1 -> lit_is_true m l || lit_is_strue m (flip l)],
forall l, forall ls, (l, ls) \in s -> ls \subset inext l,
forall l, lit_is_strue m l -> lit_cycle l &
forall l1 l2,
(forall ls, (l1, ls) \in s -> l2 \notin ls) ->
(forall ls, lit_is_strue m (flip l2) ->
(flip l2, ls) \in s -> flip l1 \notin ls) ->
l2 \in inext l1 -> lit_is_true m l1 -> lit_is_true m l2].
Definition wf_mem m := forall l1 l2,
l2 \in inext l1 -> lit_is_true m l1 -> lit_is_true m l2.
Lemma wf_nil m : valid m [::] -> wf_mem m.
Proof. by move=> [_ _ _ F] l l1 Tl l1INl; apply: F l1INl. Qed.
Lemma lit_dec l1 l2 : [\/ l1 = l2, l1 = flip l2 | l1 != l2 /\ l1 != flip l2].
Proof.
case: eqP => [->|_]; first by apply: Or31.
by case: eqP => [->|_]; [apply: Or32 | apply: Or33].
Qed.
Lemma valid_init m l (m1 := lit_set m l (Some (false, true))) :
valid m [::] -> lit_get m l = None -> valid m1 [:: (l, inext l)].
Proof.
move=> [_ _ Cl F] Gl.
split=> //= [|l1 ls|l1|l1 l2 D Dr l2INl1 Tm1l1]; first (split => [|||l1] //=).
- by rewrite /ostack /= lit_is_true_set_eq /= lit_is_strue_set_eq.
- by rewrite inE => /eqP->; rewrite lit_is_true_set_eq lit_is_strue_set_eq_flip.
- by rewrite inE xpair_eqE => /andP[/eqP->/eqP->].
- have [->|->| [Dl1l Dl1fl]] := lit_dec l1 l.
- by rewrite lit_is_strue_set_eq.
- by rewrite lit_is_strue_set_eq_flip.
by rewrite lit_is_strue_set_neq //; exact: Cl.
have [El1l|El1fl| [Dl1l Dl1fl]] := lit_dec l1 l.
- have/negP[] : l2 \notin inext l.
by apply: D; rewrite El1l inE eqxx.
by rewrite -El1l.
- by move: Tm1l1; rewrite El1fl lit_is_true_set_eq_flip.
have : lit_is_true m l2.
apply: F l2INl1 _ => //.
by move: Tm1l1; rewrite lit_is_true_set_neq.
have [->|->| [Dl2l Dl2fl]] := lit_dec l2 l.
- by rewrite lit_is_true_set_eq.
- by rewrite /lit_is_true lit_get_flip Gl.
by rewrite lit_is_true_set_neq.
Qed.
Lemma valid_cons m l ls s :
valid m ((l, ls) :: s) -> ~~ lit_is_true m l -> valid m s.
Proof.
move=> [[V1 V2 V3 V4] V5 V6 V7] NTml;
split => [|l1 ls1 Il1||l1 l2 D Dr Tml1 l2INl1] //;
first (split=> [|||l1 l1Is] //).
- by apply: subseq_uniq V1; apply: map_subseq; apply: subseq_cons.
- by apply: istack_consE V2.
- by move: V3; rewrite /ostack /= (negPf NTml).
- by apply: V4; rewrite inE l1Is orbT.
- by apply: V5; rewrite inE Il1 orbT.
have [/eqP El1l | Dl1l] := boolP (l1 == l).
by case/negP:NTml ; rewrite -El1l.
have [/eqP El2l | Dfl2l] := boolP (flip l2 == l).
rewrite -(flipK l2) El2l.
have/V4 : l \in [seq i.1 | i <- (l, ls) :: s] by rewrite /= inE eqxx.
by move: NTml; rewrite /lit_is_true /lit_is_strue lit_get_flip; case: lit_get.
apply: V7 l2INl1 => // [ls1|V ls1];
rewrite inE xpair_eqE ?(negPf Dl1l) ?(negPf Dfl2l) //=.
by apply: D.
by apply: Dr.
Qed.
Lemma valid_cons_nil m l s : valid m ((l, [::]) :: s) -> valid m s.
Proof.
move=> [[V1 V2 V3 V4] V5 V6 V7]; split => [|l1 ls1 Il1||l1 l2 D Dr Tml1 Il1] //;
first (split => [|||l1 Il1]).
- by apply: subseq_uniq V1; apply: map_subseq; apply: subseq_cons.
- by apply: istack_consE V2.
- by apply: ostackE V3.
- by apply: V4; rewrite inE Il1 orbT.
- by apply: V5; rewrite inE Il1 orbT.
apply: V7 Il1 => // [ls|V ls]; rewrite inE xpair_eqE => /orP[/andP[HH/eqP->]|] //.
by apply: D.
by apply: Dr.
Qed.
Lemma valid_cons_true m l l1 ls1 s :
valid m ((l, l1 :: ls1) :: s) ->
lit_is_true m l -> lit_is_true m l1 ->
valid m ((l, ls1) :: s).
Proof.
move=> [[V1 V2 V3 V4] V5 V6 V7] Tml Tml1.
split => [|l2 ls2||l2 l3 D Dr Il3 Tml2] //.
rewrite inE => /orP[/eqP[]->->|Il].
apply: subset_trans (_ : l1 :: ls1 \subset _) => //.
by apply/subsetP=> l3 Il3; rewrite inE Il3 orbT.
by apply: V5; rewrite inE eqxx.
by apply: V5; rewrite inE Il orbT.
have [/eqP->//| Dl3l1] := boolP (l3 == l1).
apply: V7 Il3 _ => // [ls|V ls].
rewrite inE xpair_eqE => /orP[/andP[/eqP El2l /eqP ->]|Il2].
rewrite inE negb_or Dl3l1.
by apply: D; rewrite El2l inE eqxx.
by apply: D; rewrite inE Il2 orbT.
have [/eqP Efl2l1| Dfl2l1] := boolP (flip l2 == l1).
by have := Tml1; rewrite -Efl2l1=> /lit_is_true_flip/negP[].
rewrite inE xpair_eqE => /orP[/andP[/eqP Efl3l /eqP ->]|If].
by rewrite inE negb_or Dfl2l1 //= Dr // inE Efl3l eqxx.
by rewrite Dr // inE If orbT.
Qed.
Lemma valid_add_true m b l l1 ls1 s :
valid m ((l, l1 :: ls1) :: s) ->
lit_get m l == Some (b, true) ->
lit_get m l1 == None ->
valid (lit_set m l1 (Some (b, true))) [:: (l1, inext l1), (l, ls1) & s].
Proof.
move=> [[V1 V2 V3 V4] V5 V6 V7] Gml Gml1.
have [/eqP El1l | Dl1l] := boolP (l1 == l).
by move: Gml Gml1; rewrite El1l => /eqP->.
have l1INl : l1 \in inext l.
have /subsetP->// : (l1 :: ls1) \subset inext l.
by apply: V5; rewrite inE eqxx.
by rewrite inE eqxx.
have Us : uniq [seq i.1 | i <- [:: (l1, inext l1), (l, ls1) & s]].
rewrite map_cons cons_uniq V1 andbT /=.
rewrite inE negb_or (negPf Dl1l).
apply/negP=> Il1.
case: (orP (V4 l1 _)).
- by rewrite map_cons inE Il1 orbT.
- by rewrite /lit_is_true; case: lit_get Gml1 => [[[] []]|].
by rewrite /lit_is_strue lit_get_flip; case: lit_get Gml1 => [[[] []]|].
split => [|l2 ls2|l2|l2 l3 D Dr Il3 Tm1l2] //;
first (split => [|||l2] //=).
- by apply: istack_cons.
- have Dl1fl : l1 != flip l.
by apply/eqP=> HH; move: Gml1; rewrite HH lit_get_flip (eqP Gml).
apply: ostack_same.
rewrite lit_set_eq lit_set_neq ?(eqP Gml) 1?eq_sym //.
by apply: contra Dl1fl => /eqP<-; rewrite flipK.
apply: ostack_weak V3 => [l2 Hl2|l2 Hl2].
have [/eqP El2l| Dl2l1] := boolP (l2 == l1).
move: Hl2 Us; rewrite /= El2l !inE negb_or => /orP[/eqP->//|->//].
by rewrite eqxx.
by rewrite andbF.
move=> HH; move: (HH).
by rewrite lit_is_true_set_neq // (lit_is_true_set_flip _ _ _ _ HH).
have [El2l1|->|[Dl2l1 Dl2fl1]] := lit_dec l2 l1.
- move: Hl2 Us; rewrite /= El2l1 !inE negb_or => /orP[/eqP->//|->//].
by rewrite eqxx.
by rewrite andbF.
- by rewrite /lit_is_strue !lit_get_flip lit_set_eq (eqP Gml1).
by rewrite lit_is_strue_set_neq.
- have [->|->|[Dl2l1 Dl2fl1]] := lit_dec l2 l1.
- by rewrite lit_is_true_set_eq.
- rewrite inE (negPf (flip_neq _)) => /V4.
by rewrite flipK /lit_is_true /lit_is_strue lit_get_flip (eqP Gml1).
rewrite inE (negPf Dl2l1) => /V4.
by rewrite lit_is_true_set_neq // lit_is_strue_set_neq_flip.
- rewrite !inE => /or3P[/eqP[]->->|/eqP[]->->|Il2] //.
apply: subset_trans (_ : l1 :: ls1 \subset _).
by apply/subsetP=> l4; rewrite inE orbC => ->.
by apply: V5; rewrite inE eqxx.
by apply: V5; rewrite inE Il2 orbT.
- have [->|->|[Dl2l1 Dl2fl1]] := lit_dec l2 l1.
- rewrite lit_is_strue_set_eq => /= /andP[B _].
have F : lit_cycle l.
by apply: V6; rewrite /lit_is_strue (eqP Gml).
by apply: lit_cycle_inext F.
- by rewrite lit_is_strue_set_eq_flip /= andbF.
by rewrite lit_is_strue_set_neq //; exact: V6.
have [El2l1|El2fl1|[Dl2l1 Dl2fl1]] := lit_dec l2 l1.
- have: l3 \notin inext l1.
by apply: D; rewrite El2l1 inE eqxx.
by rewrite -El2l1 Il3.
- by move : Tm1l2; rewrite El2fl1 lit_is_true_set_eq_flip.
have Tml2 : lit_is_true m l2.
by move: Tm1l2; rewrite lit_is_true_set_neq.
have [->|El3fl1|[Dl3l1 Dl3fl1]] := lit_dec l3 l1.
- by rewrite lit_is_true_set_eq.
- suff: lit_is_true m l3.
by rewrite El3fl1 /lit_is_true lit_get_flip (eqP Gml1).
apply: V7 Il3 _ => // [ls|].
rewrite El3fl1 !inE xpair_eqE => /orP[/andP[/eqP El2l /eqP->]|Il2].
by rewrite inE negb_or (negPf (flip_neq _)) -El3fl1 D //
El2l !inE eqxx orbT.
by rewrite -El3fl1; apply: D; rewrite !inE Il2 !orbT.
by rewrite El3fl1 flipK /lit_is_strue (eqP Gml1).
rewrite lit_is_true_set_neq //.
apply: V7 Il3 _ => // [ls|HH ls];
rewrite !inE ?xpair_eqE => /orP[/andP[/eqP El /eqP->]|Il].
- by rewrite inE negb_or Dl3l1 D // El !inE eqxx orbT.
- by apply: D; rewrite !inE Il !orbT.
- rewrite inE negb_or Dr ?andbT //.
- by apply: contra Dl2fl1 => /eqP<-; rewrite flipK.
- by rewrite lit_is_strue_set_neq_flip.
by rewrite El !inE eqxx orbT.
apply: Dr; first by rewrite lit_is_strue_set_neq_flip.
by rewrite !inE Il !orbT.
Qed.
Lemma valid_add_true_rev m b l l1 ls1 s :
valid m ((l, l1 :: ls1) :: s) ->
lit_get m l == Some (b, true) ->
lit_get m l1 == Some (false, false) ->
valid (lit_set m l1 (Some (true, true))) [:: (l1, inext l1), (l, ls1) & s].
Proof.
move=> [[V1 V2 V3 V4] V5 V6 V7] Gml Gml1.
have [/eqP El1l | Dl1l] := boolP (l1 == l).
by move: Gml Gml1; rewrite El1l => /eqP->; case: b.
have l1INl : l1 \in inext l.
have /subsetP->// : (l1 :: ls1) \subset inext l.
by apply: V5; rewrite inE eqxx.
by rewrite inE eqxx.
have Us : uniq [seq i.1 | i <- [:: (l1, inext l1), (l, ls1) & s]].
rewrite map_cons cons_uniq V1 andbT /=.
rewrite inE negb_or (negPf Dl1l).
apply/negP=> Il1.
case: (orP (V4 l1 _)).
- by rewrite map_cons inE Il1 orbT.
- by rewrite /lit_is_true; case: lit_get Gml1 => [[[] []]|].
by rewrite /lit_is_strue lit_get_flip; case: lit_get Gml1 => [[[] []]|].
split => [|l2 ls2|l2|l2 l3 D Dr Il3 Tm1l2] //;
first (split => [|||l2] //=).
- by apply: istack_cons.
- apply: ostack_strue; first by rewrite lit_is_strue_set_eq.
apply: ostack_weak V3 => l2 Il2.
have [/eqP El2l1| Dl2l1] := boolP (l2 == l1).
move: Il2 Us; rewrite /= El2l1 !inE negb_or => /orP[/eqP->//|->//].
by rewrite eqxx.
by rewrite andbF.
move=> HH; move: (HH).
by rewrite lit_is_true_set_neq // (lit_is_true_set_flip _ _ _ _ HH).
have [El2l1| ->| [Dl2l1 Dl2fl1]] := lit_dec l2 l1.
- move: Il2 Us; rewrite /= El2l1 !inE negb_or => /orP[/eqP->//|->//].
by rewrite eqxx.
by rewrite andbF.
- by rewrite lit_is_strue_set_eq_flip /lit_is_strue lit_get_flip (eqP Gml1).
by rewrite lit_is_strue_set_neq.
- have [->|->| [Dl2l1 Dl2fl1]] := lit_dec l2 l1.
- by rewrite lit_is_true_set_eq.
- by rewrite flipK lit_is_strue_set_eq orbT.
rewrite inE (negPf Dl2l1) lit_is_true_set_neq //
lit_is_strue_set_neq_flip //=.
by apply: V4.
- rewrite !inE => /or3P[/eqP[]->->|/eqP[]->->|Il2] //.
apply: subset_trans (_ : l1 :: ls1 \subset _).
by apply/subsetP=> l4; rewrite inE orbC => ->.
by apply: V5; rewrite inE eqxx.
by apply: V5; rewrite inE Il2 orbT.
- have [-> _|->|[Dl2l1 Dl2fl1]] := lit_dec l2 l1.
- have F : lit_is_true m (flip l1).
by rewrite /lit_is_true lit_get_flip (eqP Gml1).
have [Ifl1|NIfl1] :=
boolP (flip l1 \in [seq i.1 | i <- (l, l1 :: ls1) :: s]).
apply: connect_trans (_ : connect imply l l1).
by apply: mem_istack V2 _.
by apply: connect1; rewrite -inext_imply.
case: b Gml => Gml.
have : lit_cycle l by apply: V6; rewrite /lit_is_strue (eqP Gml).
by apply: lit_cycle_inext.
have: lit_is_true m (flip l).
apply: V7 F => // [ls Hls||].
by case/negP: NIfl1; apply: map_f Hls.
by rewrite /lit_is_strue flipK (eqP Gml).
by rewrite inext_flip.
by rewrite /lit_is_true lit_get_flip (eqP Gml).
- by rewrite lit_is_strue_set_eq_flip.
by rewrite lit_is_strue_set_neq //; exact: V6.
have [El2l1|El2fl1| [Dl21l Dl2fl1]] := lit_dec l2 l1.
- suff: l3 \notin inext l1 by rewrite -El2l1 Il3.
by apply: D; rewrite inE El2l1 eqxx.
- by move : Tm1l2; rewrite El2fl1 lit_is_true_set_eq_flip.
have Tml2 : lit_is_true m l2 by move: Tm1l2; rewrite lit_is_true_set_neq.
have [->|El3fl1| [Dl3l1 Dl3fl1]] := lit_dec l3 l1.
- by rewrite lit_is_true_set_eq.
- have: flip l2 \notin (inext l1).
apply: Dr; first by rewrite El3fl1 flipK lit_is_strue_set_eq.
by rewrite El3fl1 flipK inE eqxx.
by rewrite -(flipK l1) -El3fl1 inext_flip Il3.
suff: lit_is_true m l3 by rewrite lit_is_true_set_neq.
apply: V7 Il3 _ => // [ls|HH ls].
rewrite !inE xpair_eqE => /orP[/andP[/eqP El2l/eqP->]|Il2].
by rewrite inE negb_or Dl3l1 D // El2l !inE eqxx orbT.
by apply: D; rewrite !inE Il2 !orbT.
rewrite !inE xpair_eqE => /orP[/andP[/eqP Efl3l/eqP->]|Ifl3].
rewrite inE negb_or; apply/andP; split.
by apply: contra Dl2fl1 => /eqP<-; rewrite flipK.
apply: Dr => //.
by rewrite lit_is_strue_set_neq_flip.
by rewrite Efl3l !inE eqxx orbT.
apply: Dr => //.
by rewrite lit_is_strue_set_neq_flip.
by rewrite !inE Ifl3 !orbT.
Qed.
Lemma valid_propage_true n m m1 s k :
valid m s -> propagate n m s = Some (true, k, m1) -> valid m1 [::].
Proof.
elim: n m m1 s => //= n iH m m1 [H1 [_ <-]|[l ls] s1 Vm] //.
case E : lit_get => [[b []]|]; last 2 first.
- apply: iH; apply: valid_cons Vm _.
by rewrite /lit_is_true /= E.
- have [[_ _ _ H] _ _ _] := Vm.
have : l \in [seq i.1 | i <- (l, ls) :: s1] by rewrite inE eqxx.
by move/H; rewrite /lit_is_true /lit_is_strue lit_get_flip E.
case: ls Vm => [Vm|l1 ls1 Vm].
by apply: iH; apply: valid_cons_nil Vm.
case E1 : lit_get => [[b1 []]|] //.
- apply: iH; apply: valid_cons_true Vm _ _.
by rewrite /lit_is_true E.
by rewrite /lit_is_true E1.
- case: b1 E1 => // E1.
apply: iH.
by apply: valid_add_true_rev => //; apply/eqP.
apply: iH.
by apply: valid_add_true => //; [rewrite /lit_is_true E | rewrite E1].
Qed.
Lemma valid_propage_false n m m1 s k :
valid m s -> propagate n m s = Some (false, k, m1) ->
exists l, lit_cycle l /\ lit_cycle (flip l).
Proof.
elim: n m m1 s => //= n iH m m1 [|[l ls] s Vm] //.
case E : lit_get => [[b []]|]; last 2 first.
- apply: iH; apply: valid_cons Vm _.
by rewrite /lit_is_true /= E.
- have [[_ _ _ H] _ _ _] := Vm.
have : l \in [seq i.1 | i <- (l, ls) :: s] by rewrite inE eqxx.
by move/H; rewrite /lit_is_true /lit_is_strue lit_get_flip E.
case: ls Vm => [Vm|l1 ls1 Vm].
by apply: iH; apply: valid_cons_nil Vm.
have X1 : l1 \in inext l.
have/subsetP->// : l1 :: ls1 \subset inext l.
have [_ HH _ _] := Vm.
by apply: HH; rewrite !inE eqxx.
by rewrite inE eqxx.
case E1 : lit_get => [[b1 []]|] //.
- apply: iH; apply: valid_cons_true Vm _ _.
by rewrite /lit_is_true E.
by rewrite /lit_is_true E1.
- case: b1 E1 => // E1.
have F1 : lit_is_strue m (flip l1).
by rewrite /lit_is_strue lit_get_flip E1.
case: b E => E _.
have F : lit_cycle l.
have [_ _ HH _] := Vm.
by apply: HH; rewrite /lit_is_strue E.
exists l1; split; first by apply: lit_cycle_inext F.
have [_ _ HH _] := Vm.
by apply: HH.
have [F2 | F2] := boolP (flip l1 \in [seq i.1 | i <- (l, l1 :: ls1) :: s]).
have [[_ _ HH _] _ _ _] := Vm.
have : ~~ lit_is_strue m (flip l1).
apply: ostack_neg_lit_is_strue HH _ => //=.
- by rewrite /lit_is_true E.
- by rewrite /lit_is_strue E.
by rewrite F1.
have : lit_is_true m (flip l).
have F : flip l \in inext (flip l1) by rewrite inext_flip.
have [_ _ _ HH] := Vm.
apply: HH F _ => // [ls||].
- by move/(map_f (fun x => x.1)) => HH; case/negP: F2.
- by rewrite flipK /lit_is_strue E.
by apply: lit_is_strueW.
by rewrite /lit_is_true lit_get_flip E.
apply: iH.
by apply: valid_add_true_rev => //; apply/eqP.
apply: iH.
by apply: valid_add_true => //; [rewrite /lit_is_true E | rewrite E1].
Qed.
(* Compute the number of iterations that are needed to end the computation *)
Definition mweight m (s : seq (lit * seq lit)) :=
\sum_(i <- s) (size i.2).+1 +
\sum_(l | (l \notin [seq i.1 | i <- s]) &&
((lit_get m l == None) || (lit_get m l == Some (false, false))))
(size (inext l)).+1.
Lemma mweight_lt1 b m l ls s :
valid m ((l, ls) :: s) -> lit_get m l = Some (b, false) ->
mweight m s < mweight m ((l, ls) :: s).
Proof.
move=> Hv Hg.
rewrite /mweight /= big_cons.
set n1 := \sum_(j <- s) _; set n2 := \sum_(j | _) _; set n3 := \sum_(j | _) _.
suff->: n3 = n2.
by rewrite !addSn ltnS -!addnA leq_addl.
apply: eq_bigl => l1; rewrite inE negb_or.
case: (l1 =P l) => [->|//].
rewrite Hg //=.
have : lit_is_true m l || lit_is_strue m (flip l).
have [[_ _ _ HH] _ _ _] := Hv.
by apply: HH; rewrite inE eqxx.
rewrite /lit_is_true /lit_is_strue lit_get_flip Hg.
by case: (b); rewrite //= andbF.
Qed.
Lemma mweight_lt2 m l ls s :
valid m ((l, ls) :: s) -> lit_get m l = None ->
mweight m s < mweight m ((l, ls) :: s).
Proof.
move=> Hv Hg.
rewrite /mweight /= big_cons.
set n1 := \sum_(j <- s) _; set n2 := \sum_(j | _) _; set n3 := \sum_(j | _) _.
suff->: n3 = n2.
by rewrite !addSn ltnS -addnA leq_addl.
apply: eq_bigl => l1; rewrite inE negb_or.
case: (l1 =P l) => [->|//].
rewrite Hg //=.
have : lit_is_true m l || lit_is_strue m (flip l).
have [[_ _ _ HH1] _ _ _] := Hv.
by apply: HH1; rewrite inE eqxx.
by rewrite /lit_is_true /lit_is_strue lit_get_flip Hg.
Qed.
Lemma mweight_lt3 m b l s :
valid m ((l, [::]) :: s) -> lit_get m l = Some (b, true) ->
mweight m s < mweight m ((l, [::]) :: s).
Proof.
move=> Hv Hg.
rewrite /mweight /= big_cons.
set n1 := \sum_(j <- s) _; set n2 := \sum_(j | _) _; set n3 := \sum_(j | _) _.
suff->: n3 = n2 by [].
apply: eq_bigl => l1; rewrite inE negb_or.
case: (l1 =P l) => [->|//].
by rewrite Hg //=; case: (b); rewrite andbF.
Qed.
Lemma mweight_lt4 m l l1 ls1 s (m1 := lit_set m l1 (Some (true, true))) :
valid m1 [:: (l1, inext l1), (l, ls1) & s] ->
lit_get m l1 = Some (false, false) ->
mweight m1 [:: (l1, inext l1), (l, ls1) & s] <
mweight m ((l, l1 :: ls1) :: s).
Proof.
move=> Hv Hg.
rewrite /mweight /= !big_cons /=.
set n1 := \sum_(j <- s) _; set n2 := \sum_(j | _) _; set n3 := \sum_(j | _) _.
rewrite {n3}[n3](bigD1 l1) /=; last first.
rewrite Hg andbT.
by have [[/= /andP[HH _] _ _ _] _ _ _] := Hv.
set n3 := \sum_(j | _) _.
suff->: n2 = n3.
rewrite !(addSn, addnS, addnA) ltnS.
by rewrite [_ + size (inext l1)]addnC addnA.
apply: eq_bigl => l2; rewrite inE negb_or.
have [->|->|[Dl2l1 Dl2fl1]] := lit_dec l2 l1.
- by rewrite eqxx andbF.
- by rewrite !lit_get_flip Hg lit_set_eq /= !andbF.
by rewrite lit_set_neq // Dl2l1 /= andbT.
Qed.
Lemma mweight_lt5 m b l l1 ls1 s (m1 := lit_set m l1 (Some (b, true))) :
valid m1 [:: (l1, inext l1), (l, ls1) & s] ->
lit_get m l1 = None ->
mweight m1 [:: (l1, inext l1), (l, ls1) & s] < mweight m ((l, l1 :: ls1) :: s).
Proof.
move=> Hv Hg.
rewrite /mweight /= !big_cons /=.
set n1 := \sum_(j <- s) _; set n2 := \sum_(j | _) _; set n3 := \sum_(j | _) _.
rewrite {n3}[n3](bigD1 l1) /=; last first.
rewrite Hg andbT.
by have [[/= /andP[HH _] _ _ _] _ _ _] := Hv.
set n3 := \sum_(j | _) _.
suff FF : n2 <= n3.
rewrite !(addSn, addnS, addnA) ltnS.
rewrite [_ + size (inext l1)]addnC addnA.
by rewrite !ltnS leq_add2l.
have [H1|] := boolP ((flip l1 \in l :: [seq i.1 | i <- s]) || ~~b).
suff->: n2 = n3 by [].
apply: eq_bigl => l2; rewrite inE negb_or.
have [->|->|[Dl2l1 Dl2fl1]] := lit_dec l2 l1.
- by rewrite eqxx andbF.
- rewrite !lit_get_flip Hg lit_set_eq /= .
by case: (_ \in _) H1 => //; case: (b); rewrite ?andbF flip_neq.
by rewrite lit_set_neq // Dl2l1 andbT.
rewrite negb_or negbK !inE negb_or => /andP[/andP[H1 H2] H3].
rewrite [n3](bigD1 (flip l1)) /=; last first.
rewrite lit_get_flip Hg !inE negb_or H1 H2 //=.
by case: (l1) => [] [].
set n4 := \sum_(j | _) _.
suff->: n4 = n2 by apply: leq_addl.
apply: eq_bigl => l2; rewrite inE negb_or.
have [->|->|[Dl2l1 Dl2fl1]] := lit_dec l2 l1.
- by rewrite Hg !inE !eqxx !negb_or //= andbF.
- by rewrite !lit_get_flip lit_set_eq /= H3 eqxx !andbF.
rewrite !inE (negPf Dl2l1) !negb_or !andbT lit_set_neq //=.
by rewrite Dl2fl1 andbT.
Qed.
Lemma mweight_init m l l1 (m1 := lit_set m l1 (Some (false, true))) :
valid m1 [:: (l1, inext l1)] ->
lit_get m l1 = None ->
mweight m1 [:: (l1, inext l1)] = mweight m [::].
Proof.
move=> Hv Hg.
rewrite /mweight /= !big_cons /= big_nil.
set n1 := \sum_(j | _) _; set n2 := \sum_(j | _) _.
rewrite {n2}[n2](bigD1 l1) /=; last first.
by rewrite Hg.
set n2 := \sum_(j | _) _.
rewrite {n2}[n2](bigD1 (flip l1)) /=; last first.
rewrite lit_get_flip Hg /=.
by case: (l1) => [] [].
rewrite {n1}[n1](bigD1 (flip l1)) /=; last first.
rewrite lit_get_flip lit_set_eq //= inE eqxx andbT.
by case: (l1) => [] [].
set n1 := \sum_(j | _) _; set n2 := \sum_(j | _) _.
rewrite !(addSn, addnS, addn0, add0n).
congr (_ + (_ + _)).+2.
apply: eq_bigl => l2.
have [->|->|[Dl2l1 Dl2fl1]] := lit_dec l2 l1.
- by rewrite inE eqxx andbF.
- by rewrite eqxx !andbF.
by rewrite !inE Dl2l1 lit_set_neq ?andbT.
Qed.
Lemma valid_propage_none n m s :
valid m s -> mweight m s < n -> propagate n m s != None.
Proof.
elim: n m s => //= n iH m [|[l ls] s HH VV] //=.
rewrite ltnS in VV.
case E : lit_get => [[b []]|]; last 2 first.
- apply: iH => //.
apply: valid_cons HH _.
by rewrite /lit_is_true /= E.
apply: leq_trans VV.
by apply: mweight_lt1 E.
- apply: iH => //.
apply: valid_cons HH _.
by rewrite /lit_is_true /= E.
apply: leq_trans VV.
by apply: mweight_lt2 E.
case: ls HH VV => [Hv|l1 ls1 Hv] VV.
apply: iH.
by apply: valid_cons_nil Hv.
apply: leq_trans VV.
by apply: mweight_lt3 E.
case E1 : lit_get => [[b1 []]|] //.
- apply: iH.
- apply: valid_cons_true Hv _ _.
by rewrite /lit_is_true E.
- by rewrite /lit_is_true E1.
by move: VV; rewrite /mweight /= !big_cons //.
- case: b1 E1 => // E1.
have Va :
valid (lit_set m l1 (Some (true, true))) [:: (l1, inext l1), (l, ls1) & s]
by apply: valid_add_true_rev => //; apply/eqP.
apply: iH => //.
apply: leq_trans VV.
by apply: mweight_lt4 E1.
have Va :
valid (lit_set m l1 (Some (b, true))) [:: (l1, inext l1), (l, ls1) & s].
by apply: valid_add_true => //; [rewrite /lit_is_true E | rewrite E1].
apply: iH => //.
apply: leq_trans VV.
by apply: mweight_lt5 E1.
Qed.
Lemma valid_propage_red n k m m1 s :
valid m s -> propagate n m s = Some (true, k, m1) ->
mweight m s < n -> mweight m1 [::] < k.
Proof.
elim: n k m m1 s => //= n iH k m m1 [|[l ls] s HH PP VV] //=.
by move=> H1 [<- <-].
rewrite ltnS in VV.
case E : lit_get PP => [[b []]|] PP; last 2 first.
- apply: iH PP _ => //.
apply: valid_cons HH _.
by rewrite /lit_is_true /= E.
apply: leq_trans VV.
by apply: mweight_lt1 E.
- apply: iH PP _ => //.
apply: valid_cons HH _.
by rewrite /lit_is_true /= E.
apply: leq_trans VV.
by apply: mweight_lt2 E.
case: ls HH VV PP => [Hv|l1 ls1 Hv] VV PP.
apply: iH PP _.
by apply: valid_cons_nil Hv.
apply: leq_trans VV.
by apply: mweight_lt3 E.
case E1 : lit_get PP => [[b1 []]|] PP //.
- apply: iH PP _.
- apply: valid_cons_true Hv _ _.
by rewrite /lit_is_true E.
- by rewrite /lit_is_true E1.
by move: VV; rewrite /mweight /= !big_cons.
- case: b1 E1 PP => // E1 PP.
have Va :
valid (lit_set m l1 (Some (true, true))) [:: (l1, inext l1), (l, ls1) & s]
by apply: valid_add_true_rev => //; apply/eqP.
apply: iH (Va) _ _ => //.
apply: leq_trans VV.
by apply: mweight_lt4 E1.
have Va :
valid (lit_set m l1 (Some (b, true))) [:: (l1, inext l1), (l, ls1) & s].
by apply: valid_add_true => //; [rewrite /lit_is_true E | rewrite E1].
apply: iH (Va) _ _ => //.
apply: leq_trans VV.
by apply: mweight_lt5 E1.
Qed.
Lemma propage_reduce_none n k m m1 s l :
propagate n m s = Some (true, k, m1) ->
lit_get m1 l = None -> lit_get m l = None.
Proof.
elim: n m m1 s => //= n iH m m1[|[l1 ls] s] //=.
by move=> [_ <-].
case E : lit_get => [[b []]|]; last 2 first.
- by apply: iH.
- by apply: iH.
case: ls => [|l2 ls1].
by apply: iH.
case E1 : lit_get => [[[] []]|] //.
- by apply: iH.
- by apply: iH.
- move=> H1 H2.
have := iH _ _ _ H1 H2.
have [->|->|[Dll2 Dlfl2]] := lit_dec l l2.
- by rewrite lit_set_eq.
- by rewrite lit_get_flip lit_set_eq.
by rewrite lit_set_neq.
move=> H1 H2.
have := iH _ _ _ H1 H2.
have [->|->|[Dll2 Dxfl2]] := lit_dec l l2.
- by rewrite lit_set_eq.
- by rewrite lit_get_flip lit_set_eq.
by rewrite lit_set_neq.
Qed.
(* Set the unset variable to true and propagate *)
Fixpoint check_satl m n ls :=
if ls is l :: ls1 then
if lit_get m l is None then
let m1 := lit_set m l (Some (false, true)) in
if propagate n m1 [:: (l, inext l)] is Some (true, n2, m2) then
check_satl m2 n2 ls1
else None
else check_satl m n ls1
else Some m.
Lemma check_satl_correct m n ls :
mweight m [::] < n -> valid m [::] ->
if check_satl m n ls is Some m1 then
[/\ valid m1 [::],
forall l, l \in ls -> lit_get m1 l != None &
forall l, lit_get m1 l = None -> lit_get m l = None]
else exists l, lit_cycle l /\ lit_cycle (flip l).
Proof.
elim: ls m n => //= l ls1 IH m n Hms Hv.
case E: lit_get => [bb|].
have := IH _ _ Hms Hv.
case: check_satl => // m1 [H1 H2 H3]; split => // l1.
rewrite inE => /orP[/eqP->|/H2] //.
by apply/eqP=> /H3; rewrite E.
set M := lit_set _ _ _.
have Mv : valid M [:: (l, inext l)] by apply: valid_init.
have Mms : mweight M [:: (l, inext l)] < n by rewrite mweight_init.
case E1 : propagate => [[[[] n1] m1]|].
- have F : valid m1 [::] by apply: valid_propage_true Mv E1.
have G : mweight m1 [::] < n1 by apply: valid_propage_red E1 _.
have := IH _ _ G F.
case: check_satl => // m2 [H1 H2 H3]; split => // l1.
rewrite inE => /orP[/eqP->|/H2] //.
apply/eqP=> /H3 /(propage_reduce_none _ _ _ _ _ _ E1).
by rewrite lit_set_eq.
move/H3/(propage_reduce_none _ _ _ _ _ _ E1).
have [->|->|[Dl1l Dl1fl]] := lit_dec l1 l.
- by rewrite lit_set_eq.
- by rewrite lit_get_flip lit_set_eq.
by rewrite lit_set_neq.
- by apply: valid_propage_false Mv E1.
have : propagate n M [:: (l, inext l)] != None.
by apply: valid_propage_none.
by rewrite E1.
Qed.
(* Top function *)
Definition check_sat :=
let m := [ffun x => None] in
let n := mweight m [::] in
check_satl m n.+1 [seq (true, v) | v <- enum var].
Definition valuation := {ffun var -> bool}.
Definition eval (val : valuation) l :=
if l.1 then val l.2 else ~~ val l.2.
Lemma eval_flip val l : eval val (flip l) = ~~ eval val l.
Proof.
by case: l => [] [] v //=; rewrite /eval //= negbK.
Qed.
Definition satisfiable :=
[exists val : valuation,
forall cl, (cl \in cls) ==> (eval val cl.1 || eval val cl.2)].
Lemma check_sat_correct : satisfiable = check_sat.
Proof.
rewrite /check_sat.
set m := [ffun x => None].
set n := mweight _ _.
set ls := [seq _ | _ <- _].
have V : valid m [::].
by split => // [[[] b1]|[[] b1] l1 _ _];
rewrite /lit_is_true /lit_is_strue /lit_get ffunE.
have := check_satl_correct m n.+1 ls (leqnn _) V.
case: check_satl => [m1 [H1m H2m H3m]|HH] /=.
apply/idP/existsP.
pose M := [ffun v => (odflt (false, false) (m1 v)).2].
have F1 l : lit_get m1 l != None.
case: l => [b v].
have F2 : lit_get m1 (true, v) != None.
by apply: H2m; apply: map_f => //; rewrite mem_enum.
case: b; rewrite ?(lit_get_flip _ (true, v)) //.
by case: lit_get F2.
have HM l : eval M l = lit_is_true m1 l.
have := F1 l.
by case: l => [[] v];
rewrite /M /eval /lit_is_true /lit_get /= ffunE; case: (m1 _).
exists M.
apply/forallP => [[l1 l2]]; apply/implyP => H1 /=.
rewrite !HM.
have F : l2 \in inext (flip l1).
by rewrite [_ \in _](rgraphK) /= flipK H1.
case E: lit_is_true => //=.
have [_ _ _ HH] := H1m.
apply: HH F _ => //.
by move: E (F1 l1); rewrite /lit_is_true lit_get_flip;
case: lit_get => //= [[[] []]].
apply/idP/negP; rewrite negb_exists; apply/forallP=> /= m1.
rewrite negb_forall; apply/negP=> /forallP /= HF.
have F l1 l2 : l1 [->] l2 -> eval m1 l1 -> eval m1 l2.
by move => /orP[] /(implyP (HF _)) /=;
rewrite eval_flip; do 2 case: eval.
have G l1 l2 : connect imply l1 l2 -> eval m1 l1 -> eval m1 l2.
move=> /connectP [p e_p ->].
elim: p l1 e_p => //= l ls1 IH l1 /andP[/F oH /IH oH1] eH.
by apply/oH1/oH.
case: HH => l [/G H1 /G H2].
move: H1 H2; rewrite flipK eval_flip.
case: eval => //= H1 H2.
by have: false by apply: H2.
by have: false by apply: H1.
Qed.
End TwoSat.
Section MWeightInit.
Variable var : finType.
Lemma card_l : #|[finType of (bool * var)]| = 2 * #|var|.
Proof. by rewrite eq_card_prod //= card_bool. Qed.
Lemma inext_nil l : inext var [::] l = [::].
Proof.
case E : (inext var [::] l) => [|l1 ls] //.
have: l1 \in inext var [::] l by rewrite E inE eqxx.
by rewrite [_ \in _]rgraphK.
Qed.
Lemma card_inext_size cls l : #|inext var cls l| = size (inext var cls l).
Proof.
by rewrite -cardE; apply: eq_card => l1 //=; rewrite [_ \in _]rgraphK.
Qed.
Lemma inext_incr_l cls l1 l2 :
#|inext var ((l1, l2) :: cls) (flip _ l1)| <= #|inext var cls (flip _ l1)|.+1.
Proof.
rewrite (cardD1 l2) /= [_ \in _]rgraphK /imply /= flipK inE eqxx /= ltnS.
apply: subset_leq_card; apply/subsetP => i.
rewrite !inE ![_ \in _]rgraphK /= flipK !inE !xpair_eqE eqxx /=.
case: eqP => //= H1.
case: (_ \in _) => //=.
case: (_ \in _) => //=; rewrite orbF.
by case: eqP => //= <-; case: eqP.
Qed.
Lemma inext_incr_r cls l1 l2 :
#|inext var ((l1, l2) :: cls) (flip _ l2)| <= #|inext var cls (flip _ l2)|.+1.
Proof.
rewrite (cardD1 l1) /= [_ \in _]rgraphK /imply /= flipK !inE eqxx /= orbT ltnS.
apply: subset_leq_card; apply/subsetP => i.
rewrite !inE ![_ \in _]rgraphK /= flipK !inE !xpair_eqE eqxx /=.
case: eqP => //= H1.
case: (_ \in _) => //=.
case: (_ \in _) => //=; rewrite orbF.
by case: eqP => //= ->; case: eqP.
Qed.
Lemma inext_same cls l l1 l2 :
l != flip _ l1 -> l != flip _ l2 ->
#|inext var ((l1, l2) :: cls) l| = #|inext var cls l|.
Proof.
move=> H1 H2.
apply: eq_card => l3.
rewrite ![_ \in _]rgraphK /imply /= !inE !xpair_eqE.
case: eqP => [HH|_ /=]; first by rewrite -HH flipK eqxx in H1.
case: (_ =P l2) => [HH|_ /=]; first by rewrite -HH flipK eqxx in H2.
by rewrite andbF.
Qed.
(* Show that the complexity is linear *)
Lemma check_sat_mweight cls :
mweight var cls [ffun _ => None] [::] <= 2 * (size cls + #|var|).
Proof.
rewrite /mweight /=.
rewrite big_nil add0n.
set s := \sum_(l | _) _.
have {s}->: s = \sum_l (size (inext var cls l)).+1.
by apply: eq_bigl => [[[] v]] /=; rewrite /lit_get /= ffunE.
elim: cls => /= [|[l1 l2] cls IH].
set s := \sum_(l | _) _.
have {s}->: s = \sum_(l : (bool * var)) 1.
by apply: eq_bigr => l _; rewrite inext_nil.
by rewrite sum1_card /= card_l.
rewrite !addSn mulnS !addSn add0n.
apply: leq_trans (_ : (\sum_l (size (inext var cls l)).+1).+1 < _); last first.
by rewrite !ltnS.
rewrite (bigD1 (flip _ l1)) //=.
have [/eqP<-|Dl1l2] := boolP (l1 == l2).
rewrite [X in _ <= X.+2](bigD1 (flip _ l1)) //= -!card_inext_size.
set s1 := \sum_(l | _) _; set s2 := \sum_(l | _) _.
have {s2}->: s2 = s1.
apply: eq_bigr => /= l3 Hl3.
by rewrite -!card_inext_size inext_same.
rewrite -!addSn leq_add2r ltnS ltnW // ltnS.
by apply: inext_incr_l.
have F : flip _ l2 != flip _ l1.
by apply: contra Dl1l2 => HH; rewrite -(flipK _ l2) (eqP HH) flipK.
rewrite (bigD1 (flip _ l2)) //=.
rewrite [X in _ <= X.+2](bigD1 (flip _ l1)) //= -addSn.
rewrite [X in _ <= (_ + X).+1](bigD1 (flip _ l2)) //= !addnA -addSn.
set s1 := \sum_(l | _) _; set s2 := \sum_(l | _) _.
have {s2}->: s2 = s1.
apply: eq_bigr => /= l3 /andP[H1l3 H2l3].
by rewrite -!card_inext_size inext_same.
rewrite leq_add2r -addnS.
apply: leq_add; rewrite ltnS -!card_inext_size.
by apply: inext_incr_l.
by apply: inext_incr_r.
Qed.
End MWeightInit.
Require Import path fingraph.
Section TwoSat.
(* The set of variables *)
Variable var : finType.
Implicit Type v : var.
(* A litteral is a signed variable *)
Notation lit := (bool * var)%type.
Implicit Type l : lit.
Definition flip l := (~~ l.1, l.2).
Lemma flipK : cancel flip flip.
Proof. by do 2 case. Qed.
Lemma flip_neq l : flip l != l.
Proof. by case: l => [] []. Qed.
(* A clause is a pair of litterals *)
Local Notation clause := (lit * lit)%type.
Implicit Type cl : clause.
(* Clauses are sequences of clauses *)
Local Notation clauses := (seq clause).
Implicit Type cls : clauses.
(* An assignment is a function for var to bool *)
Local Notation val := (option (bool * bool)).
Local Notation mem:= {ffun var -> val}.
Implicit Types m : mem.
(* The list of clauses *)
Variable cls : clauses.
(* Implication between literals *)
Definition imply := [rel a b | ((flip a, b) \in cls) || ((b, flip a) \in cls)].
Notation " a [->] b " := (imply a b) (at level 40).
Lemma imply_flip l1 l2 : flip l1 [->] flip l2 = l2 [->] l1.
Proof. by rewrite /imply /= flipK orbC. Qed.
Lemma path_flip l1 l2 p :
path imply (flip l1) (rcons p (flip l2)) =
path imply l2 (rcons (map flip (rev p)) l1).
Proof.
elim: p l1 l2 => [l1 l2 /=|l p IH l1 l2].
by (rewrite !andbT; exact: imply_flip).
rewrite /= -{3}(flipK l) IH rev_cons map_rcons [X in _ = X]rcons_path andbC.
by rewrite last_rcons -{3}(flipK l1) imply_flip.
Qed.
Lemma connect_flip l1 l2 :
connect imply (flip l1) (flip l2) = connect imply l2 l1.
Proof.
apply/connectP/connectP => [] [p e_p e_f].
elim/last_ind: p e_p e_f => //= [_ /(can_inj flipK)->|p l3 _ e_p e_f].
by exists [::].
exists (rcons (map flip (rev p)) l1); rewrite last_rcons in e_f.
by rewrite -path_flip e_f.
by rewrite last_rcons.
elim/last_ind: p e_p e_f => //= [_ ->|p l3 _ e_p e_f]; first by exists [::].
exists (rcons (map flip (rev p)) (flip l2)); rewrite last_rcons in e_f.
by rewrite -path_flip !flipK e_f.
by rewrite last_rcons.
Qed.
(* Flip value *)
Definition vflip (x : val) : val :=
omap (fun x => (x.1, negb x.2)) x.
Lemma vflipK : cancel vflip vflip.
Proof. by move=> [] // [] [] []. Qed.
(* Getting the value of a literal *)
Definition lit_get m l : val := if l.1 then m l.2 else vflip (m l.2).
Lemma lit_get_flip m l : lit_get m (flip l) = vflip (lit_get m l).
Proof. by case: l => [] // [] b; rewrite /lit_get /= ?vflipK. Qed.
(* Setting the value of a literal *)
Definition lit_set m l r : mem :=
[ffun x => if x == l.2 then if l.1 then r else vflip r
else m x].
Lemma lit_set_eq m l x : lit_get (lit_set m l x) l = x.
Proof.
by rewrite /lit_get /lit_set !ffunE eqxx; case: l.1; rewrite ?vflipK.
Qed.
Lemma lit_set_neq m l1 l2 x : l2 != l1 -> l2 != flip l1 ->
lit_get (lit_set m l1 x) l2 = lit_get m l2.
Proof.
by ((case: l1 => [[] v1]; case: l2 => [[] v2];
rewrite /lit_set /lit_get !ffunE //=; case: (v2 =P v1))
=> //->) => [|_|_|] /negP[].
Qed.
(* The list of literals implied by a literal *)
Definition inext : lit -> seq lit := rgraph imply.
Lemma inext_flip l1 l2 :
flip l1 \in inext (flip l2) = (l2 \in inext l1).
Proof. by rewrite  imply_flip. Qed.
Lemma inext_imply l l1 : l1 \in inext l = l [->] l1.
Proof. by rewrite [_ \in _]rgraphK. Qed.
(* The propagation algorithm *)
Fixpoint propagate n m s :=
if n is n1.+1 then
if s is (l, ls) :: s1 then
if lit_get m l is Some (b1, true) then
(* We check that l is still set to true not to propagate
wrong values. Example:
A -> {~B, E, B}, ~A -> {}, B -> {A}, ~B -> {~E, A}, E -> {B}, ~E -> {~A}
*)
if ls is l1 :: ls1 then
if lit_get m l1 is Some (b, v) then
if v then propagate n1 m ((l, ls1) :: s1)
else
if b then Some (false, n1.+1, m)
else
let m1 := lit_set m l1 (Some (true, true)) in
propagate n1 m1 [:: (l1, inext l1), (l, ls1) & s1]
else
let m1 := lit_set m l1 (Some (b1, true)) in
propagate n1 m1 [:: (l1, inext l1), (l, ls1) & s1]
else propagate n1 m s1
else propagate n1 m s1
else Some (true, n1.+1, m)
else None.
(* Check if a literal is true *)
Definition lit_is_true m l := oapp (fun x => x.2) false (lit_get m l).
Lemma lit_is_true_set_eq m x l :
lit_is_true (lit_set m l x) l = oapp (fun x => x.2) false x.
Proof. by rewrite /lit_is_true lit_set_eq. Qed.
Lemma lit_is_true_flip m l : lit_is_true m (flip l) -> ~~ lit_is_true m l.
Proof. by rewrite /lit_is_true lit_get_flip; case: lit_get => // [[[] []]]. Qed.
Lemma lit_is_true_set_eq_flip m x l :
lit_is_true (lit_set m l x) (flip l) = oapp (fun x => x.2) false (vflip x).
Proof. by rewrite /lit_is_true lit_get_flip lit_set_eq. Qed.
Lemma lit_is_true_set_neq m x l1 l2 :
l2 != l1 -> l2 != flip l1 ->
lit_is_true (lit_set m l1 x) l2 = lit_is_true m l2.
Proof. by move=> H1 H2; rewrite /lit_is_true lit_set_neq. Qed.
Lemma lit_is_true_set_neq_flip m x l1 l2 :
l2 != l1 -> l2 != flip l1 ->
lit_is_true (lit_set m l1 x) (flip l2) = lit_is_true m (flip l2).
Proof.
by move=> H1 H2; rewrite /lit_is_true lit_get_flip lit_set_neq // lit_get_flip.
Qed.
Lemma lit_is_true_set_flip m b l l1 :
lit_is_true (lit_set m l (Some (b, true))) l1 -> l1 != flip l.
Proof.
move=> H; apply/eqP => El1fl.
by move: H; rewrite El1fl lit_is_true_set_eq_flip.
Qed.
(* Check if a literal is strongly true, i.e. its value can't be changed *)
Definition lit_is_strue m l := oapp (fun x => x.2 && x.1) false (lit_get m l).
Lemma lit_is_strueW m l : lit_is_strue m l -> lit_is_true m l.
Proof.
by rewrite /lit_is_true /lit_is_strue; case: lit_get => // [] [[] []].
Qed.
Lemma lit_is_strue_set_eq m x l :
lit_is_strue (lit_set m l x) l = oapp (fun i => i.1 && i.2) false x.
Proof. by rewrite /lit_is_strue lit_set_eq; case: x => // [[[] []]]. Qed.
Lemma lit_is_strue_set_eq_flip m x l :
lit_is_strue (lit_set m l x) (flip l) = oapp (fun i => i.1 && ~~ i.2) false x.
Proof.
by rewrite /lit_is_strue lit_get_flip lit_set_eq; case: x => // [[[] []]].
Qed.
Lemma lit_is_strue_set_neq m x l1 l2 :
l2 != l1 -> l2 != flip l1 ->
lit_is_strue (lit_set m l1 x) l2 = lit_is_strue m l2.
Proof. by move=> H1 H2; rewrite /lit_is_strue lit_set_neq. Qed.
Lemma lit_is_strue_set_neq_flip m x l1 l2 :
l2 != l1 -> l2 != flip l1 ->
lit_is_strue (lit_set m l1 x) (flip l2) = lit_is_strue m (flip l2).
Proof.
by move=> H1 H2; rewrite /lit_is_strue lit_get_flip lit_set_neq // lit_get_flip.
Qed.
Lemma lit_is_strue_set_flip m b l l1 :
lit_is_strue (lit_set m l (Some (b, true))) l1 -> l1 != flip l.
Proof.
move=> H; apply/eqP => El1fl.
by move: H; rewrite El1fl lit_is_strue_set_eq_flip /= andbF.
Qed.
(* l has an implication cycle, so it must be true *)
Definition lit_cycle l := connect imply (flip l) l.
Lemma lit_cycle_inext l l1 :
l1 \in inext l -> lit_cycle l -> lit_cycle l1.
Proof.
move=> Il1 Cl.
have Coll1 : connect imply l l1 by apply: connect1; rewrite -inext_imply.
have Cofl1fl : connect imply (flip l1) (flip l).
by apply: connect1; rewrite -inext_imply inext_flip.
apply: connect_trans Coll1.
by apply: connect_trans Cofl1fl _.
Qed.
(* Stack is composed of an implication *)
Definition istack s := if rev s is l :: ls then path imply l ls else true.
Lemma istack_cons l l1 ls :
istack (l :: ls) -> l1 \in inext l -> istack [:: l1, l & ls].
Proof.
rewrite inext_imply /istack !rev_cons; case: rev => /= [|l2 ls1 H1 H2].
by rewrite andbT.
by rewrite rcons_path H1 last_rcons.
Qed.
Lemma istack_consE l ls : istack (l :: ls) -> istack ls.
Proof.
rewrite /istack rev_cons; case: rev => //= l2 ls1.
by rewrite rcons_path => /andP[].
Qed.
Lemma path_head_connect (A : finType) (r : rel A) (a b c : A) p :
path r a (rcons p b) -> c \in (a :: p) -> connect r c b.
Proof.
elim: p a c => /= [a c | d p IH a c].
by rewrite inE andbT => H /eqP->; apply: connect1.
rewrite inE => /andP[H1 H2] /orP[/eqP->|]; last by exact: IH.
apply: connect_trans (connect1 H1) _.
by apply/connectP; exists (rcons p b) => //; rewrite last_rcons.
Qed.
Lemma mem_istack l l1 ls :
istack (l :: ls) -> l1 \in l :: ls -> connect imply l1 l.
Proof.
rewrite inE => H1 /orP[/eqP->//|H2].
have : l1 \in rev ls by rewrite mem_rev.
move : H1; rewrite /istack rev_cons; case: rev => //= l2 ls1 H3 H4.
by apply: path_head_connect H4.
Qed.
(* Ordered stack, i.e. strong values are at the top of the stack *)
Definition ostack m (s : seq lit) (s1 := [seq x <- s | lit_is_true m x]) :=
s1 = [seq x <- s1 | lit_is_strue m x] ++ [seq x <- s1 | ~~ lit_is_strue m x].
Lemma ostackE m l s : ostack m (l :: s) -> ostack m s.
Proof.
rewrite /ostack /=.
case Ll : lit_is_true => //=.
case Sl : lit_is_strue => /=; first by case.
case Es : [seq _ <- [seq _ <- _ | _]| _] => /= [|l1 s1]; first by case.
case => El.
have: l1 \in l1 :: s1 by rewrite inE eqxx.
by rewrite -Es -El mem_filter Sl.
Qed.
Lemma ostack_neg_lit_is_strue m l1 l2 s :
lit_is_true m l1 -> ~~ lit_is_strue m l1 ->
ostack m (l1 :: s) -> l2 \in (l1 :: s) -> ~~ lit_is_strue m l2.
Proof.
move=> Ll1 Sl1.
rewrite /ostack inE /= Ll1 /= Sl1 (negPf Sl1) => El1s /orP[/eqP->//|l2Is].
apply/negP => Sl2; move: El1s.
set d := [seq x <- [seq x <- s | _] | _].
have: l2 \in d by rewrite !mem_filter Sl2 lit_is_strueW.
case Ed : d => [|l3 ls3] //= l2Il2 [] El1l3.
have: l1 \notin d by rewrite mem_filter negb_and Sl1.
by rewrite Ed -El1l3 inE eqxx.
Qed.
Lemma ostack_strue m l s :
lit_is_strue m l -> ostack m s -> ostack m (l :: s).
Proof.
by move=> Sl; rewrite /ostack /= (lit_is_strueW _ _ Sl) /= Sl /= => <-.
Qed.
Lemma filter_cons (T : Type) (p : pred T) (s : seq T) x:
filter p (x :: s) = if p x then x :: filter p s else filter p s.
Proof. by []. Qed.
Lemma ostack_same m l1 l2 s :
lit_get m l1 = lit_get m l2 ->
ostack m (l1 :: s) -> ostack m (l2 :: l1 :: s).
Proof.
move=> Egl1gl2; rewrite /ostack !filter_cons.
have ETl1Tl2 : lit_is_true m l1 = lit_is_true m l2.
by rewrite /lit_is_true Egl1gl2.
have ESl1Sl2 : lit_is_strue m l1 = lit_is_strue m l2.
by rewrite /lit_is_strue Egl1gl2.
rewrite -ETl1Tl2 /=.
case: lit_is_true => //=.
rewrite -ESl1Sl2.
case E : lit_is_strue => //=; first by move->.
set d := [seq x <- s | lit_is_true m x].
case E1 : [seq x <- d | lit_is_strue m x] => [|l3 d1] //=.
by case=> <-.
case=> El1l3.
have: l1 \in l1 :: d1 by rewrite inE eqxx.
by rewrite El1l3 -E1 mem_filter -El1l3 E.
Qed.
Lemma ostack_weak m1 m2 s :
(forall l, l \in s -> lit_is_true m1 l -> lit_is_true m2 l) ->
(forall l, l \in s -> lit_is_strue m1 l = lit_is_strue m2 l) ->
ostack m2 s -> ostack m1 s.
Proof.
move=> FL FSL.
rewrite /ostack => Om2.
suff {1}-> : [seq x <- s | lit_is_true m1 x] =
[seq x <- [seq x <- s | lit_is_true m1 x] | lit_is_strue m2 x] ++
[seq x <- [seq x <- s | lit_is_true m1 x] | ~~ lit_is_strue m2 x].
by congr (_ ++ _); apply: eq_in_filter=> l;
rewrite mem_filter => /andP[_ HH]; rewrite FSL.
have Hf P :
[seq x <- [seq x <- s | lit_is_true m1 x] | P x] =
[seq x <-
[seq x <- [seq x <- s | lit_is_true m2 x] | P x] | lit_is_true m1 x].
rewrite -!filter_predI.
apply: eq_in_filter=> l lIs /=.
by case: (P _); case: lit_is_true (FL _ lIs); case: lit_is_true => //=
/(_ is_true_true).
rewrite !Hf -filter_cat -Om2 -filter_predI.
apply: eq_in_filter=> l lIs /=.
by case: lit_is_true (FL _ lIs); case: lit_is_true => //= /(_ is_true_true).
Qed.
(* Main invariant *)
Definition valid m (s : seq (lit * seq lit)) :=
[/\
let s1 := [seq i.1 | i <- s] in
[/\ uniq s1, istack s1, ostack m s1 &
forall l, l \in s1 -> lit_is_true m l || lit_is_strue m (flip l)],
forall l, forall ls, (l, ls) \in s -> ls \subset inext l,
forall l, lit_is_strue m l -> lit_cycle l &
forall l1 l2,
(forall ls, (l1, ls) \in s -> l2 \notin ls) ->
(forall ls, lit_is_strue m (flip l2) ->
(flip l2, ls) \in s -> flip l1 \notin ls) ->
l2 \in inext l1 -> lit_is_true m l1 -> lit_is_true m l2].
Definition wf_mem m := forall l1 l2,
l2 \in inext l1 -> lit_is_true m l1 -> lit_is_true m l2.
Lemma wf_nil m : valid m [::] -> wf_mem m.
Proof. by move=> [_ _ _ F] l l1 Tl l1INl; apply: F l1INl. Qed.
Lemma lit_dec l1 l2 : [\/ l1 = l2, l1 = flip l2 | l1 != l2 /\ l1 != flip l2].
Proof.
case: eqP => [->|_]; first by apply: Or31.
by case: eqP => [->|_]; [apply: Or32 | apply: Or33].
Qed.
Lemma valid_init m l (m1 := lit_set m l (Some (false, true))) :
valid m [::] -> lit_get m l = None -> valid m1 [:: (l, inext l)].
Proof.
move=> [_ _ Cl F] Gl.
split=> //= [|l1 ls|l1|l1 l2 D Dr l2INl1 Tm1l1]; first (split => [|||l1] //=).
- by rewrite /ostack /= lit_is_true_set_eq /= lit_is_strue_set_eq.
- by rewrite inE => /eqP->; rewrite lit_is_true_set_eq lit_is_strue_set_eq_flip.
- by rewrite inE xpair_eqE => /andP[/eqP->/eqP->].
- have [->|->| [Dl1l Dl1fl]] := lit_dec l1 l.
- by rewrite lit_is_strue_set_eq.
- by rewrite lit_is_strue_set_eq_flip.
by rewrite lit_is_strue_set_neq //; exact: Cl.
have [El1l|El1fl| [Dl1l Dl1fl]] := lit_dec l1 l.
- have/negP[] : l2 \notin inext l.
by apply: D; rewrite El1l inE eqxx.
by rewrite -El1l.
- by move: Tm1l1; rewrite El1fl lit_is_true_set_eq_flip.
have : lit_is_true m l2.
apply: F l2INl1 _ => //.
by move: Tm1l1; rewrite lit_is_true_set_neq.
have [->|->| [Dl2l Dl2fl]] := lit_dec l2 l.
- by rewrite lit_is_true_set_eq.
- by rewrite /lit_is_true lit_get_flip Gl.
by rewrite lit_is_true_set_neq.
Qed.
Lemma valid_cons m l ls s :
valid m ((l, ls) :: s) -> ~~ lit_is_true m l -> valid m s.
Proof.
move=> [[V1 V2 V3 V4] V5 V6 V7] NTml;
split => [|l1 ls1 Il1||l1 l2 D Dr Tml1 l2INl1] //;
first (split=> [|||l1 l1Is] //).
- by apply: subseq_uniq V1; apply: map_subseq; apply: subseq_cons.
- by apply: istack_consE V2.
- by move: V3; rewrite /ostack /= (negPf NTml).
- by apply: V4; rewrite inE l1Is orbT.
- by apply: V5; rewrite inE Il1 orbT.
have [/eqP El1l | Dl1l] := boolP (l1 == l).
by case/negP:NTml ; rewrite -El1l.
have [/eqP El2l | Dfl2l] := boolP (flip l2 == l).
rewrite -(flipK l2) El2l.
have/V4 : l \in [seq i.1 | i <- (l, ls) :: s] by rewrite /= inE eqxx.
by move: NTml; rewrite /lit_is_true /lit_is_strue lit_get_flip; case: lit_get.
apply: V7 l2INl1 => // [ls1|V ls1];
rewrite inE xpair_eqE ?(negPf Dl1l) ?(negPf Dfl2l) //=.
by apply: D.
by apply: Dr.
Qed.
Lemma valid_cons_nil m l s : valid m ((l, [::]) :: s) -> valid m s.
Proof.
move=> [[V1 V2 V3 V4] V5 V6 V7]; split => [|l1 ls1 Il1||l1 l2 D Dr Tml1 Il1] //;
first (split => [|||l1 Il1]).
- by apply: subseq_uniq V1; apply: map_subseq; apply: subseq_cons.
- by apply: istack_consE V2.
- by apply: ostackE V3.
- by apply: V4; rewrite inE Il1 orbT.
- by apply: V5; rewrite inE Il1 orbT.
apply: V7 Il1 => // [ls|V ls]; rewrite inE xpair_eqE => /orP[/andP[HH/eqP->]|] //.
by apply: D.
by apply: Dr.
Qed.
Lemma valid_cons_true m l l1 ls1 s :
valid m ((l, l1 :: ls1) :: s) ->
lit_is_true m l -> lit_is_true m l1 ->
valid m ((l, ls1) :: s).
Proof.
move=> [[V1 V2 V3 V4] V5 V6 V7] Tml Tml1.
split => [|l2 ls2||l2 l3 D Dr Il3 Tml2] //.
rewrite inE => /orP[/eqP[]->->|Il].
apply: subset_trans (_ : l1 :: ls1 \subset _) => //.
by apply/subsetP=> l3 Il3; rewrite inE Il3 orbT.
by apply: V5; rewrite inE eqxx.
by apply: V5; rewrite inE Il orbT.
have [/eqP->//| Dl3l1] := boolP (l3 == l1).
apply: V7 Il3 _ => // [ls|V ls].
rewrite inE xpair_eqE => /orP[/andP[/eqP El2l /eqP ->]|Il2].
rewrite inE negb_or Dl3l1.
by apply: D; rewrite El2l inE eqxx.
by apply: D; rewrite inE Il2 orbT.
have [/eqP Efl2l1| Dfl2l1] := boolP (flip l2 == l1).
by have := Tml1; rewrite -Efl2l1=> /lit_is_true_flip/negP[].
rewrite inE xpair_eqE => /orP[/andP[/eqP Efl3l /eqP ->]|If].
by rewrite inE negb_or Dfl2l1 //= Dr // inE Efl3l eqxx.
by rewrite Dr // inE If orbT.
Qed.
Lemma valid_add_true m b l l1 ls1 s :
valid m ((l, l1 :: ls1) :: s) ->
lit_get m l == Some (b, true) ->
lit_get m l1 == None ->
valid (lit_set m l1 (Some (b, true))) [:: (l1, inext l1), (l, ls1) & s].
Proof.
move=> [[V1 V2 V3 V4] V5 V6 V7] Gml Gml1.
have [/eqP El1l | Dl1l] := boolP (l1 == l).
by move: Gml Gml1; rewrite El1l => /eqP->.
have l1INl : l1 \in inext l.
have /subsetP->// : (l1 :: ls1) \subset inext l.
by apply: V5; rewrite inE eqxx.
by rewrite inE eqxx.
have Us : uniq [seq i.1 | i <- [:: (l1, inext l1), (l, ls1) & s]].
rewrite map_cons cons_uniq V1 andbT /=.
rewrite inE negb_or (negPf Dl1l).
apply/negP=> Il1.
case: (orP (V4 l1 _)).
- by rewrite map_cons inE Il1 orbT.
- by rewrite /lit_is_true; case: lit_get Gml1 => [[[] []]|].
by rewrite /lit_is_strue lit_get_flip; case: lit_get Gml1 => [[[] []]|].
split => [|l2 ls2|l2|l2 l3 D Dr Il3 Tm1l2] //;
first (split => [|||l2] //=).
- by apply: istack_cons.
- have Dl1fl : l1 != flip l.
by apply/eqP=> HH; move: Gml1; rewrite HH lit_get_flip (eqP Gml).
apply: ostack_same.
rewrite lit_set_eq lit_set_neq ?(eqP Gml) 1?eq_sym //.
by apply: contra Dl1fl => /eqP<-; rewrite flipK.
apply: ostack_weak V3 => [l2 Hl2|l2 Hl2].
have [/eqP El2l| Dl2l1] := boolP (l2 == l1).
move: Hl2 Us; rewrite /= El2l !inE negb_or => /orP[/eqP->//|->//].
by rewrite eqxx.
by rewrite andbF.
move=> HH; move: (HH).
by rewrite lit_is_true_set_neq // (lit_is_true_set_flip _ _ _ _ HH).
have [El2l1|->|[Dl2l1 Dl2fl1]] := lit_dec l2 l1.
- move: Hl2 Us; rewrite /= El2l1 !inE negb_or => /orP[/eqP->//|->//].
by rewrite eqxx.
by rewrite andbF.
- by rewrite /lit_is_strue !lit_get_flip lit_set_eq (eqP Gml1).
by rewrite lit_is_strue_set_neq.
- have [->|->|[Dl2l1 Dl2fl1]] := lit_dec l2 l1.
- by rewrite lit_is_true_set_eq.
- rewrite inE (negPf (flip_neq _)) => /V4.
by rewrite flipK /lit_is_true /lit_is_strue lit_get_flip (eqP Gml1).
rewrite inE (negPf Dl2l1) => /V4.
by rewrite lit_is_true_set_neq // lit_is_strue_set_neq_flip.
- rewrite !inE => /or3P[/eqP[]->->|/eqP[]->->|Il2] //.
apply: subset_trans (_ : l1 :: ls1 \subset _).
by apply/subsetP=> l4; rewrite inE orbC => ->.
by apply: V5; rewrite inE eqxx.
by apply: V5; rewrite inE Il2 orbT.
- have [->|->|[Dl2l1 Dl2fl1]] := lit_dec l2 l1.
- rewrite lit_is_strue_set_eq => /= /andP[B _].
have F : lit_cycle l.
by apply: V6; rewrite /lit_is_strue (eqP Gml).
by apply: lit_cycle_inext F.
- by rewrite lit_is_strue_set_eq_flip /= andbF.
by rewrite lit_is_strue_set_neq //; exact: V6.
have [El2l1|El2fl1|[Dl2l1 Dl2fl1]] := lit_dec l2 l1.
- have: l3 \notin inext l1.
by apply: D; rewrite El2l1 inE eqxx.
by rewrite -El2l1 Il3.
- by move : Tm1l2; rewrite El2fl1 lit_is_true_set_eq_flip.
have Tml2 : lit_is_true m l2.
by move: Tm1l2; rewrite lit_is_true_set_neq.
have [->|El3fl1|[Dl3l1 Dl3fl1]] := lit_dec l3 l1.
- by rewrite lit_is_true_set_eq.
- suff: lit_is_true m l3.
by rewrite El3fl1 /lit_is_true lit_get_flip (eqP Gml1).
apply: V7 Il3 _ => // [ls|].
rewrite El3fl1 !inE xpair_eqE => /orP[/andP[/eqP El2l /eqP->]|Il2].
by rewrite inE negb_or (negPf (flip_neq _)) -El3fl1 D //
El2l !inE eqxx orbT.
by rewrite -El3fl1; apply: D; rewrite !inE Il2 !orbT.
by rewrite El3fl1 flipK /lit_is_strue (eqP Gml1).
rewrite lit_is_true_set_neq //.
apply: V7 Il3 _ => // [ls|HH ls];
rewrite !inE ?xpair_eqE => /orP[/andP[/eqP El /eqP->]|Il].
- by rewrite inE negb_or Dl3l1 D // El !inE eqxx orbT.
- by apply: D; rewrite !inE Il !orbT.
- rewrite inE negb_or Dr ?andbT //.
- by apply: contra Dl2fl1 => /eqP<-; rewrite flipK.
- by rewrite lit_is_strue_set_neq_flip.
by rewrite El !inE eqxx orbT.
apply: Dr; first by rewrite lit_is_strue_set_neq_flip.
by rewrite !inE Il !orbT.
Qed.
Lemma valid_add_true_rev m b l l1 ls1 s :
valid m ((l, l1 :: ls1) :: s) ->
lit_get m l == Some (b, true) ->
lit_get m l1 == Some (false, false) ->
valid (lit_set m l1 (Some (true, true))) [:: (l1, inext l1), (l, ls1) & s].
Proof.
move=> [[V1 V2 V3 V4] V5 V6 V7] Gml Gml1.
have [/eqP El1l | Dl1l] := boolP (l1 == l).
by move: Gml Gml1; rewrite El1l => /eqP->; case: b.
have l1INl : l1 \in inext l.
have /subsetP->// : (l1 :: ls1) \subset inext l.
by apply: V5; rewrite inE eqxx.
by rewrite inE eqxx.
have Us : uniq [seq i.1 | i <- [:: (l1, inext l1), (l, ls1) & s]].
rewrite map_cons cons_uniq V1 andbT /=.
rewrite inE negb_or (negPf Dl1l).
apply/negP=> Il1.
case: (orP (V4 l1 _)).
- by rewrite map_cons inE Il1 orbT.
- by rewrite /lit_is_true; case: lit_get Gml1 => [[[] []]|].
by rewrite /lit_is_strue lit_get_flip; case: lit_get Gml1 => [[[] []]|].
split => [|l2 ls2|l2|l2 l3 D Dr Il3 Tm1l2] //;
first (split => [|||l2] //=).
- by apply: istack_cons.
- apply: ostack_strue; first by rewrite lit_is_strue_set_eq.
apply: ostack_weak V3 => l2 Il2.
have [/eqP El2l1| Dl2l1] := boolP (l2 == l1).
move: Il2 Us; rewrite /= El2l1 !inE negb_or => /orP[/eqP->//|->//].
by rewrite eqxx.
by rewrite andbF.
move=> HH; move: (HH).
by rewrite lit_is_true_set_neq // (lit_is_true_set_flip _ _ _ _ HH).
have [El2l1| ->| [Dl2l1 Dl2fl1]] := lit_dec l2 l1.
- move: Il2 Us; rewrite /= El2l1 !inE negb_or => /orP[/eqP->//|->//].
by rewrite eqxx.
by rewrite andbF.
- by rewrite lit_is_strue_set_eq_flip /lit_is_strue lit_get_flip (eqP Gml1).
by rewrite lit_is_strue_set_neq.
- have [->|->| [Dl2l1 Dl2fl1]] := lit_dec l2 l1.
- by rewrite lit_is_true_set_eq.
- by rewrite flipK lit_is_strue_set_eq orbT.
rewrite inE (negPf Dl2l1) lit_is_true_set_neq //
lit_is_strue_set_neq_flip //=.
by apply: V4.
- rewrite !inE => /or3P[/eqP[]->->|/eqP[]->->|Il2] //.
apply: subset_trans (_ : l1 :: ls1 \subset _).
by apply/subsetP=> l4; rewrite inE orbC => ->.
by apply: V5; rewrite inE eqxx.
by apply: V5; rewrite inE Il2 orbT.
- have [-> _|->|[Dl2l1 Dl2fl1]] := lit_dec l2 l1.
- have F : lit_is_true m (flip l1).
by rewrite /lit_is_true lit_get_flip (eqP Gml1).
have [Ifl1|NIfl1] :=
boolP (flip l1 \in [seq i.1 | i <- (l, l1 :: ls1) :: s]).
apply: connect_trans (_ : connect imply l l1).
by apply: mem_istack V2 _.
by apply: connect1; rewrite -inext_imply.
case: b Gml => Gml.
have : lit_cycle l by apply: V6; rewrite /lit_is_strue (eqP Gml).
by apply: lit_cycle_inext.
have: lit_is_true m (flip l).
apply: V7 F => // [ls Hls||].
by case/negP: NIfl1; apply: map_f Hls.
by rewrite /lit_is_strue flipK (eqP Gml).
by rewrite inext_flip.
by rewrite /lit_is_true lit_get_flip (eqP Gml).
- by rewrite lit_is_strue_set_eq_flip.
by rewrite lit_is_strue_set_neq //; exact: V6.
have [El2l1|El2fl1| [Dl21l Dl2fl1]] := lit_dec l2 l1.
- suff: l3 \notin inext l1 by rewrite -El2l1 Il3.
by apply: D; rewrite inE El2l1 eqxx.
- by move : Tm1l2; rewrite El2fl1 lit_is_true_set_eq_flip.
have Tml2 : lit_is_true m l2 by move: Tm1l2; rewrite lit_is_true_set_neq.
have [->|El3fl1| [Dl3l1 Dl3fl1]] := lit_dec l3 l1.
- by rewrite lit_is_true_set_eq.
- have: flip l2 \notin (inext l1).
apply: Dr; first by rewrite El3fl1 flipK lit_is_strue_set_eq.
by rewrite El3fl1 flipK inE eqxx.
by rewrite -(flipK l1) -El3fl1 inext_flip Il3.
suff: lit_is_true m l3 by rewrite lit_is_true_set_neq.
apply: V7 Il3 _ => // [ls|HH ls].
rewrite !inE xpair_eqE => /orP[/andP[/eqP El2l/eqP->]|Il2].
by rewrite inE negb_or Dl3l1 D // El2l !inE eqxx orbT.
by apply: D; rewrite !inE Il2 !orbT.
rewrite !inE xpair_eqE => /orP[/andP[/eqP Efl3l/eqP->]|Ifl3].
rewrite inE negb_or; apply/andP; split.
by apply: contra Dl2fl1 => /eqP<-; rewrite flipK.
apply: Dr => //.
by rewrite lit_is_strue_set_neq_flip.
by rewrite Efl3l !inE eqxx orbT.
apply: Dr => //.
by rewrite lit_is_strue_set_neq_flip.
by rewrite !inE Ifl3 !orbT.
Qed.
Lemma valid_propage_true n m m1 s k :
valid m s -> propagate n m s = Some (true, k, m1) -> valid m1 [::].
Proof.
elim: n m m1 s => //= n iH m m1 [H1 [_ <-]|[l ls] s1 Vm] //.
case E : lit_get => [[b []]|]; last 2 first.
- apply: iH; apply: valid_cons Vm _.
by rewrite /lit_is_true /= E.
- have [[_ _ _ H] _ _ _] := Vm.
have : l \in [seq i.1 | i <- (l, ls) :: s1] by rewrite inE eqxx.
by move/H; rewrite /lit_is_true /lit_is_strue lit_get_flip E.
case: ls Vm => [Vm|l1 ls1 Vm].
by apply: iH; apply: valid_cons_nil Vm.
case E1 : lit_get => [[b1 []]|] //.
- apply: iH; apply: valid_cons_true Vm _ _.
by rewrite /lit_is_true E.
by rewrite /lit_is_true E1.
- case: b1 E1 => // E1.
apply: iH.
by apply: valid_add_true_rev => //; apply/eqP.
apply: iH.
by apply: valid_add_true => //; [rewrite /lit_is_true E | rewrite E1].
Qed.
Lemma valid_propage_false n m m1 s k :
valid m s -> propagate n m s = Some (false, k, m1) ->
exists l, lit_cycle l /\ lit_cycle (flip l).
Proof.
elim: n m m1 s => //= n iH m m1 [|[l ls] s Vm] //.
case E : lit_get => [[b []]|]; last 2 first.
- apply: iH; apply: valid_cons Vm _.
by rewrite /lit_is_true /= E.
- have [[_ _ _ H] _ _ _] := Vm.
have : l \in [seq i.1 | i <- (l, ls) :: s] by rewrite inE eqxx.
by move/H; rewrite /lit_is_true /lit_is_strue lit_get_flip E.
case: ls Vm => [Vm|l1 ls1 Vm].
by apply: iH; apply: valid_cons_nil Vm.
have X1 : l1 \in inext l.
have/subsetP->// : l1 :: ls1 \subset inext l.
have [_ HH _ _] := Vm.
by apply: HH; rewrite !inE eqxx.
by rewrite inE eqxx.
case E1 : lit_get => [[b1 []]|] //.
- apply: iH; apply: valid_cons_true Vm _ _.
by rewrite /lit_is_true E.
by rewrite /lit_is_true E1.
- case: b1 E1 => // E1.
have F1 : lit_is_strue m (flip l1).
by rewrite /lit_is_strue lit_get_flip E1.
case: b E => E _.
have F : lit_cycle l.
have [_ _ HH _] := Vm.
by apply: HH; rewrite /lit_is_strue E.
exists l1; split; first by apply: lit_cycle_inext F.
have [_ _ HH _] := Vm.
by apply: HH.
have [F2 | F2] := boolP (flip l1 \in [seq i.1 | i <- (l, l1 :: ls1) :: s]).
have [[_ _ HH _] _ _ _] := Vm.
have : ~~ lit_is_strue m (flip l1).
apply: ostack_neg_lit_is_strue HH _ => //=.
- by rewrite /lit_is_true E.
- by rewrite /lit_is_strue E.
by rewrite F1.
have : lit_is_true m (flip l).
have F : flip l \in inext (flip l1) by rewrite inext_flip.
have [_ _ _ HH] := Vm.
apply: HH F _ => // [ls||].
- by move/(map_f (fun x => x.1)) => HH; case/negP: F2.
- by rewrite flipK /lit_is_strue E.
by apply: lit_is_strueW.
by rewrite /lit_is_true lit_get_flip E.
apply: iH.
by apply: valid_add_true_rev => //; apply/eqP.
apply: iH.
by apply: valid_add_true => //; [rewrite /lit_is_true E | rewrite E1].
Qed.
(* Compute the number of iterations that are needed to end the computation *)
Definition mweight m (s : seq (lit * seq lit)) :=
\sum_(i <- s) (size i.2).+1 +
\sum_(l | (l \notin [seq i.1 | i <- s]) &&
((lit_get m l == None) || (lit_get m l == Some (false, false))))
(size (inext l)).+1.
Lemma mweight_lt1 b m l ls s :
valid m ((l, ls) :: s) -> lit_get m l = Some (b, false) ->
mweight m s < mweight m ((l, ls) :: s).
Proof.
move=> Hv Hg.
rewrite /mweight /= big_cons.
set n1 := \sum_(j <- s) _; set n2 := \sum_(j | _) _; set n3 := \sum_(j | _) _.
suff->: n3 = n2.
by rewrite !addSn ltnS -!addnA leq_addl.
apply: eq_bigl => l1; rewrite inE negb_or.
case: (l1 =P l) => [->|//].
rewrite Hg //=.
have : lit_is_true m l || lit_is_strue m (flip l).
have [[_ _ _ HH] _ _ _] := Hv.
by apply: HH; rewrite inE eqxx.
rewrite /lit_is_true /lit_is_strue lit_get_flip Hg.
by case: (b); rewrite //= andbF.
Qed.
Lemma mweight_lt2 m l ls s :
valid m ((l, ls) :: s) -> lit_get m l = None ->
mweight m s < mweight m ((l, ls) :: s).
Proof.
move=> Hv Hg.
rewrite /mweight /= big_cons.
set n1 := \sum_(j <- s) _; set n2 := \sum_(j | _) _; set n3 := \sum_(j | _) _.
suff->: n3 = n2.
by rewrite !addSn ltnS -addnA leq_addl.
apply: eq_bigl => l1; rewrite inE negb_or.
case: (l1 =P l) => [->|//].
rewrite Hg //=.
have : lit_is_true m l || lit_is_strue m (flip l).
have [[_ _ _ HH1] _ _ _] := Hv.
by apply: HH1; rewrite inE eqxx.
by rewrite /lit_is_true /lit_is_strue lit_get_flip Hg.
Qed.
Lemma mweight_lt3 m b l s :
valid m ((l, [::]) :: s) -> lit_get m l = Some (b, true) ->
mweight m s < mweight m ((l, [::]) :: s).
Proof.
move=> Hv Hg.
rewrite /mweight /= big_cons.
set n1 := \sum_(j <- s) _; set n2 := \sum_(j | _) _; set n3 := \sum_(j | _) _.
suff->: n3 = n2 by [].
apply: eq_bigl => l1; rewrite inE negb_or.
case: (l1 =P l) => [->|//].
by rewrite Hg //=; case: (b); rewrite andbF.
Qed.
Lemma mweight_lt4 m l l1 ls1 s (m1 := lit_set m l1 (Some (true, true))) :
valid m1 [:: (l1, inext l1), (l, ls1) & s] ->
lit_get m l1 = Some (false, false) ->
mweight m1 [:: (l1, inext l1), (l, ls1) & s] <
mweight m ((l, l1 :: ls1) :: s).
Proof.
move=> Hv Hg.
rewrite /mweight /= !big_cons /=.
set n1 := \sum_(j <- s) _; set n2 := \sum_(j | _) _; set n3 := \sum_(j | _) _.
rewrite {n3}[n3](bigD1 l1) /=; last first.
rewrite Hg andbT.
by have [[/= /andP[HH _] _ _ _] _ _ _] := Hv.
set n3 := \sum_(j | _) _.
suff->: n2 = n3.
rewrite !(addSn, addnS, addnA) ltnS.
by rewrite [_ + size (inext l1)]addnC addnA.
apply: eq_bigl => l2; rewrite inE negb_or.
have [->|->|[Dl2l1 Dl2fl1]] := lit_dec l2 l1.
- by rewrite eqxx andbF.
- by rewrite !lit_get_flip Hg lit_set_eq /= !andbF.
by rewrite lit_set_neq // Dl2l1 /= andbT.
Qed.
Lemma mweight_lt5 m b l l1 ls1 s (m1 := lit_set m l1 (Some (b, true))) :
valid m1 [:: (l1, inext l1), (l, ls1) & s] ->
lit_get m l1 = None ->
mweight m1 [:: (l1, inext l1), (l, ls1) & s] < mweight m ((l, l1 :: ls1) :: s).
Proof.
move=> Hv Hg.
rewrite /mweight /= !big_cons /=.
set n1 := \sum_(j <- s) _; set n2 := \sum_(j | _) _; set n3 := \sum_(j | _) _.
rewrite {n3}[n3](bigD1 l1) /=; last first.
rewrite Hg andbT.
by have [[/= /andP[HH _] _ _ _] _ _ _] := Hv.
set n3 := \sum_(j | _) _.
suff FF : n2 <= n3.
rewrite !(addSn, addnS, addnA) ltnS.
rewrite [_ + size (inext l1)]addnC addnA.
by rewrite !ltnS leq_add2l.
have [H1|] := boolP ((flip l1 \in l :: [seq i.1 | i <- s]) || ~~b).
suff->: n2 = n3 by [].
apply: eq_bigl => l2; rewrite inE negb_or.
have [->|->|[Dl2l1 Dl2fl1]] := lit_dec l2 l1.
- by rewrite eqxx andbF.
- rewrite !lit_get_flip Hg lit_set_eq /= .
by case: (_ \in _) H1 => //; case: (b); rewrite ?andbF flip_neq.
by rewrite lit_set_neq // Dl2l1 andbT.
rewrite negb_or negbK !inE negb_or => /andP[/andP[H1 H2] H3].
rewrite [n3](bigD1 (flip l1)) /=; last first.
rewrite lit_get_flip Hg !inE negb_or H1 H2 //=.
by case: (l1) => [] [].
set n4 := \sum_(j | _) _.
suff->: n4 = n2 by apply: leq_addl.
apply: eq_bigl => l2; rewrite inE negb_or.
have [->|->|[Dl2l1 Dl2fl1]] := lit_dec l2 l1.
- by rewrite Hg !inE !eqxx !negb_or //= andbF.
- by rewrite !lit_get_flip lit_set_eq /= H3 eqxx !andbF.
rewrite !inE (negPf Dl2l1) !negb_or !andbT lit_set_neq //=.
by rewrite Dl2fl1 andbT.
Qed.
Lemma mweight_init m l l1 (m1 := lit_set m l1 (Some (false, true))) :
valid m1 [:: (l1, inext l1)] ->
lit_get m l1 = None ->
mweight m1 [:: (l1, inext l1)] = mweight m [::].
Proof.
move=> Hv Hg.
rewrite /mweight /= !big_cons /= big_nil.
set n1 := \sum_(j | _) _; set n2 := \sum_(j | _) _.
rewrite {n2}[n2](bigD1 l1) /=; last first.
by rewrite Hg.
set n2 := \sum_(j | _) _.
rewrite {n2}[n2](bigD1 (flip l1)) /=; last first.
rewrite lit_get_flip Hg /=.
by case: (l1) => [] [].
rewrite {n1}[n1](bigD1 (flip l1)) /=; last first.
rewrite lit_get_flip lit_set_eq //= inE eqxx andbT.
by case: (l1) => [] [].
set n1 := \sum_(j | _) _; set n2 := \sum_(j | _) _.
rewrite !(addSn, addnS, addn0, add0n).
congr (_ + (_ + _)).+2.
apply: eq_bigl => l2.
have [->|->|[Dl2l1 Dl2fl1]] := lit_dec l2 l1.
- by rewrite inE eqxx andbF.
- by rewrite eqxx !andbF.
by rewrite !inE Dl2l1 lit_set_neq ?andbT.
Qed.
Lemma valid_propage_none n m s :
valid m s -> mweight m s < n -> propagate n m s != None.
Proof.
elim: n m s => //= n iH m [|[l ls] s HH VV] //=.
rewrite ltnS in VV.
case E : lit_get => [[b []]|]; last 2 first.
- apply: iH => //.
apply: valid_cons HH _.
by rewrite /lit_is_true /= E.
apply: leq_trans VV.
by apply: mweight_lt1 E.
- apply: iH => //.
apply: valid_cons HH _.
by rewrite /lit_is_true /= E.
apply: leq_trans VV.
by apply: mweight_lt2 E.
case: ls HH VV => [Hv|l1 ls1 Hv] VV.
apply: iH.
by apply: valid_cons_nil Hv.
apply: leq_trans VV.
by apply: mweight_lt3 E.
case E1 : lit_get => [[b1 []]|] //.
- apply: iH.
- apply: valid_cons_true Hv _ _.
by rewrite /lit_is_true E.
- by rewrite /lit_is_true E1.
by move: VV; rewrite /mweight /= !big_cons //.
- case: b1 E1 => // E1.
have Va :
valid (lit_set m l1 (Some (true, true))) [:: (l1, inext l1), (l, ls1) & s]
by apply: valid_add_true_rev => //; apply/eqP.
apply: iH => //.
apply: leq_trans VV.
by apply: mweight_lt4 E1.
have Va :
valid (lit_set m l1 (Some (b, true))) [:: (l1, inext l1), (l, ls1) & s].
by apply: valid_add_true => //; [rewrite /lit_is_true E | rewrite E1].
apply: iH => //.
apply: leq_trans VV.
by apply: mweight_lt5 E1.
Qed.
Lemma valid_propage_red n k m m1 s :
valid m s -> propagate n m s = Some (true, k, m1) ->
mweight m s < n -> mweight m1 [::] < k.
Proof.
elim: n k m m1 s => //= n iH k m m1 [|[l ls] s HH PP VV] //=.
by move=> H1 [<- <-].
rewrite ltnS in VV.
case E : lit_get PP => [[b []]|] PP; last 2 first.
- apply: iH PP _ => //.
apply: valid_cons HH _.
by rewrite /lit_is_true /= E.
apply: leq_trans VV.
by apply: mweight_lt1 E.
- apply: iH PP _ => //.
apply: valid_cons HH _.
by rewrite /lit_is_true /= E.
apply: leq_trans VV.
by apply: mweight_lt2 E.
case: ls HH VV PP => [Hv|l1 ls1 Hv] VV PP.
apply: iH PP _.
by apply: valid_cons_nil Hv.
apply: leq_trans VV.
by apply: mweight_lt3 E.
case E1 : lit_get PP => [[b1 []]|] PP //.
- apply: iH PP _.
- apply: valid_cons_true Hv _ _.
by rewrite /lit_is_true E.
- by rewrite /lit_is_true E1.
by move: VV; rewrite /mweight /= !big_cons.
- case: b1 E1 PP => // E1 PP.
have Va :
valid (lit_set m l1 (Some (true, true))) [:: (l1, inext l1), (l, ls1) & s]
by apply: valid_add_true_rev => //; apply/eqP.
apply: iH (Va) _ _ => //.
apply: leq_trans VV.
by apply: mweight_lt4 E1.
have Va :
valid (lit_set m l1 (Some (b, true))) [:: (l1, inext l1), (l, ls1) & s].
by apply: valid_add_true => //; [rewrite /lit_is_true E | rewrite E1].
apply: iH (Va) _ _ => //.
apply: leq_trans VV.
by apply: mweight_lt5 E1.
Qed.
Lemma propage_reduce_none n k m m1 s l :
propagate n m s = Some (true, k, m1) ->
lit_get m1 l = None -> lit_get m l = None.
Proof.
elim: n m m1 s => //= n iH m m1[|[l1 ls] s] //=.
by move=> [_ <-].
case E : lit_get => [[b []]|]; last 2 first.
- by apply: iH.
- by apply: iH.
case: ls => [|l2 ls1].
by apply: iH.
case E1 : lit_get => [[[] []]|] //.
- by apply: iH.
- by apply: iH.
- move=> H1 H2.
have := iH _ _ _ H1 H2.
have [->|->|[Dll2 Dlfl2]] := lit_dec l l2.
- by rewrite lit_set_eq.
- by rewrite lit_get_flip lit_set_eq.
by rewrite lit_set_neq.
move=> H1 H2.
have := iH _ _ _ H1 H2.
have [->|->|[Dll2 Dxfl2]] := lit_dec l l2.
- by rewrite lit_set_eq.
- by rewrite lit_get_flip lit_set_eq.
by rewrite lit_set_neq.
Qed.
(* Set the unset variable to true and propagate *)
Fixpoint check_satl m n ls :=
if ls is l :: ls1 then
if lit_get m l is None then
let m1 := lit_set m l (Some (false, true)) in
if propagate n m1 [:: (l, inext l)] is Some (true, n2, m2) then
check_satl m2 n2 ls1
else None
else check_satl m n ls1
else Some m.
Lemma check_satl_correct m n ls :
mweight m [::] < n -> valid m [::] ->
if check_satl m n ls is Some m1 then
[/\ valid m1 [::],
forall l, l \in ls -> lit_get m1 l != None &
forall l, lit_get m1 l = None -> lit_get m l = None]
else exists l, lit_cycle l /\ lit_cycle (flip l).
Proof.
elim: ls m n => //= l ls1 IH m n Hms Hv.
case E: lit_get => [bb|].
have := IH _ _ Hms Hv.
case: check_satl => // m1 [H1 H2 H3]; split => // l1.
rewrite inE => /orP[/eqP->|/H2] //.
by apply/eqP=> /H3; rewrite E.
set M := lit_set _ _ _.
have Mv : valid M [:: (l, inext l)] by apply: valid_init.
have Mms : mweight M [:: (l, inext l)] < n by rewrite mweight_init.
case E1 : propagate => [[[[] n1] m1]|].
- have F : valid m1 [::] by apply: valid_propage_true Mv E1.
have G : mweight m1 [::] < n1 by apply: valid_propage_red E1 _.
have := IH _ _ G F.
case: check_satl => // m2 [H1 H2 H3]; split => // l1.
rewrite inE => /orP[/eqP->|/H2] //.
apply/eqP=> /H3 /(propage_reduce_none _ _ _ _ _ _ E1).
by rewrite lit_set_eq.
move/H3/(propage_reduce_none _ _ _ _ _ _ E1).
have [->|->|[Dl1l Dl1fl]] := lit_dec l1 l.
- by rewrite lit_set_eq.
- by rewrite lit_get_flip lit_set_eq.
by rewrite lit_set_neq.
- by apply: valid_propage_false Mv E1.
have : propagate n M [:: (l, inext l)] != None.
by apply: valid_propage_none.
by rewrite E1.
Qed.
(* Top function *)
Definition check_sat :=
let m := [ffun x => None] in
let n := mweight m [::] in
check_satl m n.+1 [seq (true, v) | v <- enum var].
Definition valuation := {ffun var -> bool}.
Definition eval (val : valuation) l :=
if l.1 then val l.2 else ~~ val l.2.
Lemma eval_flip val l : eval val (flip l) = ~~ eval val l.
Proof.
by case: l => [] [] v //=; rewrite /eval //= negbK.
Qed.
Definition satisfiable :=
[exists val : valuation,
forall cl, (cl \in cls) ==> (eval val cl.1 || eval val cl.2)].
Lemma check_sat_correct : satisfiable = check_sat.
Proof.
rewrite /check_sat.
set m := [ffun x => None].
set n := mweight _ _.
set ls := [seq _ | _ <- _].
have V : valid m [::].
by split => // [[[] b1]|[[] b1] l1 _ _];
rewrite /lit_is_true /lit_is_strue /lit_get ffunE.
have := check_satl_correct m n.+1 ls (leqnn _) V.
case: check_satl => [m1 [H1m H2m H3m]|HH] /=.
apply/idP/existsP.
pose M := [ffun v => (odflt (false, false) (m1 v)).2].
have F1 l : lit_get m1 l != None.
case: l => [b v].
have F2 : lit_get m1 (true, v) != None.
by apply: H2m; apply: map_f => //; rewrite mem_enum.
case: b; rewrite ?(lit_get_flip _ (true, v)) //.
by case: lit_get F2.
have HM l : eval M l = lit_is_true m1 l.
have := F1 l.
by case: l => [[] v];
rewrite /M /eval /lit_is_true /lit_get /= ffunE; case: (m1 _).
exists M.
apply/forallP => [[l1 l2]]; apply/implyP => H1 /=.
rewrite !HM.
have F : l2 \in inext (flip l1).
by rewrite [_ \in _](rgraphK) /= flipK H1.
case E: lit_is_true => //=.
have [_ _ _ HH] := H1m.
apply: HH F _ => //.
by move: E (F1 l1); rewrite /lit_is_true lit_get_flip;
case: lit_get => //= [[[] []]].
apply/idP/negP; rewrite negb_exists; apply/forallP=> /= m1.
rewrite negb_forall; apply/negP=> /forallP /= HF.
have F l1 l2 : l1 [->] l2 -> eval m1 l1 -> eval m1 l2.
by move => /orP[] /(implyP (HF _)) /=;
rewrite eval_flip; do 2 case: eval.
have G l1 l2 : connect imply l1 l2 -> eval m1 l1 -> eval m1 l2.
move=> /connectP [p e_p ->].
elim: p l1 e_p => //= l ls1 IH l1 /andP[/F oH /IH oH1] eH.
by apply/oH1/oH.
case: HH => l [/G H1 /G H2].
move: H1 H2; rewrite flipK eval_flip.
case: eval => //= H1 H2.
by have: false by apply: H2.
by have: false by apply: H1.
Qed.
End TwoSat.
Section MWeightInit.
Variable var : finType.
Lemma card_l : #|[finType of (bool * var)]| = 2 * #|var|.
Proof. by rewrite eq_card_prod //= card_bool. Qed.
Lemma inext_nil l : inext var [::] l = [::].
Proof.
case E : (inext var [::] l) => [|l1 ls] //.
have: l1 \in inext var [::] l by rewrite E inE eqxx.
by rewrite [_ \in _]rgraphK.
Qed.
Lemma card_inext_size cls l : #|inext var cls l| = size (inext var cls l).
Proof.
by rewrite -cardE; apply: eq_card => l1 //=; rewrite [_ \in _]rgraphK.
Qed.
Lemma inext_incr_l cls l1 l2 :
#|inext var ((l1, l2) :: cls) (flip _ l1)| <= #|inext var cls (flip _ l1)|.+1.
Proof.
rewrite (cardD1 l2) /= [_ \in _]rgraphK /imply /= flipK inE eqxx /= ltnS.
apply: subset_leq_card; apply/subsetP => i.
rewrite !inE ![_ \in _]rgraphK /= flipK !inE !xpair_eqE eqxx /=.
case: eqP => //= H1.
case: (_ \in _) => //=.
case: (_ \in _) => //=; rewrite orbF.
by case: eqP => //= <-; case: eqP.
Qed.
Lemma inext_incr_r cls l1 l2 :
#|inext var ((l1, l2) :: cls) (flip _ l2)| <= #|inext var cls (flip _ l2)|.+1.
Proof.
rewrite (cardD1 l1) /= [_ \in _]rgraphK /imply /= flipK !inE eqxx /= orbT ltnS.
apply: subset_leq_card; apply/subsetP => i.
rewrite !inE ![_ \in _]rgraphK /= flipK !inE !xpair_eqE eqxx /=.
case: eqP => //= H1.
case: (_ \in _) => //=.
case: (_ \in _) => //=; rewrite orbF.
by case: eqP => //= ->; case: eqP.
Qed.
Lemma inext_same cls l l1 l2 :
l != flip _ l1 -> l != flip _ l2 ->
#|inext var ((l1, l2) :: cls) l| = #|inext var cls l|.
Proof.
move=> H1 H2.
apply: eq_card => l3.
rewrite ![_ \in _]rgraphK /imply /= !inE !xpair_eqE.
case: eqP => [HH|_ /=]; first by rewrite -HH flipK eqxx in H1.
case: (_ =P l2) => [HH|_ /=]; first by rewrite -HH flipK eqxx in H2.
by rewrite andbF.
Qed.
(* Show that the complexity is linear *)
Lemma check_sat_mweight cls :
mweight var cls [ffun _ => None] [::] <= 2 * (size cls + #|var|).
Proof.
rewrite /mweight /=.
rewrite big_nil add0n.
set s := \sum_(l | _) _.
have {s}->: s = \sum_l (size (inext var cls l)).+1.
by apply: eq_bigl => [[[] v]] /=; rewrite /lit_get /= ffunE.
elim: cls => /= [|[l1 l2] cls IH].
set s := \sum_(l | _) _.
have {s}->: s = \sum_(l : (bool * var)) 1.
by apply: eq_bigr => l _; rewrite inext_nil.
by rewrite sum1_card /= card_l.
rewrite !addSn mulnS !addSn add0n.
apply: leq_trans (_ : (\sum_l (size (inext var cls l)).+1).+1 < _); last first.
by rewrite !ltnS.
rewrite (bigD1 (flip _ l1)) //=.
have [/eqP<-|Dl1l2] := boolP (l1 == l2).
rewrite [X in _ <= X.+2](bigD1 (flip _ l1)) //= -!card_inext_size.
set s1 := \sum_(l | _) _; set s2 := \sum_(l | _) _.
have {s2}->: s2 = s1.
apply: eq_bigr => /= l3 Hl3.
by rewrite -!card_inext_size inext_same.
rewrite -!addSn leq_add2r ltnS ltnW // ltnS.
by apply: inext_incr_l.
have F : flip _ l2 != flip _ l1.
by apply: contra Dl1l2 => HH; rewrite -(flipK _ l2) (eqP HH) flipK.
rewrite (bigD1 (flip _ l2)) //=.
rewrite [X in _ <= X.+2](bigD1 (flip _ l1)) //= -addSn.
rewrite [X in _ <= (_ + X).+1](bigD1 (flip _ l2)) //= !addnA -addSn.
set s1 := \sum_(l | _) _; set s2 := \sum_(l | _) _.
have {s2}->: s2 = s1.
apply: eq_bigr => /= l3 /andP[H1l3 H2l3].
by rewrite -!card_inext_size inext_same.
rewrite leq_add2r -addnS.
apply: leq_add; rewrite ltnS -!card_inext_size.
by apply: inext_incr_l.
by apply: inext_incr_r.
Qed.
End MWeightInit.