monotone coercion

Stream: Is there code for X?

[Yaël Dillies]

Is there an instance to say that a coercion is monotone (↑x ≤ ↑y ↔ x ≤ y)?

[Yakov Pechersky]

It can be antimono, like the coe for docs#order.pfilter.set.has_coe, if I understood correctly

[Yakov Pechersky]

Hmm I think I'm wrong about that

[Yaël Dillies]

In my case I can stick to mono, but my prominent problem is that I need an instance to stick in lemmas.

[Kevin Buzzard]

mono is normally only a one-way implication.

[Yaël Dillies]

Hmm... Surely I'm not the first to ask for a coercion to be well-behaved wrt orders?

[Patrick Massot]

Do you know about norm_cast?

[Kevin Buzzard]

I'm sure there are plenty of coe_le lemmas, but they're not instances.

[Patrick Massot]

They are registered as norm_cast lemmas.

[Yaël Dillies]

Are all coercions assumed to respect the order? Surely not.

[Yaël Dillies]

Here's a MWE

import order.basic
import order.preorder_hom
import order.galois_connection
import tactic.monotonicity

universes u v

variables (α : Type u) [partial_order α] (β : Type v) [partial_order β] [has_coe_t β α]

structure closure_operator extends α →ₘ β :=
(le_closure' : ∀ x, x ≤ to_fun x)
(idempotent' : ∀ x, to_fun (to_fun x) = to_fun x)

[Kevin Buzzard]

No, you prove coe_le_coe (which does seem to be an iff in all cases I looked at) and tag it with norm_cast and simp. It's this word "instance" I don't understand.

[Kevin Buzzard]

Aah, coe_mono is the one way implication

[Yaël Dillies]

I have two types α and βand I require βto coerce to α. Now, I want to require it to coerce "nicely".

[Eric Wieser]

I think we have docs#set_like.coe_mono

[Yaël Dillies]

This looks quite good! But I think my α can be more general than a set. And in general I would like the coercion stuff to go smoothly as I'm basically introducing coercions everywhere.

[Eric Wieser]

I think it's pretty unusual to require a has_coe typeclass in another definition

[Yaël Dillies]

Does that mean I am doing my definition wrong? Do you have any workaround?

[Eric Wieser]

If you go down your current path you'll need a new coe_monotone typeclass

[Eric Wieser]

And likely some others

[Yaël Dillies]

Yeah... I had assumed they already existed because it sounds sensible to have them.

[Eric Wieser]

What other objects are you thinking of that aren't set-like?

[Patrick Massot]

This sounds very #xy

[Yaël Dillies]

What about the radical of a natural? Or do we think of it as a multiset of its prime factors?

[Yaël Dillies]

I must say that I can't really think of an example where set_like wouldn't apply. But then I'm still worried about the amount of norm casting I would introduce.

[Yaël Dillies]

I mean, I'm virtually talking about ALL closure operators across mathlib. Surely we don't want to deal with norm_cast that often when the instance system could take care of it for us.

[Eric Wieser]

You're talking about all closure operators for which one direction is always spelled coe, right?

[Eric Wieser]

What makes those more interesting than closure operators which are spelt with a different function name?

[Yaël Dillies]

More or less. I noticed that I could unify bundled and unbundled closure operators (where the bundling refers to their output) if only I could make Lean use id as a coercion from α to α when α = β.

[Yaël Dillies]

Eric Wieser said:

What makes those more interesting than closure operators which are spelt with a different function name?

You mean affine_span/span_points, for example? I thought it would simplify the API by reducing the amount of duplication that goes into such an approach.

[Eric Wieser]

docs#affine_span, docs#span_points?

[Eric Wieser]

Are there any interesting closure operators that do use coe but aren't set_like (ie, don't have a compatible has_mem)

[Yaël Dillies]

I can't think of any.

[Yaël Dillies]

Actually I think the cleanest thing to do is to just ditch the ordering on beta and go full coercion. I still have the problem with alpha = beta but at worst this could be solved by defining another structure called endo_closure_operator or something.

[Mario Carneiro]

Why not just use a function f? I don't see why it has to be a coercion

[Yaël Dillies]

The whole point is that, for example, the subgroup closure of a set will be a subgroup, which can be coerced back to a set.

[Mario Carneiro]

yes, that coercion is a function

[Mario Carneiro]

if you want to be generic over possible closure systems then you should use a function, like is done with galois insertions

[Yaël Dillies]

Hmm, that's interesting. If I then feed a coercion as the function, will it automatically appear with up arrows in the pretty print?

[Yaël Dillies]

Also, if I feed in id, will it simplify it automatically?

[Mario Carneiro]

No, but you can use simp lemmas to clean up the expression

[Mario Carneiro]

you need such a thing anyway for applying a typeclass function on a particular instance

[Mario Carneiro]

Actually yes to the first thing: if you use coe as the function coe x will be in the expression and this gets displayed as \u x. But id x is not displayed as x

[Yaël Dillies]

Okay well. It appears that what I want to do is really a Galois insertion, but bundled.

[Mario Carneiro]

In that case, you will have a special map associated to your structure, like closure_operator.to_fun, and there should be simp lemmas like closure_operator.to_fun (set X) x = x, closure_operator.to_fun (subgroup X) x = \u x, and so on

[Eric Wieser]

A galois insertion bundling both l and u or just one of them?

[Yaël Dillies]

Both I'd say. I want c : closure_operator a b to coerce to l : a -> b, but I also want any term of b to go through u : b -> a when stating inequalities. In practice, u will be the coercion from b to a most of the time.

[Yaël Dillies]

I really feel like people here have thought harder about that than I did. But I still think there's something to be done about the way it is set up.

[Yaël Dillies]

We shouldn't have both span_points and affine_span. Only the latter ought to exist. And lemmas about closure operators should be accessible by dot notation: the proof of subset_affine_span should be affine_span.le_closure.

[Yaël Dillies]

What I want is to bundle the current closure operators we have with the information that they are in fact closure operators, and that through a structure that would support dot notation.

[Yaël Dillies]

This bundled structure would require as inputs: the closure operation so to speak l : a -> b, the operation to get back to the original type u : b -> a, the proof that u o l is inflationary, the proof that u o l is idempotent.

[Eric Wieser]

Eric Wieser said:

A galois insertion bundling both l and u or just one of them?

To be precise here, I'm suggesting the choice between these two:

import order.galois_connection

structure fully_bundled (α β : Type*) [preorder α] [preorder β] :=
(l : α → β)
(u : β → α)
(gc : galois_connection l u)

structure partially_bundled {α β : Type*} [preorder α] [preorder β] (u : β → α) :=
(l : α → β)
(gc : galois_connection l u)

[Eric Wieser]

closure could then have type fully_bundled (subgroup G) (set G) or partially_bundled (coe : subgroup G → set G)

[Mario Carneiro]

I think fully_bundled makes more sense here given the aim

[Yaël Dillies]

That's what I think too. But there's not much difference functionally?

[Yaël Dillies]

The types would be slightly different but it doesn't matter much as we'll define concrete terms.

[Mario Carneiro]

the advantage of the partially bundled approach, or parameters more generally, is that you will not have to rewrite a term: in the lemma about u (l x) = x, when you apply that with partially_bundled it looks like u (bundle.l x) = x where u is whatever term you want, including coe

[Mario Carneiro]

I think that is one of the reasons why galois insertion uses parameters for l and u

[Yaël Dillies]

Ah, I see. Well, no I don't really. But it sounds as if I could see.

[Yaël Dillies]

You still have to feed in both u and l at some point, right?

[Yaël Dillies]

What woild it look like with fully_bundled?

[Mario Carneiro]

import order.galois_connection

structure fully_bundled (α β : Type*) [preorder α] [preorder β] :=
(l : α → β)
(u : β → α)
(gi : galois_insertion l u)

structure partially_bundled {α β : Type*} [preorder α] [preorder β] (u : β → α) :=
(l : α → β)
(gi : galois_insertion l u)

theorem fully_bundled.l_u {α β : Type} [preorder α] [partial_order β]
  (bu : fully_bundled α β) (x) : bu.l (bu.u x) = x := bu.gi.l_u_eq x

theorem partially_bundled.l_u {α β : Type} [preorder α] [partial_order β] {u : β → α}
  (bu : partially_bundled u) (x) : bu.l (u x) = x := bu.gi.l_u_eq x

def foo : Type := sorry
def bar : Type := sorry
instance : partial_order foo := sorry
instance : partial_order bar := sorry
instance : has_coe bar foo := sorry
def span : foo → bar := sorry
def gi : galois_insertion span coe := sorry

def full : fully_bundled foo bar :=
{ l := span,
  u := coe,
  gi := gi }

@[simp] lemma full_l : full.l = span := rfl
@[simp] lemma full_u : full.u = coe := rfl

def part : partially_bundled (coe : bar → foo) :=
{ l := span,
  gi := gi }

@[simp] lemma part_l : part.l = span := rfl

example : false :=
begin
  have h_full := full.l_u, -- ∀ (x : bar), full.l (full.u x) = x
  have h_part := part.l_u, -- ∀ (x : bar), part.l ↑x = x
  simp at h_full h_part,
  -- both are now ∀ (x : bar), span ↑x = x
end

[Anne Baanen]

My intuition says you want this partially bundled, so that you can instantiate α := set α and u := coe : β → set α, so you can state lemmas along the lines of:

lemma subset_closure [set_like β] (closure : closure_operator (coe : β → set α)) : s ⊆ closure s :=
c.gi.gc.le_u (le_refl _)

[Joseph Myers]

Yaël Dillies said:

We shouldn't have both span_points and affine_span. Only the latter ought to exist. And lemmas about closure operators should be accessible by dot notation: the proof of subset_affine_span should be affine_span.le_closure.

The purpose of span_points is really (a) as a detail of how affine_span is implemented, which might go away with some more general infrastructure handling closure operators, and (b) as an explicit description of what points are in the affine span, in relation to vector_span. The latter is still relevant in the presence of more general infrastructure, though maybe as a lemma rather than a definition.

(Lemmas about span_points should have corresponding affine_span lemmas, but I'm not sure they all do at present. Anything that uses a span_points lemma in a context where it actually has an affine_span ought to be fixed to avoid that abuse of defeq and use an affine_span lemma instead, independent of any more general refactoring of closure operators.)

[Yaël Dillies]

Wait, let's move to https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Closure.20operators