proposition: Lemma eval_annot_is_unsat : forall m u (l:Annot.t literal) d (WL : check_annot has_literal m l) (WU : wf_units_lit u m) (ED : eval_annot eval_literal m l) (EU : eval_annot_units u m) (US : is_unsat u l = Some d), eval_pset m d -> False.
proof: Proof. intros. unfold is_unsat in US. destruct (Annot.elt l) eqn:EQ. - destruct (is_hFF f) eqn:FF. + apply is_hFF_true in FF. subst. inv US. unfold eval_annot in ED. rewrite EQ in ED. apply ED ;auto. + destruct (IntMap.get' (id f) u) eqn:FD; try congruence. assert (FD':= FD). apply units_has_literal_of_form with (m:= m) in FD; auto. apply EU in FD. apply WU in FD'. destruct FD' as (WI & WFT). unfold eval_annot, Annot.map, Annot.lift in *. simpl in *. destruct_in_hyp US b; try discriminate. rewrite negb_true_iff in b. inv US. apply eval_pset_union in H; auto. destruct H as (E1 & E2). rewrite b in FD. simpl in FD. apply FD ;auto. rewrite EQ in ED. apply ED;auto. destruct WFT ; auto. destruct WL;auto. destruct wf_deps0;auto. destruct WL;auto. unfold Annot.lift in wf_elt0. rewrite EQ in wf_elt0. auto. - simpl; intros. destruct (IntMap.get' (id f) u) eqn:FD; try congruence. assert (FD':= FD). apply units_has_literal_of_form with (m:= m) in FD; auto. apply EU in FD. apply WU in FD'. destruct FD' as (WI & WFT). unfold eval_annot, Annot.map, Annot.lift in *. simpl in *. destruct_in_hyp US b; try discriminate. inv US. apply eval_pset_union in H; auto. destruct H as (E1 & E2). simpl in FD. rewrite EQ in ED. simpl in ED. apply ED;auto. destruct WFT ; auto. destruct WL;auto. destruct wf_deps0;auto. destruct WL;auto. unfold Annot.lift in wf_elt0. rewrite EQ in wf_elt0. auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause