proposition: Theorem Scombine_spec : forall A B C (f : A -> B -> C) g h x v m₁ m₂, S.find x (Scombine f g h m₁ m₂) = Some v <-> (exists v₁ v₂, S.find x m₁ = Some v₁ ∧ S.find x m₂ = Some v₂ ∧ v = f v₁ v₂) ∨ (exists v₁, S.find x m₁ = Some v₁ ∧ S.find x m₂ = None ∧ v = g v₁) ∨ (exists v₂, S.find x m₁ = None ∧ S.find x m₂ = Some v₂ ∧ v = h v₂).
proof: Proof. intros A B C f g h x v m₁ m₂. unfold Scombine. rewrite Dom.fold_spec. rewrite Scombine_spec_aux. * rewrite Dom.elements_spec1, Dom.union_spec, Sdom, Sdom. split; intro Hin. + destruct Hin as [[_ ?] | [_ Habs]]. - assumption. - apply S.find_2, S.empty_1 in Habs. elim Habs. + left. split; trivial. destruct Hin as [[v' [? [Hin _]]] | [[v' [? _]] | [v' [_ [? _]]]]]; left + right; exists v'; apply S.find_2; assumption. * eapply SortA_NoDupA; refine _. apply Dom.elements_spec2. Qed.
imports: Utf8 MSets FMaps Orders Coqlib DepMapInterface