feat(data/alist,data/finmap): union

* Also for finmap: induction_on₂, decidable_eq, ext_iff
* And some other basic theorems

src/data/finmap.lean

@@ -79,9 +79,16 @@ by cases s₁; cases s₂; refl
   {C : finmap β → Prop} (s : finmap β) (H : ∀ (a : alist β), C ⟦a⟧) : C s :=
 by rcases s with ⟨⟨a⟩, h⟩; exact H ⟨a, h⟩
 
+@[elab_as_eliminator] theorem induction_on₂ {C : finmap β → finmap β → Prop}
+  (s₁ s₂ : finmap β) (H : ∀ (a₁ a₂ : alist β), C ⟦a₁⟧ ⟦a₂⟧) : C s₁ s₂ :=
+induction_on s₁ $ λ l₁, induction_on s₂ $ λ l₂, H l₁ l₂
+
 @[extensionality] theorem ext : ∀ {s t : finmap β}, s.entries = t.entries → s = t
 | ⟨l₁, h₁⟩ ⟨l₂, h₂⟩ H := by congr'
 
+@[simp] theorem ext_iff {s t : finmap β} : s.entries = t.entries ↔ s = t :=
+⟨ext, congr_arg _⟩
+
 /-- The predicate `a ∈ s` means that `s` has a value associated to the key `a`. -/
 instance : has_mem α (finmap β) := ⟨λ a s, a ∈ s.entries.keys⟩
 
@@ -124,13 +131,19 @@ def singleton (a : α) (b : β a) : finmap β :=
 
 variables [decidable_eq α]
 
+instance has_decidable_eq [∀ a, decidable_eq (β a)] : decidable_eq (finmap β)
+| s₁ s₂ := decidable_of_iff _ ext_iff
+
 /-- Look up the value associated to a key in a map. -/
 def lookup (a : α) (s : finmap β) : option (β a) :=
 lift_on s (lookup a) (λ s t, perm_lookup)
 
 @[simp] theorem lookup_to_finmap (a : α) (s : alist β) :
   lookup a ⟦s⟧ = s.lookup a := rfl
 
+@[simp] theorem lookup_empty (a) : lookup a (∅ : finmap β) = none :=
+rfl
+
 theorem lookup_is_some {a : α} {s : finmap β} :
   (s.lookup a).is_some ↔ a ∈ s :=
 induction_on s $ λ s, alist.lookup_is_some
@@ -187,7 +200,7 @@ induction_on s $ λ s, by simp
 induction_on s $ lookup_erase a
 
 @[simp] theorem lookup_erase_ne {a a'} {s : finmap β} (h : a ≠ a') :
