Structured proofs / to_additive

Stream: mathlib4

[Antoine Chambert-Loir]

I have two questions related to the proof of B. H. Neumann Lemma that @Richard Copley and I managed to formalize.

The first proof is in branch#ACL/Neumann and is the object of a WIP PR #13047
As you can observe, there is an intricate construction of which one needs to keep a ton of invariants to get the clean main theorems.

Inspired by comments of @Patrick Massot , I tried to split the proof into shorter shunks, creating structures that hold the result of the constructions. The result is in branch#ACL/Neumann-attempt

A lot of things can certainly be golfed, but opinions would be welcome whether this is useful work, or not, and whether it can be improved in one way or another.

Moreover, the whole file is supposed to have @[to_additive] tags, but the automatic system breaks down in two or three proofs, where Lean is confused by the presence of multiplicative inverses of rational numbers which it (apparently) tries to replace by negation. Any help here would also be appreciated.

[Floris van Doorn]

Can you make a Mathlib branch that I can check out where the first/only error is a failure of @[to_additive]?

[Richard Copley]

I may have such a thing hanging around in my reflog ...

[Floris van Doorn]

to_additive is using some heuristics to decide whether to additivize an operation. It does so by looking at the type on which the multiplicative operation happens. If that type is Rat, then the heuristic should catch this and leave it alone.

[Floris van Doorn]

You can also try the steps here, and see if any of them are useful:
https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/ToAdditive.lean#L130

[Richard Copley]

Floris van Doorn said:

Can you make a Mathlib branch that I can check out where the first/only error is a failure of @[to_additive]?

Are you able to try the content of GroupTheory.CosetCover from commit d9cd5b18d3 on Antoine's branch (uncomment @[to_additive] on line 481), with the cache from commit b7e495e480? (It's a little awkward, because a branch with errors doesn't really get a cache ... )

[Richard Copley]

Floris van Doorn said:

You can also try the steps here, and see if any of them are useful:
https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/ToAdditive.lean#L130

I spent a while staring at that. It really looked like the chosen type should be the Group G as intended. I didn't make progress.

[Floris van Doorn]

On commit d9cd5b18d33 I get a bunch of unknown identifier errors and no error raised by to_additive.

[Floris van Doorn]

Oh, I missed your parenthetical

[Floris van Doorn]

This looks like #10830, presumably when using simp with a GroupWithZero lemma. You can try the workaround mentioned there.

[Floris van Doorn]

By specifying the type explicitly 4 times and adding @[to_additive] on line 340 it now works:

