From f7ac27f54a76582354964bae21ee03937c108187 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Fri, 12 Jul 2024 22:01:57 +0200
Subject: Squashed commit of the following:

commit 7aeefe2e761a4892ff2f438e00f3ec7e6d286c5c
Author: Andreas Grois <andi@grois.info>
Date:   Fri Jul 12 21:59:44 2024 +0200

    Finish Lean 4.9 update.

commit 8a5576ae983203035f6bf0c807b36f1b4d7b63a6
Author: Andreas Grois <andi@grois.info>
Date:   Fri Jul 12 21:40:21 2024 +0200

    Lean 4.9 upgrade, heap is where it was before...

commit db34881e21391c96a6a0b939552b0f6f77d05bd8
Author: Andreas Grois <andi@grois.info>
Date:   Fri Jul 12 00:31:22 2024 +0200

    Further Lean 4.9 compat...

commit 22444613d58c5bd1a3fcdad0cd6c8d3aee1f3214
Author: Andreas Grois <andi@grois.info>
Date:   Thu Jul 11 22:15:11 2024 +0200

    Further Lean 4.9 porting

commit a4ace32cbb02959f9625578b511c2486e0816367
Author: Andreas Grois <andi@grois.info>
Date:   Wed Jul 10 23:18:29 2024 +0200

    Continue porting to Lean 4.9

commit d0f411bcc42b5cb7c72c2ed65ae35875c72e95dd
Author: Andreas Grois <andi@grois.info>
Date:   Wed Jul 10 23:10:34 2024 +0200

    Continue port to Lean 4.9

commit 835ce644b97840048de0df40676ff6f3a8b99985
Author: Andreas Grois <andi@grois.info>
Date:   Wed Jul 10 22:14:59 2024 +0200

    Partial port to Lean 4.9. Not compiling yet.
---
 Common/Nat.lean | 23 ++++++-----------------
 1 file changed, 6 insertions(+), 17 deletions(-)

(limited to 'Common/Nat.lean')

diff --git a/Common/Nat.lean b/Common/Nat.lean
index 9d4d538..e921f2b 100644
--- a/Common/Nat.lean
+++ b/Common/Nat.lean
@@ -30,10 +30,10 @@ private theorem mul2_isPowerOfTwo_smaller_smaller_equal (n : Nat) (power : Nat)
 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
+  case isTrue 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 isFalse h₄ => rewrite[Nat.not_lt_eq power n] at h₄
+                     exact Nat.le_antisymm h₃ h₄
+termination_by n - power
 decreasing_by
   simp_wf
   have := Nat.pos_of_isPowerOfTwo h₂
@@ -75,17 +75,6 @@ theorem Nat.mul2_ispowerOfTwo_iff_isPowerOfTwo (n : Nat) : n.isPowerOfTwo ↔ (2
       | 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₄
@@ -128,7 +117,7 @@ mutual
                 exact (Nat.not_odd_even (by simp[h₁]))
   private theorem Nat.not_odd_even {n : Nat} (h₁ : ¬Nat.isOdd n) : (Nat.isEven n) := by
     cases n with
-    | zero => trivial
+    | zero => simp[isEven]
     | succ o => simp[Nat.isEven, Nat.isOdd] at *
                 exact (Nat.not_even_odd (by simp[h₁]))
 end
@@ -141,7 +130,7 @@ mutual
                 simp[Nat.odd_not_even h₁]
   private theorem Nat.odd_not_even {n : Nat} (h₁ : Nat.isOdd n) : ¬(Nat.isEven n ):= by
     cases n with
-    | zero => contradiction
+    | zero => unfold isOdd at h₁; contradiction
     | succ o => simp[Nat.isEven, Nat.isOdd] at *
                 simp[Nat.even_not_odd h₁]
 end
-- 
cgit v1.2.3