-  lookup a' (erase a s) = lookup a' s :=
+  lookup a (erase a' s) = lookup a s :=
 induction_on s $ λ s, lookup_erase_ne h
 
 /- insert -/
@@ -206,8 +219,8 @@ theorem insert_entries_of_neg {a : α} {b : β a} {s : finmap β} : a ∉ s →
 induction_on s $ λ s h,
 by simp [insert_entries_of_neg (mt mem_to_finmap.1 h)]
 
-@[simp] theorem mem_insert {a a' : α} {b : β a} {s : finmap β} :
-  a' ∈ insert a b s ↔ a = a' ∨ a' ∈ s :=
+@[simp] theorem mem_insert {a a' : α} {b' : β a'} {s : finmap β} :
+  a ∈ insert a' b' s ↔ a = a' ∨ a ∈ s :=
 induction_on s mem_insert
 
 @[simp] theorem lookup_insert {a} {b : β a} (s : finmap β) :
@@ -226,4 +239,32 @@ lift_on s (λ t, prod.map id to_finmap (extract a t)) $
   extract a s = (lookup a s, erase a s) :=
 induction_on s $ λ s, by simp [extract]
 
+/- union -/
+
+/-- `s₁ ∪ s₂` is the key-based union of two finite maps. It is left-biased: if
+there exists an `a ∈ s₁`, `lookup a (s₁ ∪ s₂) = lookup a s₁`. -/
+def union (s₁ s₂ : finmap β) : finmap β :=
+lift_on₂ s₁ s₂ (λ s₁ s₂, ⟦s₁ ∪ s₂⟧) $
+λ s₁ s₂ s₃ s₄ p₁₃ p₂₄, to_finmap_eq.mpr $ perm_union p₁₃ p₂₄
+
+instance : has_union (finmap β) := ⟨union⟩
+
+@[simp] theorem mem_union {a} {s₁ s₂ : finmap β} :
+  a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ ∨ a ∈ s₂ :=
+induction_on₂ s₁ s₂ $ λ _ _, mem_union
+
+@[simp] theorem union_to_finmap (s₁ s₂ : alist β) : ⟦s₁⟧ ∪ ⟦s₂⟧ = ⟦s₁ ∪ s₂⟧ :=
+by simp [(∪), union]
+
+theorem keys_union {s₁ s₂ : finmap β} : (s₁ ∪ s₂).keys = s₁.keys ∪ s₂.keys :=
+induction_on₂ s₁ s₂ $ λ s₁ s₂, finset.ext' $ by simp [keys]
+
+@[simp] theorem lookup_union_left {a} {s₁ s₂ : finmap β} :
+  a ∈ s₁ → lookup a (s₁ ∪ s₂) = lookup a s₁ :=
+induction_on₂ s₁ s₂ $ λ s₁ s₂, lookup_union_left
+
+@[simp] theorem lookup_union_right {a} {s₁ s₂ : finmap β} :
+  a ∉ s₁ → lookup a (s₁ ∪ s₂) = lookup a s₂ :=
+induction_on₂ s₁ s₂ $ λ s₁ s₂, lookup_union_right
+
 end finmap

src/data/list/alist.lean

@@ -48,6 +48,8 @@ instance : has_emptyc (alist β) := ⟨⟨[], nodupkeys_nil⟩⟩
 theorem not_mem_empty (a : α) : a ∉ (∅ : alist β) :=
 not_mem_nil a
 
+@[simp] theorem empty_entries : (∅ : alist β).entries = [] := rfl
+
 @[simp] theorem keys_empty : (∅ : alist β).keys = [] := rfl
 
 /- singleton -/
@@ -56,6 +58,9 @@ not_mem_nil a
 def singleton (a : α) (b : β a) : alist β :=
 ⟨[⟨a, b⟩], nodupkeys_singleton _⟩
 
+@[simp] theorem singleton_entries (a : α) (b : β a) :
+  (singleton a b).entries = [sigma.mk a b] := rfl
+
 @[simp] theorem keys_singleton (a : α) (b : β a) : (singleton a b).keys = [a] := rfl
 
 variables [decidable_eq α]
@@ -66,6 +71,9 @@ variables [decidable_eq α]
 def lookup (a : α) (s : alist β) : option (β a) :=
 s.entries.lookup a
 
+@[simp] theorem lookup_empty (a) : lookup a (∅ : alist β) = none :=
+rfl
+
 theorem lookup_is_some {a : α} {s : alist β} :
   (s.lookup a).is_some ↔ a ∈ s := lookup_is_some
 
@@ -124,7 +132,7 @@ perm_kerase s₁.nodupkeys
 lookup_kerase a s.nodupkeys
 
 @[simp] theorem lookup_erase_ne {a a'} {s : alist β} (h : a ≠ a') :
-  lookup a' (erase a s) = lookup a' s :=
+  lookup a (erase a' s) = lookup a s :=
 lookup_kerase_ne h
 
 /- insert -/
@@ -142,8 +150,8 @@ theorem insert_entries_of_neg {a} {b : β a} {s : alist β} (h : a ∉ s) :
   (insert a b s).entries = ⟨a, b⟩ :: s.entries :=
 by rw [insert_entries, kerase_of_not_mem_keys h]
 
-@[simp] theorem mem_insert {a a'} {b : β a} (s : alist β) :
-  a' ∈ insert a b s ↔ a = a' ∨ a' ∈ s :=
+@[simp] theorem mem_insert {a a'} {b' : β a'} (s : alist β) :
+  a ∈ insert a' b' s ↔ a = a' ∨ a ∈ s :=
 mem_keys_kinsert
 
 @[simp] theorem keys_insert {a} {b : β a} (s : alist β) :
@@ -157,8 +165,8 @@ by simp only [insert_entries]; exact perm_kinsert s₁.nodupkeys p
 @[simp] theorem lookup_insert {a} {b : β a} (s : alist β) : lookup a (insert a b s) = some b :=
 by simp only [lookup, insert, lookup_kinsert]
 
-@[simp] theorem lookup_insert_ne {a a'} {b : β a} {s : alist β} (h : a ≠ a') :
-  lookup a' (insert a b s) = lookup a' s :=
+@[simp] theorem lookup_insert_ne {a a'} {b' : β a'} {s : alist β} (h : a ≠ a') :
+  lookup a (insert a' b' s) = lookup a s :=
 lookup_kinsert_ne h
 
 /- extract -/
@@ -175,4 +183,41 @@ end
   extract a s = (lookup a s, erase a s) :=
 by simp [extract]; split; refl
 
+/- union -/
+
+/-- `s₁ ∪ s₂` is the key-based union of two association lists. It is
+left-biased: if there exists an `a ∈ s₁`, `lookup a (s₁ ∪ s₂) = lookup a s₁`.
+-/
+def union (s₁ s₂ : alist β) : alist β :=
+⟨kunion s₁.entries s₂.entries, kunion_nodupkeys s₁.nodupkeys s₂.nodupkeys⟩
+
+instance : has_union (alist β) := ⟨union⟩
+
+@[simp] theorem union_entries {s₁ s₂ : alist β} :
+  (s₁ ∪ s₂).entries = kunion s₁.entries s₂.entries :=
+rfl
+
+@[simp] theorem empty_union {s : alist β} : (∅ : alist β) ∪ s = s :=
+ext rfl
+
+@[simp] theorem union_empty {s : alist β} : s ∪ (∅ : alist β) = s :=
+ext $ by simp
+
+@[simp] theorem mem_union {a} {s₁ s₂ : alist β} :
+  a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ ∨ a ∈ s₂ :=
+mem_keys_kunion
+
+theorem perm_union {s₁ s₂ s₃ s₄ : alist β}
+  (p₁₂ : s₁.entries ~ s₂.entries) (p₃₄ : s₃.entries ~ s₄.entries) :
+  (s₁ ∪ s₃).entries ~ (s₂ ∪ s₄).entries :=
+by simp [perm_kunion s₃.nodupkeys p₁₂ p₃₄]
+
+@[simp] theorem lookup_union_left {a} {s₁ s₂ : alist β} :
+  a ∈ s₁ → lookup a (s₁ ∪ s₂) = lookup a s₁ :=
+lookup_kunion_left
+
+@[simp] theorem lookup_union_right {a} {s₁ s₂ : alist β} :
+  a ∉ s₁ → lookup a (s₁ ∪ s₂) = lookup a s₂ :=
+lookup_kunion_right
+
 end alist

src/data/list/sigma.lean

@@ -363,7 +363,7 @@ end
 lookup_eq_none.mpr (not_mem_keys_kerase a nd)
 
 @[simp] theorem lookup_kerase_ne {a a'} {l : list (sigma β)} (h : a ≠ a') :
-  lookup a' (kerase a l) = lookup a' l :=
+  lookup a (kerase a' l) = lookup a l :=
 begin
   induction l,
   case list.nil { refl },
@@ -377,6 +377,43 @@ begin
   }
 end
 
+theorem kerase_append_left {a} : ∀ {l₁ l₂ : list (sigma β)},
+  a ∈ l₁.keys → kerase a (l₁ ++ l₂) = kerase a l₁ ++ l₂
+| []        _  h  := by cases h
+| (s :: l₁) l₂ h₁ :=
+  if h₂ : a = s.1 then
+    by simp [h₂]
+  else
+    by simp at h₁;
+       cases h₁;
+       [exact absurd h₁ h₂, simp [h₂, kerase_append_left h₁]]
+
+theorem kerase_append_right {a} : ∀ {l₁ l₂ : list (sigma β)},
+  a ∉ l₁.keys → kerase a (l₁ ++ l₂) = l₁ ++ kerase a l₂
+| []        _  h := rfl
+| (_ :: l₁) l₂ h := by simp [not_or_distrib] at h;
+                       simp [h.1, kerase_append_right h.2]
+
+theorem kerase_comm (a₁ a₂) (l : list (sigma β)) :
+  kerase a₂ (kerase a₁ l) = kerase a₁ (kerase a₂ l) :=
+if h : a₁ = a₂ then
+  by simp [h]
+else if ha₁ : a₁ ∈ l.keys then
+  if ha₂ : a₂ ∈ l.keys then
+    match l, kerase a₁ l, exists_of_kerase ha₁, ha₂ with
+    | _, _, ⟨b₁, l₁, l₂, a₁_nin_l₁, rfl, rfl⟩, a₂_in_l₁_app_l₂ :=
+      if h' : a₂ ∈ l₁.keys then
+        by simp [kerase_append_left h',
+                 kerase_append_right (mt (mem_keys_kerase_of_ne h).mp a₁_nin_l₁)]
+      else
+        by simp [kerase_append_right h', kerase_append_right a₁_nin_l₁,
+                 @kerase_cons_ne _ _ _ a₂ ⟨a₁, b₁⟩ _ (ne.symm h)]
+    end
+  else
+    by simp [ha₂, mt mem_keys_of_mem_keys_kerase ha₂]
+else
+  by simp [ha₁, mt mem_keys_of_mem_keys_kerase ha₁]
+
 /- kinsert -/
 
 /-- Insert the pair `⟨a, b⟩` and erase the first pair with the key `a`. -/
@@ -386,9 +423,9 @@ def kinsert (a : α) (b : β a) (l : list (sigma β)) : list (sigma β) :=
 @[simp] theorem kinsert_def {a} {b : β a} {l : list (sigma β)} :
   kinsert a b l = ⟨a, b⟩ :: kerase a l := rfl
 
-@[simp] theorem mem_keys_kinsert {a a'} {b : β a} {l : list (sigma β)} :
-  a' ∈ (kinsert a b l).keys ↔ a = a' ∨ a' ∈ l.keys :=
-by by_cases h : a = a'; [simp [h], simp [h, ne.symm h]]
+@[simp] theorem mem_keys_kinsert {a a'} {b' : β a'} {l : list (sigma β)} :
+  a ∈ (kinsert a' b' l).keys ↔ a = a' ∨ a ∈ l.keys :=
+by by_cases h : a = a'; simp [h]
 
 theorem kinsert_nodupkeys (a) (b : β a) {l : list (sigma β)} (nd : l.nodupkeys) :
   (kinsert a b l).nodupkeys :=
@@ -402,9 +439,9 @@ perm.skip ⟨a, b⟩ $ perm_kerase nd₁ p
   lookup a (kinsert a b l) = some b :=
 by simp only [kinsert, lookup_cons_eq]
 
-@[simp] theorem lookup_kinsert_ne {a a'} {b : β a} {l : list (sigma β)} (h : a ≠ a') :
-  lookup a' (kinsert a b l) = lookup a' l :=
-by simp [h, lookup_cons_ne _ ⟨a, b⟩ (ne.symm h)]
+@[simp] theorem lookup_kinsert_ne {a a'} {b' : β a'} {l : list (sigma β)} (h : a ≠ a') :
+  lookup a (kinsert a' b' l) = lookup a l :=
+by simp [h, lookup_cons_ne _ ⟨a', b'⟩ h]
 
 /- kextract -/
 
@@ -422,4 +459,90 @@ def kextract (a : α) : list (sigma β) → option (β a) × list (sigma β)
     { simp [kextract, ne.symm h, kextract_eq_lookup_kerase l, kerase] }
   end
 
+/- kunion -/
+
+/-- `kunion l₁ l₂` is the append to l₁ of l₂ after, for each key in l₁, the
+first matching pair in l₂ is erased. -/
+def kunion : list (sigma β) → list (sigma β) → list (sigma β)
+| []        l₂ := l₂
+| (s :: l₁) l₂ := s :: kunion l₁ (kerase s.1 l₂)
+
+@[simp] theorem nil_kunion {l : list (sigma β)} : kunion [] l = l :=
+rfl
+
+@[simp] theorem kunion_nil : ∀ {l : list (sigma β)}, kunion l [] = l
+| []       := rfl
+| (_ :: l) := by rw [kunion, kerase_nil, kunion_nil]
+
+@[simp] theorem kunion_cons {s} {l₁ l₂ : list (sigma β)} :
+  kunion (s :: l₁) l₂ = s :: kunion l₁ (kerase s.1 l₂) :=
+rfl
+
+@[simp] theorem mem_keys_kunion {a} {l₁ l₂ : list (sigma β)} :
+  a ∈ (kunion l₁ l₂).keys ↔ a ∈ l₁.keys ∨ a ∈ l₂.keys :=
+begin
+  induction l₁ generalizing l₂,
+  case list.nil { simp },
+  case list.cons : s l₁ ih { by_cases h : a = s.1; [simp [h], simp [h, ih]] }
+end
+
+@[simp] theorem kunion_kerase {a} : ∀ {l₁ l₂ : list (sigma β)},
+  kunion (kerase a l₁) (kerase a l₂) = kerase a (kunion l₁ l₂)
+| []       _ := rfl
+| (s :: _) l := by by_cases h : a = s.1;
+                   simp [h, kerase_comm a s.1 l, kunion_kerase]
+
+theorem kunion_nodupkeys {l₁ l₂ : list (sigma β)}
+  (nd₁ : l₁.nodupkeys) (nd₂ : l₂.nodupkeys) : (kunion l₁ l₂).nodupkeys :=
+begin
+  induction l₁ generalizing l₂,
+  case list.nil { simp only [nil_kunion, nd₂] },
+  case list.cons : s l₁ ih {
+    simp at nd₁,
+    simp [not_or_distrib, nd₁.1, nd₂, ih nd₁.2 (kerase_nodupkeys s.1 nd₂)] }
+end
+
+theorem perm_kunion_left {l₁ l₂ : list (sigma β)} (p : l₁ ~ l₂) (l) :
+  kunion l₁ l ~ kunion l₂ l :=
+begin
+  induction p generalizing l,
+  case list.perm.nil { refl },
+  case list.perm.skip : hd tl₁ tl₂ p ih {
+    simp [ih (kerase hd.1 l), perm.skip] },
+  case list.perm.swap : s₁ s₂ l {
+    simp [kerase_comm, perm.swap] },
+  case list.perm.trans : l₁ l₂ l₃ p₁₂ p₂₃ ih₁₂ ih₂₃ {
+    exact perm.trans (ih₁₂ l) (ih₂₃ l) }
+end
+
+theorem perm_kunion_right : ∀ l {l₁ l₂ : list (sigma β)},
+  l₁.nodupkeys → l₁ ~ l₂ → kunion l l₁ ~ kunion l l₂
+| []       _  _  _   p := p
+| (s :: l) l₁ l₂ nd₁ p :=
+  by simp [perm.skip s
+    (perm_kunion_right l (kerase_nodupkeys s.1 nd₁) (perm_kerase nd₁ p))]
+
+theorem perm_kunion {l₁ l₂ l₃ l₄ : list (sigma β)} (nd₃ : l₃.nodupkeys)
+  (p₁₂ : l₁ ~ l₂) (p₃₄ : l₃ ~ l₄) : kunion l₁ l₃ ~ kunion l₂ l₄ :=
+perm.trans (perm_kunion_left p₁₂ l₃) (perm_kunion_right l₂ nd₃ p₃₄)
+
+@[simp] theorem lookup_kunion_left {a} {l₁ l₂ : list (sigma β)} (h : a ∈ l₁.keys) :
+  lookup a (kunion l₁ l₂) = lookup a l₁ :=
+begin
+  induction l₁ with s _ ih generalizing l₂; simp at h; cases h; cases s with a',
+  { subst h, simp },
+  { rw kunion_cons,
+    by_cases h' : a = a',
+    { subst h', simp },
+    { simp [h', ih h] } }
+end
+
+@[simp] theorem lookup_kunion_right {a} {l₁ l₂ : list (sigma β)} (h : a ∉ l₁.keys) :
+  lookup a (kunion l₁ l₂) = lookup a l₂ :=
+begin
+  induction l₁ generalizing l₂,
+  case list.nil { simp },
+  case list.cons : _ _ ih { simp [not_or_distrib] at h, simp [h.1, ih h.2] }
+end
+
 end list