From 49a87ceb4d3fd8ac77f364019fac1951ef79ba69 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 28 Jul 2021 16:18:55 -0700 Subject: [PATCH] feat: add basic `isDefEq` cache --- src/Lean/Meta/Basic.lean | 9 +- src/Lean/Meta/ExprDefEq.lean | 76 +++++++++--- tests/lean/infoTree.lean.expected.out | 40 +++--- tests/lean/run/tryHeuristicPerfIssue.lean | 2 - tests/lean/run/tryHeuristicPerfIssue2.lean | 134 +++++++++++++++++++++ 5 files changed, 223 insertions(+), 38 deletions(-) create mode 100644 tests/lean/run/tryHeuristicPerfIssue2.lean diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 5305ea0ad3..fb46c1cf98 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -98,12 +98,19 @@ abbrev SynthInstanceCache := PersistentHashMap Expr (Option Expr) abbrev InferTypeCache := PersistentExprStructMap Expr abbrev FunInfoCache := PersistentHashMap InfoCacheKey FunInfo abbrev WhnfCache := PersistentExprStructMap Expr + +/- A set of pairs. TODO: consider more efficient representations (e.g., a proper set) and caching policies (e.g., imperfect cache). + We should also investigate the impact on memory consumption. -/ +abbrev DefEqCache := PersistentHashMap (Expr × Expr) Unit + structure Cache where inferType : InferTypeCache := {} funInfo : FunInfoCache := {} synthInstance : SynthInstanceCache := {} whnfDefault : WhnfCache := {} -- cache for closed terms and `TransparencyMode.default` whnfAll : WhnfCache := {} -- cache for closed terms and `TransparencyMode.all` + defEqDefault : DefEqCache := {} + defEqAll : DefEqCache := {} deriving Inhabited /-- @@ -218,7 +225,7 @@ variable [MonadControlT MetaM n] [Monad n] modify fun ⟨mctx, cache, zetaFVarIds, postponed⟩ => ⟨mctx, f cache, zetaFVarIds, postponed⟩ @[inline] def modifyInferTypeCache (f : InferTypeCache → InferTypeCache) : MetaM Unit := - modifyCache fun ⟨ic, c1, c2, c3, c4⟩ => ⟨f ic, c1, c2, c3, c4⟩ + modifyCache fun ⟨ic, c1, c2, c3, c4, c5, c6⟩ => ⟨f ic, c1, c2, c3, c4, c5, c6⟩ def getLocalInstances : MetaM LocalInstances := return (← read).localInstances diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index 7d2d4f724d..ba959017c5 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/src/Lean/Meta/ExprDefEq.lean @@ -999,8 +999,6 @@ private def tryHeuristic (t s : Expr) : MetaM Bool := do when `t` and `s` do not have metavariables, are not structurally equal, and `f` is an abbreviation. On the other hand, by unfolding `f`, we often produce smaller terms. -/ unless info.hints.isRegular do - t ← instantiateMVars t - s ← instantiateMVars s unless t.hasExprMVar || s.hasExprMVar do return false traceCtx `Meta.isDefEq.delta do @@ -1405,6 +1403,43 @@ private def isDefEqApp (t s : Expr) : MetaM Bool := do else isDefEqOnFailure t s +private def isExprDefEqExpensive (t : Expr) (s : Expr) : MetaM Bool := do + if (← (isDefEqEta t s <||> isDefEqEta s t)) then pure true else + if (← isDefEqProj t s) then pure true else + whenUndefDo (isDefEqNative t s) do + whenUndefDo (isDefEqNat t s) do + whenUndefDo (isDefEqOffset t s) do + whenUndefDo (isDefEqDelta t s) do + if t.isConst && s.isConst then + if t.constName! == s.constName! then isListLevelDefEqAux t.constLevels! s.constLevels! else pure false + else if t.isApp && s.isApp then + isDefEqApp t s + else + whenUndefDo (isDefEqStringLit t s) do + isDefEqOnFailure t s + +-- We only check DefEq cache for default and all transparency modes +private def skipDefEqCache : MetaM Bool := do + match (← getConfig).transparency with + | TransparencyMode.default => return false + | TransparencyMode.all => return false + | _ => return true + +private def mkCacheKey (t : Expr) (s : Expr) : Expr × Expr := + if Expr.quickLt t s then (t, s) else (s, t) + +private def isCached (key : Expr × Expr) : MetaM Bool := do + match (← getConfig).transparency with + | TransparencyMode.default => return (← get).cache.defEqDefault.contains key + | TransparencyMode.all => return (← get).cache.defEqAll.contains key + | _ => return false + +private def cacheResult (key : Expr × Expr) : MetaM Unit := do + match (← getConfig).transparency with + | TransparencyMode.default => modify fun s => { s with cache.defEqDefault := s.cache.defEqDefault.insert key () } + | TransparencyMode.all => modify fun s => { s with cache.defEqAll := s.cache.defEqAll.insert key () } + | _ => pure () + partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := do trace[Meta.isDefEq.step] "{t} =?= {s}" checkMaxHeartbeats "isDefEq" @@ -1415,20 +1450,31 @@ partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := do let s' ← whnfCore s if t != t' || s != s' then isExprDefEqAuxImpl t' s' - else do - if (← (isDefEqEta t s <||> isDefEqEta s t)) then pure true else - if (← isDefEqProj t s) then pure true else - whenUndefDo (isDefEqNative t s) do - whenUndefDo (isDefEqNat t s) do - whenUndefDo (isDefEqOffset t s) do - whenUndefDo (isDefEqDelta t s) do - if t.isConst && s.isConst then - if t.constName! == s.constName! then isListLevelDefEqAux t.constLevels! s.constLevels! else pure false - else if t.isApp && s.isApp then - isDefEqApp t s + else if (← skipDefEqCache) then + isExprDefEqExpensive t s + else + /- + TODO: check whether the following `instantiateMVar`s are expensive or not in practice. + Lean 3 does not use them, and may miss caching opportunities since it is not safe to cache when `t` and `s` may contain mvars. + The unit test `tryHeuristicPerfIssue2.lean` cannot be solved without these two `instantiateMVar`s. + If it becomes a problem, we may use store a flag in the context indicating whether we have already used `instantiateMVar` in + outer invocations or not. It is not perfect (we may assign mvars in nested calls), but it should work well enough in practice, + and prevent repeated traversals in nested calls. + -/ + let t ← instantiateMVars t + let s ← instantiateMVars s + if t.hasMVar || s.hasMVar then + -- It is not safe to use DefEq cache if terms contain metavariables + isExprDefEqExpensive t s else - whenUndefDo (isDefEqStringLit t s) do - isDefEqOnFailure t s + let k := mkCacheKey t s + if (← isCached k) then + return true + else if (← isExprDefEqExpensive t s) then + cacheResult k + return true + else + return false builtin_initialize isExprDefEqAuxRef.set isExprDefEqAuxImpl diff --git a/tests/lean/infoTree.lean.expected.out b/tests/lean/infoTree.lean.expected.out index 0c3845e526..7df6659f5c 100644 --- a/tests/lean/infoTree.lean.expected.out +++ b/tests/lean/infoTree.lean.expected.out @@ -1,6 +1,6 @@ [Elab.info] command @ ⟨13, 0⟩-⟨15, 6⟩ @ Lean.Elab.Command.elabDeclaration Nat : Type @ ⟨13, 11⟩-⟨13, 14⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.534} @ ⟨13, 11⟩-⟨13, 14⟩ + [.] `Nat : some Sort.{?_uniq.535} @ ⟨13, 11⟩-⟨13, 14⟩ Nat : Type @ ⟨13, 11⟩-⟨13, 14⟩ x : Nat @ ⟨13, 7⟩-⟨13, 8⟩ Nat × Nat : Type @ ⟨13, 18⟩-⟨13, 27⟩ @ myMacro._@.Init.Notation._hyg.2258 @@ -11,10 +11,10 @@ Nat × Nat : Type @ ⟨13, 18⟩†-⟨13, 27⟩ @ Lean.Elab.Term.elabApp Prod : Type → Type → Type @ ⟨13, 18⟩†-⟨13, 27⟩† Nat : Type @ ⟨13, 18⟩-⟨13, 21⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Type.{?_uniq.538} @ ⟨13, 18⟩-⟨13, 21⟩ + [.] `Nat : some Type.{?_uniq.539} @ ⟨13, 18⟩-⟨13, 21⟩ Nat : Type @ ⟨13, 18⟩-⟨13, 21⟩ Nat : Type @ ⟨13, 24⟩-⟨13, 27⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Type.{?_uniq.537} @ ⟨13, 24⟩-⟨13, 27⟩ + [.] `Nat : some Type.{?_uniq.538} @ ⟨13, 24⟩-⟨13, 27⟩ Nat : Type @ ⟨13, 24⟩-⟨13, 27⟩ let y : Nat × Nat := (x, x); id y : Nat × Nat @ ⟨14, 2⟩-⟨15, 6⟩ @ Lean.Elab.Term.elabLetDecl @@ -39,16 +39,16 @@ [Elab.info] command @ ⟨17, 0⟩-⟨19, 8⟩ @ Lean.Elab.Command.elabDeclaration ∀ (x y : Nat), Bool → x + 0 = x : Prop @ ⟨17, 8⟩-⟨17, 44⟩ @ Lean.Elab.Term.elabDepArrow Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.567} @ ⟨17, 15⟩-⟨17, 18⟩ + [.] `Nat : some Sort.{?_uniq.566} @ ⟨17, 15⟩-⟨17, 18⟩ Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩ x : Nat @ ⟨17, 9⟩-⟨17, 10⟩ Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.569} @ ⟨17, 15⟩-⟨17, 18⟩ + [.] `Nat : some Sort.{?_uniq.568} @ ⟨17, 15⟩-⟨17, 18⟩ Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩ y : Nat @ ⟨17, 11⟩-⟨17, 12⟩ Bool → x + 0 = x : Prop @ ⟨17, 22⟩-⟨17, 44⟩ @ Lean.Elab.Term.elabDepArrow Bool : Type @ ⟨17, 27⟩-⟨17, 31⟩ @ Lean.Elab.Term.elabIdent - [.] `Bool : some Sort.{?_uniq.572} @ ⟨17, 27⟩-⟨17, 31⟩ + [.] `Bool : some Sort.{?_uniq.571} @ ⟨17, 27⟩-⟨17, 31⟩ Bool : Type @ ⟨17, 27⟩-⟨17, 31⟩ b : Bool @ ⟨17, 23⟩-⟨17, 24⟩ x + 0 = x : Prop @ ⟨17, 35⟩-⟨17, 44⟩ @ myMacro._@.Init.Notation._hyg.9563 @@ -115,20 +115,20 @@ [Elab.info] command @ ⟨21, 0⟩-⟨25, 10⟩ @ Lean.Elab.Command.elabDeclaration Nat → Nat → Bool → Nat : Type @ ⟨21, 9⟩-⟨21, 39⟩ @ Lean.Elab.Term.elabDepArrow Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.880} @ ⟨21, 16⟩-⟨21, 19⟩ + [.] `Nat : some Sort.{?_uniq.865} @ ⟨21, 16⟩-⟨21, 19⟩ Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩ x : Nat @ ⟨21, 10⟩-⟨21, 11⟩ Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.882} @ ⟨21, 16⟩-⟨21, 19⟩ + [.] `Nat : some Sort.{?_uniq.867} @ ⟨21, 16⟩-⟨21, 19⟩ Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩ y : Nat @ ⟨21, 12⟩-⟨21, 13⟩ Bool → Nat : Type @ ⟨21, 23⟩-⟨21, 39⟩ @ Lean.Elab.Term.elabDepArrow Bool : Type @ ⟨21, 28⟩-⟨21, 32⟩ @ Lean.Elab.Term.elabIdent - [.] `Bool : some Sort.{?_uniq.885} @ ⟨21, 28⟩-⟨21, 32⟩ + [.] `Bool : some Sort.{?_uniq.870} @ ⟨21, 28⟩-⟨21, 32⟩ Bool : Type @ ⟨21, 28⟩-⟨21, 32⟩ b : Bool @ ⟨21, 24⟩-⟨21, 25⟩ Nat : Type @ ⟨21, 36⟩-⟨21, 39⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.887} @ ⟨21, 36⟩-⟨21, 39⟩ + [.] `Nat : some Sort.{?_uniq.872} @ ⟨21, 36⟩-⟨21, 39⟩ Nat : Type @ ⟨21, 36⟩-⟨21, 39⟩ fun (x y : Nat) (b : Bool) => let x : Nat × Nat := (x + y, x - y); @@ -239,10 +239,10 @@ Nat × Array (Array Nat) : Type @ ⟨27, 12⟩†-⟨27, 35⟩ @ Lean.Elab.Term.elabApp Prod : Type → Type → Type @ ⟨27, 12⟩†-⟨27, 35⟩† Nat : Type @ ⟨27, 12⟩-⟨27, 15⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Type.{?_uniq.1890} @ ⟨27, 12⟩-⟨27, 15⟩ + [.] `Nat : some Type.{?_uniq.1827} @ ⟨27, 12⟩-⟨27, 15⟩ Nat : Type @ ⟨27, 12⟩-⟨27, 15⟩ Array (Array Nat) : Type @ ⟨27, 18⟩-⟨27, 35⟩ @ Lean.Elab.Term.elabApp - [.] `Array : some Type.{?_uniq.1889} @ ⟨27, 18⟩-⟨27, 23⟩ + [.] `Array : some Type.{?_uniq.1826} @ ⟨27, 18⟩-⟨27, 23⟩ Array : Type → Type @ ⟨27, 18⟩-⟨27, 23⟩ Array Nat : Type @ ⟨27, 24⟩-⟨27, 35⟩ @ Lean.Elab.Term.expandParen Macro expansion @@ -250,17 +250,17 @@ ===> Array Nat Array Nat : Type @ ⟨27, 25⟩-⟨27, 34⟩ @ Lean.Elab.Term.elabApp - [.] `Array : some Type.{?_uniq.1891} @ ⟨27, 25⟩-⟨27, 30⟩ + [.] `Array : some Type.{?_uniq.1828} @ ⟨27, 25⟩-⟨27, 30⟩ Array : Type → Type @ ⟨27, 25⟩-⟨27, 30⟩ Nat : Type @ ⟨27, 31⟩-⟨27, 34⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Type.{?_uniq.1892} @ ⟨27, 31⟩-⟨27, 34⟩ + [.] `Nat : some Type.{?_uniq.1829} @ ⟨27, 31⟩-⟨27, 34⟩ Nat : Type @ ⟨27, 31⟩-⟨27, 34⟩ s : Nat × Array (Array Nat) @ ⟨27, 8⟩-⟨27, 9⟩ Array Nat : Type @ ⟨27, 39⟩-⟨27, 48⟩ @ Lean.Elab.Term.elabApp - [.] `Array : some Sort.{?_uniq.1894} @ ⟨27, 39⟩-⟨27, 44⟩ + [.] `Array : some Sort.{?_uniq.1831} @ ⟨27, 39⟩-⟨27, 44⟩ Array : Type → Type @ ⟨27, 39⟩-⟨27, 44⟩ Nat : Type @ ⟨27, 45⟩-⟨27, 48⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Type.{?_uniq.1895} @ ⟨27, 45⟩-⟨27, 48⟩ + [.] `Nat : some Type.{?_uniq.1832} @ ⟨27, 45⟩-⟨27, 48⟩ Nat : Type @ ⟨27, 45⟩-⟨27, 48⟩ Array.push (Array.getOp s.snd 1) s.fst : Array Nat @ ⟨28, 2⟩-⟨28, 17⟩ @ Lean.Elab.Term.elabApp s : Nat × Array (Array Nat) @ ⟨28, 2⟩-⟨28, 3⟩ @@ -274,11 +274,11 @@ Prod.fst : {α β : Type} → α × β → α @ ⟨28, 16⟩-⟨28, 17⟩ [Elab.info] command @ ⟨30, 0⟩-⟨31, 20⟩ @ Lean.Elab.Command.elabDeclaration B : Type @ ⟨30, 14⟩-⟨30, 15⟩ @ Lean.Elab.Term.elabIdent - [.] `B : some Sort.{?_uniq.1936} @ ⟨30, 14⟩-⟨30, 15⟩ + [.] `B : some Sort.{?_uniq.1872} @ ⟨30, 14⟩-⟨30, 15⟩ B : Type @ ⟨30, 14⟩-⟨30, 15⟩ arg : B @ ⟨30, 8⟩-⟨30, 11⟩ Nat : Type @ ⟨30, 19⟩-⟨30, 22⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.1938} @ ⟨30, 19⟩-⟨30, 22⟩ + [.] `Nat : some Sort.{?_uniq.1874} @ ⟨30, 19⟩-⟨30, 22⟩ Nat : Type @ ⟨30, 19⟩-⟨30, 22⟩ A.val arg.pair.fst 0 : Nat @ ⟨31, 2⟩-⟨31, 20⟩ @ Lean.Elab.Term.elabApp arg : B @ ⟨31, 2⟩-⟨31, 5⟩ @@ -291,11 +291,11 @@ 0 : Nat @ ⟨31, 19⟩-⟨31, 20⟩ @ Lean.Elab.Term.elabNumLit [Elab.info] command @ ⟨33, 0⟩-⟨35, 1⟩ @ Lean.Elab.Command.elabDeclaration Nat : Type @ ⟨33, 12⟩-⟨33, 15⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.1958} @ ⟨33, 12⟩-⟨33, 15⟩ + [.] `Nat : some Sort.{?_uniq.1894} @ ⟨33, 12⟩-⟨33, 15⟩ Nat : Type @ ⟨33, 12⟩-⟨33, 15⟩ x : Nat @ ⟨33, 8⟩-⟨33, 9⟩ B : Type @ ⟨33, 19⟩-⟨33, 20⟩ @ Lean.Elab.Term.elabIdent - [.] `B : some Sort.{?_uniq.1960} @ ⟨33, 19⟩-⟨33, 20⟩ + [.] `B : some Sort.{?_uniq.1896} @ ⟨33, 19⟩-⟨33, 20⟩ B : Type @ ⟨33, 19⟩-⟨33, 20⟩ { pair := ({ val := id }, { val := id }) } : B @ ⟨33, 24⟩-⟨35, 1⟩ @ Lean.Elab.Term.StructInst.elabStructInst ({ val := id }, { val := id }) : A × A @ ⟨34, 10⟩-⟨34, 40⟩ @ Lean.Elab.Term.expandParen diff --git a/tests/lean/run/tryHeuristicPerfIssue.lean b/tests/lean/run/tryHeuristicPerfIssue.lean index 11d22c10e4..8f173d566c 100644 --- a/tests/lean/run/tryHeuristicPerfIssue.lean +++ b/tests/lean/run/tryHeuristicPerfIssue.lean @@ -100,8 +100,6 @@ class T1 (α : Type u) where addc8 : ∀ (x y : α), @Add.add α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ (@L7.toL6 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6, addc7⟩))))))) x y = @Add.add α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ (@L7.toL6 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6, addc7⟩))))))) y x addc9 : ∀ (x y : α), @Add.add α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ (@L7.toL6 _ (@L8.toL7 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6, addc7, addc8⟩)))))))) x y = @Add.add α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ (@L7.toL6 _ (@L8.toL7 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6, addc7, addc8⟩)))))))) y x -set_option maxHeartbeats 10000000 - -- slow instance T1.toL9 [inst : T1 α] : L9 α := { inst with } diff --git a/tests/lean/run/tryHeuristicPerfIssue2.lean b/tests/lean/run/tryHeuristicPerfIssue2.lean new file mode 100644 index 0000000000..e02dce2bc0 --- /dev/null +++ b/tests/lean/run/tryHeuristicPerfIssue2.lean @@ -0,0 +1,134 @@ +def myAdd [Add α] (x y : α) := x + y + +class L1 (α : Type u) where + add : α → α → α + addc1 : ∀ (x y : α), @myAdd α ⟨add⟩ x y = @myAdd α ⟨add⟩ y x + +instance L1.toAdd [inst : L1 α] : Add α := { inst with } + +class L2 (α : Type u) where + add : α → α → α + addc1 : ∀ (x y : α), @myAdd α ⟨add⟩ x y = @myAdd α ⟨add⟩ y x + addc2 : ∀ (x y : α), @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) x y = @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) y x + +instance L2.toL1 [inst : L2 α] : L1 α := { inst with } + +class L3 (α : Type u) where + add : α → α → α + addc1 : ∀ (x y : α), @myAdd α ⟨add⟩ x y = @myAdd α ⟨add⟩ y x + addc2 : ∀ (x y : α), @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) x y = @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) y x + addc3 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ ⟨add, addc1, addc2⟩)) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ ⟨add, addc1, addc2⟩)) y x + +instance L3.toL2 [inst : L3 α] : L2 α := { inst with } + +class L4 (α : Type u) where + add : α → α → α + addc1 : ∀ (x y : α), @myAdd α ⟨add⟩ x y = @myAdd α ⟨add⟩ y x + addc2 : ∀ (x y : α), @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) x y = @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) y x + addc3 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ ⟨add, addc1, addc2⟩)) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ ⟨add, addc1, addc2⟩)) y x + addc4 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ ⟨add, addc1, addc2, addc3⟩))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ ⟨add, addc1, addc2, addc3⟩))) y x + +instance L4.toL3 [inst : L4 α] : L3 α := { inst with } + +class L5 (α : Type u) where + add : α → α → α + addc1 : ∀ (x y : α), @myAdd α ⟨add⟩ x y = @myAdd α ⟨add⟩ y x + addc2 : ∀ (x y : α), @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) x y = @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) y x + addc3 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ ⟨add, addc1, addc2⟩)) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ ⟨add, addc1, addc2⟩)) y x + addc4 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ ⟨add, addc1, addc2, addc3⟩))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ ⟨add, addc1, addc2, addc3⟩))) y x + addc5 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ ⟨add, addc1, addc2, addc3, addc4⟩)))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ ⟨add, addc1, addc2, addc3, addc4⟩)))) y x + +instance L5.toL4 [inst : L5 α] : L4 α := { inst with } + +class L6 (α : Type u) where + add : α → α → α + addc1 : ∀ (x y : α), @myAdd α ⟨add⟩ x y = @myAdd α ⟨add⟩ y x + addc2 : ∀ (x y : α), @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) x y = @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) y x + addc3 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ ⟨add, addc1, addc2⟩)) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ ⟨add, addc1, addc2⟩)) y x + addc4 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ ⟨add, addc1, addc2, addc3⟩))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ ⟨add, addc1, addc2, addc3⟩))) y x + addc5 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ ⟨add, addc1, addc2, addc3, addc4⟩)))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ ⟨add, addc1, addc2, addc3, addc4⟩)))) y x + addc6 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ ⟨add, addc1, addc2, addc3, addc4, addc5⟩))))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ ⟨add, addc1, addc2, addc3, addc4, addc5⟩))))) y x + +instance L6.toL5 [inst : L6 α] : L5 α := { inst with } + +class L7 (α : Type u) where + add : α → α → α + addc1 : ∀ (x y : α), @myAdd α ⟨add⟩ x y = @myAdd α ⟨add⟩ y x + addc2 : ∀ (x y : α), @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) x y = @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) y x + addc3 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ ⟨add, addc1, addc2⟩)) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ ⟨add, addc1, addc2⟩)) y x + addc4 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ ⟨add, addc1, addc2, addc3⟩))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ ⟨add, addc1, addc2, addc3⟩))) y x + addc5 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ ⟨add, addc1, addc2, addc3, addc4⟩)))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ ⟨add, addc1, addc2, addc3, addc4⟩)))) y x + addc6 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ ⟨add, addc1, addc2, addc3, addc4, addc5⟩))))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ ⟨add, addc1, addc2, addc3, addc4, addc5⟩))))) y x + addc7 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6⟩)))))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6⟩)))))) y x + +instance L7.toL6 [inst : L7 α] : L6 α := { inst with } + +class L8 (α : Type u) where + add : α → α → α + addc1 : ∀ (x y : α), @myAdd α ⟨add⟩ x y = @myAdd α ⟨add⟩ y x + addc2 : ∀ (x y : α), @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) x y = @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) y x + addc3 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ ⟨add, addc1, addc2⟩)) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ ⟨add, addc1, addc2⟩)) y x + addc4 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ ⟨add, addc1, addc2, addc3⟩))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ ⟨add, addc1, addc2, addc3⟩))) y x + addc5 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ ⟨add, addc1, addc2, addc3, addc4⟩)))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ ⟨add, addc1, addc2, addc3, addc4⟩)))) y x + addc6 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ ⟨add, addc1, addc2, addc3, addc4, addc5⟩))))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ ⟨add, addc1, addc2, addc3, addc4, addc5⟩))))) y x + addc7 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6⟩)))))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6⟩)))))) y x + addc8 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ (@L7.toL6 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6, addc7⟩))))))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ (@L7.toL6 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6, addc7⟩))))))) y x + +instance L8.toL7 [inst : L8 α] : L7 α := { inst with } + +class L9 (α : Type u) where + add : α → α → α + addc1 : ∀ (x y : α), @myAdd α ⟨add⟩ x y = @myAdd α ⟨add⟩ y x + addc2 : ∀ (x y : α), @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) x y = @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) y x + addc3 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ ⟨add, addc1, addc2⟩)) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ ⟨add, addc1, addc2⟩)) y x + addc4 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ ⟨add, addc1, addc2, addc3⟩))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ ⟨add, addc1, addc2, addc3⟩))) y x + addc5 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ ⟨add, addc1, addc2, addc3, addc4⟩)))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ ⟨add, addc1, addc2, addc3, addc4⟩)))) y x + addc6 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ ⟨add, addc1, addc2, addc3, addc4, addc5⟩))))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ ⟨add, addc1, addc2, addc3, addc4, addc5⟩))))) y x + addc7 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6⟩)))))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6⟩)))))) y x + addc8 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ (@L7.toL6 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6, addc7⟩))))))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ (@L7.toL6 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6, addc7⟩))))))) y x + addc9 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ (@L7.toL6 _ (@L8.toL7 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6, addc7, addc8⟩)))))))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ (@L7.toL6 _ (@L8.toL7 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6, addc7, addc8⟩)))))))) y x + +instance L9.toL8 [inst : L9 α] : L8 α := { inst with } + +class T1 (α : Type u) where + add : α → α → α + addc1 : ∀ (x y : α), @myAdd α ⟨add⟩ x y = @myAdd α ⟨add⟩ y x + addc2 : ∀ (x y : α), @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) x y = @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) y x + addc3 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ ⟨add, addc1, addc2⟩)) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ ⟨add, addc1, addc2⟩)) y x + addc4 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ ⟨add, addc1, addc2, addc3⟩))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ ⟨add, addc1, addc2, addc3⟩))) y x + addc5 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ ⟨add, addc1, addc2, addc3, addc4⟩)))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ ⟨add, addc1, addc2, addc3, addc4⟩)))) y x + addc6 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ ⟨add, addc1, addc2, addc3, addc4, addc5⟩))))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ ⟨add, addc1, addc2, addc3, addc4, addc5⟩))))) y x + addc7 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6⟩)))))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6⟩)))))) y x + addc8 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ (@L7.toL6 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6, addc7⟩))))))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ (@L7.toL6 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6, addc7⟩))))))) y x + addc9 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ (@L7.toL6 _ (@L8.toL7 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6, addc7, addc8⟩)))))))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ (@L7.toL6 _ (@L8.toL7 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6, addc7, addc8⟩)))))))) y x + +-- slow +instance T1_toL9 {α : Type u} [inst : T1 α] : L9 α := { inst with } + +class T2 (α : Type u) where + add : α → α → α + addc1 : ∀ (x y : α), @myAdd α ⟨add⟩ x y = @myAdd α ⟨add⟩ y x + addc2 : ∀ (x y : α), @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) x y = @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) y x + addc3 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ ⟨add, addc1, addc2⟩)) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ ⟨add, addc1, addc2⟩)) y x + addc4 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ ⟨add, addc1, addc2, addc3⟩))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ ⟨add, addc1, addc2, addc3⟩))) y x + addc5 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ ⟨add, addc1, addc2, addc3, addc4⟩)))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ ⟨add, addc1, addc2, addc3, addc4⟩)))) y x + addc6 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ ⟨add, addc1, addc2, addc3, addc4, addc5⟩))))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ ⟨add, addc1, addc2, addc3, addc4, addc5⟩))))) y x + addc7 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6⟩)))))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6⟩)))))) y x + addc8 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ (@L7.toL6 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6, addc7⟩))))))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ (@L7.toL6 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6, addc7⟩))))))) y x + addc9 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ (@L7.toL6 _ (@L8.toL7 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6, addc7, addc8⟩)))))))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ (@L7.toL6 _ (@L8.toL7 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6, addc7, addc8⟩)))))))) y x + +-- slow +instance T2_toL9 {α : Type u} [inst : T2 α] : L9 α := { inst with } + + +set_option pp.all true in +-- #print T2.toL9 + +axiom C : Type +axiom C.add : C → C → C + +noncomputable instance C.T1 : T1 C := ⟨add, sorry, sorry, sorry, sorry, sorry, sorry, sorry, sorry, sorry⟩ +noncomputable instance C.T2 : T2 C := ⟨add, sorry, sorry, sorry, sorry, sorry, sorry, sorry, sorry, sorry⟩ + +-- slow +theorem ex : @T1_toL9 _ C.T1 = @T2_toL9 _ C.T2 := rfl