proposition: Lemma cnf_plus_impl_correct : forall m l r hf g acc (HF : has_form m hf) (EQ : elt hf = LIMPL l r) (ACC : (Forall eval_watched_clause acc -> eval_ohformula g) -> eval_ohformula g), (Forall eval_watched_clause (cnf_plus_impl (is_classic g) l r hf acc) -> eval_ohformula g) -> eval_ohformula g.
proof: Proof. unfold cnf_plus_impl. intros. rewrite Forall_rew in H. rewrite! xmap_filter_rev in H. rewrite Forall_app in H. rewrite! map_rev in H. rewrite! Forall_rev_iff in H. rewrite modus_ponens_and in H by (apply cnf_plus_impli with (l:= l); auto). apply ACC. intro. rewrite and_comm in H. rewrite modus_ponens_and in H by auto. clear ACC H0. unfold is_classic ; destruct g. - simpl in *. apply H. rewrite Forall_forall. intros. rewrite in_map_iff in H0. destruct H0 as (f' & E & I). subst. rewrite filter_In in I. destruct I. simpl in H1. assert (has_form m f'). { inv HF; try discriminate. simpl in *. inv EQ. revert H0. rewrite Forall_forall in H2; auto. } apply eval_formula_dec with (m:=m) in H1; auto. unfold eval_watched_clause. simpl. destruct H1. tauto. right. left. rewrite EQ. rewrite eval_formula_rew. rewrite <- eval_impl_list_eq. intro. rewrite eval_and_list_Forall in H3. rewrite Forall_forall in H3. exfalso ; apply H1 ; auto. - simpl in *. unfold is_classic_or_dec in H. rewrite filter_true in H. revert H. apply Forall_Exists_neg_neg. intros. rewrite Exists_exists in H. destruct H. rewrite in_map_iff in H. destruct H. destruct H. destruct H; subst. unfold eval_watched_clause in H0. simpl in H0. rewrite EQ in H0. rewrite (eval_formula_rew (LIMPL l r)) in H0. rewrite <- eval_impl_list_eq in H0. rewrite eval_and_list_Forall in H0. unfold not in H0. assert (((eval_formula (elt x0) \/ ~ eval_formula (elt x0)) -> False) -> False). { tauto. } apply H. intro D. destruct D. tauto. apply H0. right. left. intros. rewrite Forall_forall in H3. specialize (H3 _ H1). tauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause