injectivity of my own inductive

Stream: Type theory

[Malvin Gattinger]

I am wondering if we can prove that an inductive Nat → Type is injective.

inductive Thing : Nat → Type where
  | Bike : Thing 10
  | House : Thing 100

theorem Thing.injective {n k} (sameThing : Thing n = Thing k) : n = k := by
  by_cases n = 10 <;> by_cases n = 100 <;> by_cases k = 10 <;> by_cases k = 100
  all_goals
    try simp_all [Thing]
  -- Morally, I would now want to do something like `cases (Thing 10)` now?!
  -- cases sameThing -- fails with "dependent elimination failed, failed to solve equation Thing 100 = Thing 10"
  -- Could I somehow use `HEq.rec` or `Eq.rec` manually for this?
  all_goals
    -- Is the last goal here a contradiction or true, if `Thing 19` is empty?
    sorry

I tried to find related conversations but only found things like "equality of types is not mathematics" :wink:

Ah, I now found this thread about whether the Pi constructor is injective and there the answer was no, referring to a cardinality model of Lean(s type theory). Does this also apply here? That Thing 10 = Thing 100 is consistent but not provable?

[Aaron Liu]

Malvin Gattinger said:

That Thing 10 = Thing 100 is consistent but not provable?

I think this is true

[Kyle Miller]

Yeah the cardinality model says it's consistent if Thing 10 = Unit, Thing 100 = Unit, and Thing n = Empty for all other n.

[Kenny Lau]

Malvin Gattinger said:

I tried to find related conversations but only found things like "equality of types is not mathematics"

I hope they at least also included the information that it's independent of the axioms of Lean

[Fernando Chu]

Kyle Miller said:

Yeah the cardinality model says it's consistent if Thing 10 = Unit, Thing 100 = Unit, and Thing n = Empty for all other n.

Is this right? I'd imagine its provable that Σ n, Thing n ≅ Bool, and therefore Thing 10 != Thing 100 should be provable.

[Fernando Chu]

With regard to the Pi-types, they just behave somewhat weirdly in type theory. Thing is an inductive type, these are pretty well behaved in type theory (idk about Lean specifically), so I wouldn't compare these two things that much

[Kenny Lau]

@Fernando Chu Σ i : Fin 2, Unit is also equivalent to Bool

[Kenny Lau]

therefore Unit != Unit?

[Aaron Liu]

Fernando Chu said:

Is this right? I'd imagine its provable that Σ n, Thing n ≅ Bool, and therefore Thing 10 != Thing 100 should be provable.

What is provable here since Σ n, Thing n ≅ Bool we can get @Sigma.mk Nat Thing 10 Thing.Bike ≠ @Sigma.mk Nat Thing 100 Thing.House, but this is only because 10 ≠ 100 and this doesn't tell you anything about Thing.Bike and Thing.House.

[Fernando Chu]

Right, my bad, thanks for the explanations; in HoTT it would even be the case that Thing 10 = Thing 100 so I should have noticed this.

[Kenny Lau]

oh no, have we lost fernando to hott?

[Robin Arnez]

You can even define Thing in such a way that you can disprove injectivity:

def Thing : Nat → Type
  | 10 => Unit
  | 100 => Unit
  | _ => Empty

def Thing.Bike : Thing 10 := ()
def Thing.House : Thing 100 := ()

@[elab_as_elim, induction_eliminator]
def Thing.rec {motive : (n : Nat) → Thing n → Sort _}
    (Bike : motive 10 Bike) (House : motive 100 House)
    {n : Nat} (t : Thing n) : motive n t :=
  if h : n = 10 then
    Eq.rec (fun _ => Bike) h.symm t
  else if h' : n = 100 then
    Eq.rec (fun _ => House) h'.symm t
  else by
    exfalso
    simp only [Thing] at t
    exact t.elim

theorem Thing.rec_Bike {motive : (n : Nat) → Thing n → Sort _}
    (Bike : motive 10 Bike) (House : motive 100 House) :
    Thing.rec Bike House .Bike = Bike := rfl

theorem Thing.rec_House {motive : (n : Nat) → Thing n → Sort _}
    (Bike : motive 10 Bike) (House : motive 100 House) :
    Thing.rec Bike House .House = House := rfl

theorem Thing.not_injective : ¬∀ {n k}, Thing n = Thing k → n = k := by
  intro h
  specialize @h 10 100 rfl
  contradiction

[Kenny Lau]

I've golfed and improved your code:

def Thing (n : Nat) : Type :=
  if n = 10 ∨ n = 100 then Unit else Empty

def Thing.bike : Thing 10 := ()
def Thing.house : Thing 100 := ()

@[elab_as_elim, induction_eliminator]
def Thing.rec {motive : (n : Nat) → Thing n → Sort _}
    (bike : motive 10 bike) (house : motive 100 house)
    {n : Nat} (t : Thing n) : motive n t :=
  if h : n = 10 then
    Eq.rec (fun _ => bike) h.symm t
  else if h' : n = 100 then
    Eq.rec (fun _ => house) h'.symm t
  else Empty.elim <| by rwa [Thing, if_neg (by simp_all)] at t

theorem Thing.rec_bike {motive : (n : Nat) → Thing n → Sort _}
    (bike : motive 10 bike) (house : motive 100 house) :
    Thing.rec bike house .bike = bike := rfl

theorem Thing.rec_house {motive : (n : Nat) → Thing n → Sort _}
    (bike : motive 10 bike) (house : motive 100 house) :
    Thing.rec bike house .house = house := rfl

theorem Thing.not_injective : ¬∀ {n k}, Thing n = Thing k → n = k :=
  fun h ↦ absurd (@h 10 100 rfl) (by decide)