Reasoning about functions

Stream: new members

[Julia Scheaffer]

Yesterday while trying to prove something I came up with a question:
Are all functions of the type (α : Type u) → α → α equal to the identity function?

I have written a noncomputable function as a counter example, so it's not universally true. Is it possible to construct a computable counterexample for this or somehow change the definition to only include computable functions?

[Julia Scheaffer]

Here is my counterexample noncomputable function:

import Mathlib

universe u

noncomputable def badFunc {α : Type u} : α -> α := by
  by_cases h : α = ULift Nat
  · subst h
    apply ULift.up ∘ Nat.succ ∘ ULift.down
  · exact id

theorem badFunc.not_id : ¬ ∀ {α : Type u} (a : α), badFunc a = a := by
  push_neg
  use ULift Nat
  use ULift.up 0
  simp [badFunc.eq_def]

[suhr]

See https://homotopytypetheory.org/2017/01/26/parametricity-automorphisms-of-the-universe-and-excluded-middle/

[suhr]

(del)

[Julia Scheaffer]

I guess I should read further into HoTT. :sweat_smile:

[Julia Scheaffer]

I am borrowing a copy from a friend, but I've only made it to chapter 2 so far.

[Julia Scheaffer]

Thank you for the link! I will try reading that.

[Robin Arnez]

Here's a "computable" counterexample:

def badFunc {α : Type u} (x : α) : α :=
  badFunc x
partial_fixpoint

theorem badFunc.not_id : ¬ ∀ {α : Type} (a : α), badFunc a = a := by
  intro h
  have (x : Nat) : badFunc x = Classical.ofNonempty := by
    apply badFunc.fixpoint_induct x (· = Classical.ofNonempty)
    · exact Lean.Order.admissible_flatOrder _ rfl
    · simp
  have : badFunc 0 = badFunc 1 := this 0 ▸ this 1 ▸ rfl
  simp [h] at this

"computable" because it never terminates

[Robin Arnez]

If we restrict ourselves to terminating functions, I believe the theorem is true but there's no way to state it directly

[Robin Arnez]

You would need to build a meta-theory of Lean or something

[Kevin Buzzard]

Isn't this what Wadler's "theorems for free" paper is all about?

[suhr]

Kevin Buzzard said:

Isn't this what Wadler's "theorems for free" paper is all about?

It's about System F rather than MLTT.