diff options
| -rw-r--r-- | Common.lean | 1 | ||||
| -rw-r--r-- | Common/BinaryHeap.lean | 144 | ||||
| -rw-r--r-- | Common/Nat.lean | 93 |
3 files changed, 119 insertions, 119 deletions
diff --git a/Common.lean b/Common.lean index 1eedec8..d433fa6 100644 --- a/Common.lean +++ b/Common.lean @@ -6,3 +6,4 @@ import Common.List import Common.Char import Common.Euclid import Common.BinaryHeap +import Common.Nat diff --git a/Common/BinaryHeap.lean b/Common/BinaryHeap.lean index 922e9bf..741318b 100644 --- a/Common/BinaryHeap.lean +++ b/Common/BinaryHeap.lean @@ -1,3 +1,5 @@ +import Common.Nat + namespace BinaryHeap /--A heap, represented as a binary indexed tree. The heap predicate is a type parameter, the index is the element count.-/ @@ -39,122 +41,11 @@ def BinaryHeap.length : BinaryHeap α lt n → Nat := λ_ ↦ n /--Creates an empty BinaryHeap. Needs the heap predicate as parameter.-/ abbrev BinaryHeap.empty {α : Type u} (lt : α → α → Bool ) := BinaryHeap.leaf (α := α) (lt := lt) -private theorem eq_power_of_two_power_of_two (n : Nat) : (n.nextPowerOfTwo = n) → n.isPowerOfTwo := by - have h₂ := Nat.isPowerOfTwo_nextPowerOfTwo n - intro h₁ - revert h₂ - rewrite[h₁] - intro - assumption - -private theorem power_of_two_go_eq_eq (n : Nat) (p : n >0) : Nat.nextPowerOfTwo.go n n p = n := by - unfold Nat.nextPowerOfTwo.go - simp_arith - -private theorem smaller_smaller_exp {n m : Nat} (p : 2 ^ n < 2 ^ m) : n < m := - if h₁ : m ≤ n then - by have h₂ := Nat.pow_le_pow_of_le_right (by decide : 2 > 0) h₁ - have h₃ := Nat.lt_of_le_of_lt h₂ p - simp_arith at h₃ - else - by rewrite[Nat.not_ge_eq] at h₁ - trivial - - - -private theorem mul2_isPowerOfTwo_smaller_smaller_equal (n : Nat) (power : Nat) (h₁ : n.isPowerOfTwo) (h₂ : power.isPowerOfTwo) (h₃ : power < n) : power * 2 ≤ n := by - unfold Nat.isPowerOfTwo at h₁ h₂ - have ⟨k, h₄⟩ := h₁ - have ⟨l, h₅⟩ := h₂ - rewrite [h₅] - rewrite[←Nat.pow_succ 2 l] - rewrite[h₄] - have h₆ : 2 > 0 := by decide - apply (Nat.pow_le_pow_of_le_right h₆) - rewrite [h₅] at h₃ - rewrite [h₄] at h₃ - have h₃ := smaller_smaller_exp h₃ - simp_arith at h₃ - assumption - - -private theorem power_of_two_go_one_eq (n : Nat) (power : Nat) (h₁ : n.isPowerOfTwo) (h₂ : power.isPowerOfTwo) (h₃ : power ≤ n) : Nat.nextPowerOfTwo.go n power (Nat.pos_of_isPowerOfTwo h₂) = n := by - unfold Nat.nextPowerOfTwo.go - split - case inl h₄ => exact power_of_two_go_one_eq n (power*2) (h₁) (Nat.mul2_isPowerOfTwo_of_isPowerOfTwo h₂) (mul2_isPowerOfTwo_smaller_smaller_equal n power h₁ h₂ h₄) - case inr h₄ => rewrite[Nat.not_lt_eq power n] at h₄ - exact Nat.le_antisymm h₃ h₄ -termination_by power_of_two_go_one_eq _ p _ _ _ => n - p -decreasing_by - simp_wf - have := Nat.pos_of_isPowerOfTwo h₂ - apply Nat.nextPowerOfTwo_dec <;> assumption - -private theorem power_of_two_eq_power_of_two (n : Nat) : n.isPowerOfTwo → (n.nextPowerOfTwo = n) := by - intro h₁ - unfold Nat.nextPowerOfTwo - apply power_of_two_go_one_eq - case h₁ => assumption - case h₂ => exact Nat.one_isPowerOfTwo - case h₃ => exact (Nat.pos_of_isPowerOfTwo h₁) - -theorem power_of_two_iff_next_power_eq (n : Nat) : n.isPowerOfTwo ↔ (n.nextPowerOfTwo = n) := - Iff.intro (power_of_two_eq_power_of_two n) (eq_power_of_two_power_of_two n) - -theorem power_of_two_mul_two_lt {n m : Nat} (h₁ : m.isPowerOfTwo) (h₂ : n < 2*m) (h₃ : ¬(n+1).isPowerOfTwo) : n+1 < 2*m := - if h₄ : n+1 > 2*m then by - have h₂ := Nat.succ_le_of_lt h₂ - rewrite[←Nat.not_ge_eq] at h₂ - simp_arith at h₄ - contradiction - else if h₅ : n+1 = 2*m then by - have h₆ := Nat.mul2_isPowerOfTwo_of_isPowerOfTwo h₁ - rewrite[Nat.mul_comm 2 m] at h₅ - rewrite[←h₅] at h₆ - contradiction - else by - simp_arith at h₄ - exact Nat.lt_of_le_of_ne h₄ h₅ - -theorem Nat.mul2_ispowerOfTwo_iff_isPowerOfTwo (n : Nat) : n.isPowerOfTwo ↔ (2*n).isPowerOfTwo := - have h₁ : n.isPowerOfTwo → (2*n).isPowerOfTwo := by - simp[Nat.mul_comm] - apply Nat.mul2_isPowerOfTwo_of_isPowerOfTwo - have h₂ : (2*n).isPowerOfTwo → n.isPowerOfTwo := - if h₂ : n.nextPowerOfTwo = n then by - simp[power_of_two_iff_next_power_eq,h₂] - else by - intro h₃ - simp[←power_of_two_iff_next_power_eq] at h₂ - have h₅ := h₃ - unfold Nat.isPowerOfTwo at h₃ - let ⟨k,h₄⟩ := h₃ - cases n with - | zero => contradiction - | succ m => cases k with - | zero => simp_arith at h₄ - have h₆ (m : Nat) : 2*m+2 > 2^0 := by - induction m with - | zero => decide - | succ o o_ih => simp_arith at * - have h₆ := Nat.le_step $ Nat.le_step o_ih - simp_arith at h₆ - assumption - have h₆ := Nat.ne_of_lt (h₆ m) - simp_arith at h₆ - rewrite[h₄] at h₆ --why is this needed?!? - contradiction - | succ l => rewrite[Nat.pow_succ 2 l] at h₄ - rewrite[Nat.mul_comm (2^l) 2] at h₄ - have h₄ := Nat.eq_of_mul_eq_mul_left (by decide : 0<2) h₄ - exists l - Iff.intro h₁ h₂ - mutual - def Nat.isEven : Nat → Bool + def Nat.isEven : Nat → Prop | .zero => True | .succ n => Nat.isOdd n - def Nat.isOdd : Nat → Bool + def Nat.isOdd : Nat → Prop | .zero => False | .succ n => Nat.isEven n end @@ -210,6 +101,21 @@ theorem Nat.pred_even_odd {n : Nat} (h₁ : Nat.isEven n) (h₂ : n > 0) : Nat.i | succ o => simp[Nat.isEven] at h₁ assumption +theorem power_of_two_mul_two_lt {n m : Nat} (h₁ : m.isPowerOfTwo) (h₂ : n < 2*m) (h₃ : ¬(n+1).isPowerOfTwo) : n+1 < 2*m := + if h₄ : n+1 > 2*m then by + have h₂ := Nat.succ_le_of_lt h₂ + rewrite[←Nat.not_ge_eq] at h₂ + simp_arith at h₄ + contradiction + else if h₅ : n+1 = 2*m then by + have h₆ := Nat.mul2_isPowerOfTwo_of_isPowerOfTwo h₁ + rewrite[Nat.mul_comm 2 m] at h₅ + rewrite[←h₅] at h₆ + contradiction + else by + simp_arith at h₄ + exact Nat.lt_of_le_of_ne h₄ h₅ + theorem power_of_two_mul_two_le {n m : Nat} (h₁ : (n+1).isPowerOfTwo) (h₂ : n < 2*(m+1)) (h₃ : ¬(m+1).isPowerOfTwo) (h₄ : m > 0): n < 2*m := if h₅ : n > 2*m then by simp_arith at h₂ @@ -253,7 +159,7 @@ def BinaryHeap.insert (elem : α) (heap : BinaryHeap α lt o) : BinaryHeap α lt rewrite[s] simp[r] have difference_decreased := Nat.le_succ_of_le $ Nat.le_succ_of_le max_height_difference - let result := branch a left (right.insert elem) (q) difference_decreased (by simp[(eq_power_of_two_power_of_two (n+1)), r]) + let result := branch a left (right.insert elem) (q) difference_decreased (by simp[(Nat.power_of_two_iff_next_power_eq (n+1)), r]) result else have q : m ≤ n+1 := by apply (Nat.le_of_succ_le) @@ -274,7 +180,7 @@ def BinaryHeap.insert (elem : α) (heap : BinaryHeap α lt o) : BinaryHeap α lt contradiction else by simp at h₁ - rewrite[←power_of_two_iff_next_power_eq] at h₁ + rewrite[←Nat.power_of_two_iff_next_power_eq] at h₁ cases subtree_complete case inl => contradiction case inr => trivial @@ -283,7 +189,7 @@ def BinaryHeap.insert (elem : α) (heap : BinaryHeap α lt o) : BinaryHeap α lt cases r case inl h₁ => rewrite[Nat.not_gt_eq n m] at h₁ simp_arith[Nat.le_antisymm h₁ p] - case inr h₁ => simp[←power_of_two_iff_next_power_eq] at h₁ + case inr h₁ => simp[←Nat.power_of_two_iff_next_power_eq] at h₁ simp[h₁] at subtree_complete exact power_of_two_mul_two_lt subtree_complete max_height_difference h₁ let result := branch a (left.insert elem) right q still_in_range (Or.inr right_is_power_of_two) @@ -342,7 +248,7 @@ def BinaryHeap.popLast {α : Type u} {lt : α → α → Bool} (heap : BinaryHea simp[a] have rightIsFull : (m+1).isPowerOfTwo := by have r := And.right r - simp[←power_of_two_iff_next_power_eq] at r + simp[←Nat.power_of_two_iff_next_power_eq] at r assumption have l_lt_2_m_succ : l < 2 * (m+1) := by apply Nat.lt_of_succ_lt; assumption (res, q▸BinaryHeap.branch a newLeft right s l_lt_2_m_succ (Or.inr rightIsFull)) @@ -380,7 +286,7 @@ def BinaryHeap.popLast {α : Type u} {lt : α → α → Bool} (heap : BinaryHea rewrite[←h₂] at subtree_complete simp at subtree_complete assumption - case inr h₁ => simp_arith[←power_of_two_iff_next_power_eq] at h₁ + case inr h₁ => simp_arith[←Nat.power_of_two_iff_next_power_eq] at h₁ rewrite[h₂] at h₁ simp[h₁] at subtree_complete assumption @@ -393,7 +299,7 @@ def BinaryHeap.popLast {α : Type u} {lt : α → α → Bool} (heap : BinaryHea have h₄ := Nat.mul_lt_mul_of_pos_right (by decide : 1 < 2) this simp at h₄ assumption - | inr h₁ => simp[←power_of_two_iff_next_power_eq, h₂] at h₁ + | inr h₁ => simp[←Nat.power_of_two_iff_next_power_eq, h₂] at h₁ apply power_of_two_mul_two_le <;> assumption (res, BinaryHeap.branch a left newRight s still_in_range (Or.inl leftIsFull)) diff --git a/Common/Nat.lean b/Common/Nat.lean new file mode 100644 index 0000000..71420ed --- /dev/null +++ b/Common/Nat.lean @@ -0,0 +1,93 @@ + +theorem Nat.power_of_two_go_eq_eq (n : Nat) (p : n >0) : Nat.nextPowerOfTwo.go n n p = n := by + unfold Nat.nextPowerOfTwo.go + simp_arith + +theorem Nat.smaller_smaller_exp {n m o : Nat} (p : o ^ n < o ^ m) (q : o > 0) : n < m := + if h₁ : m ≤ n then + by have h₂ := Nat.pow_le_pow_of_le_right (q) h₁ + have h₃ := Nat.lt_of_le_of_lt h₂ p + simp_arith at h₃ + else + by rewrite[Nat.not_ge_eq] at h₁ + trivial + +private theorem mul2_isPowerOfTwo_smaller_smaller_equal (n : Nat) (power : Nat) (h₁ : n.isPowerOfTwo) (h₂ : power.isPowerOfTwo) (h₃ : power < n) : power * 2 ≤ n := by + unfold Nat.isPowerOfTwo at h₁ h₂ + have ⟨k, h₄⟩ := h₁ + have ⟨l, h₅⟩ := h₂ + rewrite [h₅] + rewrite[←Nat.pow_succ 2 l] + rewrite[h₄] + have h₆ : 2 > 0 := by decide + apply (Nat.pow_le_pow_of_le_right h₆) + rewrite [h₅] at h₃ + rewrite [h₄] at h₃ + have h₃ := Nat.smaller_smaller_exp h₃ + simp_arith at h₃ + assumption + +private theorem power_of_two_go_one_eq (n : Nat) (power : Nat) (h₁ : n.isPowerOfTwo) (h₂ : power.isPowerOfTwo) (h₃ : power ≤ n) : Nat.nextPowerOfTwo.go n power (Nat.pos_of_isPowerOfTwo h₂) = n := by + unfold Nat.nextPowerOfTwo.go + split + case inl h₄ => exact power_of_two_go_one_eq n (power*2) (h₁) (Nat.mul2_isPowerOfTwo_of_isPowerOfTwo h₂) (mul2_isPowerOfTwo_smaller_smaller_equal n power h₁ h₂ h₄) + case inr h₄ => rewrite[Nat.not_lt_eq power n] at h₄ + exact Nat.le_antisymm h₃ h₄ +termination_by power_of_two_go_one_eq _ p _ _ _ => n - p +decreasing_by + simp_wf + have := Nat.pos_of_isPowerOfTwo h₂ + apply Nat.nextPowerOfTwo_dec <;> assumption + +private theorem power_of_two_eq_power_of_two (n : Nat) : n.isPowerOfTwo → (n.nextPowerOfTwo = n) := by + intro h₁ + unfold Nat.nextPowerOfTwo + apply power_of_two_go_one_eq + case h₁ => assumption + case h₂ => exact Nat.one_isPowerOfTwo + case h₃ => exact (Nat.pos_of_isPowerOfTwo h₁) + +private theorem eq_power_of_two_power_of_two (n : Nat) : (n.nextPowerOfTwo = n) → n.isPowerOfTwo := by + have h₂ := Nat.isPowerOfTwo_nextPowerOfTwo n + intro h₁ + revert h₂ + rewrite[h₁] + intro + assumption + +theorem Nat.power_of_two_iff_next_power_eq (n : Nat) : n.isPowerOfTwo ↔ (n.nextPowerOfTwo = n) := + Iff.intro (power_of_two_eq_power_of_two n) (eq_power_of_two_power_of_two n) + +theorem Nat.mul2_ispowerOfTwo_iff_isPowerOfTwo (n : Nat) : n.isPowerOfTwo ↔ (2*n).isPowerOfTwo := + have h₁ : n.isPowerOfTwo → (2*n).isPowerOfTwo := by + simp[Nat.mul_comm] + apply Nat.mul2_isPowerOfTwo_of_isPowerOfTwo + have h₂ : (2*n).isPowerOfTwo → n.isPowerOfTwo := + if h₂ : n.nextPowerOfTwo = n then by + simp[power_of_two_iff_next_power_eq,h₂] + else by + intro h₃ + simp[←power_of_two_iff_next_power_eq] at h₂ + have h₅ := h₃ + unfold Nat.isPowerOfTwo at h₃ + let ⟨k,h₄⟩ := h₃ + cases n with + | zero => contradiction + | succ m => cases k with + | zero => simp_arith at h₄ + have h₆ (m : Nat) : 2*m+2 > 2^0 := by + induction m with + | zero => decide + | succ o o_ih => simp_arith at * + have h₆ := Nat.le_step $ Nat.le_step o_ih + simp_arith at h₆ + assumption + have h₆ := Nat.ne_of_lt (h₆ m) + simp_arith at h₆ + rewrite[h₄] at h₆ --why is this needed?!? + contradiction + | succ l => rewrite[Nat.pow_succ 2 l] at h₄ + rewrite[Nat.mul_comm (2^l) 2] at h₄ + have h₄ := Nat.eq_of_mul_eq_mul_left (by decide : 0<2) h₄ + exists l + Iff.intro h₁ h₂ |