Zulip Chat Archive

Stream: new members

Topic: Building up types


Marcus Rossel (Jul 13 2021 at 15:52):

The following question is not about the specific types I'm showing, but rather about how to approach formalization. Excuse the vaguery.

Say we have a type and some function for it:

structure network :=
  (l : list )

def network.count (n : network) :  :=
  n.l.length

We often need to use networks with some specific constraints, so we define a new type to make this more ergonomic:

structure constrained_network :=
  (underlying : network)
  (constraint1 : underlying.count > 2)
  (constraint2 : underlying.count < 5)

Quite naturally, it would be nice to be able to use the network.count on this type, but since constrained_network is a different type, we need to lift the implementation:

def constrained_network.count (c : constrained_network) : constrained_network :=
  c.underlying.count

Say we have a hundred properties like count, then we'll need to lift all of these, which is quite a nuisance.

So instead we decide to formalize constrained_network as a subtype with accessors on it:

def constrained_network := { n : network // n.count > 2  n.count < 5 }

def constrained_network.constaint1 (c : constrained_network) : c.val.count > 2 := c.property.left
def constrained_network.constaint2 (c : constrained_network) : c.val.count < 5 := c.property.right

But even then we always have to dig down to the underlying network to use count:

example (c : constrained_network) :  := c.val.count

Is there some approach to building up concrete types from more general ones (like constrained_network from network), such that there is some form of inheritance of properties from the more general type? Or is this fundamentally not possible, as functions like the following couldn't be trivially lifted?

-- Can't easily be adapted to `constrained_network`, as we need to make sure that the constraints aren't broken.
def network.add1 (n : network) : network := 1 :: n.l

In other words, am I fundamentally stuck with manually adding new (duplicate) definitions for the more constrained types?

Eric Wieser (Jul 13 2021 at 15:59):

Have you tried

structure constrained_network extends network :=
(constraint1 : count > 2)
(constraint2 : count < 5)

Marcus Rossel (Jul 13 2021 at 16:09):

@Eric Wieser
That might be the solution I'm looking for.
There's one nitpick I have with it right now though:
I can't use network.count in the definition of constrained_network, since there's no available network upon which to use the property.
So instead I'd have to "unwrap" network.count and write:

structure constrained_network extends network :=
  (constraint1 : l.length > 2)
  (constraint2 : l.length < 5)

I think this is fundamentally not solvable though, as otherwise Lean would have to provide some instance of network during the definition of constrained_network , which would be very strange.

Eric Wieser (Jul 13 2021 at 16:19):

structure constrained_network extends network :=
(constraint1 : to_network.count > 2)
(constraint2 : to_network.count < 5)

Eric Wieser (Jul 13 2021 at 16:20):

Or

structure constrained_network extends underlying : network :=
(constraint1 : underlying.count > 2)
(constraint2 : underlying.count < 5)

Marcus Rossel (Jul 13 2021 at 16:20):

Oh brilliant! :D
Thanks

Eric Wieser (Jul 13 2021 at 16:21):

Note you'll get different behavior with and without set_option old_structure_cmd true - you might want to try both and see which behaves best for you

Marcus Rossel (Jul 13 2021 at 16:24):

Eric Wieser said:

Note you'll get different behavior with and without set_option old_structure_cmd true - you might want to try both and see which behaves best for you

Is that a Lean 4 thing? I'm still on Lean 3.

Eric Wieser (Jul 13 2021 at 16:24):

No, that's a lean3 thing

Eric Wieser (Jul 13 2021 at 16:24):

Lean4 has no old structures. Lean3 has them behind a section-local flag

Notification Bot (Jul 14 2021 at 09:06):

Marcus Rossel has marked this topic as resolved.

Notification Bot (Jul 14 2021 at 09:06):

Marcus Rossel has marked this topic as unresolved.


Last updated: Dec 20 2023 at 11:08 UTC