Procrasination.lean

section cantor

  /-
    Mapping from natural numbers to integers is injective.
    We map even numbers to positive integers and odd numbers to negative integers.
    0 => 0
    1 => -1
    2 => 1
    3 => -2
    4 => 2
    5 => -3
  -/
  def nat_to_int : Nat -> Int :=
    fun n =>
    match n % 2 == 0 with
    | true => n / 2
    | false => - (n + 1) / 2


  def int_to_nat : Int -> Nat
  | Int.ofNat n => 2 * n
  | Int.negSucc n => 2 * n + 1

/-
  #eval nat_to_int (int_to_nat (-700))
  #eval int_to_nat (nat_to_int 3)
-/
  theorem nat_to_int_injective : ∀ (n : Int),
    nat_to_int (int_to_nat n) = n := by
    intro n
    rcases n with n | n; simp
    . simp [nat_to_int, int_to_nat]
    . simp [int_to_nat, nat_to_int]
      have Ha : (2 * n + 1) % 2 = 1 := by omega
      simp [Ha]
      have Hb : -(2 * ↑n + 1 + 1) / 2 = Int.negSucc ((2 * n + 1) / 2) := by
        exact rfl
      rw [Hb]; simp; omega


  theorem nat_odd : forall (n : Nat), (n % 2 == 0) = false ->
    ∃ m : Nat, n = 2 * m + 1 := by
    intro n ha
    induction n with
    | zero => simp at ha
    | succ n ih =>
      sorry

  theorem nat_even : forall (n : Nat), (n % 2 == 0) = true ->
    ∃ m : Nat, n = 2 * m := by sorry


  theorem int_to_nat_injective : ∀ (n : Nat),
    int_to_nat (nat_to_int n) = n := by
    intro n
    simp [int_to_nat, nat_to_int]
    rcases h : n % 2 == 0 with _ | _; simp
    . have Ha : -(↑n + 1) / 2 = Int.negSucc (n / 2) := by exact rfl
      rw [Ha]; simp
      have Hb : ∃ m : Nat, n = 2 * m + 1 := by
        exact nat_odd n h
      /- I know that n is odd here -/
      omega
    . have Ha : ↑n / 2 = Int.ofNat (n / 2) := by exact rfl
      rw [Ha]; simp
      have Hb : ∃ m : Nat, n = 2 * m := by
        exact nat_even n h
      /- I know n is even here -/
      omega


  def gcd : Nat -> Nat -> Nat
  | 0, b => b
  | a, 0 => a
  | a, b =>
    have ha : 0 < a := by sorry
    have hb : 0 < b := by sorry
    if a < b then gcd a (b % a)
    else gcd (a % b) b
  termination_by a b => a + b
  decreasing_by
    . have hc : a + (b % a) < a + b := by sorry
      exact hc
    . have hc : (a % b) + b < a + b := by sorry
      exact hc



  #eval gcd 3 2
  #check Nat.mod_lt

  def gcd_proof : Nat -> Nat -> Nat := by
    intro a b
    rcases ha : a with _ | ar
    . exact b
    . rcases hb : b with _ | br
      . exact a
      . refine' (if hc : a < b then _ else _)
        . have hd : (b % a) < a  := by
            apply Nat.mod_lt; omega
          exact (gcd_proof a (b % a))
        . have hd : (a % b) < b := by
            apply Nat.mod_lt; omega
          exact (gcd_proof (a % b) b)
    termination_by a b => a + b


  #eval gcd_proof 200 300