Zulip Chat Archive

Stream: lean4

Topic: performance of equality with projections/mutual


Sébastien Michelland (Jul 13 2022 at 21:35):

@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 (Jul 13 2022 at 22:38):

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 (Jul 20 2022 at 11:35):

@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 (Jul 20 2022 at 11:37):

@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 (Jul 20 2022 at 21:59):

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 (Jul 24 2022 at 18:49):

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

Sébastien Michelland (Jul 25 2022 at 20:39):

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:


Last updated: Dec 20 2023 at 11:08 UTC