From af4a7d7e984e275d2d7091908c7172d4414e2128 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 15 Jan 2025 17:22:06 -0800 Subject: [PATCH] fix: `grind` term preprocessor (#6659) This PR fixes a bug in the `grind` term preprocessor. It was abstracting nested proofs **before** reducible constants were unfolded. --------- Co-authored-by: Kim Morrison --- src/Lean/Meta/Tactic/Grind/Simp.lean | 2 +- tests/lean/run/grind_cat.lean | 119 ++++++++++++++++++++++++++- 2 files changed, 119 insertions(+), 2 deletions(-) diff --git a/src/Lean/Meta/Tactic/Grind/Simp.lean b/src/Lean/Meta/Tactic/Grind/Simp.lean index bf0c7a7bfce3..e10637e8d82c 100644 --- a/src/Lean/Meta/Tactic/Grind/Simp.lean +++ b/src/Lean/Meta/Tactic/Grind/Simp.lean @@ -28,9 +28,9 @@ def simp (e : Expr) : GoalM Simp.Result := do let e ← instantiateMVars e let r ← simpCore e let e' := r.expr + let e' ← unfoldReducible e' let e' ← abstractNestedProofs e' let e' ← markNestedProofs e' - let e' ← unfoldReducible e' let e' ← eraseIrrelevantMData e' let e' ← foldProjs e' let e' ← normalizeLevels e' diff --git a/tests/lean/run/grind_cat.lean b/tests/lean/run/grind_cat.lean index bc4101848b55..41143c034315 100644 --- a/tests/lean/run/grind_cat.lean +++ b/tests/lean/run/grind_cat.lean @@ -36,6 +36,8 @@ structure Functor (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category. /-- A functor preserves composition. -/ map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = (map f) ≫ (map g) := by cat_tac +scoped infixr:26 " ⥤ " => Functor + attribute [simp] Functor.map_id Functor.map_comp attribute [grind =] Functor.map_id @@ -51,6 +53,8 @@ def comp (F : Functor C D) (G : Functor D E) : Functor C E where map f := G.map (F.map f) -- Note `map_id` and `map_comp` are handled by `cat_tac`. +infixr:80 " ⋙ " => Functor.comp + variable {X Y : C} {G : Functor D E} @[simp, grind =] theorem comp_obj : (F.comp G).obj X = G.obj (F.obj X) := rfl @@ -73,7 +77,7 @@ variable {X : C} protected def id (F : Functor C D) : NatTrans F F where app X := 𝟙 (F.obj X) -@[simp, grind =] theorem id_app : (NatTrans.id F).app X = 𝟙 (F.obj X) := rfl +@[simp, grind =] theorem id_app' : (NatTrans.id F).app X = 𝟙 (F.obj X) := rfl protected def vcomp (α : NatTrans F G) (β : NatTrans G H) : NatTrans F H where app X := α.app X ≫ β.app X @@ -96,6 +100,11 @@ instance Functor.category : Category.{max u₁ v₂} (Functor C D) where comp α β := NatTrans.vcomp α β -- Here we're okay: all the proofs are handled by `cat_tac`. +namespace NatTrans + +@[ext] +theorem ext' {α β : F ⟶ G} (w : α.app = β.app) : α = β := NatTrans.ext w + @[simp, grind =] theorem id_app (F : Functor C D) (X : C) : (𝟙 F : F ⟶ F).app X = 𝟙 (F.obj X) := rfl @@ -122,6 +131,30 @@ def hcomp {H I : Functor D E} (α : F ⟶ G) (β : H ⟶ I) : F.comp H ⟶ G.com -- rw [Functor.comp_map, Functor.comp_map, ← assoc, naturality, assoc, ← I.map_comp, naturality, -- map_comp, assoc] +/-- Notation for horizontal composition of natural transformations. -/ +infixl:80 " ◫ " => hcomp + +@[simp] theorem hcomp_app {H I : Functor D E} (α : F ⟶ G) (β : H ⟶ I) (X : C) : + (α ◫ β).app X = β.app (F.obj X) ≫ I.map (α.app X) := rfl + +attribute [grind =] hcomp_app + +theorem hcomp_id_app {H : D ⥤ E} (α : F ⟶ G) (X : C) : (α ◫ 𝟙 H).app X = H.map (α.app X) := by + cat_tac + +theorem id_hcomp_app {H : E ⥤ C} (α : F ⟶ G) (X : E) : (𝟙 H ◫ α).app X = α.app _ := by cat_tac + +-- Note that we don't yet prove a `hcomp_assoc` lemma here: even stating it is painful, because we +-- need to use associativity of functor composition. (It's true without the explicit associator, +-- because functor composition is definitionally associative, +-- but relying on the definitional equality causes bad problems with elaboration later.) +theorem exchange {I J K : D ⥤ E} (α : F ⟶ G) (β : G ⟶ H) (γ : I ⟶ J) (δ : J ⟶ K) : + (α ≫ β) ◫ (γ ≫ δ) = (α ◫ γ) ≫ β ◫ δ := by + ext X + cat_tac + +end NatTrans + structure Iso {C : Type u} [Category.{v} C] (X Y : C) where hom : X ⟶ Y inv : Y ⟶ X @@ -179,4 +212,88 @@ def homToEquiv (α : X ≅ Y) {Z : C} : (Z ⟶ X) ≃ (Z ⟶ Y) where right_inv := sorry end Iso + +section Mathlib.CategoryTheory.Functor.Category + + +open NatTrans Category CategoryTheory.Functor + +variable (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D] + +attribute [local simp] vcomp_app + +variable {C D} {E : Type u₃} [Category.{v₃} E] +variable {E' : Type u₄} [Category.{v₄} E'] +variable {F G H I : C ⥤ D} + + +namespace NatTrans + +@[simp] +theorem vcomp_eq_comp (α : F ⟶ G) (β : G ⟶ H) : NatTrans.vcomp α β = α ≫ β := rfl + +theorem vcomp_app' (α : F ⟶ G) (β : G ⟶ H) (X : C) : (α ≫ β).app X = α.app X ≫ β.app X := rfl + +theorem congr_app {α β : F ⟶ G} (h : α = β) (X : C) : α.app X = β.app X := by rw [h] + +theorem naturality_app_app {F G : C ⥤ D ⥤ E ⥤ E'} + (α : F ⟶ G) {X₁ Y₁ : C} (f : X₁ ⟶ Y₁) (X₂ : D) (X₃ : E) : + ((F.map f).app X₂).app X₃ ≫ ((α.app Y₁).app X₂).app X₃ = + ((α.app X₁).app X₂).app X₃ ≫ ((G.map f).app X₂).app X₃ := + congr_app (NatTrans.naturality_app α X₂ f) X₃ + +end NatTrans + +open NatTrans + +namespace Functor + +/-- Flip the arguments of a bifunctor. See also `Currying.lean`. -/ +protected def flip (F : C ⥤ D ⥤ E) : D ⥤ C ⥤ E where + obj k := + { obj := fun j => (F.obj j).obj k, + map := fun f => (F.map f).app k, } + map f := { app := fun j => (F.obj j).map f } + map_id k := by cat_tac + map_comp f g := sorry + +@[simp] theorem flip_obj_obj (F : C ⥤ D ⥤ E) (k : D) : (F.flip.obj k).obj = fun j => (F.obj j).obj k := rfl +@[simp] theorem flip_obj_map (F : C ⥤ D ⥤ E) (k : D) {X Y : C}(f : X ⟶ Y) : (F.flip.obj k).map f = (F.map f).app k := rfl +@[simp] theorem flip_map_app (F : C ⥤ D ⥤ E) {X Y : D} (f : X ⟶ Y) (k : C) : (F.flip.map f).app k = (F.obj k).map f := rfl + +attribute [grind =] flip_obj_obj flip_obj_map flip_map_app + +end Functor + +variable (C D E) in +/-- The functor `(C ⥤ D ⥤ E) ⥤ D ⥤ C ⥤ E` which flips the variables. -/ +def flipFunctor : (C ⥤ D ⥤ E) ⥤ D ⥤ C ⥤ E where + obj F := F.flip + map {F₁ F₂} φ := + { app := fun Y => + { app := fun X => (φ.app X).app Y + naturality := fun X₁ X₂ f => by + dsimp + simp only [← NatTrans.comp_app, naturality] } + naturality := sorry } + map_id := sorry + map_comp := sorry + +namespace Iso + +@[simp] +theorem map_hom_inv_id_app {X Y : C} (e : X ≅ Y) (F : C ⥤ D ⥤ E) (Z : D) : + (F.map e.hom).app Z ≫ (F.map e.inv).app Z = 𝟙 _ := by + cat_tac + +@[simp] +theorem map_inv_hom_id_app {X Y : C} (e : X ≅ Y) (F : C ⥤ D ⥤ E) (Z : D) : + (F.map e.inv).app Z ≫ (F.map e.hom).app Z = 𝟙 _ := by + cat_tac + +end Iso + + +end Mathlib.CategoryTheory.Functor.Category + end CategoryTheory