Zulip Chat Archive

Stream: lean4

Topic: structure inheritance coercions/aliases?


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Jason Gross (Mar 10 2021 at 19:47):

Ah, neat, thanks!


Last updated: May 18 2021 at 23:14 UTC