Change nat to positive in Sat proof

8 files changed, 202 insertions, 68 deletions

diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v
index 180c7d7..3daf162 100644
--- a/src/hls/Abstr.v
+++ b/src/hls/Abstr.v
@@ -941,11 +941,10 @@ Proof.
   induction p; crush.
   - destruct_match. inv Heqp0. destruct b.
     cbn. specialize (H p0).
-    rewrite Pos2Nat.id in *.
     apply sem_pexpr_determ with (b2 := false) in H; auto.
     specialize (H p0).
     apply sem_pexpr_determ with (b2 := true) in H; auto.
-    cbn. rewrite Pos2Nat.id in *. rewrite H. auto.
+    cbn. rewrite H. auto.
     replace false with (negb true) in H0 by trivial.
     apply sem_pexpr_negate2 in H0. auto.
   - inv H0.
@@ -964,11 +963,10 @@ Proof.
   induction p; crush.
   - destruct_match. inv Heqp0. destruct b.
     cbn. specialize (H p0).
-    rewrite Pos2Nat.id in *.
     apply sem_pexpr_determ with (b2 := true) in H; auto.
     specialize (H p0).
     apply sem_pexpr_determ with (b2 := false) in H; auto.
-    cbn. rewrite Pos2Nat.id in *. rewrite H. auto.
+    cbn. rewrite H. auto.
     replace true with (negb false) in H0 by trivial.
     apply sem_pexpr_negate2 in H0. auto.
   - inv H0.
@@ -1073,19 +1071,19 @@ Definition check f1 f2 :=
   && PTree.beq beq_pred_pexpr f1.(forest_preds) f2.(forest_preds)
   && beq_pred_eexpr f1.(forest_exit) f2.(forest_exit).
 
-Lemma inj_asgn_eg : forall a b, (a =? b)%nat = (a =? a)%nat -> a = b.
+Lemma inj_asgn_eg : forall a b, (a =? b)%positive = (a =? a)%positive -> a = b.
 Proof.
-  intros. destruct (Nat.eq_dec a b); subst.
-  auto. apply Nat.eqb_neq in n.
-  rewrite n in H. rewrite Nat.eqb_refl in H. discriminate.
+  intros. destruct (peq a b); subst.
+  auto. rewrite OrdersEx.Positive_as_OT.eqb_refl in H.
+  now apply Peqb_true_eq.
 Qed.
 
 Lemma inj_asgn :
-  forall a b, (forall (f: nat -> bool), f a = f b) -> a = b.
+  forall a b, (forall (f: positive -> bool), f a = f b) -> a = b.
 Proof. intros. apply inj_asgn_eg. eauto. Qed.
 
 Lemma inj_asgn_false:
-  forall n1 n2 , ~ (forall c: nat -> bool, c n1 = negb (c n2)).
+  forall n1 n2 , ~ (forall c: positive -> bool, c n1 = negb (c n2)).
 Proof.
   unfold not; intros. specialize (H (fun x => true)).
   simplify. discriminate.
@@ -1101,11 +1099,10 @@ Lemma sat_predicate_Plit_inj :
     Plit p1 == Plit p2 -> p1 = p2.
 Proof.
   simplify. destruct p1, p2.
-  destruct b, b0. assert (p = p0).
-  { apply Pos2Nat.inj. eapply inj_asgn. eauto. } solve [subst; auto].
-  exfalso; eapply inj_asgn_false; eauto.
-  exfalso; eapply inj_asgn_false; eauto.
-  assert (p = p0). apply Pos2Nat.inj. eapply inj_asgn. intros. specialize (H f).
+  destruct b, b0. f_equal. unfold sat_equiv in H. cbn in H. now apply inj_asgn.
+  solve [exfalso; eapply inj_asgn_false; eauto].
+  solve [exfalso; eapply inj_asgn_false; eauto].
+  assert (p = p0). eapply inj_asgn. intros. specialize (H f).
   apply negb_inj in H. auto. rewrite H0; auto.
 Qed.
 
diff --git a/src/hls/CondElimproof.v b/src/hls/CondElimproof.v
index f4362d7..565adb1 100644
--- a/src/hls/CondElimproof.v
+++ b/src/hls/CondElimproof.v
@@ -60,7 +60,7 @@ Proof.
   induction p; crush.
   - repeat destruct_match. inv H1.
     unfold eval_predf; simpl.
-    inv H0. rewrite H. eauto. rewrite Pos2Nat.id; auto.
+    inv H0. rewrite H; eauto.
   - apply Forall_app in H1; inv H1.
     rewrite ! eval_predf_Pand.
     erewrite IHp1; eauto.
@@ -176,7 +176,7 @@ Lemma eval_predf_match_ps :
 Proof.
   induction p0; crush.
   - unfold eval_predf. simplify. destruct p0.
-    rewrite Pos2Nat.id. inv H. inv H0. rewrite H1; auto.
+    inv H. inv H0. rewrite H1; auto.
   - eapply Forall_app in H0. inv H0.
     rewrite ! eval_predf_Pand.
     erewrite IHp0_1; eauto.
@@ -249,12 +249,12 @@ Lemma eval_predf_set_gt:
     wf_predicate v p -> match_ps v ps tps -> eval_predf tps # p <- b p1 = true.
 Proof.
   induction p1; crush.
-  - unfold eval_predf. simplify. destruct p. rewrite Pos2Nat.id.
+  - unfold eval_predf. simplify. destruct p.
     assert (p <> p0).
     { inv H0. unfold wf_predicate in H1. lia. }
     rewrite ! PMap.gso by auto. inv H2.
     inv H0. rewrite <- H4 by auto. unfold eval_predf in H.
-    simplify. rewrite Pos2Nat.id in H. auto.
+    simplify. auto.
   - rewrite eval_predf_Pand. apply Forall_app in H0.
     rewrite eval_predf_Pand in H. apply andb_true_iff in H.
     apply andb_true_iff; simplify.
@@ -275,7 +275,7 @@ Lemma eval_predf_in_ps :
 Proof.
   intros.
   rewrite eval_predf_Pand. apply andb_true_iff. split.
-  unfold eval_predf. simplify. rewrite Pos2Nat.id.
+  unfold eval_predf. simplify.
   rewrite PMap.gss. destruct b; auto.
   eapply eval_predf_set_gt; eauto.
 Qed.
@@ -292,7 +292,7 @@ Proof.
   intros.
   rewrite eval_predf_Pand. apply andb_false_iff.
   unfold eval_predf. simplify. left.
-  rewrite Pos2Nat.id. rewrite PMap.gss.
+  rewrite PMap.gss.
   now destruct b, b'.
 Qed.
 
@@ -510,7 +510,7 @@ Section CORRECTNESS.
       constructor.
       econstructor. simplify. destruct p1.
       constructor. inv H4. eapply eval_predf_in_ps; eauto.
-      constructor. unfold eval_predf; simplify. rewrite Pos2Nat.id.
+      constructor. unfold eval_predf; simplify.
       apply PMap.gss.
       apply match_ps_set_gt; auto.
       constructor; auto.
@@ -521,9 +521,9 @@ Section CORRECTNESS.
       eapply truthy_match_ps; eauto; intros; match goal with H: _ = Some _ |- _ => inv H end; auto.
       econstructor. eapply exec_RB_falsy. simplify. destruct p1.
       constructor. inv H4. eapply eval_predf_in_ps2; eauto.
-      constructor. unfold eval_predf; simplify. rewrite Pos2Nat.id. apply PMap.gss.
+      constructor. unfold eval_predf; simplify. apply PMap.gss.
       constructor. econstructor. inv H4. constructor. unfold eval_predf; simplify.
-      rewrite Pos2Nat.id. rewrite PMap.gss. auto.
+      rewrite PMap.gss. auto.
       constructor. eapply eval_predf_in_ps; eauto.
       apply match_ps_set_gt; auto.
       constructor; auto.
diff --git a/src/hls/Gible.v b/src/hls/Gible.v
index cc35640..d04c78a 100644
--- a/src/hls/Gible.v
+++ b/src/hls/Gible.v
@@ -156,16 +156,16 @@ Definition regset := Regmap.t val.
 Definition predset := PMap.t bool.
 
 Definition eval_predf (pr: predset) (p: pred_op) :=
-  sat_predicate p (fun x => pr !! (Pos.of_nat x)).
+  sat_predicate p (fun x => pr !! x).
 
 Lemma sat_pred_agree0 :
   forall a b p,
-    (forall x, x <> 0%nat -> a x = b x) ->
+    (forall x, a x = b x) ->
     sat_predicate p a = sat_predicate p b.
 Proof.
   induction p; auto; intros.
-  - destruct p. cbn. assert (Pos.to_nat p <> 0%nat) by lia.
-    apply H in H0. now rewrite H0.
+  - destruct p. cbn.
+    now rewrite H.
   - specialize (IHp1 H). specialize (IHp2 H).
     cbn. rewrite IHp1. rewrite IHp2. auto.
   - specialize (IHp1 H). specialize (IHp2 H).
@@ -210,7 +210,7 @@ Lemma eval_predf_not_PredIn :
     eval_predf (ps # p <- b) op = eval_predf ps op.
 Proof.
   induction op; auto.
-  - intros. destruct p0. cbn. rewrite Pos2Nat.id.
+  - intros. destruct p0. cbn.
     destruct (peq p p0); subst.
       { exfalso; apply H; constructor. }
     rewrite Regmap.gso; auto.
diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v
index 1bcc352..6bfc654 100644
--- a/src/hls/GiblePargenproof.v
+++ b/src/hls/GiblePargenproof.v
@@ -576,13 +576,11 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
     induction p; crush.
     - destruct_match. inv Heqp0.
       destruct b.
-      + cbn in H0. rewrite <- H0.
-        rewrite Pos2Nat.id. eauto.
+      + cbn in H0. rewrite <- H0. eauto.
       + replace false with (negb true) by auto.
         apply sem_pexpr_negate. cbn in H0.
         apply negb_true_iff in H0. rewrite negb_involutive in H0.
-        rewrite <- H0. rewrite Pos2Nat.id.
-        eauto.
+        rewrite <- H0. eauto.
      - constructor.
      - rewrite eval_predf_Pand in H0.
        apply andb_false_iff in H0. inv H0. eapply IHp1 in H1.
@@ -611,13 +609,11 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
     induction p; crush.
     - destruct_match. inv Heqp0.
       destruct b.
-      + cbn in H0. rewrite <- H0.
-        rewrite Pos2Nat.id. eauto.
+      + cbn in H0. rewrite <- H0. eauto.
       + replace true with (negb false) by auto.
         apply sem_pexpr_negate. cbn in H0.
         apply negb_true_iff in H0.
-        rewrite <- H0. rewrite Pos2Nat.id.
-        eauto.
+        rewrite <- H0. eauto.
      - constructor.
      - rewrite eval_predf_Pand in H0.
        apply andb_true_iff in H0. inv H0.
diff --git a/src/hls/IfConversionproof.v b/src/hls/IfConversionproof.v
index 2d8cfac..f24a4c4 100644
--- a/src/hls/IfConversionproof.v
+++ b/src/hls/IfConversionproof.v
@@ -697,7 +697,7 @@ Section CORRECTNESS.
     - destruct_match. inv Heqp1. simplify.
       unfold not in *.
       destruct (peq p1 p0); subst; try solve [exfalso; auto].
-      unfold eval_predf. simplify. rewrite ! Pos2Nat.id.
+      unfold eval_predf. simplify.
       rewrite ! Regmap.gso; auto.
     - rewrite eval_predf_Pand in *.
       assert ((~ In p0 (predicate_use p1_1)) /\ (~ In p0 (predicate_use p1_2))).
diff --git a/src/hls/Predicate.v b/src/hls/Predicate.v
index 105c2da..99f0ce5 100644
--- a/src/hls/Predicate.v
+++ b/src/hls/Predicate.v
@@ -176,7 +176,7 @@ Notation "A → B" := (Pimplies A B) (at level 30) : pred_op.
 
 Fixpoint sat_predicate (p: pred_op) (a: asgn) : bool :=
   match p with
-  | Plit (b, p') => if b then a (Pos.to_nat p') else negb (a (Pos.to_nat p'))
+  | Plit (b, p') => if b then a p' else negb (a p')
   | Ptrue => true
   | Pfalse => false
   | Pand p1 p2 => sat_predicate p1 a && sat_predicate p2 a
@@ -185,7 +185,7 @@ Fixpoint sat_predicate (p: pred_op) (a: asgn) : bool :=
 
 Inductive sat_predicateP (a: asgn): pred_op -> bool -> Prop :=
 | sat_prediacteP_Plit: forall b p',
-  sat_predicateP a (Plit (b, p')) (if b then a (Pos.to_nat p') else negb (a (Pos.to_nat p')))
+  sat_predicateP a (Plit (b, p')) (if b then a p' else negb (a p'))
 | sat_prediacteP_Ptrue:
   sat_predicateP a Ptrue true
 | sat_prediacteP_Pfalse:
@@ -509,7 +509,7 @@ Fixpoint trans_pred (p: pred_op) :
       sat_predicate p a = true <-> satFormula fm a}.
   refine
     (match p with
-     | Plit (b, p') => exist _ (((b, Pos.to_nat p') :: nil) :: nil) _
+     | Plit (b, p') => exist _ (((b, p') :: nil) :: nil) _
      | Ptrue => exist _ nil _
      | Pfalse => exist _ (nil::nil) _
      | Pand p1 p2 =>
@@ -548,21 +548,21 @@ Definition stseytin_and (cur p1 p2: lit) : formula :=
     :: (bar cur :: p1 :: nil)
     :: (bar cur :: p2 :: nil) :: nil.
 
-Fixpoint xtseytin (next: nat) (p: pred_op) {struct p} : (nat * lit * formula) :=
+Fixpoint xtseytin (next: positive) (p: pred_op) {struct p} : (positive * lit * formula) :=
   match p with
-  | Plit (b, p') => (next, (b, Pos.to_nat p'), nil)
+  | Plit (b, p') => (next, (b, p'), nil)
   | Ptrue =>
-      ((next+1)%nat, (true, next), ((true, next)::nil)::nil)
+      ((next+1)%positive, (true, next), ((true, next)::nil)::nil)
   | Pfalse =>
-      ((next+1)%nat, (true, next), ((false, next)::nil)::nil)
+      ((next+1)%positive, (true, next), ((false, next)::nil)::nil)
   | Por p1 p2 =>
       let '(m1, n1, f1) := xtseytin next p1 in
       let '(m2, n2, f2) := xtseytin m1 p2 in
-      ((m2+1)%nat, (true, m2), stseytin_or (true, m2) n1 n2 ++ f1 ++ f2)
+      ((m2+1)%positive, (true, m2), stseytin_or (true, m2) n1 n2 ++ f1 ++ f2)
   | Pand p1 p2 =>
       let '(m1, n1, f1) := xtseytin next p1 in
       let '(m2, n2, f2) := xtseytin m1 p2 in
-      ((m2+1)%nat, (true, m2), stseytin_and (true, m2) n1 n2 ++ f1 ++ f2)
+      ((m2+1)%positive, (true, m2), stseytin_and (true, m2) n1 n2 ++ f1 ++ f2)
   end.
 
 Lemma stseytin_and_correct :
@@ -631,7 +631,7 @@ Proof.
     apply andb_prop in H0. inv H0.
     cbn in H.
     repeat destruct_match; try discriminate; []. inv H. eapply IHp1 in Heqp.
-    eapply IHp2 in Heqp1. apply Heqp1 in H2.
+(*    eapply IHp2 in Heqp1. apply Heqp1 in H2.
     apply Heqp in H1. inv H1. inv H2.
     assert
       (satFormula
@@ -640,7 +640,7 @@ Proof.
             :: (bar (true, n1) :: l1 :: nil) :: nil) c).
     eapply stseytin_and_correct. unfold stseytin_and. eauto.
     unfold satLit. simpl. admit.
-    inv H; try contradiction. inv H1; try contradiction. eauto.
+    inv H; try contradiction. inv H1; try contradiction. eauto.*)
 Admitted.
 
 Fixpoint max_predicate (p: pred_op) : positive :=
@@ -656,15 +656,15 @@ Definition tseytin (p: pred_op) :
   {fm: formula | forall a,
       sat_predicate p a = true <-> satFormula fm a}.
   refine (
-      (match xtseytin (Pos.to_nat (max_predicate p + 1)) p as X
-             return xtseytin (Pos.to_nat (max_predicate p + 1)) p = X ->
+      (match xtseytin (max_predicate p + 1) p as X
+             return xtseytin (max_predicate p + 1) p = X ->
                     {fm: formula | forall a, sat_predicate p a = true <-> satFormula fm a}
        with (m, n, fm) => fun H => exist _ ((n::nil) :: fm) _
-       end) (eq_refl (xtseytin (Pos.to_nat (max_predicate p + 1)) p))).
+       end) (eq_refl (xtseytin (max_predicate p + 1) p))).
   intros. eapply xtseytin_correct; eauto. Defined.
 
 Definition tseytin_simple (p: pred_op) : formula :=
-  let m := Pos.to_nat (max_predicate p + 1) in
+  let m := (max_predicate p + 1)%positive in
   let '(m, n, fm) := xtseytin m p in
   (n::nil) :: fm.
 
@@ -846,15 +846,14 @@ Qed.
 
 Lemma sat_predicate_pred_not_in :
   forall p a a' op,
-    (forall x, x <> (Pos.to_nat p) -> a x = a' x) ->
+    (forall x, x <> p -> a x = a' x) ->
     ~ PredIn p op ->
     sat_predicate op a = sat_predicate op a'.
 Proof.
   induction op; intros H; auto.
   - destruct p0. intros. destruct (peq p p0); subst.
     + exfalso. apply H0. constructor.
-    + cbn. assert (Pos.to_nat p0 <> Pos.to_nat p). unfold not; intros; apply n.
-      now apply Pos2Nat.inj. apply H in H1. rewrite H1. auto.
+    + cbn. assert (p0 <> p) by auto. apply H in H1. rewrite H1. auto.
   - intros. assert (~ PredIn p op1 /\ ~ PredIn p op2).
     split; unfold not; intros; apply H0; constructor; tauto.
     inv H1. specialize (IHop1 H H2). specialize (IHop2 H H3).
diff --git a/src/hls/RTLParFU.v b/src/hls/RTLParFU.v
index fe48ac5..b677be7 100644
--- a/src/hls/RTLParFU.v
+++ b/src/hls/RTLParFU.v
@@ -102,7 +102,7 @@ Definition regset := Regmap.t val.
 Definition predset := PMap.t bool.
 
 Definition eval_predf (pr: predset) (p: pred_op) :=
-  sat_predicate p (fun x => pr !! (Pos.of_nat x)).
+  sat_predicate p (fun x => pr !! x).
 
 #[global]
  Instance eval_predf_Proper : Proper (eq ==> equiv ==> eq) eval_predf.
diff --git a/src/hls/Sat.v b/src/hls/Sat.v
index 615c22c..3924ce7 100644
--- a/src/hls/Sat.v
+++ b/src/hls/Sat.v
@@ -6,14 +6,15 @@ UC Berkeley *)
 
 Require Import Arith Bool List.
 Require Import Coq.funind.Recdef.
-Require Coq.MSets.MSetList.
+Require Coq.MSets.MSetPositive.
+Require Coq.MSets.MSetProperties.
 Require Import Coq.Structures.OrderedTypeEx.
 Require Import Coq.Structures.OrdersAlt.
 Require Import Coq.Program.Wf.
 Require Import Vericertlib.
 
-Module Positive_OT := Update_OT Positive_as_OT.
-Module PSet := MSetList.Make Positive_OT.
+Module PSet := MSetPositive.PositiveSet.
+Module PSetProp := MSetProperties.OrdProperties(PSet).
 
 #[local] Open Scope positive.
 
@@ -61,6 +62,13 @@ Definition bool_eq_dec : forall (x y : bool), {x = y} + {x <> y}.
   decide equality.
 Defined.
 
+(** You'll probably want to compare booleans for equality at some point. *)
+Definition boolpositive_eq_dec : forall (x y : (bool * positive)), {x = y} + {x <> y}.
+  pose proof bool_eq_dec.
+  pose proof peq.
+  decide equality.
+Defined.
+
 (** A literal and its negation can't be true simultaneously. *)
 Lemma contradictory_assignment : forall s l cl a,
     s <> fst l
@@ -480,11 +488,40 @@ Eval compute in boundedSatSimple 100 (((false, 0) :: (true, 1) :: nil) :: ((fals
 Definition lit_set_cl (cl: clause) :=
   fold_right PSet.add PSet.empty (map snd cl).
 
+Lemma lit_set_cl_in_set :
+  forall cl v,
+    In v (map snd cl) ->
+    PSet.In v (lit_set_cl cl).
+Proof.
+  induction cl; crush.
+  destruct a; cbn [snd] in *; inv H.
+  - cbn. apply PSetProp.P.FM.add_1; auto.
+  - cbn. apply PSetProp.P.FM.add_2.
+    now apply IHcl.
+Qed.
+
+Lemma lit_set_cl_not_in_set :
+  forall cl v,
+    ~ In v (map snd cl) ->
+    ~ PSet.In v (lit_set_cl cl).
+Proof.
+  induction cl; crush.
+  destruct a; cbn [snd] in *.
+  assert (p <> v /\ ~ In v (map snd cl))
+    by (split; unfold not; intros; apply H; tauto).
+  inv H0. cbn. unfold not; intros. 
+  eapply IHcl; eauto.
+  unfold lit_set_cl.
+  eapply PSetProp.P.Dec.F.add_3; eassumption.
+Qed.
+
 Definition lit_set (fm: formula) :=
   fold_right PSet.union PSet.empty (map lit_set_cl fm).
 
 (* Compute NSet.cardinal (lit_set (((true, 1)::(true, 1)::(true, 1)::nil)::nil)). *)
 
+Definition sat_measure_cl (cl: clause) := PSet.cardinal (lit_set_cl cl).
+
 Definition sat_measure (fm: formula) := PSet.cardinal (lit_set fm).
 
 Lemma elim_clause :
@@ -604,15 +641,119 @@ Definition hasNoNil : forall fm: formula, {In nil fm} + {~ In nil fm}.
   - apply in_cons; assumption.
 Defined.
 
-Lemma setFormula_set_cl :
-  forall fm cl fm' b l A,
-    setFormula (cl :: fm) (b, l) = inleft (exist _ fm' A) ->
-    exists cl' fm'' B, fm' = cl' :: fm''
-      /\ setClause cl (b, l) = inleft (exist _ cl' B).
+Lemma sat_measure_setClause :
+  forall cl cl' l b A,
+    (forall b', ~ In (b', l) cl) ->
+    setClause cl (b, l) = inleft (exist _ cl' A) ->
+    lit_set_cl cl = lit_set_cl cl'.
 Proof.
-  intros. cbn in H. repeat (destruct_match; try discriminate; []).
-  destruct_match. admit.
-  inv H.
+  induction cl; intros.
+  - inv H0. auto.
+  - cbn in H0. repeat (destruct_match; try discriminate; []).
+    destruct_match.
+    + repeat (destruct_match; try discriminate; []).
+      inv H0. cbn [snd fst] in *.
+      exfalso.
+      eapply H. econstructor. auto.
+    + repeat (destruct_match; try discriminate; []).
+      inv H0. cbn [snd fst] in *.
+      assert (forall b', ~ In (b', l) cl).
+      { unfold not; intros. eapply H. apply in_cons. eassumption. }
+      eapply IHcl in Heqs; [|assumption].
+      unfold sat_measure_cl. cbn -[PSet.cardinal].
+      unfold sat_measure_cl in Heqs.
+      replace (fold_right PSet.add PSet.empty (map snd cl))
+        with (lit_set_cl cl); auto.
+      rewrite Heqs. auto.
+Qed.
+
+Lemma in_map_snd_forall :
+  forall A B (cl: list (A * B)) l,
+    ~ In l (map snd cl) ->
+    (forall b', ~ In (b', l) cl).
+Proof.
+  unfold not; intros; apply H.
+  replace l with (snd (b', l)) by auto.
+  now apply in_map.
+Qed.
+
+Lemma sat_measure_setClause_In_neq :
+  forall cl cl' l v b A,
+    In v (map snd cl) ->
+    setClause cl (b, l) = inleft (exist _ cl' A) ->
+    v <> l ->
+    In v (map snd cl').
+Proof.
+    induction cl; intros.
+  - inv H0. auto.
+  - cbn in H0. repeat (destruct_match; try discriminate; []).
+    destruct_match.
+    + repeat (destruct_match; try discriminate; []).
+      inv H0. cbn [snd fst] in *. eapply IHcl; eauto.
+      inv H; auto. contradiction.
+    + repeat (destruct_match; try discriminate; []).
+      inv H0. cbn [snd fst] in *.
+      destruct (peq v v0); subst.
+      { now constructor. }
+      cbn. right. eapply IHcl; eauto. inv H; auto.
+      contradiction.
+Qed.
+
+Lemma sat_measure_setClause_In :
+  forall cl cl' l b A,
+    In l (map snd cl) ->
+    setClause cl (b, l) = inleft (exist _ cl' A) ->
+    (sat_measure_cl cl' < sat_measure_cl cl)%nat.
+Proof.
+  induction cl; intros.
+  - crush.
+  - cbn in H0. repeat (destruct_match; try discriminate; []).
+    destruct_match.
+    + repeat (destruct_match; try discriminate; []).
+      inv H0. cbn [snd fst] in *. clear Heqs2. clear Heqs1.
+      inv H; cbn [snd fst] in *.
+      * destruct (in_dec peq v (map snd cl)).
+        -- exploit IHcl; eauto; intros. unfold sat_measure_cl in *.
+           cbn -[PSet.cardinal]. apply lit_set_cl_in_set in i0.
+           rewrite PSetProp.P.add_cardinal_1; auto.
+        -- apply sat_measure_setClause in Heqs; [|now apply in_map_snd_forall].
+           unfold sat_measure_cl in *. cbn -[PSet.cardinal].
+           setoid_rewrite Heqs.
+           apply lit_set_cl_not_in_set in n0.
+           rewrite PSetProp.P.add_cardinal_2; auto.
+           now rewrite <- Heqs.
+      * exploit IHcl; eauto; intros. unfold sat_measure_cl in *.
+        cbn. rewrite PSetProp.P.add_cardinal_1; auto.
+        now apply lit_set_cl_in_set.
+    + repeat (destruct_match; try discriminate; []). inv H0.
+      cbn [snd fst] in *. cbn in H. inv H; [contradiction|].
+      exploit IHcl; eauto; intros.
+      unfold sat_measure_cl in *. cbn.
+      destruct (in_dec peq v (map snd cl)); destruct (in_dec peq v (map snd x)).
+      * apply lit_set_cl_in_set in i0. apply lit_set_cl_in_set in i1.
+        repeat rewrite PSetProp.P.add_cardinal_1 by auto. auto.
+      * exploit sat_measure_setClause_In_neq. eapply i0. eauto. auto. intros.
+        contradiction.
+      * apply lit_set_cl_in_set in i0. apply lit_set_cl_not_in_set in n0.
+        rewrite PSetProp.P.add_cardinal_1 by auto.
+        rewrite PSetProp.P.add_cardinal_2 by auto. unfold lit_set_cl in *; lia.
+      * apply lit_set_cl_not_in_set in n0. apply lit_set_cl_not_in_set in n1.
+        repeat rewrite PSetProp.P.add_cardinal_2 by auto.
+        unfold lit_set_cl in *; lia.
+Qed.
+
+(* Lemma sat_measure_setFormula :
+  forall cl cl' l b b' A,
+    In (b', l) cl ->
+    setClause cl (b, l) = inleft (exist _ cl' A) ->
+    (sat_measure_cl cl' < sat_measure_cl cl)%nat.
+Proof.
+  induction cl; intros.
+  - crush.
+  - cbn in H0. repeat (destruct_match; try discriminate; []).
+    destruct_match.
+    + repeat (destruct_match; try discriminate; []).
+      inv H0. cbn [snd fst] in *.*)
 
 Lemma sat_measure_setFormula :
   forall fm fm' l b A,
@@ -623,6 +764,7 @@ Proof.
   induction fm.
   - intros. inv H. inv H1. inv H. inv H1.
   - intros. unfold sat_measure, lit_set. cbn -[PSet.cardinal].
+    Admitted.
 
 Lemma sat_measure_propagate_unit :
   forall fm' fm H,