Automatic inference of supertypes

Stream: new members

[Plamen Dimitrov]

Hi all, I find myself in situations where I gradually extend types with subtypes with the original type remaining within a val and the added property under property. This is especially useful when I am discovering new properties of a type and incrementally adding them one by one rather than using a structure with more than one property is not possible.

However, after a while I find myself in a situation where I have to access x.val.val in order to use a partial order defined on the super-super-type or even have to propagate x ⊓ y from the .val.val all the way to the subtype with the added property. So here is what I wonder now - can Lean 4 infer properties of the supertype like shared ones from type classes? If a property x.property holds for a supertype x : Xthen doesn't it also hold for a subtype { x : X // property2 } where the subtype is essentially a type X with both properties 1 and 2?

[Aaron Liu]

What sort of properties are you using?

[Plamen Dimitrov]

Properties like equality of a length of a list, partial order, joins/unions of a lattice, etc. For instance, can I somehow do x ≤ y if I have only defined the LE on a supertype without the .val.val... access?

[Aaron Liu]

It's not always the case that if you have a lattice then a subtype will also be a lattice

[Robin Arnez]

Yeah if this is the case though it might be worth adding the instances you need yourself

[Aaron Liu]

for example Fin 2 × Fin 2 is a lattice but { i : Fin 2 × Fin 2 // i < ⊤ } is not a lattice since ⟨(1, 0), by decide⟩ and ⟨(0, 1), by decide⟩ don't have a supremum

[Aaron Liu]

subtypes do inherit an order, though

[Aaron Liu]

the ordering is in mathlib

[Aaron Liu]

and you can do x ≤ y even if the order is only on a supertype by importing Mathlib.Order.Basic

[Plamen Dimitrov]

I assume there is no easy way to simplify the syntax in the case of purely additive properties? For instance if I have a valid x ⊓ y on a lattice of a type where the subtype also has a property that doesn't affect the lattice structure is there an easy way to simply "inherit" the simple notation instead of having to use (x.val ⊓ y.val).val?

[Aaron Liu]

docs#Sublattice

[Aaron Liu]

what do you mean by "property that doesn't affect the lattice structure"?

[Plamen Dimitrov]

For example if I define a lattice on hypercube vertices with elementwise max and min for join/meet and want to add the property that the dimension I want to consider is < 100 as in { x : Fin n → ℝ // n ≤ 100 }. We can produce a lattice in any dimension n here but if I restrict its value I get into a subtype and a lot of the lattice goodies are no longer accessible unless I use .val.

[Plamen Dimitrov]

and you can do x ≤ y even if the order is only on a supertype by importing Mathlib.Order.Basic

Indeed a good point and it clarifies a lot - so it seems that certain properties are inherited while others are not based on what could be translated to a substructure. In the case of partial order for instance I managed to inherit this into the subtype but not the decidability of it.

[Plamen Dimitrov]

Plamen Dimitrov said:

For example if I define a lattice on hypercube vertices with elementwise max and min for join/meet and want to add the property that the dimension I want to consider is < 100 as in { x : Fin n → ℝ // n ≤ 100 }. We can produce a lattice in any dimension n here but if I restrict its value I get into a subtype and a lot of the lattice goodies are no longer accessible unless I use .val.

Is this example good enough to illustrate what I mean?

[Plamen Dimitrov]

Or is is possible to somehow customize what properties are inherited and what properties are not inherited e.g. via a proof about the inheritance?

[Aaron Liu]

Plamen Dimitrov said:

Plamen Dimitrov said:

For example if I define a lattice on hypercube vertices with elementwise max and min for join/meet and want to add the property that the dimension I want to consider is < 100 as in { x : Fin n → ℝ // n ≤ 100 }. We can produce a lattice in any dimension n here but if I restrict its value I get into a subtype and a lot of the lattice goodies are no longer accessible unless I use .val.

Is this example good enough to illustrate what I mean?

Why are you using a subtype for this?

[Aaron Liu]

the subtype isn't putting any constraints on x (only on n)

[Aaron Liu]

I think you should put a subtype on n instead (make it Fin or something) instead of on x

[Aaron Liu]

unless you have a good reason?

[Plamen Dimitrov]

Aaron Liu said:

unless you have a good reason?

This was just a contrived example to illustrate that one might want to have a subtype and transfer the lattice structure there and I hope it served its purpose.

Let me reiterate the actual question in case someone has any suggestions:

Is it possible to somehow customize what properties are inherited and what properties are not inherited e.g. via a proof about the inheritance? In other words, is it possible to avoid writing (x.val ⊓ y.val).val and simply write x ⊓ y if x.val and y.val are lattice elements and we could prove (but it is not trivial for Lean to automatically prove) that the subtype also forms a lattice?

[Aaron Liu]

Make a docs#Sublattice