@[to_additive]
theorem Subgroup.LeftCosetCover.sieve_density
    [Finite c.carrier]
    [DecidableEq (Subgroup G)]
    [DecidablePred (Subgroup.FiniteIndex : Subgroup G → Prop)] :
    Subgroup.LeftCosetCover.density (Subgroup.LeftCosetCover.sieve c)
      = Subgroup.LeftCosetCover.density c := by
  unfold density
  have _ : Fintype c.carrier := Fintype.ofFinite _
  have _ : Fintype (sieve c).carrier := Fintype.ofFinite (sieve c).carrier
  rw [finsum_eq_finset_sum_of_support_subset _ (s := Finset.univ)]
  rw [finsum_eq_finset_sum_of_support_subset _ (s := Finset.univ)]
  classical
  rw [← Finset.sum_fiberwise_of_maps_to
    (s := Finset.univ) (t := Finset.univ) (g := fun k ↦ k.1)]
  · apply Finset.sum_congr rfl
    intro x _
    by_cases hx : (c.subgroup x).FiniteIndex
    · rw [Finset.sum_congr rfl (g := fun y ↦ ((core c).index : ℚ)⁻¹)]
      rw [Finset.sum_const]
      simp only [nsmul_eq_mul]
      rw [mul_inv_eq_iff_eq_mul₀]
      rw [← Subgroup.relindex_mul_index (core_le c hx), mul_comm]
      simp only [Nat.cast_mul (α := ℚ),  mul_assoc (G := ℚ)]
      rw [(mul_inv_eq_one₀ _).mpr rfl, mul_one]
      simp only [Nat.cast_inj]
      unfold sieve
      simp only [id_eq, smul_eq_mul, eq_mpr_eq_cast, cast_eq]
      have : (core c).FiniteIndex := core_finiteIndex c
      set t := fun y hy ↦ (Subgroup.exists_leftTransversal_of_FiniteIndex (H := c.subgroup y) (Subgroup.LeftCosetCover.core_le c hy)).choose with ht_eq
      let ht := fun y hy ↦ (Subgroup.exists_leftTransversal_of_FiniteIndex (H := c.subgroup y) (Subgroup.LeftCosetCover.core_le c hy)).choose_spec

      rw [Finset.card_congr (f := fun y hy ↦ (⟨y.snd, by
        simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hy
        rw [← hy]
        exact sieve_carrier_fiber_le_subgroup c y⟩ : c.subgroup x))
        (t := t x hx)]
      have := Subgroup.card_left_transversal (ht x hx).1
      simp only [Finset.coe_sort_coe, Nat.card_eq_fintype_card, Fintype.card_coe] at this
      rw [this]
      simp only [Subgroup.subgroupOf, Subgroup.index_comap,
        Subgroup.subtype_range]
      · rintro ⟨y1, ⟨y2, hy2⟩⟩ hy
        simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hy2 hy
        have hy1 : (c.subgroup y1).FiniteIndex := hy ▸ hx
        rw [dif_pos hy1] at hy2
        simp only
        have hy2 : y2 ∈ t y1 hy1 := by
          rw [ht_eq]
          exact hy2
        convert hy2
        all_goals
          rw [hy]
      · rintro ⟨y1, ⟨y2, hy2⟩⟩ ⟨y'1, ⟨y'2, hy'2⟩⟩ h h'
        simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hy2 hy'2 h h'
        simp only [Subtype.mk.injEq, Sigma.mk.inj_iff]
        intro h2
        constructor
        · rw [h, h']
        · refine (Subtype.heq_iff_coe_heq ?_ ?_).mpr ?_
          rw [h, h']
          rw [h, h']
          refine (Subtype.heq_iff_coe_heq rfl ?_).mpr ?_
          rw [h, h']
          simp only [h2, heq_eq_eq]
      · intro g hg
        have hg' : g ∈ if (c.subgroup x).FiniteIndex then t x hx else {1} := by
          rw [if_pos hx]
          exact hg
        use ⟨x, ⟨g, hg'⟩⟩
        simp only [Subtype.coe_eta, Finset.mem_filter, Finset.mem_univ, and_self, exists_const]
      · simp only [ne_eq, Nat.cast_eq_zero]
        exact hx.finiteIndex
      · simp only [ne_eq, Nat.cast_eq_zero]
        exact (core_finiteIndex c).finiteIndex
      · simp only [Finset.mem_filter, Finset.mem_univ, true_and, inv_inj (G := ℚ), Nat.cast_inj]
        intro y hy
        apply congr_arg
        rw [sieve_subgroup_eq_core_iff, hy]
        exact hx
    · rw [Finset.sum_congr rfl (g := fun _ ↦ 0)]
      simp only [Finset.sum_const_zero, zero_eq_inv (G₀ := ℚ)]
      rw [eq_comm, Nat.cast_eq_zero]
      by_contra hx'
      exact hx ⟨hx'⟩
      · simp only [Finset.mem_filter, Finset.mem_univ, true_and, inv_eq_zero (G₀ := ℚ), Nat.cast_eq_zero]
        intro y hy
        suffices ¬ ((sieve c).subgroup y).FiniteIndex by
          by_contra hy'
          exact this ⟨hy'⟩
        rw [sieve_subgroup_finite_index_iff, hy]
        exact hx
  · exact fun _ _ ↦ Finset.mem_univ _
  · simp only [Finset.coe_univ, Set.subset_univ]
  · simp only [Finset.coe_univ, Set.subset_univ]

[Antoine Chambert-Loir]

Thanks!

[Floris van Doorn]

Yesterday someone (@Patrick Massot, @Kevin Buzzard or @Johan Commelin) remarked to me "I haven't seen people having issues with to_additive recently. It seems like you've solved all the issues with it."
Clearly they jinxed it :grinning:

[Richard Copley]

(@Yaël Dillies left the comment

  -- Must specify the argument `α` to avoid mathlib4#10830

dangling when they removed the explicit argument in bb349f30dee, which makes #10830 a little confusing.)

[Patrick Massot]

I was exactly thinking I jinxed you. I’m really sorry about that.

[Patrick Massot]

And at the same time I’m asking questions to Kyle who should be urgently grading exams. I am really an awful ex-postdoc employer.

[Antoine Chambert-Loir]

Richard Copley said:

(Yaël Dillies left the comment

  -- Must specify the argument `α` to avoid mathlib4#10830

dangling when they removed the explicit argument in bb349f30dee, which makes #10830 a little confusing.)

Is it possible to write a linter to detect that?

[Antoine Chambert-Loir]

Patrick Massot said:

And at the same time I’m asking questions to Kyle who should be urgently grading exams. I am really an awful ex-postdoc employer.

Real bad employers shame themselves yet go on…

[Patrick Massot]

Sure, I always have new meta-programming questions for Kyle.

[Patrick Massot]

I’m less sure about my jinxing abilities.

[Antoine Chambert-Loir]

That's a cool way to be an awful employer. (Checking in a dictionary what “jinxing” means…)

[Patrick Massot]

And I’m no longer employing them, I’m their ex-employer only.

[Antoine Chambert-Loir]

Sometimes ex-es are toxic too… (unfortunately, more than often)