free_abelian_group

Stream: general

[Yaël Dillies]

Does anyone know what's going on in file#group_theory/free_abelian_group? I've broke something there by accident and just spent several hours trying to fix it.

[Yaël Dillies]

Really weird stuff is going on there. For example, why does dsimp unfold 0 : free_abelian_group α to add_comm_group.zero?

[Floris van Doorn]

You will have to be more specific if you want anyone to help you.
I agree dsimp shouldn't do that. Does simp also do it? Does squeeze_simp suggest a culprit causing it?

[Yaël Dillies]

No, squeeze_simp returns simp only, dsimp returns dsimp only, I went looking for lemmas tagged simp around and could not find anything suspicious...

[Eric Wieser]

Is this breakage on a branch? Does the dsimp thing happen on master?

[Yaël Dillies]

It's on branch#stronger_div_inv_monoid. I have yet to try on master but I expect it is the same, because my changes do not concern this.

[Yaël Dillies]

When working on this file, there's an overall feeling that the API is not stratified. Everything leaks through. There's a bunch of unfolds, lemmas which visually should not rewrite do, lemmas which should do not...

[Yaël Dillies]

To be clear, the change from my branch that broke the file is that I generalized the second argument of docs#map_inv from group to division_monoid, and this breaks a bunch of instance synthesis with dot notation, some of which is used in API barrier-breaking proofs in group_theory.free_abelian_group.

[Yaël Dillies]

I am trying to confine the API barrier breakage to the API setup now, but this is a real pain due to this (possibly unrelated?) issue of overtransparency.

[Eric Wieser]

Is docs#additive.add_comm_monoid the issue somehow?

[Yaël Dillies]

Oh! I was just thinking the same!

[Eric Wieser]

It looks fine

[Eric Wieser]

docs#abelianization.comm_group would be the next place to look

[Eric Wieser]

That looks possible

[Eric Wieser]

Does adding one := 1 there help?

[Yaël Dillies]

Oh, problem partly solved. The latter instances all use free_abelian_group.add_comm_group, but they did not have add := (+),, so dsimp was happily turning x + y into add_comm_group.add x y.

[Yaël Dillies]

You really have to learn slow-typing :grinning:

[Eric Wieser]

This is the same .. issue that blew up my bimodule PR

[Yaël Dillies]

Is there even any way to fix it? Can .. detect ancestors?

[Jireh Loreaux]

I think I was experiencing something like this recently (although not in the context of free_abelian_group) with turning lp _ \infty into a ring, under appropriate hypotheses on the hole _.

[Yaël Dillies]

And now I'm hitting a timeout.

[Kevin Buzzard]

Lean's telling you that it's time to revise for your forthcoming exams ;-)

[Yaël Dillies]

#14089. I would greatly appreciate help to kill off the timeout.

[Kevin Buzzard]

Oh it's one of those beasts -- the one where if you put sorry at the end it complains there are no goals to solve, but if you remove the sorry then the kernel doesn't buy it and you get a timeout. noncomputable! doesn't fix it either, and neither does recover. Yeah those are ugly :-( Johan solved one in LTE recently by just taking out some sublemma.

[Yaël Dillies]

Arf! DId you ever manage to get rid of one of those?

[Kevin Buzzard]

Even this times out on the branch:

def foo (α : Type u) [monoid α]
  (x y z : free_abelian_group α) :
  x * y * z = x * (y * z) :=
begin
  refine free_abelian_group.induction_on z rfl (λ L3, _) (λ L3 ih, _) (λ z₁ z₂ ih₁ ih₂, _),
  { sorry },
  { rw [mul_neg, mul_neg, mul_neg, ih] },
  { rw [mul_add, mul_add, mul_add, ih₁, ih₂] },
end

[Yaël Dillies]

Does replacing the rfl by (by simp) have a chance to fix it?

[Eric Wieser]

Yaël, does my comment above about abelianization help?

[Eric Wieser]

Your PR seems not to include that change

[Yaël Dillies]

Adding one := 1? We're proving semigroup.

[Kevin Buzzard]

Replacing rfl by sorry fixes it. So maybe it's some kind of abuse of defeq which tactic mode accepts but the kernel doesn't for some reason?

[Yaël Dillies]

Hmm... Those goals are of the form x * y * 0 = x * (y * 0). If we could prove mul_zero_class (free_abelian_group α) beforehand, that would solve it.

[Kevin Buzzard]

assuming that it doesn't time out :-)

[Kevin Buzzard]

@Chris Hughes never liked this definition from the start. He was always adamant that the definition should be completely rewritten in terms of finsupp. I never properly understood his objections to the definition, but then again I know a lot less about implementation than him.

[Kevin Buzzard]

Maybe I'm beginning to understand them now :-/

[Eric Wieser]

Adding explicit data fields to src#abelianization.comm_group

[Yaël Dillies]

Oh I see. Let's try.

[Kevin Buzzard]

Kenny Lau basically wrote that file to practice monads; you can certainly tell by the API!

[Kevin Buzzard]

This works (i.e. doesn't time out):

instance : mul_zero_class (free_abelian_group α) :=
{ mul := (*),
  zero := 0,
  zero_mul := λ a, begin
    have h : (0 + 0) * a = 0 * a, by simp,
    rw add_mul at h,
    simpa using h,
  end,
  mul_zero := λ a, rfl }

instance : semigroup (free_abelian_group α) :=
{ mul := (*),
  mul_assoc := λ x y z, begin
    refine free_abelian_group.induction_on z (by simp) (λ L3, _) (λ L3 ih, _) (λ z₁ z₂ ih₁ ih₂, _),
    { refine free_abelian_group.induction_on y (by simp) (λ L2, _) (λ L2 ih, _) (λ y₁ y₂ ih₁ ih₂, _),
      { refine free_abelian_group.induction_on x (by simp) (λ L1, _) (λ L1 ih, _) (λ x₁ x₂ ih₁ ih₂, _),
        { rw [of_mul_of, of_mul_of, of_mul_of, of_mul_of, mul_assoc] },
        { rw [neg_mul, neg_mul, neg_mul, ih] },
        { rw [add_mul, add_mul, add_mul, ih₁, ih₂] } },
      { rw [neg_mul, mul_neg, mul_neg, neg_mul, ih] },
      { rw [add_mul, mul_add, mul_add, add_mul, ih₁, ih₂] } },
    { rw [mul_neg, mul_neg, mul_neg, ih] },
    { rw [mul_add, mul_add, mul_add, ih₁, ih₂] },
    recover,
  end }

Change the dodgy rfls to simps

[Kevin Buzzard]

Note that the proof of mul_zero is a dodgy rfl but Lean doesn't seem to care this time.

[Yaël Dillies]

You just saved me enough time for a past paper :smiley:

[Kevin Buzzard]

Looks to me like zero_mul might not even be rfl, so your proposed proof really somehow shouldn't work, and yet tactic mode accepts it?

[Yaël Dillies]

Yeah, something fishy going on there.

[Chris Hughes]

Kevin Buzzard said:

Chris Hughes never liked this definition from the start. He was always adamant that the definition should be completely rewritten in terms of finsupp. I never properly understood his objections to the definition, but then again I know a lot less about implementation than him.

It's basically because I think that the universal property on its own is kind of useless if you want to prove any remotely nontrivial theorem about a free abelian group. The universal property is there to transfer what we know about free abelian groups to other objects, but we need more than the universal property to understand anything about free abelian groups in the first place.