Application type mismatch in inductive type

Stream: lean4

[Yicheng Qian]

I came across an "application type mismatch" problem when I was trying to define an inductive type. I managed to reduce it to this example:

inductive WF.{u} : ((α : Type u) × α) → Type (u + 1)
  | ofApp (α β : Type u) (fn : α → β) (arg : α) : WF ⟨β, fn arg⟩

How can I fix this?

[Yury G. Kudryashov]

β has type Type u, not α.

[Yicheng Qian]

Where is the β that has type α?

[Mario Carneiro]

it helps to show the error message:

application type mismatch
  WF.ofApp α β fn
argument has type
  α✝ → β
but function has type
  (fn : α → β) → (arg : α) → WF { fst := β, snd := fn arg }

[Yicheng Qian]

Yeah, I saw that. I was wondering what is α✝.

[Mario Carneiro]

it appears that there is a second α in scope, at least somewhere internal to the inductive validity check

[Yicheng Qian]

If I change (Type (u + 1)) to Prop, the error disappears.

[Yicheng Qian]

But Type (u + 1) should be a valid universe level for this inductive type.

[Yicheng Qian]

Also this works:

inductive WF.{u} : ((α : Type u) × α) → Type (u + 1)
  | ofApp (α β : Type u) (fnarg : (α → β) × α) : WF ⟨β, fnarg.1 fnarg.2⟩

[Mario Carneiro]

minimized some more:

inductive WF : Nat → Type 1
  | mk (α : Type) (fn : α → Nat) (arg : α) : WF (fn arg)

application type mismatch
  WF.mk α fn
argument has type
  α✝ → Nat
but function has type
  (fn : α → Nat) → (arg : α) → WF (fn arg)

[Mario Carneiro]

it does seem to be a bug

[Mario Carneiro]

it looks like the failure is somewhere in mkInjectiveTheorems

[Mario Carneiro]

and indeed setting set_option genInjectivity false in makes the issue go away

[Mario Carneiro]

here's the lean equivalent of what mkInjectiveTheorems does:

set_option genInjectivity false in
inductive WF : Nat → Type 1
  | mk (α : Type) (fn : α → Nat) (arg : α) : WF (fn arg)

example :
  ∀ {α : Type} {fn : α → Nat} {arg : α} {α_1 : Type}, WF.mk α fn arg = WF.mk α_1 fn arg → α = α_1 :=
  fun {α} {fn} {arg} {α_1} x ↦ WF.noConfusion x fun α_eq fn_eq arg_eq ↦ α_eq

application type mismatch
  WF.mk α_1 fn
argument
  fn
has type
  α → Nat : Type
but is expected to have type
  α_1 → Nat : Type

[Mario Carneiro]

it is a fair point that it's not clear what the statement of the injectivity theorem for this inductive should be

[Mario Carneiro]

here's what it looks like for a very similar variation on the inductive type that works:

set_option genInjectivity false in
inductive WF : Nat → Type 1
  | mk (α : Type) (fn : α → Nat) (arg : α) (x) : x = fn arg → WF x

example :
  ∀ {α : Type} {fn : α → Nat} {arg : α} {x : Nat} {a : x = fn arg} {α_1 : Type} {fn_1 : α_1 → Nat} {arg_1 : α_1}
    {a_1 : x = fn_1 arg_1}, WF.mk α fn arg x a = WF.mk α_1 fn_1 arg_1 x a_1 → α = α_1 ∧ HEq fn fn_1 ∧ HEq arg arg_1 :=
  fun {α} {fn} {arg} {x} {a} {α_1} {fn_1} {arg_1} {a_1} x_1 ↦
  WF.noConfusion x_1 fun α_eq fn_eq arg_eq x_eq ↦ { left := α_eq, right := { left := fn_eq, right := arg_eq } }

[Yicheng Qian]

Mario Carneiro said:

it is a fair point that it's not clear what the statement of the injectivity theorem for this inductive should be

What about

example :
  ∀ {α : Type} {fn : α → Nat} {arg : α} {fn_1 : α_1 → Nat} {arg_1 : α_1},
    HEq (WF.mk α fn arg) (WF.mk α_1 fn_1 arg_1) → α = α_1 ∧ HEq fn fn_1 ∧ HEq arg arg_1 := sorry

[Mario Carneiro]

I pushed a basic fix as lean4#2355, which solves the issue by treating not only fn and arg, but also α, as fixed because they are required for the type of the equality to work out. In this case that means there is nothing to equate and so no theorem is generated, but you can add another argument and it will assert equality of those arguments

[Mario Carneiro]

Yicheng Qian said:

Mario Carneiro said:

it is a fair point that it's not clear what the statement of the injectivity theorem for this inductive should be

What about

example :
  ∀ {α : Type} {fn : α → Nat} {arg : α} {fn_1 : α_1 → Nat} {arg_1 : α_1},
    HEq (WF.mk α fn arg) (WF.mk α_1 fn_1 arg_1) → α = α_1 ∧ HEq fn fn_1 ∧ HEq arg arg_1 := sorry

This theorem is (surprisingly) not true, as it relies on the injectivity of WF the type constructor itself, which is a non-theorem in lean's axiomatics

[Yicheng Qian]

