proposition: Lemma split_polarity_ieval: forall (env : HFormula -> Prop) (p : HFormula) (l lp ln lo : cnf) (WF : Forall wf l) , Elim.split_polarity p l = (lp, ln, lo) -> eval_cnf env l -> (eval_cnf env lo /\ eval_cnf env (map (cons_lit (POS p)) lp) /\ eval_cnf env (map (cons_lit (NEG p)) ln)).
proof: Proof. induction l. - simpl; intros. inv H. simpl. tauto. - intros. simpl in H. simpl. destruct (Elim.split_polarity p l) as [[lp' ln'] lo'] eqn:E. inv WF. specialize (IHl lp' ln' lo' H4 eq_refl). simpl in H0. rewrite eval_normalise in H0;auto. destruct (Elim.normalise a) eqn:N; simpl. + apply wf_normalise in N; auto. generalize (get_polarity_ispec env p c N). destruct (Elim.get_polarity_rec p c). * destruct p0 as [b cl']. inv H. intros. simpl in H0. destruct b; simpl; intuition. * inv H. simpl in *. intuition. + inv H. tauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause