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

import Mathlib

-- example [Monoid S] (h₁ : ∀ x : S, e₁ * x = x ∧ x * e₁ = x) (h₂ : ∀ x : S, e₂ * x = x ∧ x * e₂ = x) : e₁ = e₂ := by
--   grind [h₁ e₂]


def g : Bool → ℕ
  | true => 0
  | false => 1

#print g

#check Bool.rec (motive := fun _ ↦ ℕ) 0 1

noncomputable def g'' := Bool.rec (motive := fun _ ↦ ℕ) 0 1

example : g'' true = 1 := by decide

#check fun t ↦ Bool.recOn (motive := fun _ ↦ ℕ) t 0 1

-- noncomputable def g' t := Bool.recOn (motive := fun _ ↦ ℕ) t 0 1


#check List.rec

#check List.brecOn

def len : List α → ℕ
  | [] => 0
  | _ :: xs => 1 + len xs

#print len

noncomputable def len' (x : List α) : ℕ :=
  List.rec (motive := fun _ ↦ ℕ) 0 (fun _ _ l ↦ 1 + l) x

#simp [len'] len' [1, 2, 3]

example : len' [1, 2, 3] = 3 := by decide


-- def len2.{u_1} : {α : Type u_1} → List α → ℕ :=
-- fun {α} x ↦
--   List.brecOn x fun x f ↦
--     (match (motive := (x : List α) → List.below x → ℕ) x with
--       | [] => fun x ↦ 0
--       | head :: xs => fun x ↦ 1 + x.1)
--       f


#check Lean.trustCompiler


-- https://www.joachim-breitner.de/blog/817-F91_in_Lean

def f91 (n : ℕ) : Option ℕ :=
  if n > 100 then
    pure (n - 10)
  else
    f91 (n + 11) >>= f91
partial_fixpoint

theorem f91_spec_high (n : Nat) (h : 100 < n) : f91 n = some (n - 10) := by
  unfold f91
  grind

theorem f91_spec_low (n : Nat) (h₂ : n ≤ 100) : f91 n = some 91 := by
  unfold f91

theorem f91_spec (n : Nat) : f91 n = some (if n ≤ 100 then 91 else n - 10) := by


theorem f91_total (n : Nat) : (f91 n).isSome := by
  grind