proposition: Lemma eval_annot_select_clause : forall m g u k v (WFU: wf_units_lit u m) (EU : eval_annot_units u m) (EW : eval_annot eval_watched_clause m v) (CHK : check_annot has_watched_clause m v) (EVAL : ohold (eval_annot eval_or m) (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. unfold eval_annot. intro. apply eval_literal_list_classic with (m:=m) ;auto. rewrite R in WFR;auto. simpl in WFR. destruct WFR ; auto. revert H. change (ohold (eval_annot eval_literal_list m) (Some t0)). rewrite <- R. eapply eval_annot_reduce_lits;eauto. destruct CHK ;auto. destruct CHK ; auto. - unfold eval_ohformula in *. intro. eapply eval_annot_reduce_lits in EW; eauto. rewrite R in EW. simpl in EW. revert EW. unfold eval_annot in *. intros. rewrite R in *. simpl in EVAL. specialize (eval_literal_list_neg (Annot.elt t0)). intuition. destruct CHK;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