mysterious finsupp related timeout

Stream: mathlib4

[Scott Morrison]

Minimising @Riccardo Brasca's timeout a little further:

import data.polynomial.ring_division

-- works:
structure test_no_algebra_map (K : Type) [comm_ring K] [is_domain K] [decidable_eq K] :=
(n : ℕ)
(x : (n : polynomial K).roots.to_finset)

-- works:
structure test_eq_bot (K : Type) [comm_ring K] [is_domain K] [decidable_eq K] :=
(n : ℕ)
(x : ((n : polynomial K).map (ring_hom.id K)).roots = ⊥)

-- works:
structure test_37 (K : Type) [comm_ring K] [is_domain K] [decidable_eq K] :=
(x : ((37 : polynomial K).map (ring_hom.id K)).roots.to_finset)

-- works:
structure test_mem (K : Type) [comm_ring K] [is_domain K] [decidable_eq K] :=
(n : ℕ)
(x : K)
(m : x ∈ ((n : polynomial K).map (ring_hom.id K)).roots.to_finset)

-- deterministic timeout:
structure mystery_timeout (K : Type) [comm_ring K] [is_domain K] [decidable_eq K] :=
(n : ℕ)
(x : ((n : polynomial K).map (ring_hom.id K)).roots.to_finset)

[Scott Morrison]

It's not anything about roots itself: we can replace it with a stub definition, and still see the timeout. It's something about polynomial.map?

import data.polynomial.eval

-- Mostly harmless version of `polynomial.roots`:
-- examples below are the same using this or the real one.
def polynomial.roots' {K : Type} [semiring K] (p : polynomial K) : finset K := ⊥

