proposition: Lemma elim_correct : forall env v cls (WF: Forall wf cls), eval_cnf env cls -> eval_cnf env (Elim.elim v cls).
proof: Proof. unfold Elim.elim. intros. destruct (Elim.split_polarity v cls) as ((lp,ln),lo) eqn:SP. assert (SP':=SP). apply split_polarity_ieval with (env:=env) in SP;auto. destruct SP as (SP1 & SP2 & SP3). apply wf_split_polarity in SP'; auto. rewrite eval_cnf_app. split ;auto. destruct SP' as [WF1 [WF2 WF3]]. revert ln SP3 WF2. induction lp. - simpl. auto. - simpl. intros. simpl in SP2. rewrite eval_cnf_app. intuition. clear H2. clear H1. induction ln. + simpl. auto. + simpl. simpl in SP3. assert (wf (Elim.merge_clause a a0)). { inv WF1. inv WF2. apply wf_merge_clause;auto. } generalize (eval_normalise env _ H1). destruct (Elim.normalise (Elim.merge_clause a a0)). simpl. intros. split. rewrite <- H2. eapply merge_clause_correct;eauto. inv WF1;auto. inv WF2;auto. tauto. apply IHln. tauto. inv WF2;auto. simpl. intros. apply IHln;auto. tauto. inv WF2;auto. + apply H2;auto. inv WF1;auto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause