Zulip Chat Archive

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!

Alexandre Rademaker (May 19 2022 at 01:51):

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?


Last updated: Dec 20 2023 at 11:08 UTC