proposition: Theorem combine_None : forall A B C (f : A -> B -> C) g₁ g₂ dom₁ dom₂ (m₁ : t A dom₁) (m₂ : t B dom₂) x, find x (combine f g₁ g₂ m₁ m₂) = None <-> find x m₁ = None ∧ find x m₂ = None.
proof: Proof. intros A B C f g₁ g₂ dom₁ dom₂ m₁ m₂ x. destruct (find x m₁) as [v₁ |] eqn:Hin₁, (find x m₂) as [v₂ |] eqn:Hin₂. + assert (Hin : find x (combine f g₁ g₂ m₁ m₂) = Some (f v₁ v₂)). { rewrite combine_spec. left. exists v₁, v₂. auto. } rewrite Hin. intuition discriminate. + assert (Hin : find x (combine f g₁ g₂ m₁ m₂) = Some (g₁ v₁)). { rewrite combine_spec. right; left. exists v₁. auto. } rewrite Hin. intuition discriminate. + assert (Hin : find x (combine f g₁ g₂ m₁ m₂) = Some (g₂ v₂)). { rewrite combine_spec. do 2 right. exists v₂. auto. } rewrite Hin. intuition discriminate. + destruct (find x (combine f g₁ g₂ m₁ m₂)) eqn:Hin. - rewrite combine_spec in Hin. destruct Hin as [[v₁ [v₂ [? [? ?]]]] | [[? [? [? ?]]] | [? [? [? ?]]]]]; rewrite Hin₁, Hin₂ in *; discriminate. - intuition. Qed.
imports: Utf8 Bool SetoidList RelationPairs Orders Coqlib DepMapInterface DepMapFactsInterface