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 ![_ \in _](rgraphK) 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.