proposition: Lemma cnf_correct : forall m f pol g cp cm ar acc hf (WF: has_form m hf) (EQ: hf.(elt) = f) (ACC1 : (Forall eval_watched_clause acc -> eval_ohformula g) -> eval_ohformula g) (CNF : Forall eval_watched_clause (snd (cnf pol (is_classic g) cp cm ar acc f hf)) -> eval_ohformula g), eval_ohformula g.
proof: Proof. induction f using form_ind. - simpl; intros. destruct (is_cons (id hf) (if pol then cp else cm)). tauto. tauto. - simpl; intros. destruct (is_cons (id hf) (if pol then cp else cm)). + simpl in CNF ; tauto. + revert CNF. generalize (if pol then set_cons (id hf) cp else cp) as cp'. generalize (if pol then cm else set_cons (id hf) cm) as cm'. set (acc':= ((if pol then cnf_of_op_plus else cnf_of_op_minus) (is_classic g) o l hf acc)). assert (ACC' : (Forall eval_watched_clause acc' -> eval_ohformula g) -> eval_ohformula g). { destruct pol. apply cnf_of_op_plus_correct; auto. apply cnf_of_op_minus_correct; auto. } apply cnf_correct_list with (m:=m); auto. eapply has_form_lop; eauto. - simpl. intros pol g cp cm ar acc hf. destruct (is_cons (id hf) (if pol then cp else cm)). + simpl. tauto. + set (ar' := (if negb (lazy_or (is_classic g) (fun _ : unit => forallb is_dec l)) && pol then POS hf :: ar else ar)). set (acc':= ((if pol then cnf_plus_impl (is_classic g) else cnf_minus_impl) l r hf acc)). intros HF EQ ACC. assert (ACC' : (Forall eval_watched_clause acc' -> eval_ohformula g) -> eval_ohformula g). { destruct pol. apply cnf_plus_impl_correct with (m:=m) ; auto. apply cnf_minus_impl_correct; auto. } destruct (cnf_list cnf (negb pol) (is_classic g) cp cm ar' acc' l) as (((cp0,cm0),ar0),acc0) eqn:CNF1. eapply has_form_limpl in EQ;eauto. inv EQ. apply IHf; auto. change acc0 with (snd (cp0, cm0, ar0, acc0)). rewrite <- CNF1. apply cnf_correct_list with (m:=m) ;auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause