Should I use a structure or just a pair for a... pair?

Stream: new members

[Victor Porton]

I am formalizing filtrators. By definition, a filtrator is a pair of a poset and its subset. Alternatively, define it as a poset with a subposet. Should I use just a pair or create a Filtrator structure?

[Jovan Gerbscheid]

It would probably be more principled to make a structure with 2 fields. That way you can decide the names of the projection function, and give them doc-strings (instead of having Prod.fst and Prod.snd.

However, depending on what you want to do, it may be better not to use a pair at all. In lean we typically quantify over a type (α : Type u), and then we would have e.g. a filtrator (f : Filtrator α), where Filtrator would be a structure in the same style as Subgroup.

[James E Hanson]

Do you generally consider more than one filtrator on the same poset?

[James E Hanson]

With certain kinds of objects, it makes more sense to use classes rather than structures.

[Victor Porton]

James E Hanson said:

Do you generally consider more than one filtrator on the same poset?

In advanced theory. I think, I won't formalize that part of the theory (at least in the foreseeable future).

[Victor Porton]

James E Hanson said:

With certain kinds of objects, it makes more sense to use classes rather than structures.

Can you refer to an example?

[Jovan Gerbscheid]

I might be wrong about the definition, but isn't it just this:

import Mathlib

variable (α : Type u) [PartialOrder α] (f : Set α)

[Victor Porton]

structure Filtrator (α : Type u) where
  order : PartialOrder α
  subset : Set α

[James E Hanson]

Victor Porton said:

Can you refer to an example?

Well so this the way Lean handles the common convention of conflating certain objects with their carrier sets.

ℝ is a type, but it has a field instance, which means that if I write (fun x y : ℝ => x + y), Lean is able to infer what the symbol + is supposed to mean.

If ℝ were defined as a bundled field structure, we'd have to write something like ℝ.type all the time, which would be annoying.

[Victor Porton]

Jovan Gerbscheid said:

I might be wrong about the definition, but isn't it just this:

import Mathlib

variable (α : Type u) [PartialOrder α] (f : Set α)

Which of the two definitions is better?

[Jovan Gerbscheid]

Victor Porton said:

structure Filtrator (α : Type u) where
  order : PartialOrder α
  subset : Set α

With this, you run into issues with type class inference. In order to let lean figure out the PartialOrder instance, you would have to make Filtrator a class. But then you can only have one filtrator on any given type, which is not what you want.

So, I'd say just use variable (α : Type u) [PartialOrder α] (f : Set α). I don't really see any disadvantages to this.

[Victor Porton]

Oh, I was wrong: I forget an important case when I need two filtrators at once.

[Jovan Gerbscheid]

Oh oops, I meant variable {α : Type u} [PartialOrder α] (f : Set α)

[Jovan Gerbscheid]

(or you can use {α : Type*})

[Victor Porton]

Jovan Gerbscheid said:

Oh oops, I meant variable {α : Type u} [PartialOrder α] (f : Set α)

But as follows from above, variable does not suit. Your offer to use class makes necessary to define a partial order every time when filtrators are used, doesn't it. So, it seems for me inconvenient to use a class.

[Victor Porton]

Jovan Gerbscheid said:

(or you can use {α : Type*})

What is Type*?

[Jovan Gerbscheid]

Type* is like Type u, but it generates a new/fresh universe level for you. So then you don't need to write the universe u command on top of your file.

[Jovan Gerbscheid]

Victor Porton said:

But as follows from above, variable does not suit.

What do you mean?

[Victor Porton]

Jovan Gerbscheid said:

What do you mean?

"Oh, I was wrong: I forget an important case when I need two filtrators at once."

[Jovan Gerbscheid]

In that case you should use

variable {α : Type*} [PartialOrder α] (f₁ f₂ : Set α)

[Victor Porton]

Jovan Gerbscheid said:

In that case you should use

variable {α : Type*} [PartialOrder α] (f₁ f₂ : Set α)

I dislike this variant. If may lead into issues, if I notice more than two fitrators in single theorem.

[Jovan Gerbscheid]

Or do you mean that the two filtrators have different underlying types? In that case you can do

variable {α β : Type*} [PartialOrder α] (f₁ : Set α) [PartialOrder β] (f₂ : Set β)

[Victor Porton]

Jovan Gerbscheid said:

Or do you mean that the two filtrators have different underlying types? In that case you can do

Ya, different.

[Jovan Gerbscheid]

Victor Porton said:

James E Hanson said:

Do you generally consider more than one filtrator on the same poset?

In advanced theory. I think, I won't formalize that part of the theory (at least in the foreseeable future).

But you would also want to be able to support the case of two filtrators on the same poset, if I understand correctly?

[Victor Porton]

Jovan Gerbscheid said:

Victor Porton said:

But you would also want to be able to support the case of two filtrators on the same poset, if I understand correctly?

Two filtrators on the same poset seem to be not actual now.

[Jovan Gerbscheid]

So if you do not want to support two filtrators on the same poset, then you could do something like this:

class FiltratedOrder (α : Type*) extends PartialOrder α where
  filtrator (α) : Set α

export FiltratedOrder (filtrator)

And then you can use it like this

variable {α : Type*} [FiltratedOrder α]

#check filtrator α

[Victor Porton]

Jovan Gerbscheid said:

So if you do not want to support two filtrators on the same poset, then you could do something like this:

class FiltratedOrder (α : Type*) extends PartialOrder α where
  filtrator (α) : Set α

export FiltratedOrder (filtrator)

And then you can use it like this

variable {α : Type*} [FiltratedOrder α]

#check filtrator α

After your change, this does not work:

def Filtrator.suborder {α : Type u} [F : Filtrator α] : PartialOrder F.subset :=
  @Subtype.partialOrder α F.order F.subset

How to make this .order work?

[Jovan Gerbscheid]

It would be like this:

variable {α : Type*} [FiltratedOrder α]

instance : PartialOrder (filtrator α) :=
  Subtype.partialOrder (· ∈ filtrator α)

[Jovan Gerbscheid]

Note that when you are dealing with instances, you should never need to give a name to the variable (so don't use [F : Filtrator α], but let type class search fill it in for you)

[Victor Porton]

Your code does not verify and I don't know how to make it verify.

[Victor Porton]

I need to extract the order from filtrator and don't know how.

[Jovan Gerbscheid]

Sorry, I'll share the complete code:

import Mathlib

class FiltratedOrder (α : Type*) extends PartialOrder α where
  filtrator (α) : Set α

export FiltratedOrder (filtrator)

variable {α : Type*} [FiltratedOrder α]

def Filtrator.suborder : PartialOrder (filtrator α) :=
  Subtype.partialOrder (· ∈ filtrator α)

[Victor Porton]

I don't know at all, what export means.

[Jovan Gerbscheid]

export in this case means that you can write filtrator as a shorthand for FiltratedOrder.filtrator.

[Jovan Gerbscheid]

And the (α) in filtrator (α) : Set α causes the α argument of filtrator to be explicit, so that you can write filtrator α, and then type class search will fill in the data for you, based on the type α.

[Victor Porton]

How to use two related structures in one theorem?

lemma rel_right_flt{α: Type u}{β: Type v}[PartialOrder α][Filtrator β]{Y: PartialOrder β}
    (f: PointfreeFuncoid (inferInstance : PartialOrder β) Y) (a: α) (b: β) :
    f.funcoid_rel a b ↔ ∀ y ∈ Filtrator.up b, f.funcoid_rel a y := by

Application type mismatch: The argument
  a
has type
  α
of sort `Type u` but is expected to have type
  β
of sort `Type v` in the application
  f.funcoid_rel aLean 4

f.funcoid_rel is a relation between elements of posets.

[Aaron Liu]

what is PointfreeFuncoid?

[Victor Porton]

@Aaron Liu

structure PointfreeFuncoid {α: Type u}{β: Type v}(a: PartialOrder α)(b: PartialOrder β) where
    fwd : α → β
    bwd : β → α
    rev (x: α) (y: β) : @meet _ b (fwd x) y ↔ @meet _ a (bwd y) x

[Victor Porton]

Two functions between posts that are "quasi-reverses" to each other.

[Aaron Liu]

and what is PointfreeFuncoid.funcoid_rel? (this would be much easier with a #mwe)

[Victor Porton]

Aaron Liu said:

and what is PointfreeFuncoid.funcoid_rel? (this would be much easier with a #mwe)

I've found some obvious mistakes in my code, trying now by myself.

[Victor Porton]

It seems, my message has been deleted. Probably, that's because I wrote to a wrong channel. So, I think, it is appropriate here:

How to check whether a value belongs to a class? The following code does not compile:

class Filtrator.filtered {α : Type u} extends Filtrator α where
  is_filtered : ∀ x y : α, up x ⊆ up y → y ≤ x

/-- A filtrator is up-determined if every element is the infimum of its core upper set. -/
theorem Filtrator.up_determined {α : Type u} [Filtrator α] :
  (α : Filtrator.filtered) ↔ ∀ x : α, IsGLB (Filtrator.up x) x := by sorry

Please, help to correct it.

[Notification Bot]

A message was moved here from #lean4 > Package version from git tag? by Julian Berman.

[Julian Berman]

@Victor Porton your last message seems definitely to not belong in the last 2 places you had it -- I'm not sure it belongs here either or in a new thread, but here seems better than where it was at least.

[Aaron Liu]

Victor Porton said:

How to check whether a value belongs to a class? The following code does not compile:

class Filtrator.filtered {α : Type u} extends Filtrator α where
  is_filtered : ∀ x y : α, up x ⊆ up y → y ≤ x

/-- A filtrator is up-determined if every element is the infimum of its core upper set. -/
theorem Filtrator.up_determined {α : Type u} [Filtrator α] :
  (α : Filtrator.filtered) ↔ ∀ x : α, IsGLB (Filtrator.up x) x := by sorry

Please, help to correct it.

probably I think you want Filtrator.filtered to be a mixin instead of extending Filtrator

[Aaron Liu]

see for example docs#AddCommMagma is bundled vs docs#IsAddCommutative is a mixin

[Notification Bot]

This topic was moved here from #lean4 > Should I use a structure or just a pair for a... pair? by Michael Rothgang.