From d9f8b0f3d75929eeb3e363b74f8894fb72a27a65 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 11 Apr 2015 19:46:04 -0700
Subject: [PATCH] feat(library/data/finset/comb): add cross_product to finset

---
 library/data/finset/comb.lean | 35 +++++++++++++++++++++++++++++++++++
 library/data/list/perm.lean   |  2 +-
 2 files changed, 36 insertions(+), 1 deletion(-)

diff --git a/library/data/finset/comb.lean b/library/data/finset/comb.lean
index c2ff05e1a..89fb3ce96 100644
--- a/library/data/finset/comb.lean
+++ b/library/data/finset/comb.lean
@@ -65,4 +65,39 @@ quot.induction_on₂ s₁ s₂ (λ l₁ l₂ h, list.all_intersection_of_all_lef
 theorem all_intersection_of_all_right {p : A → Prop} {s₁ : finset A} (s₂ : finset A) : all s₂ p → all (s₁ ∩ s₂) p :=
 quot.induction_on₂ s₁ s₂ (λ l₁ l₂ h, list.all_intersection_of_all_right _ h)
 end all
+
+section cross_product
+variables {A B : Type}
+definition cross_product (s₁ : finset A) (s₂ : finset B) : finset (A × B) :=
+quot.lift_on₂ s₁ s₂
+  (λ l₁ l₂,
+    to_finset_of_nodup (list.cross_product (elt_of l₁) (elt_of l₂))
+                       (nodup_cross_product (has_property l₁) (has_property l₂)))
+  (λ v₁ v₂ w₁ w₂ p₁ p₂, quot.sound (perm_cross_product p₁ p₂))
+
+infix * := cross_product
+
+theorem empty_cross_product (s : finset B) : @empty A * s = ∅ :=
+quot.induction_on s (λ l, rfl)
+
+theorem mem_cross_product {a : A} {b : B} {s₁ : finset A} {s₂ : finset B}
+        : a ∈ s₁ → b ∈ s₂ → (a, b) ∈ s₁ * s₂ :=
+quot.induction_on₂ s₁ s₂ (λ l₁ l₂ i₁ i₂, list.mem_cross_product i₁ i₂)
+
+theorem mem_of_mem_cross_product_left {a : A} {b : B} {s₁ : finset A} {s₂ : finset B}
+        : (a, b) ∈ s₁ * s₂ → a ∈ s₁ :=
+quot.induction_on₂ s₁ s₂ (λ l₁ l₂ i, list.mem_of_mem_cross_product_left i)
+
+theorem mem_of_mem_cross_product_right {a : A} {b : B} {s₁ : finset A} {s₂ : finset B}
+        : (a, b) ∈ s₁ * s₂ → b ∈ s₂ :=
+quot.induction_on₂ s₁ s₂ (λ l₁ l₂ i, list.mem_of_mem_cross_product_right i)
+
+theorem cross_product_empty (s : finset A) : s * @empty B = ∅ :=
+ext (λ p,
+  match p with
+  | (a, b) := iff.intro
+     (λ i, absurd (mem_of_mem_cross_product_right i) !not_mem_empty)
+     (λ i, absurd i !not_mem_empty)
+  end)
+end cross_product
 end finset
diff --git a/library/data/list/perm.lean b/library/data/list/perm.lean
index 90a8f8239..3b3a6b9d2 100644
--- a/library/data/list/perm.lean
+++ b/library/data/list/perm.lean
@@ -748,7 +748,7 @@ list.induction_on l
   (λ a t r p,
     perm_app (perm_map _ p) (r p))
 
-theorem perm_cross_product {l₁ l₂ t₁ t₂ : list A} : l₁ ~ l₂ → t₁ ~ t₂ → (cross_product l₁ t₁) ~ (cross_product l₂ t₂) :=
+theorem perm_cross_product {l₁ l₂ : list A} {t₁ t₂ : list B} : l₁ ~ l₂ → t₁ ~ t₂ → (cross_product l₁ t₁) ~ (cross_product l₂ t₂) :=
 assume p₁ p₂, trans (perm_cross_product_left t₁ p₁) (perm_cross_product_right l₂ p₂)
 end cross_product
 end perm