What about this (fine-grained control which ensures that the arguments of WF are equal):
(I've renamed WF to SigmaFn)

inductive DepEq {α : Sort u} (f : α → Sort v) : {x : α} → (a : f x) → {y : α} → (b : f y) → Prop where
  /-- Reflexivity of dependent equality. -/
  | refl (x : α) (a : f x) : DepEq f a a

set_option genInjectivity false in
inductive SigmaFn : Nat → Type 1
  | mk (α : Type) (fn : α → Nat) (arg : α) : SigmaFn (fn arg)

theorem SigmaFn.inj {α : Type} {fn : α → Nat} {arg : α} {fn_1 : α_1 → Nat} {arg_1 : α_1}
  (H : DepEq SigmaFn (SigmaFn.mk α fn arg) (SigmaFn.mk α_1 fn_1 arg_1)) : α = α_1 ∧ HEq arg arg_1 ∧ HEq fn fn_1

[Yicheng Qian]

Proof:

inductive DepEq {α : Sort u} (f : α → Sort v) : {x : α} → (a : f x) → {y : α} → (b : f y) → Prop where
  /-- Reflexivity of dependent equality. -/
  | refl (x : α) (a : f x) : DepEq f a a

set_option genInjectivity false in
inductive SigmaFn : Nat → Type 1
  | mk (α : Type) (fn : α → Nat) (arg : α) : SigmaFn (fn arg)

def HEq.ofSigmaEq {α β : Type u} (x : α) (y : β) (H : @Sigma.mk _ id _ x = @Sigma.mk _ id _ y) : HEq x y :=
  by cases H; apply HEq.rfl

def DepEq.toSigmaEq {α : Type u} (f : α → Type v) (x : α) (a : f x)
  (y : α) (b : f y) (H : DepEq f a b) : Sigma.mk (β:=f) x a = Sigma.mk (β:=f) y b :=
  by cases H; rfl

theorem SigmaFn.inj {α : Type} {fn : α → Nat} {arg : α} {fn_1 : α_1 → Nat} {arg_1 : α_1}
  (H : DepEq SigmaFn (SigmaFn.mk α fn arg) (SigmaFn.mk α_1 fn_1 arg_1)) : α = α_1 ∧ HEq arg arg_1 ∧ HEq fn fn_1 :=
  let lh : Sigma SigmaFn := { fst := fn arg, snd := mk α fn arg }
  let rh : Sigma SigmaFn := { fst := fn_1 arg_1, snd := mk α_1 fn_1 arg_1 }
  let lreq : lh = rh := DepEq.toSigmaEq _ _ _ _ _ H
  let rwFn₁ (x : Sigma SigmaFn) : Sigma id :=
    match x with
    | Sigma.mk fst snd =>
      match snd with
      | SigmaFn.mk α fn arg => ⟨α, arg⟩
  let rwRes₁ : rwFn₁ lh = rwFn₁ rh := by rw [lreq]
  let argHeq := HEq.ofSigmaEq _ _ rwRes₁;
  let rwFn₂ (x : Sigma SigmaFn) : Sigma id :=
    match x with
    | Sigma.mk fst snd =>
      match snd with
      | SigmaFn.mk α fn arg => ⟨α → Nat, fn⟩
  let rwRes₂ : rwFn₂ lh = rwFn₂ rh := by rw [lreq]
  let fnHeq := HEq.ofSigmaEq _ _ rwRes₂;
  And.intro (by cases argHeq; rfl) (And.intro argHeq fnHeq)

[Yicheng Qian]

If there are multiple arguments to the type constructor, we can bundle them by dependent pair.

[Yicheng Qian]

(deleted)

[Yicheng Qian]

(deleted)

[Yicheng Qian]

DepEq and HEq are probably not necessary. They can be modeled by Sigma/PSigma plus Eq.

[Yicheng Qian]

theorem SigmaFn.inj {α : Type} {fn : α → Nat} {arg : α} {fn_1 : α_1 → Nat} {arg_1 : α_1}
  (H : (⟨fn arg, SigmaFn.mk α fn arg⟩ : Sigma SigmaFn) = ⟨fn_1 arg_1, SigmaFn.mk α_1 fn_1 arg_1⟩) :
  α = α_1 ∧ (⟨α, arg⟩ : Sigma id) = ⟨α_1, arg_1⟩ ∧ (⟨α, fn⟩ : Sigma (fun α => α → Nat)) = ⟨α_1, fn_1⟩ :=
  let lh : Sigma SigmaFn := ⟨fn arg, SigmaFn.mk α fn arg⟩
  let rh : Sigma SigmaFn := ⟨fn_1 arg_1, SigmaFn.mk α_1 fn_1 arg_1⟩
  let lreq : lh = rh := H
  let rwFn₁ (x : Sigma SigmaFn) : Sigma id :=
    match x with
    | Sigma.mk fst snd =>
      match snd with
      | SigmaFn.mk α fn arg => ⟨α, arg⟩
  let rwRes₁ : rwFn₁ lh = rwFn₁ rh := by rw [lreq]
  let rwFn₂ (x : Sigma SigmaFn) : Sigma (fun (α : Type) => α → Nat) :=
    match x with
    | Sigma.mk fst snd =>
      match snd with
      | SigmaFn.mk α fn arg => ⟨α, fn⟩
  let rwRes₂ : rwFn₂ lh = rwFn₂ rh := by rw [lreq]
  And.intro (by cases rwRes₁; rfl) (And.intro rwRes₁ rwRes₂)