From ee0bcc83218db1b4bec707afa0f0d17362ec5bd5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 17 May 2024 23:14:58 +0200 Subject: [PATCH] feat: add `Simp.Config.index` (#4202) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The `simp` tactic uses a discrimination tree to select candidate theorems that will be used to rewrite an expression. This indexing data structure minimizes the number of theorems that need to be tried and improves performance. However, indexing modulo reducibility is challenging, and a theorem that could be applied, when taking reduction into account, may be missed. For example, suppose we have a `simp` theorem `foo : forall x y, f x (x, y).2 = y`, and we are trying to simplify the expression `f a b <= b`. `foo` will not be tried by `simp` because the second argument of `f a b` is not a projection of a pair. However, `f a b` is definitionally equal to `f a (a, b).2` since we can reduce `(a, b).2`. In Lean 3, we had a much simpler indexing data structure where only the head symbol was taken into account. For the theorem `foo`, the head symbol is `f`. Thus, the theorem would be considered by `simp`. This commit adds the option `Simp.Config.index`. When `simp (config := { index := false })`, only the head symbol is considered when retrieving theorems, as in Lean 3. Moreover, if `set_option diagnostics true`, `simp` will check whether every applied theorem would also have been applied if `index := true`, and report them. This feature can help users diagnose tricky issues in code that has been ported from libraries developed using Lean 3 and then ported to Lean 4. In the following example, it will report that `foo` is a problematic theorem. ```lean opaque f : Nat → Nat → Nat @[simp] theorem foo : f x (x, y).2 = y := by sorry example : f a b ≤ b := by set_option diagnostics true in simp (config := { index := false }) ``` In the example above, the following diagnostic message is produced. ```lean [simp] theorems with bad keys foo, key: [f, *, Prod.1, Prod.mk, Nat, Nat, *, *] ``` With the information above, users can annotate theorems such as `foo` using `no_index` for problematic subterms. Example: ```lean opaque f : Nat → Nat → Nat @[simp] theorem foo : f x (no_index (x, y).2) = y := by sorry example : f a b ≤ b := by simp -- `foo` is still applied ``` cc @semorrison cc @PatrickMassot --- src/Init/MetaTypes.lean | 5 + src/Lean/Meta/DiscrTree.lean | 49 ++ src/Lean/Meta/Tactic/Simp/Diagnostics.lean | 33 +- src/Lean/Meta/Tactic/Simp/Rewrite.lean | 65 +- src/Lean/Meta/Tactic/Simp/Types.lean | 33 +- tests/lean/run/4171.lean | 782 +++++++++++++++++++++ 6 files changed, 938 insertions(+), 29 deletions(-) create mode 100644 tests/lean/run/4171.lean diff --git a/src/Init/MetaTypes.lean b/src/Init/MetaTypes.lean index c5832eb4ed04..9c9465a283ef 100644 --- a/src/Init/MetaTypes.lean +++ b/src/Init/MetaTypes.lean @@ -169,6 +169,11 @@ structure Config where That is, given a local context containing entry `x : t := e`, the free variable `x` reduces to `e`. -/ zetaDelta : Bool := false + /-- + When `index` (default : `true`) is `false`, `simp` will only use the root symbol + to find candidate `simp` theorems. It approximates Lean 3 `simp` behavior. + -/ + index : Bool := true deriving Inhabited, BEq -- Configuration object for `simp_all` diff --git a/src/Lean/Meta/DiscrTree.lean b/src/Lean/Meta/DiscrTree.lean index fe782eb15607..4b6b882141fa 100644 --- a/src/Lean/Meta/DiscrTree.lean +++ b/src/Lean/Meta/DiscrTree.lean @@ -634,6 +634,55 @@ where else return result +/-- +Return the root symbol for `e`, and the number of arguments after `reduceDT`. +-/ +def getMatchKeyRootFor (e : Expr) (config : WhnfCoreConfig) : MetaM (Key × Nat) := do + let e ← reduceDT e (root := true) config + let numArgs := e.getAppNumArgs + let key := match e.getAppFn with + | .lit v => .lit v + | .fvar fvarId => .fvar fvarId numArgs + | .mvar _ => .other + | .proj s i _ .. => .proj s i numArgs + | .forallE .. => .arrow + | .const c _ => + -- This method is used by the simplifier only, we do **not** support + -- (← getConfig).isDefEqStuckEx + .const c numArgs + | _ => .other + return (key, numArgs) + +/-- +Get all results under key `k`. +-/ +private partial def getAllValuesForKey (d : DiscrTree α) (k : Key) (result : Array α) : Array α := + match d.root.find? k with + | none => result + | some trie => go trie result +where + go (trie : Trie α) (result : Array α) : Array α := Id.run do + match trie with + | .node vs cs => + let mut result := result ++ vs + for (_, trie) in cs do + result := go trie result + return result + +/-- +A liberal version of `getMatch` which only takes the root symbol of `e` into account. +We use this method to simulate Lean 3's indexing. + +The natural number in the result is the number of arguments in `e` after `reduceDT`. +-/ +def getMatchLiberal (d : DiscrTree α) (e : Expr) (config : WhnfCoreConfig) : MetaM (Array α × Nat) := do + withReducible do + let result := getStarResult d + let (k, numArgs) ← getMatchKeyRootFor e config + match k with + | .star => return (result, numArgs) + | _ => return (getAllValuesForKey d k result, numArgs) + partial def getUnify (d : DiscrTree α) (e : Expr) (config : WhnfCoreConfig) : MetaM (Array α) := withReducible do let (k, args) ← getUnifyKeyArgs e (root := true) config diff --git a/src/Lean/Meta/Tactic/Simp/Diagnostics.lean b/src/Lean/Meta/Tactic/Simp/Diagnostics.lean index df2ff3261d8a..3a07e5c172d6 100644 --- a/src/Lean/Meta/Tactic/Simp/Diagnostics.lean +++ b/src/Lean/Meta/Tactic/Simp/Diagnostics.lean @@ -9,6 +9,16 @@ import Lean.Meta.Tactic.Simp.Types namespace Lean.Meta.Simp +private def originToKey (thmId : Origin) : MetaM MessageData := do + match thmId with + | .decl declName _ _ => + if (← getEnv).contains declName then + pure m!"{MessageData.ofConst (← mkConstWithLevelParams declName)}" + else + pure m!"{declName} (builtin simproc)" + | .fvar fvarId => pure m!"{mkFVar fvarId}" + | _ => pure thmId.key + def mkSimpDiagSummary (counters : PHashMap Origin Nat) (usedCounters? : Option (PHashMap Origin Nat) := none) : MetaM DiagSummary := do let threshold := diagnostics.threshold.get (← getOptions) let entries := collectAboveThreshold counters threshold (fun _ => true) (lt := (· < ·)) @@ -17,14 +27,7 @@ def mkSimpDiagSummary (counters : PHashMap Origin Nat) (usedCounters? : Option ( else let mut data := #[] for (thmId, counter) in entries do - let key ← match thmId with - | .decl declName _ _ => - if (← getEnv).contains declName then - pure m!"{MessageData.ofConst (← mkConstWithLevelParams declName)}" - else - pure m!"{declName} (builtin simproc)" - | .fvar fvarId => pure m!"{mkFVar fvarId}" - | _ => pure thmId.key + let key ← originToKey thmId let usedMsg ← if let some usedCounters := usedCounters? then if let some c := usedCounters.find? thmId then pure s!", succeeded: {c}" else pure s!" {crossEmoji}" -- not used else @@ -32,16 +35,28 @@ def mkSimpDiagSummary (counters : PHashMap Origin Nat) (usedCounters? : Option ( data := data.push m!"{if data.isEmpty then " " else "\n"}{key} ↦ {counter}{usedMsg}" return { data, max := entries[0]!.2 } +private def mkTheoremsWithBadKeySummary (thms : PArray SimpTheorem) : MetaM DiagSummary := do + if thms.isEmpty then + return {} + else + let mut data := #[] + for thm in thms do + data := data.push m!"{if data.isEmpty then " " else "\n"}{← originToKey thm.origin}, key: {thm.keys.map (·.format)}" + pure () + return { data } + def reportDiag (diag : Simp.Diagnostics) : MetaM Unit := do if (← isDiagnosticsEnabled) then let used ← mkSimpDiagSummary diag.usedThmCounter let tried ← mkSimpDiagSummary diag.triedThmCounter diag.usedThmCounter let congr ← mkDiagSummary diag.congrThmCounter - unless used.isEmpty && tried.isEmpty && congr.isEmpty do + let thmsWithBadKeys ← mkTheoremsWithBadKeySummary diag.thmsWithBadKeys + unless used.isEmpty && tried.isEmpty && congr.isEmpty && thmsWithBadKeys.isEmpty do let m := MessageData.nil let m := appendSection m `simp "used theorems" used let m := appendSection m `simp "tried theorems" tried let m := appendSection m `simp "tried congruence theorems" congr + let m := appendSection m `simp "theorems with bad keys" thmsWithBadKeys (resultSummary := false) let m := m ++ "use `set_option diagnostics.threshold ` to control threshold for reporting counters" logInfo m diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean index bb8d9045e156..9c4827f782da 100644 --- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean +++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean @@ -189,19 +189,62 @@ def tryTheorem? (e : Expr) (thm : SimpTheorem) : SimpM (Option Result) := do Remark: the parameter tag is used for creating trace messages. It is irrelevant otherwise. -/ def rewrite? (e : Expr) (s : SimpTheoremTree) (erased : PHashSet Origin) (tag : String) (rflOnly : Bool) : SimpM (Option Result) := do - let candidates ← s.getMatchWithExtra e (getDtConfig (← getConfig)) - if candidates.isEmpty then - trace[Debug.Meta.Tactic.simp] "no theorems found for {tag}-rewriting {e}" - return none + if (← getConfig).index then + rewriteUsingIndex? else - let candidates := candidates.insertionSort fun e₁ e₂ => e₁.1.priority > e₂.1.priority - for (thm, numExtraArgs) in candidates do - unless inErasedSet thm || (rflOnly && !thm.rfl) do - if let some result ← tryTheoremWithExtraArgs? e thm numExtraArgs then - trace[Debug.Meta.Tactic.simp] "rewrite result {e} => {result.expr}" - return some result - return none + rewriteNoIndex? where + /-- For `(← getConfig).index := true`, use discrimination tree structure when collecting `simp` theorem candidates. -/ + rewriteUsingIndex? : SimpM (Option Result) := do + let candidates ← s.getMatchWithExtra e (getDtConfig (← getConfig)) + if candidates.isEmpty then + trace[Debug.Meta.Tactic.simp] "no theorems found for {tag}-rewriting {e}" + return none + else + let candidates := candidates.insertionSort fun e₁ e₂ => e₁.1.priority > e₂.1.priority + for (thm, numExtraArgs) in candidates do + unless inErasedSet thm || (rflOnly && !thm.rfl) do + if let some result ← tryTheoremWithExtraArgs? e thm numExtraArgs then + trace[Debug.Meta.Tactic.simp] "rewrite result {e} => {result.expr}" + return some result + return none + + /-- + For `(← getConfig).index := false`, Lean 3 style `simp` theorem retrieval. + Only the root symbol is taken into account. Most of the structure of the discrimination tree is ignored. + -/ + rewriteNoIndex? : SimpM (Option Result) := do + let (candidates, numArgs) ← s.getMatchLiberal e (getDtConfig (← getConfig)) + if candidates.isEmpty then + trace[Debug.Meta.Tactic.simp] "no theorems found for {tag}-rewriting {e}" + return none + else + let candidates := candidates.insertionSort fun e₁ e₂ => e₁.priority > e₂.priority + for thm in candidates do + unless inErasedSet thm || (rflOnly && !thm.rfl) do + let result? ← withNewMCtxDepth do + let val ← thm.getValue + let type ← inferType val + let (xs, bis, type) ← forallMetaTelescopeReducing type + let type ← whnf (← instantiateMVars type) + let lhs := type.appFn!.appArg! + let lhsNumArgs := lhs.getAppNumArgs + tryTheoremCore lhs xs bis val type e thm (numArgs - lhsNumArgs) + if let some result := result? then + trace[Debug.Meta.Tactic.simp] "rewrite result {e} => {result.expr}" + diagnoseWhenNoIndex thm + return some result + return none + + diagnoseWhenNoIndex (thm : SimpTheorem) : SimpM Unit := do + if (← isDiagnosticsEnabled) then + let candidates ← s.getMatchWithExtra e (getDtConfig (← getConfig)) + for (candidate, _) in candidates do + if unsafe ptrEq thm candidate then + return () + -- `thm` would not have been applied if `index := true` + recordTheoremWithBadKeys thm + inErasedSet (thm : SimpTheorem) : Bool := erased.contains thm.origin diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean index 962a936271ff..b39a70b29323 100644 --- a/src/Lean/Meta/Tactic/Simp/Types.lean +++ b/src/Lean/Meta/Tactic/Simp/Types.lean @@ -111,6 +111,13 @@ structure Diagnostics where triedThmCounter : PHashMap Origin Nat := {} /-- Number of times each congr theorem has been tried. -/ congrThmCounter : PHashMap Name Nat := {} + /-- + When using `Simp.Config.index := false`, and `set_option diagnostics true`, + for every theorem used by `simp`, we check whether the theorem would be + also applied if `index := true`, and we store it here if it would not have + been tried. + -/ + thmsWithBadKeys : PArray SimpTheorem := {} deriving Inhabited structure State where @@ -325,14 +332,14 @@ Save current cache, reset it, execute `x`, and then restore original cache. withReader (fun r => { MethodsRef.toMethods r with discharge?, wellBehavedDischarge }.toMethodsRef) x def recordTriedSimpTheorem (thmId : Origin) : SimpM Unit := do - modifyDiag fun { usedThmCounter, triedThmCounter, congrThmCounter } => - let cNew := if let some c := triedThmCounter.find? thmId then c + 1 else 1 - { usedThmCounter, triedThmCounter := triedThmCounter.insert thmId cNew, congrThmCounter } + modifyDiag fun s => + let cNew := if let some c := s.triedThmCounter.find? thmId then c + 1 else 1 + { s with triedThmCounter := s.triedThmCounter.insert thmId cNew } def recordSimpTheorem (thmId : Origin) : SimpM Unit := do - modifyDiag fun { usedThmCounter, triedThmCounter, congrThmCounter } => - let cNew := if let some c := usedThmCounter.find? thmId then c + 1 else 1 - { usedThmCounter := usedThmCounter.insert thmId cNew, triedThmCounter, congrThmCounter } + modifyDiag fun s => + let cNew := if let some c := s.usedThmCounter.find? thmId then c + 1 else 1 + { s with usedThmCounter := s.usedThmCounter.insert thmId cNew } /- If `thmId` is an equational theorem (e.g., `foo.eq_1`), we should record `foo` instead. See issue #3547. @@ -353,9 +360,17 @@ def recordSimpTheorem (thmId : Origin) : SimpM Unit := do { s with usedTheorems := s.usedTheorems.insert thmId n } def recordCongrTheorem (declName : Name) : SimpM Unit := do - modifyDiag fun { usedThmCounter, triedThmCounter, congrThmCounter } => - let cNew := if let some c := congrThmCounter.find? declName then c + 1 else 1 - { congrThmCounter := congrThmCounter.insert declName cNew, triedThmCounter, usedThmCounter } + modifyDiag fun s => + let cNew := if let some c := s.congrThmCounter.find? declName then c + 1 else 1 + { s with congrThmCounter := s.congrThmCounter.insert declName cNew } + +def recordTheoremWithBadKeys (thm : SimpTheorem) : SimpM Unit := do + modifyDiag fun s => + -- check whether it is already there + if unsafe s.thmsWithBadKeys.any fun thm' => ptrEq thm thm' then + s + else + { s with thmsWithBadKeys := s.thmsWithBadKeys.push thm } def Result.getProof (r : Result) : MetaM Expr := do match r.proof? with diff --git a/tests/lean/run/4171.lean b/tests/lean/run/4171.lean new file mode 100644 index 000000000000..e387e573e37b --- /dev/null +++ b/tests/lean/run/4171.lean @@ -0,0 +1,782 @@ +/-! +This is a minimization of a problem in Mathlib where a simp lemma `foo` would not fire, +but variants: +* `simp [(foo)]` +* `simp [foo.{v₁ + 1}]` +* `simp [foo']`, where a `no_index` is added in the statement +all work. +-/ + +section Mathlib.Data.Opposite + +universe v u + +variable (α : Sort u) + +structure Opposite := + op :: + unop : α + +notation:max α "ᵒᵖ" => Opposite α + +end Mathlib.Data.Opposite + +section Mathlib.Combinatorics.Quiver.Basic + +open Opposite + +universe v v₁ v₂ u u₁ u₂ + +class Quiver (V : Type u) where + Hom : V → V → Sort v + +infixr:10 " ⟶ " => Quiver.Hom + +structure Prefunctor (V : Type u₁) [Quiver.{v₁} V] (W : Type u₂) [Quiver.{v₂} W] where + obj : V → W + map : ∀ {X Y : V}, (X ⟶ Y) → (obj X ⟶ obj Y) +namespace Quiver + +instance opposite {V} [Quiver V] : Quiver Vᵒᵖ := + ⟨fun a b => (unop b ⟶ unop a)ᵒᵖ⟩ + +def Hom.op {V} [Quiver V] {X Y : V} (f : X ⟶ Y) : op Y ⟶ op X := ⟨f⟩ + +def Hom.unop {V} [Quiver V] {X Y : Vᵒᵖ} (f : X ⟶ Y) : unop Y ⟶ unop X := Opposite.unop f + +end Quiver + + +end Mathlib.Combinatorics.Quiver.Basic + +section Mathlib.CategoryTheory.Category.Basic + +universe v u + +namespace CategoryTheory + +class CategoryStruct (obj : Type u) extends Quiver.{v + 1} obj : Type max u (v + 1) where + id : ∀ X : obj, Hom X X + comp : ∀ {X Y Z : obj}, (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z) + +scoped notation "𝟙" => CategoryStruct.id + +scoped infixr:80 " ≫ " => CategoryStruct.comp + +class Category (obj : Type u) extends CategoryStruct.{v} obj : Type max u (v + 1) where + id_comp : ∀ {X Y : obj} (f : X ⟶ Y), 𝟙 X ≫ f = f + comp_id : ∀ {X Y : obj} (f : X ⟶ Y), f ≫ 𝟙 Y = f + +attribute [simp] Category.id_comp Category.comp_id + +end CategoryTheory + +end Mathlib.CategoryTheory.Category.Basic + +section Mathlib.CategoryTheory.Functor.Basic + +namespace CategoryTheory + +universe v v₁ v₂ v₃ u u₁ u₂ u₃ + +structure Functor (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D] + extends Prefunctor C D : Type max v₁ v₂ u₁ u₂ where + +infixr:26 " ⥤ " => Functor + +namespace Functor + +section + +variable (C : Type u₁) [Category.{v₁} C] + +protected def id : C ⥤ C where + obj X := X + map f := f + +notation "𝟭" => Functor.id + +variable {C} + +@[simp] +theorem id_obj (X : C) : (𝟭 C).obj X = X := rfl + +end + +variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] + {E : Type u₃} [Category.{v₃} E] + +@[simp] +def comp (F : C ⥤ D) (G : D ⥤ E) : C ⥤ E where + obj X := G.obj (F.obj X) + map f := G.map (F.map f) + +infixr:80 " ⋙ " => Functor.comp + +end Functor + +end CategoryTheory + + +end Mathlib.CategoryTheory.Functor.Basic + +section Mathlib.CategoryTheory.NatTrans + +namespace CategoryTheory + +universe v₁ v₂ v₃ v₄ u₁ u₂ u₃ u₄ + +variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] + +structure NatTrans (F G : C ⥤ D) : Type max u₁ v₂ where + app : ∀ X : C, F.obj X ⟶ G.obj X + +end CategoryTheory + +end Mathlib.CategoryTheory.NatTrans + +section Mathlib.CategoryTheory.Iso + +universe v u + +namespace CategoryTheory + +open Category + +structure Iso {C : Type u} [Category.{v} C] (X Y : C) where + hom : X ⟶ Y + inv : Y ⟶ X + +infixr:10 " ≅ " => Iso + +variable {C : Type u} [Category.{v} C] {X Y Z : C} + +namespace Iso + +@[simp] +def symm (I : X ≅ Y) : Y ≅ X where + hom := I.inv + inv := I.hom + +@[simp] +def refl (X : C) : X ≅ X where + hom := 𝟙 X + inv := 𝟙 X + +@[simp] +def trans (α : X ≅ Y) (β : Y ≅ Z) : X ≅ Z where + hom := α.hom ≫ β.hom + inv := β.inv ≫ α.inv + +infixr:80 " ≪≫ " => Iso.trans + +end Iso + +namespace Functor + +universe u₂ v₂ + +variable {D : Type u₂} [Category.{v₂} D] + +@[simp] +def mapIso (F : C ⥤ D) {X Y : C} (i : X ≅ Y) : F.obj X ≅ F.obj Y where + hom := F.map i.hom + inv := F.map i.inv + +end Functor + +end CategoryTheory + + +end Mathlib.CategoryTheory.Iso + +section Mathlib.CategoryTheory.Functor.Category + +namespace CategoryTheory + +universe v₁ v₂ v₃ u₁ u₂ u₃ + +variable (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D] + +instance Functor.category : Category.{max u₁ v₂} (C ⥤ D) where + Hom F G := NatTrans F G + id F := sorry + comp α β := sorry + id_comp := sorry + comp_id := sorry + +end CategoryTheory + +end Mathlib.CategoryTheory.Functor.Category + +section Mathlib.CategoryTheory.NatIso + + +open CategoryTheory + +universe v₁ v₂ v₃ v₄ u₁ u₂ u₃ u₄ + +namespace CategoryTheory + +variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] + +namespace Iso + +@[simp] +def app {F G : C ⥤ D} (α : F ≅ G) (X : C) : F.obj X ≅ G.obj X where + hom := α.hom.app X + inv := α.inv.app X + +end Iso + +namespace NatIso + +variable {F G : C ⥤ D} {X : C} + +@[simp] +def ofComponents (app : ∀ X : C, F.obj X ≅ G.obj X) : + F ≅ G where + hom := + { app := fun X => (app X).hom } + inv := + { app := fun X => (app X).inv } + +end NatIso + + +end CategoryTheory + + +end Mathlib.CategoryTheory.NatIso + +section Mathlib.CategoryTheory.Equivalence + +namespace CategoryTheory + +open CategoryTheory.Functor NatIso Category + +universe v₁ v₂ v₃ u₁ u₂ u₃ + +structure Equivalence (C : Type u₁) (D : Type u₂) [Category.{v₁} C] [Category.{v₂} D] where mk' :: + functor : C ⥤ D + inverse : D ⥤ C + unitIso : 𝟭 C ≅ functor ⋙ inverse + counitIso : inverse ⋙ functor ≅ 𝟭 D + +infixr:10 " ≌ " => Equivalence + +variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] + +@[simp] +def Equivalence.symm (e : C ≌ D) : D ≌ C := + ⟨e.inverse, e.functor, e.counitIso.symm, e.unitIso.symm⟩ + +end CategoryTheory + + +end Mathlib.CategoryTheory.Equivalence + +section Mathlib.CategoryTheory.Opposites + +universe v₁ v₂ u₁ u₂ + +open Opposite + +variable {C : Type u₁} + +@[simp] +theorem Quiver.Hom.unop_op [Quiver.{v₁} C] {X Y : C} (f : X ⟶ Y) : f.op.unop = f := + rfl + +namespace CategoryTheory + +variable [Category.{v₁} C] + +instance Category.opposite : Category.{v₁} Cᵒᵖ where + comp f g := (g.unop ≫ f.unop).op + id X := (𝟙 (unop X)).op + id_comp := sorry + comp_id := sorry + +protected def Iso.op {X Y : C} (α : X ≅ Y) : op Y ≅ op X where + hom := α.hom.op + inv := α.inv.op + +end CategoryTheory + + +end Mathlib.CategoryTheory.Opposites + +section Mathlib.CategoryTheory.Monoidal.Category + +universe v u + +namespace CategoryTheory + +class MonoidalCategoryStruct (C : Type u) [𝒞 : Category.{v} C] where + tensorObj : C → C → C + whiskerLeft (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂) : tensorObj X Y₁ ⟶ tensorObj X Y₂ + whiskerRight {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) : tensorObj X₁ Y ⟶ tensorObj X₂ Y + tensorHom {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g: X₂ ⟶ Y₂) : (tensorObj X₁ X₂ ⟶ tensorObj Y₁ Y₂) := + whiskerRight f X₂ ≫ whiskerLeft Y₁ g + tensorUnit : C + rightUnitor : ∀ X : C, tensorObj X tensorUnit ≅ X + +namespace MonoidalCategory + +scoped infixr:70 " ⊗ " => MonoidalCategoryStruct.tensorObj +scoped infixr:81 " ◁ " => MonoidalCategoryStruct.whiskerLeft +scoped infixl:81 " ▷ " => MonoidalCategoryStruct.whiskerRight +scoped infixr:70 " ⊗ " => MonoidalCategoryStruct.tensorHom +scoped notation "𝟙_ " C:max => (MonoidalCategoryStruct.tensorUnit : C) +scoped notation "ρ_" => MonoidalCategoryStruct.rightUnitor + +end MonoidalCategory + +open MonoidalCategory + +class MonoidalCategory (C : Type u) [𝒞 : Category.{v} C] extends MonoidalCategoryStruct C where + id_whiskerRight : ∀ (X Y : C), 𝟙 X ▷ Y = 𝟙 (X ⊗ Y) + +attribute [simp] MonoidalCategory.id_whiskerRight + +namespace MonoidalCategory + +variable {C : Type u} [𝒞 : Category.{v} C] [MonoidalCategory C] + +@[simp] +theorem id_tensorHom (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂) : + 𝟙 X ⊗ f = X ◁ f := sorry + +@[simp] +theorem tensorHom_id {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) : + f ⊗ 𝟙 Y = f ▷ Y := sorry + +end MonoidalCategory + +@[simp] +def tensorIso {C : Type u} {X Y X' Y' : C} [Category.{v} C] [MonoidalCategory.{v} C] (f : X ≅ Y) + (g : X' ≅ Y') : X ⊗ X' ≅ Y ⊗ Y' where + hom := f.hom ⊗ g.hom + inv := f.inv ⊗ g.inv + +infixr:70 " ⊗ " => tensorIso + +end CategoryTheory + +end Mathlib.CategoryTheory.Monoidal.Category + +section Mathlib.CategoryTheory.Monoidal.Opposite + +universe v₁ v₂ u₁ u₂ + +namespace CategoryTheory + +variable {C : Type u₁} [Category.{v₁} C] [MonoidalCategory.{v₁} C] + +open Opposite MonoidalCategory + +instance monoidalCategoryOp : MonoidalCategory Cᵒᵖ where + tensorObj X Y := op (unop X ⊗ unop Y) + whiskerLeft X _ _ f := (X.unop ◁ f.unop).op + whiskerRight f X := (f.unop ▷ X.unop).op + tensorHom f g := (f.unop ⊗ g.unop).op + tensorUnit := op (𝟙_ C) + id_whiskerRight := sorry + rightUnitor X := (ρ_ (unop X)).symm.op + + +@[simp] theorem op_whiskerLeft (X : C) {Y Z : C} (f : Y ⟶ Z) : + (X ◁ f).op = op X ◁ f.op := rfl +@[simp] theorem unop_whiskerLeft (X : Cᵒᵖ) {Y Z : Cᵒᵖ} (f : Y ⟶ Z) : + (X ◁ f).unop = unop X ◁ f.unop := rfl + +@[simp] theorem op_hom_rightUnitor (X : C) : (ρ_ X).hom.op = (ρ_ (op X)).inv := rfl +@[simp] theorem unop_hom_rightUnitor (X : Cᵒᵖ) : (ρ_ X).hom.unop = (ρ_ (unop X)).inv := rfl + +@[simp] theorem op_inv_rightUnitor (X : C) : (ρ_ X).inv.op = (ρ_ (op X)).hom := rfl +@[simp] theorem unop_inv_rightUnitor (X : Cᵒᵖ) : (ρ_ X).inv.unop = (ρ_ (unop X)).hom := rfl + +end CategoryTheory + + +end Mathlib.CategoryTheory.Monoidal.Opposite + +section Mathlib.CategoryTheory.Monoidal.Transport + +universe v₁ v₂ u₁ u₂ + +noncomputable section + +open CategoryTheory Category MonoidalCategory + +namespace CategoryTheory.Monoidal + +variable {C : Type u₁} [Category.{v₁} C] [MonoidalCategory.{v₁} C] +variable {D : Type u₂} [Category.{v₂} D] + +abbrev induced [MonoidalCategoryStruct D] (F : D ⥤ C) : + MonoidalCategory.{v₂} D where + id_whiskerRight X Y := sorry + +def transportStruct (e : C ≌ D) : MonoidalCategoryStruct.{v₂} D where + tensorObj X Y := e.functor.obj (e.inverse.obj X ⊗ e.inverse.obj Y) + whiskerLeft X _ _ f := e.functor.map (e.inverse.obj X ◁ e.inverse.map f) + whiskerRight f X := sorry + tensorHom f g := sorry + tensorUnit := e.functor.obj (𝟙_ C) + rightUnitor X := + e.functor.mapIso ((Iso.refl _ ⊗ (e.unitIso.app _).symm) ≪≫ ρ_ (e.inverse.obj X)) ≪≫ + e.counitIso.app _ + +@[simp] theorem transportStruct_whiskerLeft (e : C ≌ D) (X x x_1 : D) (f : x ⟶ x_1) : + (transportStruct e).whiskerLeft X f = e.functor.map (e.inverse.obj X ◁ e.inverse.map f) := rfl + +@[simp] theorem transportStruct_rightUnitor (e : C ≌ D) (X : D) : + (transportStruct e).rightUnitor X = + e.functor.mapIso ((Iso.refl _ ⊗ (e.unitIso.app _).symm) ≪≫ ρ_ (e.inverse.obj X)) ≪≫ + e.counitIso.app _ := rfl + +def transport (e : C ≌ D) : MonoidalCategory.{v₂} D := + letI : MonoidalCategoryStruct.{v₂} D := transportStruct e + induced e.inverse + +end CategoryTheory.Monoidal + +end + +end Mathlib.CategoryTheory.Monoidal.Transport + +section Mathlib.CategoryTheory.Monoidal.Braided.Basic + +open CategoryTheory MonoidalCategory + +universe v v₁ v₂ v₃ u u₁ u₂ u₃ + +namespace CategoryTheory + +variable (C : Type u₁) [Category.{v₁} C] [MonoidalCategory C] + +def tensor_μ (X Y : C × C) : (X.1 ⊗ X.2) ⊗ Y.1 ⊗ Y.2 ⟶ (X.1 ⊗ Y.1) ⊗ X.2 ⊗ Y.2 := + sorry + +end CategoryTheory + +end Mathlib.CategoryTheory.Monoidal.Braided.Basic + +section Mathlib.CategoryTheory.Monoidal.Mon_ + +universe v₁ v₂ u₁ u₂ u + +open CategoryTheory MonoidalCategory + +variable (C : Type u₁) [Category.{v₁} C] [MonoidalCategory.{v₁} C] + +structure Mon_ where + X : C + one : 𝟙_ C ⟶ X + mul : X ⊗ X ⟶ X + mul_one : (X ◁ one) ≫ mul = (ρ_ X).hom + +attribute [simp] Mon_.mul_one +namespace Mon_ + +@[simp] +def trivial : Mon_ C where + X := 𝟙_ C + one := 𝟙 _ + mul := sorry + mul_one := sorry + +variable {C} +variable {M : Mon_ C} + +structure Hom (M N : Mon_ C) where + hom : M.X ⟶ N.X + +@[simp] +def id (M : Mon_ C) : Hom M M where + hom := 𝟙 M.X + +@[simp] +def comp {M N O : Mon_ C} (f : Hom M N) (g : Hom N O) : Hom M O where + hom := f.hom ≫ g.hom + +instance : Category (Mon_ C) where + Hom M N := Hom M N + id := id + comp f g := comp f g + id_comp := sorry + comp_id := sorry + +@[ext] +theorem ext {X Y : Mon_ C} {f g : X ⟶ Y} (w : f.hom = g.hom) : f = g := sorry + +@[simp] +theorem id_hom' (M : Mon_ C) : (𝟙 M : Hom M M).hom = 𝟙 M.X := sorry + +@[simp] +theorem comp_hom' {M N K : Mon_ C} (f : M ⟶ N) (g : N ⟶ K) : + (f ≫ g : Hom M K).hom = f.hom ≫ g.hom := sorry + +variable (C) in +@[simp] +def forget : Mon_ C ⥤ C where + obj A := A.X + map f := f.hom + +@[simp] +def isoOfIso {M N : Mon_ C} (f : M.X ≅ N.X) : M ≅ N where + hom := { hom := f.hom } + inv := { hom := f.inv } + + + +@[simp] +instance monMonoidalStruct : MonoidalCategoryStruct (Mon_ C) := + let tensorObj (M N : Mon_ C) : Mon_ C := + { X := M.X ⊗ N.X + one := sorry + mul := tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.mul ⊗ N.mul) + mul_one := sorry } + let tensorHom {X₁ Y₁ X₂ Y₂ : Mon_ C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : + tensorObj _ _ ⟶ tensorObj _ _ := + { hom := f.hom ⊗ g.hom } + { tensorObj := tensorObj + tensorHom := tensorHom + whiskerRight := fun f Y => tensorHom f (𝟙 Y) + whiskerLeft := fun X _ _ g => tensorHom (𝟙 X) g + tensorUnit := trivial C + rightUnitor := fun M ↦ isoOfIso (ρ_ M.X) } + +@[simp] +theorem whiskerLeft_hom {X Y : Mon_ C} (f : X ⟶ Y) (Z : Mon_ C) : + (f ▷ Z).hom = f.hom ▷ Z.X := by + rw [← tensorHom_id]; rfl + +@[simp] +theorem whiskerRight_hom (X : Mon_ C) {Y Z : Mon_ C} (f : Y ⟶ Z) : + (X ◁ f).hom = X.X ◁ f.hom := by + rw [← id_tensorHom]; rfl + +@[simp] +theorem rightUnitor_inv_hom (X : Mon_ C) : (ρ_ X).inv.hom = (ρ_ X.X).inv := rfl + +instance monMonoidal : MonoidalCategory (Mon_ C) where + id_whiskerRight := sorry + +end Mon_ + +end Mathlib.CategoryTheory.Monoidal.Mon_ + +section Mathlib.CategoryTheory.Monoidal.Comon_ + +universe v₁ v₂ u₁ u₂ u + +open CategoryTheory MonoidalCategory + +variable (C : Type u₁) [Category.{v₁} C] [MonoidalCategory.{v₁} C] + +structure Comon_ where + X : C + counit : X ⟶ 𝟙_ C + comul : X ⟶ X ⊗ X + +namespace Comon_ + +variable {C} +variable {M : Comon_ C} + +structure Hom (M N : Comon_ C) where + hom : M.X ⟶ N.X + +@[simp] +def id (M : Comon_ C) : Hom M M where + hom := 𝟙 M.X + +@[simp] +def comp {M N O : Comon_ C} (f : Hom M N) (g : Hom N O) : Hom M O where + hom := f.hom ≫ g.hom + +instance : Category (Comon_ C) where + Hom M N := Hom M N + id := id + comp f g := comp f g + comp_id := sorry + id_comp := sorry + +@[ext] theorem ext {X Y : Comon_ C} {f g : X ⟶ Y} (w : f.hom = g.hom) : f = g := sorry + +@[simp] theorem id_hom' (M : Comon_ C) : (𝟙 M : Hom M M).hom = 𝟙 M.X := rfl + +@[simp] +theorem comp_hom' {M N K : Comon_ C} (f : M ⟶ N) (g : N ⟶ K) : (f ≫ g).hom = f.hom ≫ g.hom := + rfl + +open Opposite + +variable (C) + +def Comon_to_Mon_op_op_obj' (A : Comon_ C) : Mon_ (Cᵒᵖ) where + X := op A.X + one := A.counit.op + mul := A.comul.op + mul_one := sorry + +@[simp] theorem Comon_to_Mon_op_op_obj'_X (A : Comon_ C) : (Comon_to_Mon_op_op_obj' C A).X = op A.X := rfl + +@[simp] def Comon_to_Mon_op_op : Comon_ C ⥤ (Mon_ (Cᵒᵖ))ᵒᵖ where + obj A := op (Comon_to_Mon_op_op_obj' C A) + map := fun f => op <| { hom := f.hom.op } + +def Mon_op_op_to_Comon_obj' (A : (Mon_ (Cᵒᵖ))) : Comon_ C where + X := unop A.X + counit := A.one.unop + comul := A.mul.unop + +@[simp] theorem Mon_op_op_to_Comon_obj'_X (A : (Mon_ (Cᵒᵖ))) : (Mon_op_op_to_Comon_obj' C A).X = unop A.X := rfl + +@[simp] +def Mon_op_op_to_Comon : (Mon_ (Cᵒᵖ))ᵒᵖ ⥤ Comon_ C where + obj A := Mon_op_op_to_Comon_obj' C (unop A) + map := fun f => + { hom := f.unop.hom.unop } + +@[simp] +def Comon_equiv_Mon_op_op : Comon_ C ≌ (Mon_ (Cᵒᵖ))ᵒᵖ := + { functor := Comon_to_Mon_op_op C + inverse := Mon_op_op_to_Comon C + unitIso := NatIso.ofComponents (fun _ => Iso.refl _) + counitIso := NatIso.ofComponents (fun _ => Iso.refl _) } + +instance : MonoidalCategory (Comon_ C) := + Monoidal.transport (Comon_equiv_Mon_op_op C).symm + +end Comon_ + +namespace CategoryTheory.Functor + +variable {C} {D : Type u₂} [Category.{v₂} D] [MonoidalCategory.{v₂} D] + +def mapComon (F : C ⥤ D) : Comon_ C ⥤ Comon_ D where + obj A := + { X := F.obj A.X + counit := sorry + comul := sorry } + map f := sorry + +end CategoryTheory.Functor + + +end Mathlib.CategoryTheory.Monoidal.Comon_ + +section Mathlib.CategoryTheory.Monoidal.Bimon_ + +noncomputable section + +universe v₁ v₂ u₁ u₂ u + +open CategoryTheory MonoidalCategory + +variable (C : Type u₁) [Category.{v₁} C] [MonoidalCategory.{v₁} C] + +def toComon_ : Comon_ (Mon_ C) ⥤ Comon_ C := (Mon_.forget C).mapComon + +@[simp] theorem toComon_obj_X (M : Comon_ (Mon_ C)) : ((toComon_ C).obj M).X = M.X.X := rfl + +theorem foo {V} [Quiver V] {X Y x} : + @Quiver.Hom.unop V _ X Y (Opposite.op (unop := x)) = x := rfl + +example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where + X := (toComon_ C).obj M + one := { hom := M.X.one } + mul := { hom := M.X.mul } + mul_one := by + ext + simp [(foo)] -- parentheses around `foo` works + +example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where + X := (toComon_ C).obj M + one := { hom := M.X.one } + mul := { hom := M.X.mul } + mul_one := by + ext + simp [foo.{v₁ + 1}] -- specifying the universe level explicitly works! + +theorem foo' {V} [Quiver V] {X Y x} : + @Quiver.Hom.unop V _ X Y no_index (Opposite.op (unop := x)) = x := rfl + +example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where + X := (toComon_ C).obj M + one := { hom := M.X.one } + mul := { hom := M.X.mul } + mul_one := by + ext + simp [foo'] -- or adding a `no_index` in the statement + + +/-- +info: [simp] theorems with bad keys + foo, key: [Quiver.Hom.unop, + *, + *, + *, + *, + Opposite.op, + Quiver.Hom, + *, + *, + Opposite.0, + *, + Opposite.0, + *, + *]use `set_option diagnostics.threshold ` to control threshold for reporting counters +-/ +#guard_msgs in +example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where + X := (toComon_ C).obj M + one := { hom := M.X.one } + mul := { hom := M.X.mul, } + mul_one := by + ext + -- increase the threshold to ensure the guard_msgs docstring is not too big. + set_option diagnostics.threshold 100000 in + set_option diagnostics true in + -- `index := false` ignores most of the discrimination tree structure. + simp (config := { index := false }) [foo] + +attribute [simp] foo + +/-- +info: [simp] theorems with bad keys + foo, key: [Quiver.Hom.unop, + *, + *, + *, + *, + Opposite.op, + Quiver.Hom, + *, + *, + Opposite.0, + *, + Opposite.0, + *, + *]use `set_option diagnostics.threshold ` to control threshold for reporting counters +-/ +#guard_msgs in +example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where + X := (toComon_ C).obj M + one := { hom := M.X.one } + mul := { hom := M.X.mul, } + mul_one := by + ext + -- increase the threshold to ensure the guard_msgs docstring is not too big. + set_option diagnostics.threshold 100000 in + set_option diagnostics true in + -- `index := false` ignores most of the discrimination tree structure. + simp (config := { index := false }) + +end + +end Mathlib.CategoryTheory.Monoidal.Bimon_