performance of equality with projections/mutual

Stream: lean4

[Sébastien Michelland]

@Leonardo de Moura Unfortunately, while the fix above kept me going for a while, I feel that I am again blocked by this issue. I have medium-complexity proofs where every step takes 5-10 seconds, and on the larger half of my theorems the memory usage prevents completing the definition, requiring workarounds with lemmas.

I'd like to better understand what's happening. The main components seem to be a projection and mutually-recursive types. Could you maybe explain what part of the equality check is expensive in this situation, to see if can avoid it?

Mutual definitions are clearly a recurring theme in my inquiries. You've mentioned before that the current well-founded encoding will eventually be replaced by a recursor-based one, which I understand is neither coming just yet nor something I can tackle on my own. Would using the recursors for such definitions bypass the performance issue? If so, I could try to implement it for my specific structure then hide it behind some elaboration magic.

For the sake of a complete "bug report", here is a slight variation of the MWE from above, where the projection is created by a typeclass method call rather than a pair; this example still fails as of leanprover/lean4:nightly-2022-07-13, using more time and memory as the strings get longer.

mutual
inductive Op where
  | mk: String → Block → Op

inductive Assign where
  | mk : String → Op → Assign

inductive Block where
  | mk: Assign → Block
  | empty: Block
end

mutual
def runOp: Op → Nat
  | .mk _ v => let _ := runBlock v; 0

def runAssign: Assign → Nat
  | .mk _ t => runOp t

def runBlock: Block → Nat
  | .mk u => runAssign u
  | .empty => 0
end

class Run (α: Type) where
  run: α → Nat
instance: Run Assign := ⟨runAssign⟩

def x: Assign := .mk "PrettyLong" <| .mk "PrettyLong" .empty
-- (warning: high memory usage)
theorem equivalent: Run.run x = Run.run x := by simp [Run.run]

[Leonardo de Moura]

I am working on slides today and traveling tomorrow :sweat_smile:
I think I will have time to take a look during the weekend.

[Sébastien Michelland]

@Leonardo de Moura I hope the workshop is going well. In the meantime, I tried but mostly failed to understand the performance issue. Nonetheless, I was able to confirm that a fairy simple recursor-based encoding of the mutual type eliminates the problem:

inductive ProgramType := | Op | Assign | Block

section
set_option hygiene false
notation "Op"     => Program ProgramType.Op
notation "Assign" => Program ProgramType.Assign
notation "Block"  => Program ProgramType.Block
end

inductive Program: (type: ProgramType) → Type :=
  | mkOp: String → Block → Op
  | mkAssign: String → Op → Assign
  | mkBlock: Assign → Block
  | emptyBlock: Block

def runBase: Program type → Nat
  | .mkOp _ v => let _ := runBase v; 0
  | .mkAssign _ t => runBase t
  | .mkBlock u => runBase u
  | .emptyBlock => 0

class Run (α: Type) where
  run: α → Nat
instance: Run Assign := ⟨runBase⟩

def x: Assign := .mkAssign "PrettyLong" <| .mkOp "PrettyLong" .emptyBlock
-- Now runs fine
theorem equivalent: Run.run x = Run.run x := by simp [Run.run]

I'm not sure that would generalize, but it feels like a good starting point.

[Leonardo de Moura]

@Sébastien Michelland I didn't have time to look into this issue yet. I will do it as soon as I get back to Redmond.

[Sébastien Michelland]

Thank you very much. I will just log my findings here in case it helps finding the cause of the problem.

I generalized the non-mutual inductive from above and observed the problem again. I reduced again to the following truly MWE which uses a single nested inductive and no mutuals. I'm not sure if it makes a ton of difference for the compiler, but at least it rules out most hacks/workarounds on my end since I can get rid of mutual but definitely not of nesting.

inductive T: Type :=
  | mk: String → Option T → T

def runT: T → Nat
  | .mk _ none => 0
  | .mk _ (some t) => runT t

class Run (α: Type) where
  run: α → Nat
instance: Run T := ⟨runT⟩

def x := T.mk "PrettyLong" (some <| .mk "PrettyLong" none)
-- (warning: high memory usage)
theorem equivalent: Run.run x = Run.run x := by simp [Run.run]

[Leonardo de Moura]

Pushed a fix for this issue: https://github.com/leanprover/lean4/commit/2196a3518e131455cfeda715df7737778ffecea1

[Sébastien Michelland]

Thank you very much @Leonardo de Moura. I did quite a lot on testing in our project and I haven't seen the slightest problem with this fix. With some improvements in our choice of tactics, the proofs are now about 10x faster with no needs for performance workarounds. That's a fix and a half :big_smile: