diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/hls/Abstr.v | 27 | ||||
-rw-r--r-- | src/hls/CondElimproof.v | 18 | ||||
-rw-r--r-- | src/hls/Gible.v | 10 | ||||
-rw-r--r-- | src/hls/GiblePargenproof.v | 12 | ||||
-rw-r--r-- | src/hls/IfConversionproof.v | 2 | ||||
-rw-r--r-- | src/hls/Predicate.v | 35 | ||||
-rw-r--r-- | src/hls/RTLParFU.v | 2 | ||||
-rw-r--r-- | src/hls/Sat.v | 164 |
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, |