proposition: Lemma combine_OK : forall A B C (f : A -> B -> C) g₁ g₂ dom₁ dom₂ (m₁ : t A dom₁) (m₂ : t B dom₂), OK (Dom.union dom₁ dom₂) (Scombine f g₁ g₂ (proj1_sig m₁) (proj1_sig m₂)).
proof: Proof. destruct m₁ as [m₁ Hok₁], m₂ as [m₂ Hok₂]. simpl. intro x. rewrite Dom.union_spec. split; intro Hin. + destruct Hin as [v Hin]. apply S.find_1 in Hin. rewrite (Scombine_spec f) in Hin. destruct Hin as [Hin | [Hin | Hin]]. - destruct Hin as [v₁ [v₂ [Hv₁ _]]]. left. rewrite <- (Hok₁ x). exists v₁. apply S.find_2. assumption. - destruct Hin as [v₁ [Hv₁ _]]. left. rewrite <- (Hok₁ x). exists v₁. apply S.find_2. assumption. - destruct Hin as [v₂ [_ [Hv₂ _]]]. right. rewrite <- (Hok₂ x). exists v₂. apply S.find_2. assumption. + destruct (Dom.mem x dom₁) eqn:Hin₁, (Dom.mem x dom₂) eqn:Hin₂; try rewrite Dom.mem_spec in *. - rewrite <- (Hok₁ x) in Hin₁. destruct Hin₁ as [v₁ Hin₁]. rewrite <- (Hok₂ x) in Hin₂. destruct Hin₂ as [v₂ Hin₂]. exists (f v₁ v₂). apply S.find_2. rewrite Scombine_spec. left. exists v₁, v₂. now repeat split; apply S.find_1. - rewrite <- (Hok₁ x) in Hin₁. destruct Hin₁ as [v₁ Hin₁]. exists (g₁ v₁). apply S.find_2. rewrite Scombine_spec. right; left. exists v₁. repeat split; try now apply S.find_1. destruct (S.find x m₂) as [v |] eqn:Hfind; trivial. assert (Habs : S.In x m₂) by now exists v; apply S.find_2. rewrite (Hok₂ x), <- Dom.mem_spec, Hin₂ in Habs. discriminate Habs. - rewrite <- (Hok₂ x) in Hin₂. destruct Hin₂ as [v₂ Hin₂]. exists (g₂ v₂). apply S.find_2. rewrite Scombine_spec. do 2 right. exists v₂. repeat split; try now apply S.find_1. destruct (S.find x m₁) as [v |] eqn:Hfind; trivial. assert (Habs : S.In x m₁) by now exists v; apply S.find_2. rewrite (Hok₁ x), <- Dom.mem_spec, Hin₁ in Habs. discriminate Habs. - destruct Hin as [Habs | Habs]; rewrite <- Dom.mem_spec in Habs; rewrite Habs in *; discriminate. Qed.
imports: Utf8 MSets FMaps Orders Coqlib DepMapInterface