CliffordAlgebra/Even `aux_one`

Stream: mathlib4

[Kim Morrison]

Would @Eric Wieser or anyone else be able to take a look at Mathlib/LinearAlgebra/CliffordAlgebra/Even.lean, and the theorem aux_one, and help me with the following:

The written proof is currently:

theorem aux_one : aux f 1 = 1 :=
  congr_arg Prod.fst (foldr_one Q _ _ _)

and #print aux_one shows

theorem aux_one : aux f 1 = 1 :=
  congr_arg Prod.fst (foldr_one Q (CliffordAlgebra.even.lift.fFold f) (CliffordAlgebra.even.lift.fFold_fFold f) (1, 0))

However filling in the _s using these results doesn't result in an accepted proof: it fails with

failed to synthesize instance
  Module R (?m× ?m)

This seems to me like a bad sign. Moreover, it's currently failing on nightly-testing, and as such somewhat undiagnosable, since the terms found by unification aren't even accepted when written explicitly on master.

I'm not sure how much of a redesign I'm asking for here, but hopefully you'll agree that the current state is not good. I don't object to proofs containing _, but it should be possible to replace them with terms (in particular the terms found by unification!).

[Eric Wieser]

Does it really print that without the space around the ×?

[Eric Wieser]

I would guess the 1 and 0 need explicit type annotations

[Eric Wieser]

Maybe a proof that starts by unfolding aux first then using exact with the same term would work

[Richard Copley]

Adding letI : AddCommGroup (S f) := AddSubgroupClass.toAddCommGroup _ should might also work (the _ is (S f)).

[Richard Copley]

As in

@[simp, nolint simpNF] -- Added `nolint simpNF` to avoid a timeout #8386
theorem aux_one : aux f 1 = 1 :=
  letI : AddCommGroup (S f) := AddSubgroupClass.toAddCommGroup (S f)
  congr_arg Prod.fst (foldr_one Q (CliffordAlgebra.even.lift.fFold f)
    (CliffordAlgebra.even.lift.fFold_fFold f) (1, 0))

[Kim Morrison]

Thanks @Richard Copley, that's gets us unstuck.

[Eric Wieser]

How many underscores can you restore with that letI in place?

[Kim Morrison]

  congr_arg Prod.fst (foldr_one _ _
    (CliffordAlgebra.even.lift.fFold_fFold f) _)

[Eric Wieser]

If you add rw [aux] beforehand can you restore all of them?

[Kim Morrison]

No.

[Eric Wieser]

Weird

[Kim Morrison]

Actually, aux_ι, aux_algebraMap, aux_mul all suffer from this problem. I'm going to sorry them out in nightly-testing for now, and hope for now that they get repaired via lean4 fixes addressing other issues... @Richard Copley, if you are inclined, I'd be happy to have your versions of these, as you did for aux_one!

[Kim Morrison]

(And if anyone wants to send something the master that just smoothes all this out somehow, I'd love that even more. :-)

[Eric Wieser]

Can you share the commit that has this issues so that I can investigate later?

[Kim Morrison]

Current nightly-testing, 7dfbc59f645f661ea947d286693276dfa762802e.

[Utensil Song]

Lots of _s seem to be difficult to port between Lean versions, in #9111 I learned/tried to use named arguments and less _s. Don't know if there's a style guide on this.

[Richard Copley]

Kim Morrison said:

Actually, aux_ι, aux_algebraMap, aux_mul all suffer from this problem. I'm going to sorry them out in nightly-testing for now, and hope for now that they get repaired via lean4 fixes addressing other issues... Richard Copley, if you are inclined, I'd be happy to have your versions of these, as you did for aux_one!

Can do. I have DM'ed you with the new text, with which you're welcome to do what you will. (Or I'll commit it, but I don't know where to.)

[Kim Morrison]

Thanks @Richard Copley, that's very helpful. I'll use this verbatim on nightly-testing now. Would you mind making a PR to master with these changes, and if @Eric Wieser agrees that they are more robust proofs we can merge it there to reduce the upcoming diff when we try to merge nightly-testing.

[Richard Copley]

@Kim Morrison, @Eric Wieser, #12463.

[Kim Morrison]

@Eric Wieser, I'm hesistant to make these changes solely because they fix nightly-testing, unless you think they are actually helpful / more robust / more readable. If you really prefer the "all _s" proofs, then we'll hold off on this and see if further upcoming lean4 changes affect these proofs.

[Eric Wieser]

I don't care that much, but I'd like to understand why they break first

[Eric Wieser]

Conceptually the proof is just "aux is defined as the first part of this other thing, and here's a lemma that ought to unify with that other thing'

[Eric Wieser]

Having to repeat everything we wrote in the definition to use the lemma feels a bit clumsy

[Eric Wieser]

Here we're fortunate that the proof argument is already extracted into a lemma, but if the proof were inlined in the def then having to repeat it again would be pretty unacceptable

[Utensil Song]

Introducing unnecessary repetition would be some kind of a regression.

[Eric Wieser]

Eric Wieser said:

If you add rw [aux] beforehand can you restore all of them?

Kim Morrison said:

No.

This is the proof I was thinking of:

@[simp, nolint simpNF] -- Added `nolint simpNF` to avoid a timeout #8386
theorem aux_one : aux f 1 = 1 := by
  dsimp only [aux, LinearMap.comp_apply, LinearMap.fst_apply]
  exact congr_arg Prod.fst (foldr_one _ _ _ _)

[Eric Wieser]

I don't claim this is necessarily any better than Richard's solution; but maybe it makes clear why I would expect the original proof to "just work"

[Eric Wieser]

Weirdly filling in the first argument with Q makes the proof break, even though that's what is used for that argument

[Kim Morrison]

Eric Wieser said:

Eric Wieser said:

If you add rw [aux] beforehand can you restore all of them?

Kim Morrison said:

No.

This is the proof I was thinking of:

@[simp, nolint simpNF] -- Added `nolint simpNF` to avoid a timeout #8386
theorem aux_one : aux f 1 = 1 := by
  dsimp only [aux, LinearMap.comp_apply, LinearMap.fst_apply]
  exact congr_arg Prod.fst (foldr_one _ _ _ _)

Can we push this to master? (And similarly the following proofs.) It seems a strict improvement: we're relying on defeq less.

[Eric Wieser]

I feel like relying on LinearMap.comp being defeq to Function.comp or LinearMap.fst being defeq to Prod.fst shouldn't be something that we ever ought to have to worry about

[Eric Wieser]

I wonder if we ought to have a special category of dsimp lemmas that means "this is true by definition as part of a bundled API"

[Eric Wieser]

dsimp only [comp_apply, fst_apply, trans_apply, coe_coe] etc can become very noisy and is more prone to breakage when lemmas rename, while dsimp by itself is often worse for performance than just relying on the defeq.

[Kim Morrison]

Just noting that the problems discussed in this thread have now gone away due to change upstream. Thanks everyone for the help.

[Utensil Song]

Out of curiosity and some concern, can you help identifying to the breakage/fix? That could be an issue/PR/topic.