proposition: Lemma combine_spec : forall A B C (f : A -> B -> C) g₁ g₂ dom₁ dom₂ (m₁ : t A dom₁) (m₂ : t B dom₂) x v, find x (combine f g₁ g₂ m₁ m₂) = Some v <-> (exists v₁ v₂, find x m₁ = Some v₁ ∧ find x m₂ = Some v₂ ∧ v = f v₁ v₂) ∨ (exists v₁, find x m₁ = Some v₁ ∧ find x m₂ = None ∧ v = g₁ v₁) ∨ (exists v₂, find x m₁ = None ∧ find x m₂ = Some v₂ ∧ v = g₂ v₂).
proof: Proof. intros A B C f g₁ g₂ dom₁ dom₂ [m₁ Hok₁] [m₂ Hok₂] x v. unfold combine, find. simpl. rewrite Scombine_spec. split; intros [Hin | [Hin | Hin]]. + destruct Hin as [v₁ [v₂ [Hin₁ [Hin₂ Heq]]]]. left. exists v₁, v₂. auto. + destruct Hin as [v₁ [Hin₁ [Hin₂ Heq]]]. right; left. exists v₁. auto. + destruct Hin as [v₂ [Hin₁ [Hin₂ Heq]]]. do 2 right. exists v₂. auto. + destruct Hin as [v₁ [v₂ [Hin₁ [Hin₂ Heq]]]]. left. exists v₁, v₂. auto. + destruct Hin as [v₁ [Hin₁ [Hin₂ Heq]]]. right; left. exists v₁. auto. + destruct Hin as [v₂ [Hin₁ [Hin₂ Heq]]]. do 2 right. exists v₂. auto. Qed.
imports: Utf8 MSets FMaps Orders Coqlib DepMapInterface