proposition: Lemma split_polarity_eval : forall env p l lp ln lo, Elim.split_polarity p l = (lp,ln,lo) -> beval_cnf env l = (beval_cnf env lo) && (beval_cnf env (List.map (cons_lit (POS p)) lp)) && (beval_cnf env (List.map (cons_lit (NEG p)) ln)).
proof: Proof. induction l. - simpl; intros. inv H. simpl. reflexivity. - intros. simpl in H. simpl. destruct (Elim.split_polarity p l) as [[lp' ln'] lo'] eqn:E. rewrite (IHl lp' ln' lo') by auto. rewrite (beval_normalise env a). destruct (Elim.normalise a); simpl. + generalize (get_polarity_spec env p c). destruct (Elim.get_polarity_rec p c). destruct p0 as [b cl']. inv H. intros. rewrite H. rewrite !beval_cnf_cons_lit. simpl. rewrite beval_clause_cons_lit. destruct b ; simpl. btauto. btauto. inv H. intros. simpl. btauto. + inv H. btauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause