Building up types

Stream: new members

[Marcus Rossel]

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]

Have you tried

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

[Marcus Rossel]

@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]

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

[Eric Wieser]

Or

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

[Marcus Rossel]

Oh brilliant! :D
Thanks

[Eric Wieser]

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]

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]

No, that's a lean3 thing

[Eric Wieser]

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

[Notification Bot]

Marcus Rossel has marked this topic as resolved.

[Notification Bot]

Marcus Rossel has marked this topic as unresolved.