proposition: Lemma constant_None : forall A dom (v : A) x, find x (constant dom v) = None <-> ¬Dom.In x dom.
proof: Proof. intros A dom v x. unfold constant, find. simpl. rewrite Dom.fold_spec, <- Dom.elements_spec1. split; intro Hin. + intro Habs. assert (Hconj := conj Habs (eq_refl v)). apply (@or_introl _ (¬ InA X.eq (x : Dom.elt) (Dom.elements dom) ∧ S.find x (S.empty A) = Some v)) in Hconj. rewrite <- constant_aux in Hconj. - cut (None = Some v). discriminate. rewrite <- Hin. assumption. - eapply SortA_NoDupA; refine _. apply Dom.elements_spec2. + destruct (S.find x (fold_left (fun a (e : Dom.elt) => S.add e v a) (Dom.elements dom) (S.empty A))) eqn:H; trivial. rewrite constant_aux in H. destruct H as [[H _] | [_ H]]. - contradiction. - exfalso. apply S.find_2 in H. revert H. apply S.empty_1. - eapply SortA_NoDupA; refine _. apply Dom.elements_spec2. Qed.
imports: Utf8 MSets FMaps Orders Coqlib DepMapInterface