partial order on powerset

Stream: Is there code for X?

[Anthony Bordg]

Does mathlib 4 know about the partial order $(\mathcal{P}(S), \subseteq)$ on a powerset?

[Edward van de Meent]

Yes, there is Lattice (Set X)

[Anthony Bordg]

Thank you. Where can I find the corresponding instance (I don't see it in Mathlib.Order.Lattice)?

[Ruben Van de Velde]

I'm guessing https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Lattice.html

[Anthony Bordg]

(deleted)

[Eric Wieser]

You can find it with #synth Lattice (Set X)

[Anthony Bordg]

In Mathlib.Data.Set.Lattice, I found Set.completeAtomicBooleanAlgebra of type CompleteAtomicBooleanAlgebra (Set \a), so my question becomes how to get the underlying preorder from Set.completeAtomicBooleanAlgebra?

[Edward van de Meent]

generally, lean should be able to infer that by itself...
if #synth CompleteAtomicBooleanAlgebra (Set a) works, lean figures out the rest. is there a reason why you're asking?

[Edward van de Meent]

do you have a #mwe perhaps?

[Damiano Testa]

E.g., this works:

import Mathlib.Data.Set.Lattice

variable {α} {a b : Set α}
#check a ≤ b

[Anthony Bordg]

@Edward van de Meent You're right, Lean is perfectly able to infer Preorder a for Set a, but I want to consider $(\text{Set a}, \supseteq)$ (not $(\text{Set a}, \subseteq)$).

[Ruben Van de Velde]

Ah, maybe something something OrderDual?

[Yaël Dillies]

(Set \alpha)^\od

[Anthony Bordg]

I need to give \alpha^\od as an explicit argument to GaloisConnection, but then I also need to give a term of type Preorder a and I can't give OrderDual.instCompleteAtomicBooleanAlgebra.

[Edward van de Meent]

right, because a preorder on Set a is not a preorder on a. you could try inferInstance as an argument and see if it works?

[Edward van de Meent]

also, i think a pattern like (@GaloisConnection a^\od) l u should compile, making lean find the argument itself. i.e, you can stop specifying inferred arguments at any point, and continue with the explicit ones.

[Edward van de Meent]

also, you can write GaloisConnection (α:= αᵒᵈ)

[Anthony Bordg]

Sorry, I got confused, @GaloisConnection (Set α) ((Set β)^\od) _ _ arg1 arg2 works fine and this is what I want. Thank you, all.

[Matthew Ballard]

As @Edward van de Meent mentioned, this is more ergonomic

GaloisConnection (α := Set α) (β := (Set β)ᵒᵈ) arg1 arg2

and generally preferred

[Eric Wieser]

You shouldn't have to pass alpha and beta at all

[Eric Wieser]

If you need to pass them, then arg1 and arg2 have the wrong types

[Matthew Ballard]

My point was stylistic.

[Yury G. Kudryashov]

You should add docs#OrderDual.toDual and docs#OrderDual.ofDual to your functions to make them have correct types

[Anthony Bordg]

Matthew Ballard said:

As Edward van de Meent mentioned, this is more ergonomic

GaloisConnection (α := Set α) (β := (Set β)ᵒᵈ) arg1 arg2

and generally preferred

Good to know!

[Anthony Bordg]

Eric Wieser said:

If you need to pass them, then arg1 and arg2 have the wrong types

Got it!

[Anthony Bordg]

Edward van de Meent said:

generally, lean should be able to infer that by itself...
if #synth CompleteAtomicBooleanAlgebra (Set a) works, lean figures out the rest. is there a reason why you're asking?

Is this #synth command documented?

[Damiano Testa]

My understanding is that it was meant to be a debugging tool very early on. However, it proved to be so useful that it was kept, but still maintained its status of for-internal-use-even-though-everyone-uses-it.

[Damiano Testa]

Using it is very easy, though: #synth whatever gets the typeclass system working to see if it can come up with a whatever instance! :smile:

[Edward van de Meent]

If you don't like it, you could alternatively use #check (inferInstance : whatever), which should have a similar effect

[Damiano Testa]

Edward van de Meent said:

If you don't like it, you could alternatively use #check (inferInstance : whatever), which should have a similar effect

Would this give you the lemma that gives you the instance?

[Edward van de Meent]

that's a fair point, it doesn't...

[Edward van de Meent]

or actually, it does?

[Damiano Testa]

I am suspicious of inferInstance: I think that it hides the information of which lemma it used.

[Edward van de Meent]

it takes a bit extra though... you can click on inferInstance in the infoview to expand the arguments, which then shows you the lemmas used

[Damiano Testa]

Ah, yes, nice trick!

[Edward van de Meent]

honestly, i can't think of a reason to use #check with inferInstance over #synth in this case though. i just wanted to mention that it is an alternative.

[Damiano Testa]

I personally really like #synth.

[Kevin Buzzard]

I really missed #synth in Lean 3 so was very pleased when it filled the much-needed gap in Lean 4; however as Edward is pointing out, Lean 4 has so many other goodies that it's now a bit easier to get away without it :-)

[Kim Morrison]

I would love for #synth to display the whole tree of instances it found, not just the first step.

[Kevin Buzzard]

Yes, many's the time I've typed #synth bar only to be told Foo.toBar and then I have to #synth foo

[Damiano Testa]

Kim Morrison said:

I would love for #synth to display the whole tree of instances it found, not just the first step.

Oh, that may not be hard to implement...

[Mario Carneiro]

I think #synth already does this? #instances only does the first step, but #synth does the whole inference. However only the first step will usually be visible because most instances are written with square bracket hypotheses, and these are hidden in the standard pretty printing settings. Perhaps the pretty printer should treat [] arguments as explicit for pretty printing purposes when the root node is an instance?

[Yury G. Kudryashov]

Or should have an option to do this.

[Anthony Bordg]

Yury G. Kudryashov said:

You should add docs#OrderDual.toDual and docs#OrderDual.ofDual to your functions to make them have correct types

@Yury G. Kudryashov , do you mean I should write the following?

def leftAdjMap (J : Set α) := toDual {b : β | ∀ a ∈ J, R a b}

(resp.

def rightAdjMap (I : (Set β)ᵒᵈ) := {a : α | ∀ b ∈ ofDual I, R a b}

)
Instead of something like

def leftAdjMap (J : Set α) : (Set β)ᵒᵈ := {b : β | ∀ a ∈ J, R a b}

(resp.

def rightAdjMap (I : (Set β)ᵒᵈ) : Set α := {a : α | ∀ b, I b → R a b}

)
considering the fact I want leftAdjMap (resp. rightAdjMap) to have type Set α \r (Set β)ᵒᵈ (resp. (Set β)ᵒᵈ \r Set α).

[Eric Wieser]

You should write both the expected return type and the ofDual / toDuals

[Eric Wieser]

The return type alone is enough to make the GaloisInsertion have the right type, but your proofs will be awkward when you unfold the definition without the casting functions