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
75. 75
76. 76
77. 77
78. 78
79. 79
80. 80
81. 81
82. 82
83. 83
84. 84
85. 85
86. 86
87. 87
88. 88

import Std.Tactic.Do
import Mathlib


namespace Paradox

-- https://leanprover.zulipchat.com/#narrow/channel/236446-Type-theory/topic/Paradoxes.20and.20Type.20Universes/with/538016579

axiom Bad : Type

axiom bad : (α : Type) × α ↪ Bad

noncomputable def k (P : Bad → Prop) : Bad :=
  bad ⟨Bad → Prop, P⟩

def Q (b : Bad) : Prop :=
  ∃ P, k P = b ∧ ¬P b

theorem k_injective : k.Injective :=
  fun _ _ hab => eq_of_heq
    (Sigma.mk.inj (bad.injective hab)).2

theorem down (h : Q (k Q)) : ¬Q (k Q) :=
  h.elim fun _ hP =>
    (congrArg Not (congrFun (k_injective hP.1) (k Q))).mp hP.2

theorem up (h : ¬Q (k Q)) : Q (k Q) :=
  ⟨Q, rfl, h⟩

theorem false : False :=
  down (up fun h => down h h) (up fun h => down h h)

-- 'false' depends on axioms: [Bad, bad]
#print axioms Paradox.false

end Paradox



inductive Fmt where
  | Arg : Fmt → Fmt
  | Nat : Fmt → Fmt
  | Char : Char → Fmt → Fmt
  | End

def toFmt : List Char → Fmt
  | '*' :: xs => .Arg <| toFmt xs
  | '#' :: xs => .Nat <| toFmt xs
  | x :: xs => .Char x <| toFmt xs
  | [] => .End

def FormatType : Fmt → Type 1
  | .Arg fmt => {α : Type} → [ToString α] → α → FormatType fmt
  | .Nat fmt => Nat → FormatType fmt
  | .Char _ fmt => FormatType fmt
  | .End => PLift String

def format (fmt : String) : FormatType <| toFmt fmt.toList :=
  let rec formatAux (acc : String) : (fmt : Fmt) → FormatType fmt
    | .Arg fmt => fun x ↦ formatAux (acc ++ toString x) fmt
    | .Nat fmt => fun x ↦ formatAux (acc ++ "#" ++ toString x) fmt
    | .Char c fmt => formatAux (acc.push c) fmt
    | .End => .up acc
  formatAux "" <| toFmt fmt.toList

#eval format "Hello * # * *" (-1) 1 [42, 69] "Meow" |>.down





-- TODO: prove binary search

def Array.binarySearch (A : Array ℕ) (x : ℕ) := Id.run do
  let n := A.size
  let mut l : Fin (n + 1) := 0
  let mut r : Fin (n + 1) := ⟨n, by grind⟩
  while h : l < r do
    let m : Fin (n + 1) := ⟨(l.val + r.val) / 2, by grind⟩
    if A[m]'(by grind) < x then
      l := m + 1
    else
      r := m
  return l

open Std.Do in
lemma binarySearchCorrect (A : Array ℕ) (hA : A.Pairwise (· ≤ ·)) : ∀ i (hi : i < A.binarySearch x), A[i] < x := by
  sorry