feat(library/data/rbmap): add find_insert lemmas for rbmap

library/data/rbmap/default.lean

@@ -235,6 +235,52 @@ end
 lemma find_insert [is_strict_weak_order α lt] (m : rbmap α β lt) (k : α) (v : β) : (m.insert k v).find k = some v :=
 find_insert_of_eqv m v (refl k)
 
+lemma find_entry_insert_of_disj [is_strict_weak_order α lt] {k₁ k₂ : α} (m : rbmap α β lt) (v : β) : lt k₁ k₂ ∨ lt k₂ k₁ → (m.insert k₁ v).find_entry k₂ = m.find_entry k₂ :=
+begin
+  intro h,
+  have h' : ∀ {v₁ v₂ : β}, (rbmap_lt lt) (k₁, v₁) (k₂, v₂) ∨ (rbmap_lt lt) (k₂, v₂) (k₁, v₁) := λ _ _, h,
+  generalize h₁ : m = m₁,
+  generalize h₂ : insert m₁ k₁ v = m₂,
+  rw [←h₁] at h₂ ⊢, rw [←h₂],
+  cases m₁ with t₁ p₁; cases t₁; cases m₂ with t₂ p₂; cases t₂,
+  { rw [h₂, h₁] },
+  twice {
+    rw [h₂],
+    conv { to_lhs, simp [find_entry] },
+    rw [←h₂, insert, rbtree.find_insert_of_disj _ h', h₁],
+    refl },
+  any_goals { simp [insert] at h₂,
+    exact absurd h₂ (rbtree.insert_ne_mk_rbtree m (k₁, v)) },
+  any_goals {
+    rw [h₂, h₁], simp [find_entry], rw [←h₂, ←h₁, insert, rbtree.find_insert_of_disj _ h'],
+    apply rbtree.find_eq_find_of_eqv, apply eqv_entries }
+end
+
+lemma find_entry_insert_of_not_eqv [is_strict_weak_order α lt] {k₁ k₂ : α} (m : rbmap α β lt) (v : β) : ¬ k₁ ≈[lt] k₂ → (m.insert k₁ v).find_entry k₂ = m.find_entry k₂ :=
+begin
+  intro hn,
+  have he : lt k₁ k₂ ∨ lt k₂ k₁, {
+    simp [strict_weak_order.equiv, decidable.not_and_iff_or_not, decidable.not_not_iff] at hn,
+    assumption },
+  apply find_entry_insert_of_disj _ _ he
+end
+
+lemma find_entry_insert_of_ne [is_strict_total_order α lt] {k₁ k₂ : α} (m : rbmap α β lt) (v : β) : k₁ ≠ k₂ → (m.insert k₁ v).find_entry k₂ = m.find_entry k₂ :=
+begin
+  intro h,
+  have : ¬ k₁ ≈[lt] k₂ := λ h', h (eq_of_eqv_lt h'),
+  apply find_entry_insert_of_not_eqv _ _ this
+end
+
+lemma find_insert_of_disj [is_strict_weak_order α lt] {k₁ k₂ : α} (m : rbmap α β lt) (v : β) : lt k₁ k₂ ∨ lt k₂ k₁ → (m.insert k₁ v).find k₂ = m.find k₂ :=
+begin intro h, have := find_entry_insert_of_disj m v h, simp [find, this] end
+
+lemma find_insert_of_not_eqv [is_strict_weak_order α lt] {k₁ k₂ : α} (m : rbmap α β lt) (v : β) : ¬ k₁ ≈[lt] k₂ → (m.insert k₁ v).find k₂ = m.find k₂ :=
+begin intro h, have := find_entry_insert_of_not_eqv m v h, simp [find, this] end
+
+lemma find_insert_of_ne [is_strict_total_order α lt] {k₁ k₂ : α} (m : rbmap α β lt) (v : β) : k₁ ≠ k₂ → (m.insert k₁ v).find k₂ = m.find k₂ :=
+begin intro h, have := find_entry_insert_of_ne m v h, simp [find, this] end
+
 lemma mem_of_min_eq [is_strict_total_order α lt] {k : α} {v : β} {m : rbmap α β lt} : m.min = some (k, v) → k ∈ m :=
 λ h, to_rbmap_mem (rbtree.mem_of_min_eq h)
 

library/data/rbtree/insert.lean

@@ -129,7 +129,6 @@ end
 
 end rbnode
 
-
 namespace rbnode
 section membership_lemmas
 parameters {α : Type u} (lt : α → α → Prop) [decidable_rel lt]
@@ -196,6 +195,15 @@ begin
   { intros, simp [ins, *], apply balance2_node_ne_leaf, assumption },
 end
 
+lemma insert_ne_leaf (t : rbnode α) (x : α) : insert lt t x ≠ leaf :=
+begin
+  simp [insert],
+  generalize he : ins lt t x = t',
+  cases t'; simp [flip_red],
+  { have := ins_ne_leaf lt t x, contradiction },
+  all_goals { contradiction }
+end
+
 lemma mem_ins_of_incomp (t : rbnode α) {x y : α} : ∀ h : ¬ lt x y ∧ ¬ lt y x, x ∈ t.ins lt y :=
 begin
   apply ins.induction lt t y,

library/data/rbtree/main.lean

@@ -41,6 +41,9 @@ end
 
 variables [decidable_rel lt]
 
+lemma insert_ne_mk_rbtree (t : rbtree α lt) (a : α) : t.insert a ≠ mk_rbtree α lt :=
+begin cases t with n p, simp [insert, mk_rbtree], intro h, injection h with h', apply rbnode.insert_ne_leaf lt n a h' end
+
 lemma find_correct [is_strict_weak_order α lt] (a : α) (t : rbtree α lt) : a ∈ t ↔ (∃ b, t.find a = some b ∧ a ≈[lt] b) :=
 begin cases t, apply rbnode.find_correct, apply rbnode.is_searchable_of_well_formed, assumption end
 
@@ -60,13 +63,13 @@ begin cases t, intro h, apply rbnode.find_insert_of_eqv lt h, apply rbnode.is_se
 lemma find_insert [is_strict_weak_order α lt] (t : rbtree α lt) (x) : (t.insert x).find x = some x :=
 find_insert_of_eqv t (refl x)
 
-lemma find_insert_of_disj [is_strict_weak_order α lt] {x y : α} {t : rbtree α lt} : lt x y ∨ lt y x → (t.insert x).find y = t.find y :=
+lemma find_insert_of_disj [is_strict_weak_order α lt] {x y : α} (t : rbtree α lt) : lt x y ∨ lt y x → (t.insert x).find y = t.find y :=
 begin cases t, intro h, apply rbnode.find_insert_of_disj lt h, apply rbnode.is_searchable_of_well_formed, assumption end
 
-lemma find_insert_of_not_eqv [is_strict_weak_order α lt] {x y : α} {t : rbtree α lt} : ¬ x ≈[lt] y → (t.insert x).find y = t.find y :=
+lemma find_insert_of_not_eqv [is_strict_weak_order α lt] {x y : α} (t : rbtree α lt) : ¬ x ≈[lt] y → (t.insert x).find y = t.find y :=
 begin cases t, intro h, apply rbnode.find_insert_of_not_eqv lt h, apply rbnode.is_searchable_of_well_formed, assumption end
 
-lemma find_insert_of_not_eq [is_strict_total_order α lt] {x y : α} {t : rbtree α lt} : ¬ x = y → (t.insert x).find y = t.find y :=
+lemma find_insert_of_ne [is_strict_total_order α lt] {x y : α} (t : rbtree α lt) : x ≠ y → (t.insert x).find y = t.find y :=
 begin
   cases t, intro h,
   have : ¬ x ≈[lt] y := λ h', h (eq_of_eqv_lt h'),