Deterministic Timeout

Stream: new members

[Newell Jensen]

I am running into a timeout and not sure why? I am also passing as many implicit arguments that I can see to equivCoxeterGroup and the calls within equivCoxeterGroup_apply_of to try and help Lean but this doesn't help.

Below is a mwe snippet from #8223

import Mathlib.GroupTheory.PresentedGroup
import Mathlib.LinearAlgebra.Matrix.Symmetric


universe u

noncomputable section

variable {B : Type*} [DecidableEq B]

variable (M : Matrix B B ℕ)

namespace CoxeterGroup

namespace Relations

def ofMatrix : B × B → FreeGroup B :=
 Function.uncurry fun i j => (FreeGroup.of i * FreeGroup.of j) ^ M i j

def toSet : Set (FreeGroup B) :=
  Set.range <| ofMatrix M

end Relations

end CoxeterGroup

def Matrix.CoxeterGroup := PresentedGroup <| CoxeterGroup.Relations.toSet M

instance : Group (Matrix.CoxeterGroup M) := by
  exact QuotientGroup.Quotient.group _

namespace CoxeterGroup

def of (b : B) : Matrix.CoxeterGroup M := by
  unfold Matrix.CoxeterGroup
  exact PresentedGroup.of b

end CoxeterGroup

namespace CoxeterSystem

open Matrix

variable {B B' W H : Type*} [Group W] [Group H]

variable {M : Matrix B B ℕ}

@[simp]
lemma map_relations_eq_reindex_relations (e : B ≃ B') :
    (FreeGroup.freeGroupCongr e) '' CoxeterGroup.Relations.toSet M =
    CoxeterGroup.Relations.toSet (reindex e e M) := by
  simp [CoxeterGroup.Relations.toSet, CoxeterGroup.Relations.ofMatrix]
  apply le_antisymm
  · rw [Set.le_iff_subset]; intro _
    simp only [Set.mem_image, Set.mem_range, Prod.exists, Function.uncurry_apply_pair,
      forall_exists_index, and_imp]
    intro _ hb b _ heq; rw [← heq]
    use (e hb); use (e b); aesop
  · rw [Set.le_iff_subset]; intro hb'
    simp only [Set.mem_range, Prod.exists, Function.uncurry_apply_pair, Set.mem_image,
      forall_exists_index]
    intro b1' b2' heq; rw [← heq]
    use ((FreeGroup.freeGroupCongr e).symm hb')
    exact ⟨by use (e.symm b1'); use (e.symm b2'); aesop, by aesop⟩

def equivCoxeterGroup (e : B ≃ B') : CoxeterGroup M ≃* CoxeterGroup (reindex e e M) := by
  simp only [CoxeterGroup]
  have := PresentedGroup.equivPresentedGroup (α := B) (β := B') (CoxeterGroup.Relations.toSet M) e
  rwa [@map_relations_eq_reindex_relations B B' M e] at this

set_option trace.Kernel true
set_option profiler true
-- set_option maxHeartbeats 0 in
theorem equivCoxeterGroup_apply_of (b : B) (M : Matrix B B ℕ) (e : B ≃ B') :
    (equivCoxeterGroup (B := B) (B' := B') (M := M) e) (CoxeterGroup.of (B := B) M b) =
    CoxeterGroup.of (B := B') (reindex e e M) (e b) :=
  -- by unfold equivCoxeterGroup -- This just runs away!!
  rfl -- (deterministic) timeout at 'isDefEq', maximum number of heartbeats (200000) has
      -- been reached (use 'set_option maxHeartbeats <num>' to set the limit)

end CoxeterSystem

Maybe @Kyle Miller has an idea as this is just building upon #9403 ? Maybe it is related to https://github.com/leanprover-community/mathlib4/pull/9403#discussion_r1451890220 on some level?

[Newell Jensen]

Am I asking a stupid question that has an obvious answer or does really no one have any idea about this (based on the fact that it is has been about a day since posting and no responses)?

How does one troubleshoot a deterministic timeout like this? Am I doing something obviously wrong?

[Kevin Buzzard]

Debugging timeouts can be hard, and it's the weekend, when things are typically a little less fast-paced around here.

[Kevin Buzzard]

Did you try bumping up the heartbeats?

[Newell Jensen]

Yes I tried bumping up the maxHeartbeats using 0 (no limit) to no avail.

I have hit these timeouts before (as most people here probably have) and I am unsure of how to troubleshoot them other than trying to help with the implicit arguments.

Are there any other tricks one can use to try and make this work?

[Kyle Miller]

I see you defined equivCoxeterGroup using a tactic proof. Generally, it's better to write a term for definitions, restricting any tactics to proofs in sub-terms. Maybe the tactic proof is generating a term that's no good for unfolding or rfl.

[Newell Jensen]

Ah okay. I will try and see if I can find a term proof.

[Newell Jensen]

Do you know if there is a way to unfold definitions in a term proof?

[Newell Jensen]

I suppose instead of a tactic proof using where would get me there (not using tactics for the individual parts as well).

[Kyle Miller]

Do you need to unfold the definition? It would really be best if you could avoid rewriting.

[Newell Jensen]

Why would it be best to avoid this?

[Kyle Miller]

You could try doing #print equivCoxeterGroup to see what kinds of terms rewriting produces.

[Newell Jensen]

def CoxeterSystem.equivCoxeterGroup.{u_3, u_2} : {B : Type u_2} →
  {B' : Type u_3} → {M : Matrix B B ℕ} → (e : B ≃ B') → CoxeterGroup M ≃* CoxeterGroup ((reindex e e) M) :=
fun {B} {B'} {M} e ↦
  id
    (let_fun this := PresentedGroup.equivPresentedGroup (CoxeterGroup.Relations.toSet M) e;
    Eq.mp _ this)

I don't really know how to tell whether something above is generating a term that isn't good for unfolding or rfl except for maybe the underscores?

[Kevin Buzzard]

Newell Jensen said:

Why would it be best to avoid this?

Because the rw tactic generates weird terms, on the basis that it will only be used in proofs so it doesn't matter

[Kevin Buzzard]

Newell Jensen said:

Do you know if there is a way to unfold definitions in a term proof?

Term proofs see through definitions so you don't need to unfold them

[Kevin Buzzard]

For example in your definition of of what happens if you just delete by, the unfold line and exact?

[Kevin Buzzard]

docs#Eq.mp

[Kyle Miller]

Something bad in particular about rewriting is that it involves changing the types of terms. That's what Eq.mp is does. (In particular, in tends to obstruct things, like Kevin mentions below.)

[Kevin Buzzard]

That function is using Eq.rec under the hood, which is an axiom which doesn't unfold. To define an equiv you should, if at all possible, write down the maps explicitly in term mode, and just use stuff like rw for the proof fields

[Newell Jensen]

Thanks for the suggestions @Kyle Miller @Kevin Buzzard . Taking the suggestion for using rw in the proof fields I was able to get the below to compile. Now, this doesn't build upon equivPresentedGroup but it does build on the underlying QuotientGroup.congr, which seems reasonable.

import Mathlib.GroupTheory.PresentedGroup
import Mathlib.LinearAlgebra.Matrix.Symmetric


universe u

noncomputable section

variable {B : Type*} [DecidableEq B]

variable (M : Matrix B B ℕ)

namespace CoxeterGroup

namespace Relations

def ofMatrix : B × B → FreeGroup B :=
 Function.uncurry fun i j => (FreeGroup.of i * FreeGroup.of j) ^ M i j

def toSet : Set (FreeGroup B) :=
  Set.range <| ofMatrix M

end Relations

end CoxeterGroup

def Matrix.CoxeterGroup := PresentedGroup <| CoxeterGroup.Relations.toSet M

instance : Group (Matrix.CoxeterGroup M) := by
  exact QuotientGroup.Quotient.group _

namespace CoxeterGroup

def of (b : B) : Matrix.CoxeterGroup M := PresentedGroup.of b

end CoxeterGroup

namespace CoxeterSystem

open Matrix

variable {B B' W H : Type*} [Group W] [Group H]

variable {M : Matrix B B ℕ}

@[simp]
lemma map_relations_eq_reindex_relations (e : B ≃ B') :
    (MulEquiv.toMonoidHom (FreeGroup.freeGroupCongr e)) '' CoxeterGroup.Relations.toSet M =
    CoxeterGroup.Relations.toSet (reindex e e M) := by
  simp [CoxeterGroup.Relations.toSet, CoxeterGroup.Relations.ofMatrix]
  apply le_antisymm
  · rw [Set.le_iff_subset]; intro _
    simp only [Set.mem_image, Set.mem_range, Prod.exists, Function.uncurry_apply_pair,
      forall_exists_index, and_imp]
    intro _ hb b _ heq; rw [← heq]
    use (e hb); use (e b); aesop
  · rw [Set.le_iff_subset]; intro hb'
    simp only [Set.mem_range, Prod.exists, Function.uncurry_apply_pair, Set.mem_image,
      forall_exists_index]
    intro b1' b2' heq; rw [← heq]
    use ((FreeGroup.freeGroupCongr e).symm hb')
    exact ⟨by use (e.symm b1'); use (e.symm b2'); aesop, by aesop⟩

def equivCoxeterGroup (e : B ≃ B') : CoxeterGroup M ≃* CoxeterGroup (reindex e e M) :=
  QuotientGroup.congr (Subgroup.normalClosure (CoxeterGroup.Relations.toSet M))
    (Subgroup.normalClosure (CoxeterGroup.Relations.toSet (reindex e e M)))
    (FreeGroup.freeGroupCongr e) (by
      have := Subgroup.map_normalClosure (CoxeterGroup.Relations.toSet M)
        (FreeGroup.freeGroupCongr e).toMonoidHom (FreeGroup.freeGroupCongr e).surjective
      rwa [@map_relations_eq_reindex_relations B B' M e] at this)

theorem equivCoxeterGroup_apply_of (b : B) (M : Matrix B B ℕ) (e : B ≃ B') :
    (equivCoxeterGroup (M := M) e) (CoxeterGroup.of M b) = CoxeterGroup.of (reindex e e M) (e b) :=
  rfl

end CoxeterSystem