proposition: Lemma elim_complete : forall p l (EV :forall env , beval_cnf env l = true -> False) env (EL : beval_cnf env (Elim.elim p l) = true), False.
proof: Proof. unfold Elim.elim. intros. destruct (Elim.split_polarity p l) as [[lp ln] lo] eqn:SP. rewrite beval_cnf_app in EL. assert (EV' : forall env, beval_cnf env lo && beval_cnf env (map (cons_lit (POS p)) lp) && beval_cnf env (map (cons_lit (NEG p)) ln) = true -> False). { intros. apply (EV env0). rewrite (split_polarity_eval env0 p l lp ln lo) by auto. tauto. } clear EV. rewrite andb_true_iff in EL. destruct EL as (EL1 & EL2). apply split_polarity_vars in SP ; auto. generalize (EV' (set_env env p true)). generalize (EV' (set_env env p false)). clear EV'. rewrite! beval_cnf_cons_lit. unfold beval_lit; simpl. rewrite! set_env_same. simpl. rewrite! andb_true_r. rewrite! beval_no_var by tauto. rewrite EL2. simpl. intros. apply beval_cnf_exists in H. apply beval_cnf_exists in H0. destruct H as (cl1 & IN1 & E1). destruct H0 as (cl2 & IN2 & E2). eapply resolve_all_eval in EL1;eauto. intuition congruence. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause