proposition: Lemma eval_select_clause : forall m g u k v (WFU: wf_units_lit u m) (EU : eval_units m u) (EW : Annot.lift eval_watched_clause v) (CHK : check_annot has_watched_clause m v) (EVAL : ohold (Annot.lift eval_or) (select_clause (is_classic g) u k v) -> eval_ohformula g), eval_ohformula g.
proof: Proof. intros. revert EW. unfold select_clause in EVAL. destruct_in_hyp EVAL R; [|simpl in EVAL ; auto]. destruct_in_hyp EVAL C; [| simpl in EVAL ; auto]. rewrite <- R in EVAL. assert (WFR : ohold (check_annot has_conflict_clause m) (reduce_lits u (Annot.deps v) (watch1 (Annot.elt v) :: watch2 (Annot.elt v) :: unwatched (Annot.elt v)))). { apply check_annot_reduce_lits; auto. destruct CHK ; auto. destruct CHK; auto. } destruct g ; simpl in C. - intro. apply EVAL. rewrite R. simpl. apply eval_literal_list_classic with (m:=m) ;auto. rewrite R in WFR;auto. simpl in WFR. destruct WFR ; auto. change (ohold (Annot.lift eval_literal_list) (Some t0)). rewrite <- R. eapply eval_reduce_lits; eauto. destruct CHK ;auto. - unfold eval_ohformula in *. intro EVAL'. eapply eval_reduce_lits in EVAL'; eauto. rewrite R in EVAL'. simpl in EVAL'. revert EVAL'. apply eval_literal_list_neg;auto. rewrite R in *. auto. destruct CHK;auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause