Balance mantém tamanho #33
Description
No Assignment04.lean o primeiro exercício pedia para mostrarmos que (sort xs).length = xs.length depois da modificação do insert₁, inevitávelmente para fazer isso nós teriamos que ter provas de outros teoremas envolvendo o fato dos balances concervarem o tamanho de uma árvore depois dela ser planificada (.flatten.length), o primeiro motivo de eu criar esse Issue é para compartilhar que eu consegui isso para o Balance, como pode ser visto nessa bagunça ai em baixo que eu tenho a cara de pau de chamar de código, consegui provar para os todos os casos fora o balance: impossible case, ao qual não sei o que fazer com esse caso (segundo motivo de eu ter criado a Issue), um sorry pode ser encontrado nesse caso no código. Não pretendo criar um Pull Request disso pois o meu objetivo é enviar isso com a igualdade final (sort xs).length = xs.length provada, além de que meu código está desorganizado demais e eu também pretendo atualizar para algo mais organizado, dito isso segue o código para qualquer um que deseja utiliza-lo ou ter dor de cabeça devido a tanta desorganização:
lemma flatten_rotr_len (t : Tree Nat) :
(∃ h l x r, t = Tree.node h l x r ∧ ∃ o a y b, l = Tree.node o a y b) →
(rotr t).flatten.length = t.flatten.length := by
cases t with
| null => simp [rotr, Tree.flatten]
| node _ l x r =>
cases l with
| null => simp [rotr, Tree.flatten, node]
| node _ a y b =>
simp [rotr, Tree.flatten, node]
lemma flatten_rotl_len (t : Tree Nat) :
(∃ h l x r, t = Tree.node h l x r ∧ ∃ o a y b, r = Tree.node o a y b) →
(rotl t).flatten.length = t.flatten.length := by
cases t with
| null => simp [rotl, Tree.flatten]
| node _ l x r =>
cases r with
| null => simp [rotl, Tree.flatten, node]
| node _ a y b =>
simp [rotl, Tree.flatten, node]
lemma tree_nonnull_of_height_ge1 {a : Type} (t : Tree a) :
t.height ≥ 1 → t ≠ Tree.null := by
intro h
by_contra contra
rw [contra] at h
simp [Tree.height] at h
lemma exists_node_of_nonnull {a : Type} (t : Tree a) :
t ≠ Tree.null → ∃ l x r, t = Tree.node t.height l x r := by
cases t with
| null =>
intro h
contradiction
| node h l x r =>
intro _
exact ⟨l, x, r, rfl⟩
theorem sub_lt_zero_imp_lt (a b : Nat) : (a: Int) - (b: Int) < 0 → a < b := by
intro h
have := Int.add_lt_add_right h b
simp [Int.sub_eq_add_neg, Int.add_assoc, <- Int.add_assoc, Int.add_comm, Int.add_neg_cancel_right, Int.zero_add] at this
exact this
theorem sub_gt_zero_imp_lt (a b : Nat) : (a: Int) - (b: Int) > 0 → a > b := by
intro h
have := Int.add_lt_add_right h b
simp [Int.sub_eq_add_neg, Int.add_assoc, <- Int.add_assoc, Int.add_comm, Int.add_neg_cancel_right, Int.zero_add] at this
exact this
theorem flatten_balance_len (t1 t2 : Tree Nat) (x : Nat) :
(balance t1 x t2).flatten.length = (node t1 x t2).flatten.length := by
unfold balance
split_ifs with ih₁ ih₂ ih₃
· simp [balance]
· unfold balance.rotateR
split_ifs with ij
· rw [flatten_rotr_len]
rw [node]
apply Exists.intro (node.h t1 t2)
apply Exists.intro t1
apply Exists.intro x
apply Exists.intro t2
constructor
· rfl
· have ht1 : t1.height ≥ 1 := by
simp only [balance.h1, balance.h2] at ih₂
rw [ih₂]
exact Nat.le_add_left _ _
have ht2 : t1 ≠ Tree.null := tree_nonnull_of_height_ge1 t1 ht1
have ht3 : ∃ a y b, t1 = Tree.node t1.height a y b := exists_node_of_nonnull t1 ht2
rcases ht3 with ⟨a, y, b, heq⟩
exact ⟨t1.height, a, y, b, heq⟩
· rw [flatten_rotr_len]
simp[node, Tree.flatten]
rw [flatten_rotl_len]
have hij : bias t1 < 0 := Int.not_le.mp ij
have ht1 : t1.height ≥ 1 := by
simp only [balance.h1, balance.h2] at ih₂
rw [ih₂]
exact Nat.le_add_left _ _
have ht2 : t1 ≠ Tree.null := tree_nonnull_of_height_ge1 t1 ht1
have ht3 : ∃ a y b, t1 = Tree.node t1.height a y b := exists_node_of_nonnull t1 ht2
rcases ht3 with ⟨a, y, b, heq₁⟩
apply Exists.intro t1.height
apply Exists.intro a
apply Exists.intro y
apply Exists.intro b
apply And.intro
· exact heq₁
· have hij: bias t1 < 0 := Int.not_le.mp ij
have h_bias : bias t1 = ↑a.height - ↑b.height := by
rw [heq₁]
simp [bias]
rw [h_bias,] at hij
have hlt : a.height < b.height := sub_lt_zero_imp_lt a.height b.height hij
have hb : 0 < b.height := Nat.lt_of_le_of_lt (Nat.zero_le _) hlt
have hb_nonnull : b ≠ Tree.null := tree_nonnull_of_height_ge1 b hb
have hb_node : ∃ l x r, b = Tree.node b.height l x r := exists_node_of_nonnull b hb_nonnull
rcases hb_node with ⟨l, x, r, heq⟩
exact ⟨b.height, l, x, r, heq⟩
rw [node]
apply Exists.intro (node.h (rotl t1) t2)
apply Exists.intro (rotl t1)
apply Exists.intro x
apply Exists.intro t2
constructor
· rfl
· have hij : bias t1 < 0 := Int.not_le.mp ij
have ht1 : t1.height ≥ 1 := by
simp only [balance.h1, balance.h2] at ih₂
rw [ih₂]
exact Nat.le_add_left _ _
have ht2 : t1 ≠ Tree.null := tree_nonnull_of_height_ge1 t1 ht1
have ht3 : ∃ a y b, t1 = Tree.node t1.height a y b := exists_node_of_nonnull t1 ht2
rcases ht3 with ⟨a, y, b, heq₁⟩
have hij: bias t1 < 0 := Int.not_le.mp ij
have h_bias : bias t1 = ↑a.height - ↑b.height := by
rw [heq₁]
simp [bias]
rw [h_bias,] at hij
have hlt : a.height < b.height := sub_lt_zero_imp_lt a.height b.height hij
have hb : 0 < b.height := Nat.lt_of_le_of_lt (Nat.zero_le _) hlt
have hb_nonnull : b ≠ Tree.null := tree_nonnull_of_height_ge1 b hb
have hb_node : ∃ l x r, b = Tree.node b.height l x r := exists_node_of_nonnull b hb_nonnull
rcases hb_node with ⟨l, x, r, heq⟩
rw [heq₁, heq]
simp [rotl, node]
· unfold balance.rotateL
split_ifs with ij
· rw [flatten_rotl_len]
rw [node]
apply Exists.intro (node.h t1 t2)
apply Exists.intro t1
apply Exists.intro x
apply Exists.intro t2
constructor
· rfl
· have ht1 : t2.height ≥ 1 := by
simp only [balance.h1, balance.h2] at ih₃
rw [ih₃]
exact Nat.le_add_left _ _
have ht2 : t2 ≠ Tree.null := tree_nonnull_of_height_ge1 t2 ht1
have ht3 : ∃ a y b, t2 = Tree.node t2.height a y b := exists_node_of_nonnull t2 ht2
rcases ht3 with ⟨a, y, b, heq⟩
exact ⟨t2.height, a, y, b, heq⟩
· rw [flatten_rotl_len]
simp[node, Tree.flatten]
rw [flatten_rotr_len]
have hij : bias t2 > 0 := Int.not_le.mp ij
have ht1 : t2.height ≥ 1 := by
simp only [balance.h1, balance.h2] at ih₃
rw [ih₃]
exact Nat.le_add_left _ _
have ht2 : t2 ≠ Tree.null := tree_nonnull_of_height_ge1 t2 ht1
have ht3 : ∃ a y b, t2 = Tree.node t2.height a y b := exists_node_of_nonnull t2 ht2
rcases ht3 with ⟨a, y, b, heq₁⟩
apply Exists.intro t2.height
apply Exists.intro a
apply Exists.intro y
apply Exists.intro b
apply And.intro
· exact heq₁
· have hij: bias t2 > 0 := Int.not_le.mp ij
have h_bias : bias t2 = ↑a.height - ↑b.height := by
rw [heq₁]
simp [bias]
rw [h_bias,] at hij
have hlt : a.height > b.height := sub_gt_zero_imp_lt a.height b.height hij
have hb : 0 < a.height := Nat.lt_of_le_of_lt (Nat.zero_le _) hlt
have hb_nonnull : a ≠ Tree.null := tree_nonnull_of_height_ge1 a hb
have hb_node : ∃ l x r, a = Tree.node a.height l x r := exists_node_of_nonnull a hb_nonnull
rcases hb_node with ⟨l, x, r, heq⟩
exact ⟨a.height, l, x, r, heq⟩
rw [node]
apply Exists.intro (node.h t1 (rotr t2))
apply Exists.intro t1
apply Exists.intro x
apply Exists.intro (rotr t2)
constructor
· rfl
· have hij : bias t2 > 0 := Int.not_le.mp ij
have ht1 : t2.height ≥ 1 := by
simp only [balance.h1, balance.h2] at ih₃
rw [ih₃]
exact Nat.le_add_left _ _
have ht2 : t2 ≠ Tree.null := tree_nonnull_of_height_ge1 t2 ht1
have ht3 : ∃ a y b, t2 = Tree.node t2.height a y b := exists_node_of_nonnull t2 ht2
rcases ht3 with ⟨a, y, b, heq₁⟩
have hij: bias t2 > 0 := Int.not_le.mp ij
have h_bias : bias t2 = ↑a.height - ↑b.height := by
rw [heq₁]
simp [bias]
rw [h_bias,] at hij
have hlt : a.height > b.height := sub_gt_zero_imp_lt a.height b.height hij
have hb : 0 < a.height := Nat.lt_of_le_of_lt (Nat.zero_le _) hlt
have hb_nonnull : a ≠ Tree.null := tree_nonnull_of_height_ge1 a hb
have hb_node : ∃ l x r, a = Tree.node a.height l x r := exists_node_of_nonnull a hb_nonnull
rcases hb_node with ⟨l, x, r, heq⟩
rw [heq₁, heq]
simp [rotr, node]
· sorry