proposition: Lemma annot_holds_correct : forall m u d , annot_holds u d = true -> eval_units m u -> eval_pset m d.
proof: Proof. unfold annot_holds. intros. set (F := (fun (acc : bool) (i : int) (b : option bool) => if acc then match b with | Some b' => match IntMap.get' i u with | Some b2 => Bool.eqb b' (Annot.elt b2) | None => false end | None => false end else acc)) in *. rewrite IntMap.fold_elements' in H. unfold eval_pset. intros. destruct ((LitSet.get (id f) d)) eqn:GET; try discriminate. unfold LitSet.get in GET. apply IntMap.elements_correct' with (k:=nil) in GET. unfold OBool.lift_has_bool in H2. simpl in H2. revert f b H1 t0 GET H2. revert H. generalize true at 1. change (option bool) with OBool.t. induction (IntMap.elements' d nil). - simpl. tauto. - simpl. intros. destruct GET ; subst. simpl in H. destruct (F b (id f) t0) eqn:Fb. + unfold F in Fb. destruct b; try congruence. destruct t0 ; try congruence. destruct (IntMap.get' (id f) u) eqn:G' ; try congruence. rewrite eqb_true_iff in Fb. subst. simpl in H2. rewrite eqb_true_iff in H2. subst. apply eval_units_get with (m:=m) in G'; auto. + assert (fold_left (fun (a : bool) (p : int * OBool.t) => F a (fst p) (snd p)) l false = false). { clear. induction l; simpl ; auto. } congruence. + eapply IHl ;eauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause