Zulip Chat Archive

Stream: general

Topic: with_top irreducible


Yaël Dillies (Nov 06 2021 at 22:14):

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

Yury G. Kudryashov (Nov 06 2021 at 22:17):

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 (Nov 06 2021 at 22:17):

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

Yaël Dillies (Nov 06 2021 at 22:21):

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

Yury G. Kudryashov (Nov 06 2021 at 22:27):

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

Kevin Buzzard (Nov 06 2021 at 22:27):

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 (Nov 06 2021 at 22:28):

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

Yury G. Kudryashov (Nov 06 2021 at 22:29):

(and we need order_dual anyway)

Yaël Dillies (Nov 06 2021 at 22:32):

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 (Nov 06 2021 at 22:34):

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

Patrick Massot (Nov 06 2021 at 22:34):

Irreducible stuff went out of fashion because of Lean 4.

Patrick Massot (Nov 06 2021 at 22:35):

We're meant to use structures instead.

Kevin Buzzard (Nov 06 2021 at 22:35):

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

Kevin Buzzard (Nov 06 2021 at 22:35):

Heh :-)

Yaël Dillies (Nov 06 2021 at 22:35):

Uh?

Kevin Buzzard (Nov 06 2021 at 22:35):

So then this will mean masses of code duplication!

Yaël Dillies (Nov 06 2021 at 22:35):

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

Kevin Buzzard (Nov 06 2021 at 22:35):

oh wait

Kevin Buzzard (Nov 06 2021 at 22:35):

I mean "an inductive type"

Kevin Buzzard (Nov 06 2021 at 22:37):

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 (Nov 06 2021 at 22:38):

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 (Nov 06 2021 at 22:39):

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 (Nov 06 2021 at 22:41):

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 (Nov 06 2021 at 22:42):

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 (Nov 06 2021 at 22:49):

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 (Nov 06 2021 at 23:02):

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 (Nov 07 2021 at 10:07):

So what are the plans for order_dual in Lean 4?

Gabriel Ebner (Nov 08 2021 at 10:07):

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 (Nov 08 2021 at 10:30):

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

Eric Wieser (Nov 08 2021 at 10:31):

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

Reid Barton (Nov 08 2021 at 12:27):

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 (Nov 08 2021 at 16:15):

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 (Nov 09 2021 at 11:04):

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

Gabriel Ebner (Nov 09 2021 at 11:10):

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 (Nov 09 2021 at 11:13):

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 (Nov 09 2021 at 11:44):

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 (Nov 09 2021 at 11:45):

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 (Nov 09 2021 at 11:46):

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

Eric Wieser (Nov 09 2021 at 11:47):

(xref #10220)

Eric Wieser (Nov 09 2021 at 11:49):

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

Reid Barton (Nov 09 2021 at 11:50):

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 (Nov 09 2021 at 11:51):

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 (Nov 09 2021 at 11:53):

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 (Nov 09 2021 at 11:55):

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

Reid Barton (Nov 09 2021 at 11:56):

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 (Nov 09 2021 at 11:57):

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

Reid Barton (Nov 09 2021 at 12:03):

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 (Nov 09 2021 at 12:03):

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 (Nov 09 2021 at 12:04):

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

Reid Barton (Nov 09 2021 at 12:29):

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 (Nov 09 2021 at 13:26):

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

Johan Commelin (Nov 09 2021 at 13:27):

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 (Nov 09 2021 at 13:37):

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 (Nov 09 2021 at 14:17):

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

Heather Macbeth (Nov 09 2021 at 14:32):

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

Eric Wieser (Nov 09 2021 at 15:44):

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

Reid Barton (Nov 09 2021 at 18:18):

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 (Nov 09 2021 at 19:06):

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 (Nov 09 2021 at 19:21):

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

Heather Macbeth (Nov 09 2021 at 19:26):

@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 (Nov 09 2021 at 19:36):

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

Eric Wieser (Nov 09 2021 at 19:36):

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 (Nov 09 2021 at 19:37):

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

Eric Wieser (Nov 09 2021 at 19:37):

Oh good point, It's both

Heather Macbeth (Nov 09 2021 at 21:39):

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 (Nov 10 2021 at 14:03):

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

Yury G. Kudryashov (Nov 10 2021 at 14:03):

Why mul_equiv is not good enough?


Last updated: Dec 20 2023 at 11:08 UTC