## Stream: lean4

### Topic: structure inheritance coercions/aliases?

#### Jason Gross (Mar 10 2021 at 18:22):

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 (Mar 10 2021 at 18:36):

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 (Mar 10 2021 at 18:41):

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

#### Jason Gross (Mar 10 2021 at 19:47):

Ah, neat, thanks!

Last updated: May 18 2021 at 23:14 UTC