with_top irreducible

Stream: general

[Yaël Dillies]

Should we make with_top and with_bot irreducible as Yury suggested on #4273?

[Yury G. Kudryashov]

It breaks a lot of stuff. E.g., some instances on with_top/with_bot are defined in terms of the instances on the other type.

[Yury G. Kudryashov]

And once Lean fails to see through this, quite a few proofs fail.

[Yaël Dillies]

Yeah, that's what I thought. Also, isn't there something with order_dual somehow swapping with_top and with_bot?

[Yury G. Kudryashov]

Yes, and this breaks with @[irreducible] too.

[Kevin Buzzard]

I really like the idea. I think that leaky proofs (when you have a : with_top X and then all of a sudden in the goal you see a : option X) cause confusion to undergraduates (and to me, when I was a beginner). They leak because sometimes the proof of with_top.foo is just option.foo and then Lean gets confused with the types. It's annoying not being able to apply some lemma about top because all of a sudden the term has become none somewhere along the line. The objection the other way is that this can cause code duplication -- these are somehow the same people who would rather with_top.foo simply didn't exist at all because "we have it already, it's just option.foo". We like type theory because we like that things keep their types!

[Yury G. Kudryashov]

We can replace order_dual proofs with a to_additive-style machinery but this would be a huge refactor.

[Yury G. Kudryashov]

(and we need order_dual anyway)

[Yaël Dillies]

I've myself suffered from this leaky implementation and I must say it's pretty annoying. Can't we make with_top and with_bot irreducible globally but rducible during API building?

[Yaël Dillies]

Sounds like the best of both worlds, unless someone has been wrongly peeking in the API.

[Patrick Massot]

Irreducible stuff went out of fashion because of Lean 4.

[Patrick Massot]

We're meant to use structures instead.

[Kevin Buzzard]

Oh! So then is the proposal to make with_top a structure instead?

[Kevin Buzzard]

Heh :-)

[Yaël Dillies]

Uh?

[Kevin Buzzard]

So then this will mean masses of code duplication!

[Yaël Dillies]

Does that mean we have to define option five times or so?

[Kevin Buzzard]

oh wait

[Kevin Buzzard]

I mean "an inductive type"

[Kevin Buzzard]

yes, I think so Yael, unless we want to define with_top X as a structure with one field of type option X

[Kevin Buzzard]

I think continuous was made into a structure because people had problems with it unfolding to "forall open U, ..." or something? (I don't know the details -- what I do know is that continuous f is definitely not defeq to forall U,..., you have to rewrite continuous_def

[Kevin Buzzard]

This might not be the same reason, but having things made "irreducible" by wrapping them in a structure seemed to work well for continuous

[Kevin Buzzard]

Maybe defining with_top X as a structure with one field of type option X gives us the possibility of an algorithmic way of pulling definitions over a la to_additive, like maybe with_top.bind can be auto-defined using option.bind?

[Kevin Buzzard]

I guess defining it in exactly the same way as option gives us the option of actually modifying to_additive so that it pulls definitions over. It could change none to top etc

[Kevin Buzzard]

When I started with Lean, one of the things about it that I thought was really stupid was that they had defined additive groups and multiplicative groups as two different things. Later on as I began to understand that mathematicians used addition and multiplication in genuinely different ways, I realised that actually it was a great idea. Distributivity was somehow key -- it is the way addition and multiplication were related, it is the asymmetric thing that distinguishes between them when both are present. Heterogeneous distributivity is a multiplicative object acting on an additive object, e.g. "a group acting on an abelian group" as we mathematicians say, knowing full well (but never explaining) that we mean "a group with group law * acting on a group with group law +". Heterogeneous associativity is is_scalar_tower by the way. The fact that Leo explicitly decided to make two definitions not one caused (presumably) the development of to_additive and I wonder how much more we can use this tool. It seems to me to be a very similar situation -- mathematicians use the bot in with_bot in different, but similar, situations to the zero in with_zero, so maybe this approach would solve both code duplication problems and reducibility problems?

[Eric Wieser]

Making with_top a structure is quite a different thing to making order_dual a structure. If we made the latter a structure, we'd lose X = order_dual (order_dual X) (it would be unprovable), and more importantly to_dual (of_dual x) = x stops being refl. This second point is like the "we should make set a structure" discussion; unless lean gains some eta-reduction rules for one-field structures (which I think doesn't impact soundness?), it makes a lot of things more awkward.

[Kevin Buzzard]

So what are the plans for order_dual in Lean 4?

[Gabriel Ebner]

This second point is like the "we should make set a structure" discussion; unless lean gains some eta-reduction rules for one-field structures (which I think doesn't impact soundness?), it makes a lot of things more awkward.

To expand on this. What we'd lose is the definitional equality s = { x | x ∈ s }. Adding this kind of eta for structures would not impact soundness afaict, but it is a kernel change which makes it hard to sell to Leo.

Practically speaking, it is not that awkward. I got pretty far with this refactoring: https://github.com/leanprover-community/mathlib/commit/76451e89d6cbf0a145525555f1db1778285d9269 It was harder to get rid of the inductive : X -> set Y.

[Eric Wieser]

Is Leo aware that we would be interested in such a change?

[Eric Wieser]

I guess such a kennel change wouldn't help with the inductive problem you describe anyway though.

[Reid Barton]

I have mentioned it to him before in the context of opposite in category theory--I'm still not sure what our plan is there either

[Sebastian Ullrich]

It would be good to at least have an issue for it in the lean4 repo and collect use cases, references to existing implementations etc. there

[Gabriel Ebner]

https://github.com/leanprover/lean4/issues/777

[Gabriel Ebner]

At the risk of completely derailing this discussion, it would also be cool to have eta for decidable instances. That is, make it so that example (a b : Decidable p) := rfl. We have quite a bit of ugly library design in mathlib to work around decidability diamonds (i.e., if you have a theorem about classical.decidable you can't use it prove something about a computable instance). See e.g. the noncomputable polynomials issue.

[Eric Wieser]

I assume by op (op x) = x in that message you meant op (unop x) = x? The former makes the stronger claim that opposite (opposite X) = X where x : X (edit: fixed, thanks!)

[Reid Barton]

Maybe worth noting that we only really seem to need eta for structures with a single field--I sometimes think about inductives/structures as Haskell data and single-field structures with eta as Haskell newtype

[Eric Wieser]

In the linked issue @Gabriel Ebner mentions e.symm.symm = e which has two data fields, but I agree we care about that less

[Eric Rodriguez]

didn't eta for two fields come up with the splitting_field unsolvable diamond?

[Eric Wieser]

(xref #10220)

[Eric Wieser]

Actually I don't think that's an eta problem

[Reid Barton]

I'm very confused without context especially because the comment says something "should" be an instance but isn't, but in fact it is an instance. But I think we already pretty much take into account the possibility that entire class records might get eta expanded in random places.

[Reid Barton]

It tends not to matter too much because ultimately the use of a class record is to project a field out of it (even if this might require unfolding some definitions to see, so there could be a performance issue)

[Reid Barton]

I think this came up in the context of investigating that other extremely confusing bug (hopefully Eric can remember/guess which one I mean)

[Eric Wieser]

The bug about the tensor algebra ring where an irreducible made two proof fields non-defeq?

[Reid Barton]

The kind of eta expansion I have in mind is if bar extends foo and you have something like def x [h : foo T] : bar T := { ..., .. h } and then x.to_foo isn't defeq to h, because it is an eta expanded version

[Eric Wieser]

Right, which typeclass search seems to know how to perform somehow

[Reid Barton]

Hmm I was then mostly thinking about examples like if foo = group and I define the center of a group, the result will be defeq whether I used h or x.to_foo because h.mul and x.to_foo.mul are defeq... but I guess there's also the situation where you have a "mix-in" class that takes [group T] as a parameter, and then there should be an issue...

[Reid Barton]

The other reason why this isn't a big deal in practice is that once h becomes a specific instance (rather than a variable) it will usually be a constructor applied to something, and then h and x.to_foo will be defeq

[Eric Wieser]

Maybe that was the reason we got rid of module / semimodule

[Reid Barton]

Logically it seems like eta for structures with more than one field should be an issue for things like the product of two categories or a slice category... anyone encountered this?

[Johan Commelin]

What do you mean with "should be an issue"?

[Johan Commelin]

If we had eta for structures with more than one field, then (C^op)^op would have a category defeq to C. That would be cool.

[Reid Barton]

I would have to try it again to see exactly what goes wrong but if you try to make opposite a structure, things get awkward for the opposite category pretty quickly

[Heather Macbeth]

Would it even be possible to have op (op G) definitionally equal to G?

[Heather Macbeth]

I mean for monoids/groups, not just for categories like Johan asked.

[Eric Wieser]

It already is true that G = (Gᵒᵖ)ᵒᵖ I think

[Reid Barton]

I assume you are talking about the types themselves. If opposite is implemented as a one-field structure then opposite (opposite G) will be definitionally different from G, just like opposite G will be.

[Heather Macbeth]

I believe I want both of the following to work -- currently the failure of the first means the second doesn't even typecheck:

import algebra.opposites

variables {G : Type*} [group G]

example : G = (Gᵒᵖ)ᵒᵖ := rfl

example : (by apply_instance : group G) = (by apply_instance : group (Gᵒᵖ)ᵒᵖ) := rfl

[Eric Wieser]

Both are true in the presence of local attribute [semireducible] opposite I think

[Heather Macbeth]

@Eric Wieser This fails:

import algebra.opposites

variables {G : Type*} [_i : group G]

local attribute [semireducible] opposite

-- works
example : G = (Gᵒᵖ)ᵒᵖ := rfl

-- fails
example : _i = @opposite.group (Gᵒᵖ) (@opposite.group G _i) := rfl

[Eric Wieser]

Ah yep, that's because we have no rdiv field

[Eric Wieser]

This demonstrates why they mismatch:

example : _i = @opposite.group (Gᵒᵖ) (@opposite.group G _i) :=begin
  casesI _i,
  dunfold opposite.group,
  unfold_projs,
  dsimp only,
  congr' with x y,
  show div _ _ = mul x (inv y),
  sorry,  -- this is not defeq, we need to apply `div_eq_mul_inv`
end

[Reid Barton]

No, it's because we don't have eta for structures!

[Eric Wieser]

Oh good point, It's both

[Heather Macbeth]

Yes, so for a more minimal example I should change group everywhere to has_mul:

import algebra.opposites

variables {G : Type*} [_i : has_mul G]

local attribute [semireducible] opposite

-- works
example : G = (Gᵒᵖ)ᵒᵖ := rfl

-- fails
example : _i = @opposite.has_mul (Gᵒᵖ) (@opposite.has_mul G _i) := rfl

[Yury G. Kudryashov]

I guess, you'll have better luck with has_mul.mul.

[Yury G. Kudryashov]

Why mul_equiv is not good enough?