-- works:
structure test_no_map (K : Type) [semiring K] :=
(n : ℕ)
(x : (n : polynomial K).roots')

-- works:
structure test_eq_bot (K : Type) [semiring K] :=
(n : ℕ)
(x : ((n : polynomial K).map (ring_hom.id K)).roots' = ⊥)

-- works:
structure test_37 (K : Type) [semiring K]  :=
(x : ((37 : polynomial K).map (ring_hom.id K)).roots')

-- works:
structure test_mem (K : Type) [semiring K] :=
(n : ℕ)
(x : K)
(m : x ∈ ((n : polynomial K).map (ring_hom.id K)).roots')

-- works:
structure test_nonempty (K : Type) [semiring K] :=
(n : ℕ)
(m : nonempty ((n : polynomial K).map (ring_hom.id K)).roots')

noncomputable def polynomial.map' {R : Type} [semiring R] {S : Type} [semiring S]
  (p : polynomial R) (f : R →+* S) : polynomial S := 0

-- works:
structure test_map' (K : Type) [semiring K] :=
(n : ℕ)
(x : ((n : polynomial K).map' (ring_hom.id K)).roots')

-- deterministic timeout:
structure mystery_timeout (K : Type) [semiring K] :=
(n : ℕ)
(x : ((n : polynomial K).map (ring_hom.id K)).roots')

[Scott Morrison]

Note this timeout now only imports data.polynomial.eval, so #19182 can't help as that only touches downstream. Perhaps more of the same further upstream??

[Damiano Testa]

I am not sure if this counts as further minimizing, but this also times out:

import data.polynomial.eval

--  stubs for the definitions of `roots'` and `ring_hom_id` all specialized to `ℕ`
def roots' (p : polynomial ℕ) : Type := sorry
def im : ℕ →+* ℕ := sorry

--  note the positions of the final two arguments of `polynomial.eval₂`: they swap between here...
structure zero_last :=
(n : ℕ)
(x : (roots' (polynomial.eval₂ (polynomial.C.comp im) (n : polynomial ℕ) 0)))

-- ... and here
structure mystery_timeout :=
(n : ℕ)
(x : (roots' (polynomial.eval₂ (polynomial.C.comp im) 0 (n : polynomial ℕ))))

The second times out, while the first does not.

Also note that eval₂ is defined at the very beginning of data.polynomial.eval, but I do not have time to see if it times out also with eval₂ replaced by the direct polynomial.sum call, which would push the time out further up in the import hierarchy.

[Scott Morrison]

Further minimized to:

import data.polynomial.basic

--  stubs for the definitions of `roots'` and `ring_hom_id` all specialized to `ℕ`
def roots' (p : polynomial ℕ) : Type := sorry

noncomputable def eval₂ (p : polynomial ℕ) : polynomial ℕ :=
p.sum (λ e a, polynomial.C a * 1)

structure works :=
(n : ℕ)
(x : (roots' (eval₂ 0)))

structure mystery_timeout :=
(n : ℕ)
(x : (roots' (eval₂ (n : polynomial ℕ))))

so we're now right at the beginning of the polynomial development. :-(

[Damiano Testa]

I'm not sure whether I'm happy of the minimisation or said for how early it happens!

[Scott Morrison]

Now we're all the way back at monoid_algebra:

import algebra.monoid_algebra.basic

def Q (p : add_monoid_algebra ℕ ℕ) : Type := sorry

noncomputable def E (p : add_monoid_algebra ℕ ℕ) : add_monoid_algebra ℕ ℕ :=
finsupp.single 0 (p 0) * 1

structure works :=
(n : ℕ)
(x : (Q (E 0)))

structure mystery_timeout :=
(n : ℕ)
(x : (Q (E (n : add_monoid_algebra ℕ ℕ))))

[Damiano Testa]

I'm on mobile, but using finsupp instead of add_monoid_algebra might minimise further, maybe?

[Damiano Testa]

Otherwise it might be the ring structure, which was something that I suspected, since stubbing out polynomials i wasn't able to get a time-out

[Johan Commelin]

(fwiw, I've fixed the final sorry on the ml4 PR)

[Johan Commelin]

are we sure that sorry-ing a def isn't going to mess up these minimizations?

[Johan Commelin]

anyway, changing def := sorry to constant also gives a timout

[Johan Commelin]

#check Σ (n : ℕ), Q (E (n : add_monoid_algebra ℕ ℕ))

is instant :mind_blown:

[Scott Morrison]

import algebra.big_operators.basic
import data.finsupp.defs

def Q (p : finsupp ℕ ℕ) : Type := sorry

open_locale big_operators

noncomputable def E (p : finsupp ℕ ℕ) : finsupp ℕ ℕ :=
∑ (n : ℕ) in ⊥, ∑ m in (finsupp.single 0 1).support, finsupp.single 0 (p 0 * 1)

structure works :=
(n : ℕ)
(x : (Q (E 0)))

structure mystery_timeout :=
(n : ℕ)
(x : (Q (E (finsupp.single 0 n))))

[Scott Morrison]

I am increasingly fearful that it is:

def single (a : α) (b : M) : α →₀ M :=
{ support := by haveI := classical.dec_eq M; exact if b = 0 then ∅ else {a},
  ...

in data.finsupp.defs.

[Scott Morrison]

The timeout is preserved with def Q (p : finsupp ℕ ℕ) : Type := ℕ , so no, the sorry isn't implicated here.

[Johan Commelin]

import Mathlib.Algebra.MonoidAlgebra.Basic

axiom Q (p : AddMonoidAlgebra ℕ ℕ) : Type

noncomputable def E (p : AddMonoidAlgebra ℕ ℕ) : AddMonoidAlgebra ℕ ℕ :=
.single 0 (p 0) * 1

structure works :=
(n : ℕ)
(x : (Q (E 0)))

#check Σ (n : ℕ), Q (E (n : AddMonoidAlgebra ℕ ℕ))

structure mystery_timeout :=
(n : ℕ)
(x : (Q (E (n : AddMonoidAlgebra ℕ ℕ))))

also times out in ml4.

[Johan Commelin]

What is structure doing that a sigma doesn't? Could that be a hint?

[Scott Morrison]

I noticed a lot of has_sizeofs in the typeclass search trace. I did try earlier switching to inductive but that seemed to preserve the timeouts, and so didn't notice the sigma trick.

[Scott Morrison]

Curiously the lean4-ification of my last minimisation seems to run fine.

[Scott Morrison]

Have to run for a bit.

[Notification Bot]

21 messages were moved here from #mathlib4 > !4#4891 FieldTheory.SplittingField by Johan Commelin.

[Damiano Testa]

Here the timeouts are slowing down:

import algebra.big_operators.basic
import data.finsupp.defs
variable {α : Type}

def Q (p : α) : Type := ℕ

open_locale big_operators

def E (p : ℕ → ℕ) : ℕ :=
∑ m in ({0} : finset ℕ),
∑ m in ({0} : finset ℕ),
(p 0)

def MyNat_to_fun (n : ℕ): Type := Q (E (finsupp.single n 0).to_fun)

structure slow_but_works :=
(n : ℕ)
(x : MyNat_to_fun n)

def MyNat (n : ℕ): Type := Q (E (finsupp.single n 0))

structure mystery_timeout :=
(n : ℕ)
(x : MyNat n)

[Damiano Testa]

With the hint of taking the to_fun of the finsupp Lean is slow, but works in slow_but_works, whereas it still times out on mystery_timeout, without the to_fun hint.

[Damiano Testa]

Also, Lean doe not want anything to be marked nonconstructible.

[Damiano Testa]

And, if in def E you remove one of the two sums, there is no timeout and it is very quick.

[Damiano Testa]

Even using the "strong" type ascription

def MyNat (n : ℕ): Type := Q (E (id (finsupp.single n 0) : ℕ → ℕ))

gives a time out.

[Damiano Testa]

Further minimization: I got rid of the finsupp.

import algebra.big_operators.basic

variable {α : Type}
open multiset
def Q (p : α) : Type := ℕ

def E (p : ℕ → ℕ) : ℕ :=
(({0} : multiset ℕ).map
((({0} : multiset ℕ).map ((p 0) : ℕ → ℕ)).sum : ℕ → ℕ)).sum

structure myfins : Type :=
(to_fun : ℕ → ℕ)

def m0 (n : ℕ): myfins := ⟨λ m, n⟩

instance : has_coe_to_fun myfins (λ _, ℕ → ℕ) := ⟨myfins.to_fun⟩

def MyfinNat (n : ℕ): Type := Q (E (m0 n))

structure mystery_timeout :=
(n : ℕ)
(x : MyfinNat n)

[Damiano Testa]

I suspect that the coercions (p 0) : ℕ → ℕ are doing some harm.

[Scott Morrison]

Oh dear! I was just about to report that giving finsupp.single variable decidable_eq instances did not resolve the problem, but this last minimization better shows that that was not the culprit.

[Damiano Testa]

I have replaced the \sum with their explicit expressions, since I wanted to get out of big_operators, but I did not manage, so it might be clearer to revert to \sums or keep minimizing!

[Damiano Testa]

(I slightly edited the above, so that now there are only multisets, no finsets, I think.)

[Kevin Buzzard]

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/mysterious.20finsupp.20related.20timeout/near/365782829

I don't get a timeout with that code. How come I'm missing out on the fun? I have lean memory limit set to 12000 in VS Code.

[Damiano Testa]

Replacing multisets with list, it goes back to being almost instantaneous.

[Damiano Testa]

Kevin, I have memory limit 4096.

[Damiano Testa]

Anyway, if you add more of the sums, each one, on my machine, adds a significant amount of extra processing time.

[Damiano Testa]

More specifically, use

def E (p : ℕ → ℕ) : ℕ :=
∑ m in ({0} : finset ℕ),
∑ m in ({0} : finset ℕ),
∑ m in ({0} : finset ℕ),
(p 0)

for E and keep adding extra \sum lines, if that is still not timing out!

[Kevin Buzzard]

right, so it's a slowdown not a loop.

[Damiano Testa]

Yes, I think so. At least this issue on which we have zoomed in...

[Damiano Testa]

Unfortunately, I have to go back to some non-Lean slowdowns... :upside_down:

[Riccardo Brasca]

I think at least the original one was really a loop (or something similar, but not a slowdown). This one

import data.polynomial.ring_division

-- works:
structure test_no_algebra_map (K : Type) [comm_ring K] [is_domain K] [decidable_eq K] :=
(n : ℕ)
(x : (n : polynomial K).roots.to_finset)

-- works:
structure test_eq_bot (K : Type) [comm_ring K] [is_domain K] [decidable_eq K] :=
(n : ℕ)
(x : ((n : polynomial K).map (ring_hom.id K)).roots = ⊥)

-- works:
structure test_37 (K : Type) [comm_ring K] [is_domain K] [decidable_eq K] :=
(x : ((37 : polynomial K).map (ring_hom.id K)).roots.to_finset)

-- works:
structure test_mem (K : Type) [comm_ring K] [is_domain K] [decidable_eq K] :=
(n : ℕ)
(x : K)
(m : x ∈ ((n : polynomial K).map (ring_hom.id K)).roots.to_finset)

-- deterministic timeout:
structure mystery_timeout (K : Type) [comm_ring K] [is_domain K] [decidable_eq K] :=
(n : ℕ)
(x : ((n : polynomial K).map (ring_hom.id K)).roots.to_finset)

is taking forever on my machine, even on the command line.

[Riccardo Brasca]

Scott Morrison said:

import algebra.big_operators.basic
import data.finsupp.defs

def Q (p : finsupp ℕ ℕ) : Type := sorry

open_locale big_operators

noncomputable def E (p : finsupp ℕ ℕ) : finsupp ℕ ℕ :=
∑ (n : ℕ) in ⊥, ∑ m in (finsupp.single 0 1).support, finsupp.single 0 (p 0 * 1)

structure works :=
(n : ℕ)
(x : (Q (E 0)))

structure mystery_timeout :=
(n : ℕ)
(x : (Q (E (finsupp.single 0 n))))

This it works (on the command line) for me, it's just very slow. The previous one,

import algebra.monoid_algebra.basic

def Q (p : add_monoid_algebra ℕ ℕ) : Type := sorry

noncomputable def E (p : add_monoid_algebra ℕ ℕ) : add_monoid_algebra ℕ ℕ :=
finsupp.single 0 (p 0) * 1

structure works :=
(n : ℕ)
(x : (Q (E 0)))

structure mystery_timeout :=
(n : ℕ)
(x : (Q (E (n : add_monoid_algebra ℕ ℕ))))

really seems to take forever.

[Damiano Testa]

Let's see if this is my computer being slow or not: does this seem like a loop or a timeout?

import algebra.monoid_algebra.basic

def Q (p : ℕ → ℕ) : Type := ℕ

noncomputable def E (p : ℕ) : add_monoid_algebra ℕ ℕ :=
p * 1

structure works :=
(n : ℕ)
(x : Q (E 0))

structure mystery_timeout :=
(n : ℕ)
(x : Q (E n))

[Damiano Testa]

So it might really be the ring structure on add_monoid_algebra... Changing p * 1 to 1 • p or p • 1 does not give a timeout.

[Kevin Buzzard]

yeah that times out for me

[Riccardo Brasca]

Looks like a loop.

[Damiano Testa]

If you force the multiplication to happen in nat, e.g. by defining

noncomputable def E (p : ℕ) : add_monoid_algebra ℕ ℕ :=
(p * 1 : ℕ)

then it is also very quick.

[Eric Wieser]

Isn't Q (E n) nonsense? add_monoid_algebra has no function coercion, does it?

[Damiano Testa]

Eric, if I understand correctly, add_monoid_algebra does have a coercion from natural numbers, since it as a 1, an addition and maybe a 0...

[Damiano Testa]

import algebra.monoid_algebra.basic

variable (n : ℕ)
#check (n : add_monoid_algebra ℕ ℕ)  -- works: ↑n : add_monoid_algebra ℕ ℕ

#check (n : finsupp ℕ ℕ)  -- fails:
/-
invalid type ascription, term has type
  ℕ
but is expected to have type
  ℕ →₀ ℕ
-/

[Johan Commelin]

But Q eats a function, and a term of an add_monoid_algebra doesn't look like a function...

[Damiano Testa]

I am probably misunderstanding, but there is a coercion to functions:

variable (x : add_monoid_algebra ℕ ℕ)
#check (x : ℕ → ℕ)  -- ⇑x : (λ (_x : add_monoid_algebra ℕ ℕ), ℕ → ℕ) x

[Damiano Testa]

I think that there are lots of coincidences of types that are tripping me up and probably also Lean...

[Johan Commelin]

ooh, I didn't expect that to exist

[Damiano Testa]

example : has_coe_to_fun (add_monoid_algebra ℕ ℕ) (λ _, ℕ → ℕ):= add_monoid_algebra.has_coe_to_fun ℕ ℕ

docs#add_monoid_algebra.has_coe_to_fun

[Scott Morrison]

Yes, I suspect we long ago intended to remove that, but never did.

[Damiano Testa]

And this is the coercion:

noncomputable example : has_coe_t ℕ (add_monoid_algebra ℕ ℕ) := nat.cast_coe

docs#nat.cast_coe

[Eric Wieser]

That one is expected but I don't think it's relevant to your example above?

[Damiano Testa]

Eric, the definition of E seems to interpret a natural number as an element of an add_monoid_algebra, I think.

[Damiano Testa]

and i suspect that the product p * 1 in add_monoid_algebra is what is really causing damage.

[Kevin Buzzard]

So this is timing out for me:

import data.finsupp.defs

def Q (p : ℕ → ℕ) : Type := ℕ

variables {k G : Type} [semiring k]

open_locale big_operators

def finsupp.sum' {α M N : Type} [has_zero M] [add_comm_monoid N] (f : α →₀ M) (g : α → M → N) : N :=
∑ a in f.support, g a (f a)

noncomputable def E (p : ℕ) : ℕ →₀ ℕ :=
finsupp.sum' (finsupp.single 0 p) $ λa₁ b₁, finsupp.sum' (finsupp.single 0 1) $ λa₂ b₂, finsupp.single (a₁ + a₂) (b₁ * b₂)

inductive mystery_timeout
| mk (n : ℕ) (x : Q (E n : ℕ → ℕ)) -- don't even need to write `: mystery_timeout`

[Johan Commelin]

Wow, with inductive!

[Johan Commelin]

I'm still mystified why it is instant with Sigma.

[Eric Wieser]

Does any of this reproduce in Lean 4?

[Johan Commelin]

import Mathlib.Algebra.MonoidAlgebra.Basic

axiom Q (p : AddMonoidAlgebra ℕ ℕ) : Type

noncomputable def E (p : AddMonoidAlgebra ℕ ℕ) : AddMonoidAlgebra ℕ ℕ :=
.single 0 (p 0) * 1

structure works :=
(n : ℕ)
(x : (Q (E 0)))

#check Σ (n : ℕ), Q (E (n : AddMonoidAlgebra ℕ ℕ))

set_option trace.Meta.isDefEq true

structure mystery_timeout :=
(n : ℕ)
(x : (Q (E (n : AddMonoidAlgebra ℕ ℕ))))

times out

[Johan Commelin]

But that's a few minimization-stages ago

[Damiano Testa]

If you change (b₁ * b₂) at the end of E with b₁, it is just really slow...
EDIT: this comment is related to Kevin's message.

[Johan Commelin]

This is slow, but works

import Mathlib.Data.Finsupp.Defs

def Q (_p : ℕ → ℕ) : Type := ℕ

variables {k : Type} [Semiring k]

open BigOperators

def Finsupp.sum' {α M N : Type} [Zero M] [AddCommMonoid N] (f : α →₀ M) (g : α → M → N) : N :=
∑ a in f.support, g a (f a)

noncomputable def E (p : ℕ) : ℕ →₀ ℕ :=
.sum' (.single 0 p) <|
  fun a₁ b₁ ↦ .sum' (.single 0 1) <|
  fun a₂ b₂ ↦ .single (a₁ + a₂) (b₁ * b₂)

inductive mystery_timeout
| mk (n : ℕ) (x : Q (E n : ℕ → ℕ))

[Riccardo Brasca]

Looking at the trace there are a couples of

[Kernel] [1.491174s] typechecking declaration

is this normal?

[Riccardo Brasca]

Johan Commelin said:

import Mathlib.Algebra.MonoidAlgebra.Basic

axiom Q (p : AddMonoidAlgebra ℕ ℕ) : Type

noncomputable def E (p : AddMonoidAlgebra ℕ ℕ) : AddMonoidAlgebra ℕ ℕ :=
.single 0 (p 0) * 1

structure works :=
(n : ℕ)
(x : (Q (E 0)))

#check Σ (n : ℕ), Q (E (n : AddMonoidAlgebra ℕ ℕ))

set_option trace.Meta.isDefEq true

structure mystery_timeout :=
(n : ℕ)
(x : (Q (E (n : AddMonoidAlgebra ℕ ℕ))))

times out

With set_option maxHeartbeats 0 in this works, it is just very slow. The trace has various

[] [11.596550s] ❌ E ↑n✝ =?= E ↑n

[Damiano Testa]

Maybe there never was a loop, just a really long computation...

[Scott Morrison]

Yes, I think that is likely.

[Damiano Testa]

I can confirm that variations on example that Kevin sent do seem to terminate, but they also require a long time...

[Riccardo Brasca]

Maybe we should understand why the original problem does not exist in current master. In the following

import field_theory.splitting_field.construction

variables (K : Type) [field K]

structure test :=
(n : ℕ)
(x : (n : polynomial K).splitting_field)

structure test1 := -- deterministic timeout
(n : ℕ)
(x : mv_polynomial ((n : polynomial K).root_set K) K)

the first one works fine, the second gives a timeout. Is it possible that the difference is that splitting_field is defined using nat.rec?

[Sebastian Ullrich]

Riccardo Brasca said:

With set_option maxHeartbeats 0 in this works, it is just very slow. The trace has various

[] [11.596550s] ❌ E ↑n✝ =?= E ↑n

Judging from the shape of the unification problem, this is likely in automatic generation of injectivity theorems, which can be disabled with the option genInjectivity

[Riccardo Brasca]

import Mathlib.Algebra.MonoidAlgebra.Basic

axiom Q (p : AddMonoidAlgebra ℕ ℕ) : Type

noncomputable def E (p : AddMonoidAlgebra ℕ ℕ) : AddMonoidAlgebra ℕ ℕ :=
.single 0 (p 0) * 1

structure works :=
(n : ℕ)
(x : (Q (E 0)))

#check Σ (n : ℕ), Q (E (n : AddMonoidAlgebra ℕ ℕ))


set_option trace.profiler true
--set_option trace.Meta.synthInstance true
--set_option trace.Meta.isDefEq true

set_option maxHeartbeats 0 in
structure mystery_timeout := --37s
(n : ℕ)
(x : (Q (E (n : AddMonoidAlgebra ℕ ℕ))))

set_option maxHeartbeats 0 in
set_option genInjectivity false in
structure mystery_timeout' := -- 0.8s
(n : ℕ)
(x : (Q (E (n : AddMonoidAlgebra ℕ ℕ))))

From 37 seconds to 0,8!

[Riccardo Brasca]

Is there a similar option in Lean3?

[Sebastian Ullrich]

I don't think so from a quick glance

[Riccardo Brasca]

This may be relevant or not, but in #19178 I replaced (because of this timeout)

structure primitive_add_char (R : Type u) [comm_ring R] [fintype R] (R' : Type v) [field R'] :=
(n : ℕ+)
(char : add_char R (cyclotomic_field n R'))
(prim : is_primitive char)

with

def primitive_add_char (R : Type u) [comm_ring R] [fintype R] (R' : Type v) [field R'] :=
Σ (n : ℕ+), (Σ' (char : add_char R (cyclotomic_field n R')), is_primitive char)

I also wanted to have the projections, so I added

def primitive_add_char.n {R : Type u} [comm_ring R] [fintype R] {R' : Type v}
  [field R'] : primitive_add_char R R' → ℕ+ := λ χ, χ.1

(and similarly for the others). Now, this timeouts! But adding noncomputable! fixes everything. If I only add noncomputable, Lean says

unexpected 'noncomputable' modifier, definition 'primitive_add_char.n' is computable

Can this be one of the problems? Lean somehow tries to make the projection computable, but times out.

[Kevin Buzzard]

Yes, this (random timeouts in algebra being fixed by noncomputable!) is not uncommon in some parts of the lean 3 library. Probably you can just search for noncomputable! to get a feeling for where it's used.

[Mario Carneiro]

noncomputable! is just spelled noncomputable now

[Riccardo Brasca]

My code was in Lean3.

[Sebastien Gouezel]

Sebastian Ullrich said:

Judging from the shape of the unification problem, this is likely in automatic generation of injectivity theorems, which can be disabled with the option genInjectivity

Is there a way to disable this option globally and see if it breaks anything in mathlib/see if there is a significant timing difference?

[Eric Wieser]

This will surely break things in mathlib, as we use things like prod.mk.inj_iff at least 100 times

[Sebastien Gouezel]

Sure, I meant we could opt in instead of opt out for cases where we use it.

[Eric Wieser]

Can we fix the generator to not need to solve such hard elaboration problems?

[Eric Wieser]

This seems to work:

set_option genInjectivity false in
structure mystery_timeout :=
(n : ℕ)
(x : (Q (E (n : AddMonoidAlgebra ℕ ℕ))))

lemma mystery_timeout.inj {a b : mystery_timeout} : a = b ↔ a.n = b.n ∧ HEq a.x b.x := by
    cases a
    cases b
    constructor
    ·   intro h
        exact ⟨congr_arg mystery_timeout.n h, congr_arg_heq mystery_timeout.x h⟩
    ·   rintro ⟨rfl, h⟩
        congr
        exact eq_of_heq h

[Eric Wieser]

(Also @Jon Eugster, can we change the web editor to use 2-space indentation?)

[Jon Eugster]

We'll do that later today:+1:

[Eric Wieser]

Even computing the type of the injectivity lemma takes rather a long time:

open private mkInjectiveEqTheorem in Lean.Meta.mkInjectiveTheorems
open private mkInjectiveEqTheoremType? in mkInjectiveEqTheorem

set_option trace.debug true in
-- set_option profiler true in
#eval (show Lean.MetaM _ from do
    let info ← Lean.getConstInfoCtor `mystery_timeout.mk
    let (some x) ← mkInjectiveEqTheoremType? info | failure
    trace[debug] "{x}")

[Sebastian Ullrich]

Eric Wieser said:

This seems to work:

lemma mystery_timeout.inj {a b : mystery_timeout} : a = b ↔ a.n = b.n ∧ HEq a.x b.x := by

Note that it gets slow again if you "accidentally" use a.x = b.x. The slow defeq problem is from the injEq generator deciding whether to use Eq or HEq.

[Eric Wieser]

Does the naive "x depends on n so should be HEq" algorithm not work?

[Eric Rodriguez]

I guess in some usecases the types may actually be defeq anyways

[Eric Rodriguez]

But in those cases I guess the lemmas could be generated manually

[Eric Wieser]

IMO emitting HEq even if things are defeq "by accident" is a feature

[Eric Wieser]

For instance, I don't agree with

import analysis.normed_space.pi_Lp

structure why :=
(p : ennreal)
(f : pi_Lp p (λ _ : fin 3, ℝ))

#check @why.mk.inj_eq
/-
why.mk.inj_eq :
  ∀ {p : ennreal} {f : pi_Lp p (λ (_x : fin 3), ℝ)} {p_1 : ennreal} {f_1 : pi_Lp p_1 (λ (_x : fin 3), ℝ)},
    {p := p, f := f} = {p := p_1, f := f_1} = (p = p_1 ∧ f = f_1)
-/

[Eric Wieser]

If you've made the effort of creating a type synonym, structure shouldn't be unfolding it

[Eric Wieser]

Lean 4 does the same thing:

import Mathlib.Analysis.NormedSpace.PiLp

structure why :=
(p : ENNReal)
(f : PiLp p (fun _ : Fin 3 => ℝ))

#check why.mk.injEq

[Eric Wieser]

lean#812 attempts to change this in Lean 3

[Eric Wieser]

In the end, I used the easier-to-implement algorithm of "defeq but only unfold reducible". @Sebastian Ullrich, do you think this is a reasonable change for Lean4 too?

[Sebastian Ullrich]

It might be. I don't have a good guideline for when it is appropriate and when not

[Eric Wieser]

IMO we should merge leanprover-community/lean#812; that will mean we can keep our structures in lean 3, and use set_option genInjectivity false when we port them to Lean 4. We can always evaluate porting leanprover-community/lean#812 to Lean4 at a later date; the genInjectivity option makes it non-urgent.

[Scott Morrison]

I agree, and am happy to merge, but will wait a moment longer in case anyone wants to call a hold!

[Eric Wieser]

:ping_pong: