leanexe/LeanExe/Examples/Collatz.lean at main · jsmorph/leanexe · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
namespace LeanExe.Examples.Collatz

def maxSteps : Nat :=
  10000

def next (n : UInt64) : UInt64 :=
  if n % 2 == 0 then
    n / 2
  else
    n * 3 + 1

def stepsFuel : Nat → UInt64 → UInt64 → UInt64
  | 0, _, steps => steps
  | fuel + 1, n, steps =>
      if n == 0 || n == 1 then
        steps
      else
        stepsFuel fuel (next n) (steps + 1)

def steps (n : UInt64) : UInt64 :=
  stepsFuel maxSteps n 0

def maxOddBeforeTripleAddOne : UInt64 :=
  6148914691236517204

def lengthFuel : Nat -> UInt64 -> UInt64 -> Option UInt64
  | 0, n, len =>
      if n == 1 then
        some len
      else
        none
  | fuel + 1, n, len =>
      if n == 0 || n == 1 || (!(n % 2 == 0) && n > maxOddBeforeTripleAddOne) then
        if n == 1 then
          some len
        else
          none
      else
        lengthFuel fuel (if n % 2 == 0 then n / 2 else n * 3 + 1) (len + 1)

def length? (n : UInt64) : Option UInt64 :=
  if n == 0 then
    none
  else
    lengthFuel maxSteps n 1

def benchFuel : Nat → UInt64 → UInt64 → UInt64
  | 0, _, acc => acc
  | fuel + 1, n, acc =>
      benchFuel fuel n (acc + steps n)

def bench (n iters : UInt64) : UInt64 :=
  benchFuel iters.toNat n 0

theorem stepsFuel_one (fuel : Nat) (steps : UInt64) :
    stepsFuel fuel 1 steps = steps := by
  cases fuel <;> simp [stepsFuel]

theorem stepsFuel_zero (fuel : Nat) (steps : UInt64) :
    stepsFuel fuel 0 steps = steps := by
  cases fuel <;> simp [stepsFuel]

theorem steps_one :
    steps 1 = 0 := by
  exact stepsFuel_one maxSteps 0

theorem steps_zero :
    steps 0 = 0 := by
  exact stepsFuel_zero maxSteps 0

end LeanExe.Examples.Collatz