noConfusionType

Stream: mathlib4

[Emily Riehl]

I'd like to better understand Bool.noConfusionType and Nat.noConfusionType.

Firstly, is this a general construction for any inductive type? Can I see the source code anywhere?

When I print Bool.noConfusionType I see:

@[reducible] protected def Bool.noConfusionType.{u} : Sort u → Bool → Bool → Sort u :=
fun P x1 x2 ↦ Bool.casesOn x1 (Bool.casesOn x2 (P → P) P) (Bool.casesOn x2 P (P → P))

When P is False or Empty, this looks very close to the observational equality type of Bool. But how should I think about this parameter P in general? What other cases of P are useful?

When I print Nat.noConfusionType I see:

@[reducible] protected def Nat.noConfusionType.{u} : Sort u → ℕ → ℕ → Sort u :=
fun P x1 x2 ↦ Nat.casesOn x1 (Nat.casesOn x2 (P → P) fun n ↦ P) fun n ↦ Nat.casesOn x2 P fun n_1 ↦ (n = n_1 → P) → P

Again when P is False or Empty I can see that this is equivalent to the observation equality type of Nat. In the final inductive step for n n_1 : Nat it defines Nat.noConfusionType P n.succ n_1.succ to be (n = n_1 -> P) -> P which is equivalent to P -> P in the case the equality is true and P in the case the equality is false.

Tl;dr: I've never seen this construction before. Can someone explain both where it comes from (theoretically) and where it is defined in mathlib?

[Aaron Liu]

basically, it's a way to conclude constructor injectivity from pattern-matching

[Aaron Liu]

I don't think it's defined anywhere in mathlib, it's automatically generated for each inductive type you have

[Aaron Liu]

maybe I can find you the code that does this generation

[Aaron Liu]

it's stated for an arbitrary P so you don't have to compose with False.elim or Empty.elim when you're using it to derive a contradiction ...probably

[Alex Meiburg]

Kevin Buzzard has a post about noConfusion here: https://xenaproject.wordpress.com/2018/03/24/no-confusion-over-no_confusion/
and according to https://lean-lang.org/doc/reference/4.21.0/The-Type-System/Inductive-Types/ , noConfusionType is used to build that.

[Aaron Liu]

found it docs#Lean.mkNoConfusion

[Aaron Liu]

don't know how helpful it will be but that's the code that creates the no confusion types

[Aaron Liu]

I think of (n = n_1 -> P) -> P as a cps-transform of n = n_1

[Aaron Liu]

so you're actually concluding n = n_1 which you can see by setting P := (n = n_1) and passing in id

[Aaron Liu]

but this way you can pass in a continuation

[Aaron Liu]

idk maybe it's not actually that useful

[Aaron Liu]

I guess it's also good to be consistent and have your return type always be P

[Emily Riehl]

What does "cps-transform" mean?

[Emily Riehl]

I'm familiar with what this is used for (from HoTT where we use the observational equality types to similar ends). But I don't understand the specific construction with the parameter P.

[Aaron Liu]

continuation passing style

[Aaron Liu]

it takes a type C and turns it into (C -> R) -> R

[Aaron Liu]

see docs#Cont

[Emily Riehl]

Thanks. I'm understanding better.

This may be too much to hope for but is there some sort of parametricity result (warning: I don't actually understand parametricity) that proves this:

lemma nat_for_free {B S T : Type} (φ : ∀ (R : Type), (B → R) → R) (f : B → S) (g : S → T) :
  g (φ S f) = φ T (g ∘ f) := by
  have := φ (S → T)
  have := φ B
  sorry

Because if so we have

def yoneda {B : Type} : B ≃ ∀ (R : Type), (B → R) → R where
  toFun b R f := f b
  invFun φ := φ B id
  left_inv b := rfl
  right_inv φ := by
    ext R f
    simp
    apply nat_for_free

[Alex Meiburg]

Parametericity doesn't hold in Lean's theory, it's essentially incompatible with choice. (yoneda is false.)

[Kenny Lau]

Emily Riehl said:

parametricity result (warning: I don't actually understand parametricity)

the only thing i know about parametricity is that you can never prove parametricity (inside the language) :melt:

[Alex Meiburg]

See #lean4 > Parametericity @ 💬 for a nice counterexample from Kyle Miller

[Emily Riehl]

Ah, right of course. I was leveraging intuitions from a different formal system which is constructive and where a result similar to this is true. Thanks.

[Aaron Liu]

not all transformations are natural

[Kenny Lau]

Emily Riehl said:

true

but was it provable?

[Kenny Lau]

I mean it's still true in Lean that the only function you can define (without using choice) is the identity

[Chris Bailey]

This came up elsewhere recently, Kevin Buzzard had an old blog post that gave this rather concrete example of building up to 'values from different constructors are not equal' (updated for Lean 4):

inductive mytype : Type
| AA : mytype
| ZZ : mytype

-- This is the setup that guides case analysis
def mytype_equal : mytype → mytype → Prop
| .AA, .AA => True
| .AA, .ZZ => False
| .ZZ, .AA => False
| .ZZ, .ZZ => True

def mytype_no_confusion (s : mytype) (t : mytype) : s = t → mytype_equal s t := by
  intro H
  rw [H]
  -- The `simp` here just unfolds `mytype_equal`.
  cases t <;> simp [mytype_equal]

theorem unconfused : mytype.AA ≠ mytype.ZZ := mytype_no_confusion .AA .ZZ