proposition: Lemma eval_clause_classic : forall cls i (WF: Forall wf cls), (forall env, beval_cnf env cls = true -> boeval env i = true) -> (forall env, eval_cnf env cls -> oeval env i).
proof: Proof. intros. set (L := vars_of_cnf cls). assert (ND := NoDup_nodup hformula_eq_dec L). apply has_cardinal_no_dup in ND. assert (Lspec : forall v, is_var_of_cnf v cls -> In v (nodup hformula_eq_dec L)). { intros. rewrite nodup_In. apply vars_of_cnf_ok; auto. } revert ND H0. generalize (length (nodup hformula_eq_dec L)) as n. intro. unfold L in *. clear L. revert Lspec. generalize ((nodup hformula_eq_dec (vars_of_cnf cls))) as vars. revert cls WF H. induction n. - intros. inv ND. simpl in Lspec. assert (LspecFalse := is_var_of_cnf_False cls Lspec). destruct cls. + simpl in H0. specialize (H (fun x => false) eq_refl). destruct i; simpl in *;discriminate. + simpl in H0. destruct H0. assert (c = nil). apply LspecFalse. simpl; tauto. subst. simpl in H0. tauto. - intros. inv ND. destruct (match_option_dec x i). + destruct i ; simpl in *; try tauto. subst. destruct l. * assert (IN : forall v, is_var_of_cnf v cls -> h = v). { intros. apply Lspec in H1. simpl in H1. tauto. } eapply beval_clauses_one_var in H. destruct H as (cl & INC & ALLP). eapply eval_clauses_all_pos ; eauto. intros. apply Lspec in H1. simpl in H1. tauto. * set (E := Elim.elim h0 cls). eapply IHn with (cls:= E) (vars:= (h::l)); auto. apply wf_elim;auto. { rewrite neg_concl with (l:= Some h) in H. rewrite neg_concl with (l:= Some h). intros. apply elim_complete with (env:=env0) (p:= h0) in H. tauto. rewrite elim_no_vars. auto. simpl. rewrite is_var_of_cnf_cons. rewrite is_var_of_cnf_nil. rewrite is_var_of_clause_cons. rewrite is_var_of_clause_nil. simpl. simpl in H4. intuition congruence. } { intros. apply is_var_of_cnf_elim in H1. destruct H1. apply Lspec in H1. simpl in *. intuition congruence. } { inv H2. constructor;auto. simpl in H4. tauto. } { apply elim_correct; auto. } + set (E := Elim.elim x cls). eapply IHn with (cls:= E) (vars:= l); auto. apply wf_elim;auto. { intros. rewrite neg_concl with (l:= i) in H. destruct (boeval env0 i) eqn:EI;auto. exfalso. apply elim_complete with (env:=env0) (p:= x) in H; auto. rewrite elim_no_vars. rewrite beval_cnf_app. unfold E in H3. rewrite H3. rewrite eval_clause_of_opt. rewrite EI. reflexivity. destruct i; simpl in *. rewrite is_var_of_cnf_cons. rewrite is_var_of_clause_cons. rewrite is_var_of_cnf_nil. rewrite is_var_of_clause_nil. simpl. intuition congruence. rewrite is_var_of_cnf_nil. tauto. } { intros. apply is_var_of_cnf_elim in H3. destruct H3. apply Lspec in H3. simpl in *. intuition congruence. } { apply elim_correct; auto. } Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause