A Lean adaptation of https://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/.

SeeminglyImpossibleLeanPrograms.lean

import Aesop

abbrev ℕ := Nat

@[aesop norm unfold]
def InfNat := {f : ℕ → Bool // ∀ n, f n.succ → f n}

namespace InfNat

notation "ℕ∞" => InfNat

def zero : ℕ∞ := ⟨fun _ => false, fun _ => id⟩

def succ : ℕ∞ → ℕ∞
  | ⟨f, inc⟩ =>
    ⟨fun
      | .zero => true
      | .succ a => f a,
    fun
      | .zero => fun _ => rfl
      | .succ _ => inc _⟩
  
def inf : ℕ∞ := ⟨fun _ => true, fun _ => id⟩

@[aesop norm forward]
theorem step (f : ℕ∞) {n : ℕ} : f.val n.succ → f.val n := by
  have := f.property; aesop 

def ofNat : ℕ → ℕ∞
  | .zero => zero
  | .succ a => succ (ofNat a)

instance (n : ℕ) : OfNat ℕ∞ n where
  ofNat := ofNat n

instance : Coe ℕ ℕ∞ where
  coe := ofNat

@[aesop safe forward]
theorem decreasing (f : ℕ∞) {a : ℕ} : ∀ {b : ℕ}, (a ≤ b) → (f.val b → f.val a) := by
  suffices goal : ∀ b : ℕ, f.val (a + b) → f.val a from by
    intro b h hb
    apply goal (b - a)
    rw [← Nat.add_sub_assoc h, Nat.add_sub_cancel_left, hb]
  intro b
  induction b
  case zero => aesop
  case succ b' ih =>
    have := f.property
    aesop (add norm simp [Nat.add_succ])

theorem eq (b : ℕ) (f g : ℕ∞) : (∀ a : ℕ, a < b → f.val a ∧ g.val a) → (f.val b = false) → (g.val b = false) → f = g := by
  intro hbound hfb hgb
  apply Subtype.eq
  funext a
  by_cases h:a < b
  · aesop
  · rw [Nat.not_lt_eq] at h
    have : f.val a = false := by
      have := decreasing f h
      rw [← Bool.not_eq_true]
      simp [hfb] at this
      assumption
    have : g.val a = false := by
      have := decreasing g h
      rw [← Bool.not_eq_true]
      simp [hgb] at this
      assumption   
    aesop

@[aesop norm unfold]
def eval (p : ℕ∞ → Bool) : ℕ → Bool
  | .zero => p ↑.zero
  | .succ a => eval p a ∧ p ↑(.succ a)

def μ (p : ℕ∞ → Bool) : ℕ∞ :=
  ⟨eval p, by aesop⟩


section

def f : ℕ∞ → ℕ := fun _ => 0
def g : ℕ∞ → ℕ := fun n => 
  if n.val 5 then 
    20 -- the answer changes to `true` when this is set to `0`
  else 0

-- whether `f` and `g` agree on all inputs
def p (n : ℕ∞) : Bool := f n = g n

def answer := p (μ p)

#eval answer

end