structure inheritance coercions/aliases?

Stream: lean4

[Jason Gross]

Is there a way to declare aliases of substructure fields (ideally automatically), so that instead of writing

structure A where
  a0 : Type
  a1 : Type
structure B where
  a_ : A
  b0 : a_.a0 → Type
  b1 : a_.a1 → Type
structure C where
  b_ : B
  c0 : {x : b_.a_.a0} → b_.b0 x → Type
  c1 : {x : b_.a_.a1} → b_.b1 x → Type

I can write

structure A where
  a0 : Type
  a1 : Type
structure B where
  a_ : A [coercion]
  b0 : a0 → Type
  b1 : a1 → Type
structure C where
  b_ : B [coercion]
  c0 : {x : a0} → b0 x → Type
  c1 : {x : a1} → b1 x → Type

or even just

structure A where
  a0 : Type
  a1 : Type
structure B where
  a_ : A
  b0 : a_.a0 → Type
  b1 : a_.a1 → Type
structure C where
  b_ : B
  c0 : {x : b_.a0} → b_.b0 x → Type
  c1 : {x : b_.a1} → b_.b1 x → Type

? (Notably, I want C.mk to still only have three arguments, and the first one to be of type B, and I want C.b_ to still exist. I just want to be able to implicitly treat anything of type C as also being of type B and anything of type B as also being of type A, at least for the purposes of field accesses, and perhaps also in general.

[Leonardo de Moura]

Have you tried to use extends?

structure A where
  a0 : Type
  a1 : Type

structure B extends A where
  b0 : a0 → Type
  b1 : a1 → Type

structure C extends B where
  c0 : {x : a0} → b0 x → Type
  c1 : {x : a1} → b1 x → Type

-- C.mk is still 3 arguments
#check @C.mk
-- C.mk : (_toB : B) → ({x : _toB.toA.a0} → B.b0 _toB x → Type) → ({x : _toB.toA.a1} → B.b1 _toB x → Type) → C

-- The structure instance `{ ...}` notation has special support for `extends`.
theorem ex  :
  { a0 := Nat, a1 := Nat, b0 := fun _ => Nat, b1 := fun _ => Nat, c0 := fun _ => Nat, c1 := fun _ => Nat : C }
  =
  { toB := { toA := { a0 := Nat, a1 := Nat }, b0 := fun _ => Nat, b1 := fun _ => Nat },
    c0 := fun _ => Nat, c1 := fun _ => Nat : C }
  :=
rfl


def f (a : A) : Type :=
  a.a0

def g (c : C) : Type :=
  f c.toA  -- We currently do not register a coercion from `C` to `B` and `B` to `A`

instance : Coe C A where
  coe c := c.toA

def g' (c : C) : Type :=
  f c -- coercion is being used here

[Leonardo de Moura]

We haven't decided yet whether we should generate the coercions from C to B and B to A automatically or not.

[Jason Gross]

Ah, neat, thanks!

[Alexandre Rademaker]

what about https://coq.inria.fr/refman/addendum/implicit-coercions.html, that is, coercions for modeling inheritance between types... I am still trying to understand the best approach to that in Lean4. I mean, we don't necessary need the structures to use coe, right? But in the example from @Leonardo de Moura the .toA was implicated defined during the structure+extends declaration right?