diff --git a/src/Init/MetaTypes.lean b/src/Init/MetaTypes.lean index 1221a37e4a..745c68b0f5 100644 --- a/src/Init/MetaTypes.lean +++ b/src/Init/MetaTypes.lean @@ -224,7 +224,8 @@ structure Config where -/ index : Bool := true /-- - This option does not have any effect (yet). + If `implicitDefEqProofs := true`, `simp` does not create proof terms when the + input and output terms are definitionally equal. -/ implicitDefEqProofs : Bool := true deriving Inhabited, BEq diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 9767caa085..581fe806a2 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -229,7 +229,7 @@ structure ParamInfo where hasFwdDeps : Bool := false /-- `backDeps` contains the backwards dependencies. That is, the (0-indexed) position of previous parameters that this one depends on. -/ backDeps : Array Nat := #[] - /-- `isProp` is true if the parameter is always a proposition. -/ + /-- `isProp` is true if the parameter type is always a proposition. -/ isProp : Bool := false /-- `isDecInst` is true if the parameter's type is of the form `Decidable ...`. diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean index 9a3d3118c4..b68829fa9b 100644 --- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean +++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean @@ -108,13 +108,19 @@ where trace[Meta.Tactic.simp.discharge] "{← ppOrigin thmId}, failed to synthesize instance{indentExpr type}" return false +private def useImplicitDefEqProof (thm : SimpTheorem) : SimpM Bool := do + if thm.rfl then + return (← getConfig).implicitDefEqProofs + else + return false + private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInfo) (val : Expr) (type : Expr) (e : Expr) (thm : SimpTheorem) (numExtraArgs : Nat) : SimpM (Option Result) := do recordTriedSimpTheorem thm.origin let rec go (e : Expr) : SimpM (Option Result) := do if (← isDefEq lhs e) then unless (← synthesizeArgs thm.origin bis xs) do return none - let proof? ← if thm.rfl then + let proof? ← if (← useImplicitDefEqProof thm) then pure none else let proof ← instantiateMVars (mkAppN val xs) diff --git a/src/Lean/Meta/Tactic/Split.lean b/src/Lean/Meta/Tactic/Split.lean index be116ed428..c9057df013 100644 --- a/src/Lean/Meta/Tactic/Split.lean +++ b/src/Lean/Meta/Tactic/Split.lean @@ -269,7 +269,7 @@ def mkDiscrGenErrorMsg (e : Expr) : MessageData := def throwDiscrGenError (e : Expr) : MetaM α := throwError (mkDiscrGenErrorMsg e) -def splitMatch (mvarId : MVarId) (e : Expr) : MetaM (List MVarId) := do +def splitMatch (mvarId : MVarId) (e : Expr) : MetaM (List MVarId) := mvarId.withContext do let some app ← matchMatcherApp? e | throwError "internal error in `split` tactic: match application expected{indentExpr e}\nthis error typically occurs when the `split` tactic internal functions have been used in a new meta-program" let matchEqns ← Match.getEquationsFor app.matcherName let mvarIds ← applyMatchSplitter mvarId app.matcherName app.matcherLevels app.params app.discrs @@ -278,43 +278,14 @@ def splitMatch (mvarId : MVarId) (e : Expr) : MetaM (List MVarId) := do return (i+1, mvarId::mvarIds) return mvarIds.reverse -/-- Return an `if-then-else` or `match-expr` to split. -/ -partial def findSplit? (env : Environment) (e : Expr) (splitIte := true) (exceptionSet : ExprSet := {}) : Option Expr := - go e -where - go (e : Expr) : Option Expr := - if let some target := e.find? isCandidate then - if e.isIte || e.isDIte then - let cond := target.getArg! 1 5 - -- Try to find a nested `if` in `cond` - go cond |>.getD target - else - some target - else - none - - isCandidate (e : Expr) : Bool := Id.run do - if exceptionSet.contains e then - false - else if splitIte && (e.isIte || e.isDIte) then - !(e.getArg! 1 5).hasLooseBVars - else if let some info := isMatcherAppCore? env e then - let args := e.getAppArgs - for i in [info.getFirstDiscrPos : info.getFirstDiscrPos + info.numDiscrs] do - if args[i]!.hasLooseBVars then - return false - return true - else - false - end Split open Split -partial def splitTarget? (mvarId : MVarId) (splitIte := true) : MetaM (Option (List MVarId)) := commitWhenSome? do +partial def splitTarget? (mvarId : MVarId) (splitIte := true) : MetaM (Option (List MVarId)) := commitWhenSome? do mvarId.withContext do let target ← instantiateMVars (← mvarId.getType) let rec go (badCases : ExprSet) : MetaM (Option (List MVarId)) := do - if let some e := findSplit? (← getEnv) target splitIte badCases then + if let some e ← findSplit? target (if splitIte then .both else .match) badCases then if e.isIte || e.isDIte then return (← splitIfTarget? mvarId).map fun (s₁, s₂) => [s₁.mvarId, s₂.mvarId] else @@ -333,7 +304,7 @@ partial def splitTarget? (mvarId : MVarId) (splitIte := true) : MetaM (Option (L def splitLocalDecl? (mvarId : MVarId) (fvarId : FVarId) : MetaM (Option (List MVarId)) := commitWhenSome? do mvarId.withContext do - if let some e := findSplit? (← getEnv) (← instantiateMVars (← inferType (mkFVar fvarId))) then + if let some e ← findSplit? (← instantiateMVars (← inferType (mkFVar fvarId))) then if e.isIte || e.isDIte then return (← splitIfLocalDecl? mvarId fvarId).map fun (mvarId₁, mvarId₂) => [mvarId₁, mvarId₂] else diff --git a/src/Lean/Meta/Tactic/SplitIf.lean b/src/Lean/Meta/Tactic/SplitIf.lean index b1f6f7c11d..b6734f2157 100644 --- a/src/Lean/Meta/Tactic/SplitIf.lean +++ b/src/Lean/Meta/Tactic/SplitIf.lean @@ -8,6 +8,124 @@ import Lean.Meta.Tactic.Cases import Lean.Meta.Tactic.Simp.Main namespace Lean.Meta + +inductive SplitKind where + | ite | match | both + +def SplitKind.considerIte : SplitKind → Bool + | .ite | .both => true + | _ => false + +def SplitKind.considerMatch : SplitKind → Bool + | .match | .both => true + | _ => false + +namespace FindSplitImpl + +structure Context where + exceptionSet : ExprSet := {} + kind : SplitKind := .both + +unsafe abbrev FindM := ReaderT Context $ StateT (PtrSet Expr) MetaM + +/-- +Checks whether `e` is a candidate for `split`. +Returns `some e'` if a prefix is a candidate. +Example: suppose `e` is `(if b then f else g) x`, then +the result is `some e'` where `e'` is the subterm `(if b then f else g)` +-/ +private def isCandidate? (env : Environment) (ctx : Context) (e : Expr) : Option Expr := Id.run do + let ret (e : Expr) : Option Expr := + if ctx.exceptionSet.contains e then none else some e + if ctx.kind.considerIte then + if e.isAppOf ``ite || e.isAppOf ``dite then + let numArgs := e.getAppNumArgs + if numArgs >= 5 && !(e.getArg! 1 5).hasLooseBVars then + return ret (e.getBoundedAppFn (numArgs - 5)) + if ctx.kind.considerMatch then + if let some info := isMatcherAppCore? env e then + let args := e.getAppArgs + for i in [info.getFirstDiscrPos : info.getFirstDiscrPos + info.numDiscrs] do + if args[i]!.hasLooseBVars then + return none + return ret (e.getBoundedAppFn (args.size - info.arity)) + return none + +@[inline] unsafe def checkVisited (e : Expr) : OptionT FindM Unit := do + if (← get).contains e then + failure + modify fun s => s.insert e + +unsafe def visit (e : Expr) : OptionT FindM Expr := do + checkVisited e + if let some e := isCandidate? (← getEnv) (← read) e then + return e + else + -- We do not look for split candidates in proofs. + unless e.hasLooseBVars do + if (← isProof e) then + failure + match e with + | .lam _ _ b _ | .proj _ _ b -- We do not look for split candidates in the binder of lambdas. + | .mdata _ b => visit b + | .forallE _ d b _ => visit d <|> visit b -- We want to look for candidates at `A → B` + | .letE _ _ v b _ => visit v <|> visit b + | .app .. => visitApp? e + | _ => failure +where + visitApp? (e : Expr) : FindM (Option Expr) := + e.withApp fun f args => do + -- See comment at `Canonicalizer.lean` regarding the case where + -- `f` has loose bound variables. + let info ← if f.hasLooseBVars then + pure {} + else + getFunInfo f + for u : i in [0:args.size] do + let arg := args[i] + if h : i < info.paramInfo.size then + let info := info.paramInfo[i] + unless info.isProp do + if info.isExplicit then + let some found ← visit arg | pure () + return found + else + let some found ← visit arg | pure () + return found + visit f + +end FindSplitImpl + +/-- Return an `if-then-else` or `match-expr` to split. -/ +partial def findSplit? (e : Expr) (kind : SplitKind := .both) (exceptionSet : ExprSet := {}) : MetaM (Option Expr) := do + go (← instantiateMVars e) +where + go (e : Expr) : MetaM (Option Expr) := do + if let some target ← find? e then + if target.isIte || target.isDIte then + let cond := target.getArg! 1 5 + -- Try to find a nested `if` in `cond` + return (← go cond).getD target + else + return some target + else + return none + + find? (e : Expr) : MetaM (Option Expr) := do + let some candidate ← unsafe FindSplitImpl.visit e { kind, exceptionSet } |>.run' mkPtrSet + | return none + trace[split.debug] "candidate:{indentExpr candidate}" + return some candidate + +/-- Return the condition and decidable instance of an `if` expression to case split. -/ +private partial def findIfToSplit? (e : Expr) : MetaM (Option (Expr × Expr)) := do + if let some iteApp ← findSplit? e .ite then + let cond := iteApp.getArg! 1 5 + let dec := iteApp.getArg! 2 5 + return (cond, dec) + else + return none + namespace SplitIf /-- @@ -62,19 +180,9 @@ private def discharge? (numIndices : Nat) (useDecide : Bool) : Simp.Discharge := def mkDischarge? (useDecide := false) : MetaM Simp.Discharge := return discharge? (← getLCtx).numIndices useDecide -/-- Return the condition and decidable instance of an `if` expression to case split. -/ -private partial def findIfToSplit? (e : Expr) : Option (Expr × Expr) := - if let some iteApp := e.find? fun e => (e.isIte || e.isDIte) && !(e.getArg! 1 5).hasLooseBVars then - let cond := iteApp.getArg! 1 5 - let dec := iteApp.getArg! 2 5 - -- Try to find a nested `if` in `cond` - findIfToSplit? cond |>.getD (cond, dec) - else - none - -def splitIfAt? (mvarId : MVarId) (e : Expr) (hName? : Option Name) : MetaM (Option (ByCasesSubgoal × ByCasesSubgoal)) := do +def splitIfAt? (mvarId : MVarId) (e : Expr) (hName? : Option Name) : MetaM (Option (ByCasesSubgoal × ByCasesSubgoal)) := mvarId.withContext do let e ← instantiateMVars e - if let some (cond, decInst) := findIfToSplit? e then + if let some (cond, decInst) ← findIfToSplit? e then let hName ← match hName? with | none => mkFreshUserName `h | some hName => pure hName @@ -106,6 +214,7 @@ def splitIfTarget? (mvarId : MVarId) (hName? : Option Name := none) : MetaM (Opt let mvarId₁ ← simpIfTarget s₁.mvarId let mvarId₂ ← simpIfTarget s₂.mvarId if s₁.mvarId == mvarId₁ && s₂.mvarId == mvarId₂ then + trace[split.failure] "`split` tactic failed to simplify target using new hypotheses Goals:\n{mvarId₁}\n{mvarId₂}" return none else return some ({ s₁ with mvarId := mvarId₁ }, { s₂ with mvarId := mvarId₂ }) @@ -118,6 +227,7 @@ def splitIfLocalDecl? (mvarId : MVarId) (fvarId : FVarId) (hName? : Option Name let mvarId₁ ← simpIfLocalDecl s₁.mvarId fvarId let mvarId₂ ← simpIfLocalDecl s₂.mvarId fvarId if s₁.mvarId == mvarId₁ && s₂.mvarId == mvarId₂ then + trace[split.failure] "`split` tactic failed to simplify target using new hypotheses Goals:\n{mvarId₁}\n{mvarId₂}" return none else return some (mvarId₁, mvarId₂) diff --git a/tests/compiler/uset.lean b/tests/compiler/uset.lean index 9562cd7105..d83389f507 100644 --- a/tests/compiler/uset.lean +++ b/tests/compiler/uset.lean @@ -7,4 +7,3 @@ structure Point where def main : IO Unit := IO.println (Point.right ⟨0, 0⟩).x - diff --git a/tests/lean/1113.lean b/tests/lean/1113.lean index f4036fd1e3..0c4035e85a 100644 --- a/tests/lean/1113.lean +++ b/tests/lean/1113.lean @@ -4,7 +4,7 @@ def foo: {n: Nat} → Fin n → Nat theorem t3 {f: Fin (n+1)}: foo f = 0 := by - simp only [←Nat.succ_eq_add_one n] at f + dsimp only [←Nat.succ_eq_add_one n] at f -- use `dsimp` to ensure we don't copy `f` trace_state simp only [←Nat.succ_eq_add_one n, foo] diff --git a/tests/lean/rfl_simp_thm.lean b/tests/lean/rfl_simp_thm.lean index 5f84fab634..f414ea130d 100644 --- a/tests/lean/rfl_simp_thm.lean +++ b/tests/lean/rfl_simp_thm.lean @@ -3,6 +3,6 @@ def inc (x : Nat) := x + 1 @[simp] theorem inc_eq : inc x = x + 1 := rfl theorem ex (a b : Fin (inc n)) (h : a = b) : b = a := by - simp only [inc_eq] at a + simp +implicitDefEqProofs only [inc_eq] at a trace_state exact h.symm diff --git a/tests/lean/run/4595_slowdown.lean b/tests/lean/run/4595_slowdown.lean new file mode 100644 index 0000000000..3c1e2d9c55 --- /dev/null +++ b/tests/lean/run/4595_slowdown.lean @@ -0,0 +1,288 @@ +-- The final declaration blew up by a factor of about 40x heartbeats on an earlier draft of +-- https://github.com/leanprover/lean4/pull/4595, so this is here as a regression test. + +universe v v₁ v₂ v₃ u u₁ u₂ u₃ + +section Mathlib.Combinatorics.Quiver.Basic + +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) + +end Mathlib.Combinatorics.Quiver.Basic + +section Mathlib.CategoryTheory.Category.Basic + +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 + +end CategoryTheory + +end Mathlib.CategoryTheory.Category.Basic + +section Mathlib.CategoryTheory.Functor.Basic + +namespace CategoryTheory + +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 + +@[simp] +theorem id_map {X Y : C} (f : X ⟶ Y) : (𝟭 C).map f = f := rfl + +end + +variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] + {E : Type u₃} [Category.{v₃} E] + +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 + +@[simp] theorem comp_obj (F : C ⥤ D) (G : D ⥤ E) (X : C) : + (F ⋙ G).obj X = G.obj (F.obj X) := rfl + +@[simp] +theorem comp_map (F : C ⥤ D) (G : D ⥤ E) {X Y : C} (f : X ⟶ Y) : + (F ⋙ G).map f = G.map (F.map f) := rfl + +end Functor + +end CategoryTheory + + +end Mathlib.CategoryTheory.Functor.Basic + +section Mathlib.CategoryTheory.NatTrans + +namespace CategoryTheory + +variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] + +@[ext] +structure NatTrans (F G : C ⥤ D) : Type max u₁ v₂ where + app : ∀ X : C, F.obj X ⟶ G.obj X + naturality : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.map f ≫ app Y = app X ≫ G.map f + +protected def NatTrans.id (F : C ⥤ D) : NatTrans F F where + app X := 𝟙 (F.obj X) + naturality := sorry + +end CategoryTheory + +end Mathlib.CategoryTheory.NatTrans + +section Mathlib.CategoryTheory.Iso + +namespace CategoryTheory + +structure Iso {C : Type u} [Category.{v} C] (X Y : C) where + hom : X ⟶ Y + inv : Y ⟶ X + hom_inv_id : hom ≫ inv = 𝟙 X + inv_hom_id : inv ≫ hom = 𝟙 Y + +infixr:10 " ≅ " => Iso + +end CategoryTheory + +end Mathlib.CategoryTheory.Iso + +section Mathlib.CategoryTheory.Functor.Category + +namespace CategoryTheory + +variable (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D] + +namespace Functor + +instance category : Category.{max u₁ v₂} (C ⥤ D) where + Hom F G := NatTrans F G + id F := NatTrans.id F + comp α β := sorry + id_comp := sorry + comp_id := sorry + +@[ext] +theorem ext' {F G : C ⥤ D} {α β : F ⟶ G} (w : α.app = β.app) : α = β := NatTrans.ext w + +end Functor + +namespace NatTrans + +@[simp] +theorem id_app (F : C ⥤ D) (X : C) : (𝟙 F : F ⟶ F).app X = 𝟙 (F.obj X) := rfl + +@[simp] +theorem comp_app {F G H : C ⥤ D} (α : F ⟶ G) (β : G ⟶ H) (X : C) : + (α ≫ β).app X = α.app X ≫ β.app X := sorry + +end NatTrans + +end CategoryTheory + +end Mathlib.CategoryTheory.Functor.Category + +section Mathlib.CategoryTheory.Idempotents.Karoubi + +namespace CategoryTheory + +variable (C : Type _) [Category C] + +structure Karoubi where + X : C + p : X ⟶ X + +namespace Karoubi + +variable {C} + +structure Hom (P Q : Karoubi C) where + f : P.X ⟶ Q.X + comm : f = P.p ≫ f ≫ Q.p + +theorem p_comp {P Q : Karoubi C} (f : Hom P Q) : P.p ≫ f.f = f.f := sorry + +theorem comp_p {P Q : Karoubi C} (f : Hom P Q) : f.f ≫ Q.p = f.f := sorry + +/-- The category structure on the karoubi envelope of a category. -/ +instance : Category (Karoubi C) where + Hom := Karoubi.Hom + id P := ⟨P.p, sorry⟩ + comp f g := ⟨f.f ≫ g.f, sorry⟩ + comp_id := sorry + id_comp := sorry + +@[simp] +theorem hom_ext_iff {P Q : Karoubi C} {f g : P ⟶ Q} : f = g ↔ f.f = g.f := sorry + +@[ext] +theorem hom_ext {P Q : Karoubi C} (f g : P ⟶ Q) (h : f.f = g.f) : f = g := sorry + +@[simp] +theorem comp_f {P Q R : Karoubi C} (f : P ⟶ Q) (g : Q ⟶ R) : (f ≫ g).f = f.f ≫ g.f := rfl + +@[simp] +theorem id_f {P : Karoubi C} : Hom.f (𝟙 P) = P.p := rfl + +end Karoubi + +def toKaroubi : C ⥤ Karoubi C where + obj X := ⟨X, 𝟙 X⟩ + map f := ⟨f, sorry⟩ + +@[simp] theorem toKaroubi_obj_X (X : C) : ((toKaroubi C).obj X).X = X := rfl +@[simp] theorem toKaroubi_obj_p (X : C) : ((toKaroubi C).obj X).p = 𝟙 X := rfl +@[simp] theorem toKaroubi_map_f {X Y : C} (f : X ⟶ Y) : ((toKaroubi C).map f).f = f := rfl + +end CategoryTheory + +end Mathlib.CategoryTheory.Idempotents.Karoubi + +section Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi + +open CategoryTheory.Category +open CategoryTheory.Karoubi + +namespace CategoryTheory +namespace Idempotents + +variable (C : Type _) [Category C] + +theorem idem_f (P : Karoubi (Karoubi C)) : P.p.f ≫ P.p.f = P.p.f := sorry + +theorem p_comm_f {P Q : Karoubi (Karoubi C)} (f : P ⟶ Q) : P.p.f ≫ f.f.f = f.f.f ≫ Q.p.f := sorry + +def inverse : Karoubi (Karoubi C) ⥤ Karoubi C where + obj P := ⟨P.X.X, P.p.f⟩ + map f := ⟨f.f.f, sorry⟩ + +theorem inverse_obj_X (P : Karoubi (Karoubi C)) : ((inverse C).obj P).X = P.X.X := rfl +theorem inverse_obj_p (P : Karoubi (Karoubi C)) : ((inverse C).obj P).p = P.p.f := rfl +theorem inverse_map_f {X Y : Karoubi (Karoubi C)} (f : X ⟶ Y) : ((inverse C).map f).f = f.f.f := rfl + +-- In the original source this is just +-- ``` +-- def counitIso : inverse C ⋙ toKaroubi (Karoubi C) ≅ 𝟭 (Karoubi (Karoubi C)) where +-- hom := { app := fun P => { f := { f := P.p.1 } } } +-- inv := { app := fun P => { f := { f := P.p.1 } } } +-- ``` +-- but I've maximally expanded out the autoparams: +-- it seems the slow down is in the `simp only` tactics, not the automation that finds them. + +def counitIso : inverse C ⋙ toKaroubi (Karoubi C) ≅ 𝟭 (Karoubi (Karoubi C)) where + hom := + { app := fun P => + { f := + { f := P.p.1 + comm := by simp only [Functor.comp_obj, toKaroubi_obj_X, inverse_obj_X, + Functor.id_obj, inverse_obj_p, comp_p, idem_f] } + comm := by simp only [Functor.comp_obj, toKaroubi_obj_X, Functor.id_obj, toKaroubi_obj_p, + Karoubi.id_f, inverse_obj_p, hom_ext_iff, inverse_obj_X, comp_f, idem_f] } + naturality := by + intro X Y f + simp only [Functor.comp_obj, Functor.id_obj, Functor.comp_map, toKaroubi_obj_X, + Functor.id_map, hom_ext_iff, comp_f, toKaroubi_map_f, inverse_obj_X, inverse_map_f, + p_comm_f] } + inv := + { app := fun P => + { f := + { f := P.p.1 + comm := by simp only [Functor.id_obj, Functor.comp_obj, toKaroubi_obj_X, + inverse_obj_X, inverse_obj_p, idem_f, p_comp] } + comm := by simp only [Functor.id_obj, Functor.comp_obj, toKaroubi_obj_X, toKaroubi_obj_p, + Karoubi.id_f, inverse_obj_p, hom_ext_iff, inverse_obj_X, comp_f, idem_f] } + naturality := by + intro X Y f + simp only [Functor.id_obj, Functor.comp_obj, Functor.id_map, toKaroubi_obj_X, + Functor.comp_map, hom_ext_iff, comp_f, toKaroubi_map_f, inverse_obj_X, inverse_map_f, + p_comm_f] + } + hom_inv_id := by + simp only [Functor.comp_obj, Functor.id_obj, toKaroubi_obj_X] + ext x : 4 + simp only [Functor.comp_obj, toKaroubi_obj_X, inverse_obj_X, NatTrans.comp_app, + Functor.id_obj, comp_f, idem_f, NatTrans.id_app, Karoubi.id_f, toKaroubi_obj_p, + inverse_obj_p] + inv_hom_id := by + simp only [Functor.id_obj, Functor.comp_obj, toKaroubi_obj_X] + ext x : 4 + simp only [Functor.id_obj, NatTrans.comp_app, Functor.comp_obj, comp_f, toKaroubi_obj_X, + inverse_obj_X, idem_f, NatTrans.id_app, Karoubi.id_f] diff --git a/tests/lean/run/4595_split.lean b/tests/lean/run/4595_split.lean new file mode 100644 index 0000000000..f973999212 --- /dev/null +++ b/tests/lean/run/4595_split.lean @@ -0,0 +1,13 @@ +example {P} [Decidable P] {f g : Nat → Nat} {x : Nat} : (if P then f else g) x = 37 := by + split + · guard_target =ₛ f x = 37 + sorry + · guard_target =ₛ g x = 37 + sorry + +example {P} [Decidable P] {f g : Nat → Nat} {x : Nat} {b : Bool} : (match b with | true => f | false => g) x = 37 := by + split + · guard_target =ₛ f x = 37 + sorry + · guard_target =ₛ g x = 37 + sorry diff --git a/tests/lean/run/implicitRflProofs.lean b/tests/lean/run/implicitRflProofs.lean new file mode 100644 index 0000000000..aecadfbb8c --- /dev/null +++ b/tests/lean/run/implicitRflProofs.lean @@ -0,0 +1,25 @@ +def f (x : Nat) := x + 1 + +theorem f_eq (x : Nat) : f (x + 1) = x + 2 := rfl + +theorem ex1 : f (f (x + 1)) = x + 3 := by + simp -implicitDefEqProofs [f_eq] + +/-- +info: theorem ex1 : ∀ {x : Nat}, f (f (x + 1)) = x + 3 := +fun {x} => + of_eq_true + (Eq.trans (congrArg (fun x_1 => x_1 = x + 3) (Eq.trans (congrArg f (f_eq x)) (f_eq (x + 1)))) (eq_self (x + 1 + 2))) +-/ +#guard_msgs in +#print ex1 + +theorem ex2 : f (f (x + 1)) = x + 3 := by + simp +implicitDefEqProofs [f_eq] + +/-- +info: theorem ex2 : ∀ {x : Nat}, f (f (x + 1)) = x + 3 := +fun {x} => of_eq_true (eq_self (x + 1 + 2)) +-/ +#guard_msgs in +#print ex2 diff --git a/tests/lean/run/simp2.lean b/tests/lean/run/simp2.lean index 89f82bdda3..4a91608e09 100644 --- a/tests/lean/run/simp2.lean +++ b/tests/lean/run/simp2.lean @@ -4,7 +4,7 @@ def p (x : Prop) := x rfl theorem ex1 (x : Prop) (h : x) : p x := by - simp + simp +implicitDefEqProofs assumption /-- @@ -14,6 +14,17 @@ fun x h => id h #guard_msgs in #print ex1 +theorem ex1' (x : Prop) (h : x) : p x := by + simp -implicitDefEqProofs + assumption + +/-- +info: theorem ex1' : ∀ (x : Prop), x → p x := +fun x h => Eq.mpr (id (lemma1 x)) h +-/ +#guard_msgs in +#print ex1' + theorem ex2 (x : Prop) (q : Prop → Prop) (h₁ : x) (h₂ : q x = x) : q x := by simp [h₂] assumption diff --git a/tests/lean/run/simp5.lean b/tests/lean/run/simp5.lean index c2163c98aa..5d77b52d00 100644 --- a/tests/lean/run/simp5.lean +++ b/tests/lean/run/simp5.lean @@ -4,15 +4,27 @@ theorem f_Eq {α} (a b : α) : f a b = a := rfl theorem ex1 (a b c : α) : f (f a b) c = a := by - simp [f_Eq] + simp -implicitDefEqProofs [f_Eq] /-- info: theorem ex1.{u_1} : ∀ {α : Sort u_1} (a b c : α), f (f a b) c = a := -fun {α} a b c => of_eq_true (eq_self a) +fun {α} a b c => + of_eq_true + (Eq.trans (congrArg (fun x => x = a) (Eq.trans (congrArg (fun x => f x c) (f_Eq a b)) (f_Eq a c))) (eq_self a)) -/ #guard_msgs in #print ex1 +theorem ex1' (a b c : α) : f (f a b) c = a := by + simp +implicitDefEqProofs [f_Eq] + +/-- +info: theorem ex1'.{u_1} : ∀ {α : Sort u_1} (a b c : α), f (f a b) c = a := +fun {α} a b c => of_eq_true (eq_self a) +-/ +#guard_msgs in +#print ex1' + theorem ex2 (p : Nat → Bool) (x : Nat) (h : p x = true) : (if p x then 1 else 2) = 1 := by simp [h] diff --git a/tests/lean/run/splitIssue2.lean b/tests/lean/run/splitIssue2.lean new file mode 100644 index 0000000000..b35c1c122b --- /dev/null +++ b/tests/lean/run/splitIssue2.lean @@ -0,0 +1,71 @@ +namespace Batteries + +/-- Union-find node type -/ +structure UFNode where + /-- Parent of node -/ + parent : Nat + +namespace UnionFind + +/-- Parent of a union-find node, defaults to self when the node is a root -/ +def parentD (arr : Array UFNode) (i : Nat) : Nat := + if h : i < arr.size then (arr.get i h).parent else i + +/-- Rank of a union-find node, defaults to 0 when the node is a root -/ +def rankD (arr : Array UFNode) (i : Nat) : Nat := 0 + +theorem parentD_of_not_lt : ¬i < arr.size → parentD arr i = i := sorry + +theorem parentD_set {arr : Array UFNode} {x h v i} : + parentD (arr.set x v h) i = if x = i then v.parent else parentD arr i := by + rw [parentD] + sorry + +end UnionFind + +open UnionFind + +structure UnionFind where + arr : Array UFNode + +namespace UnionFind + +/-- Size of union-find structure. -/ +@[inline] abbrev size (self : UnionFind) := self.arr.size + +/-- Parent of union-find node -/ +abbrev parent (self : UnionFind) (i : Nat) : Nat := parentD self.arr i + +theorem parent_lt (self : UnionFind) (i : Nat) : self.parent i < self.size ↔ i < self.size := + sorry + +/-- Rank of union-find node -/ +abbrev rank (self : UnionFind) (i : Nat) : Nat := rankD self.arr i + +/-- Maximum rank of nodes in a union-find structure -/ +noncomputable def rankMax (self : UnionFind) := 0 + +/-- Root of a union-find node. -/ +def root (self : UnionFind) (x : Fin self.size) : Fin self.size := + let y := (self.arr.get x.1 x.2).parent + if h : y = x then + x + else + have : self.rankMax - self.rank (self.arr.get x.1 x.2).parent < self.rankMax - self.rank x := + sorry + self.root ⟨y, sorry⟩ +termination_by self.rankMax - self.rank x + +/-- Root of a union-find node. Returns input if index is out of bounds. -/ +def rootD (self : UnionFind) (x : Nat) : Nat := + if h : x < self.size then self.root ⟨x, h⟩ else x + +theorem rootD_parent (self : UnionFind) (x : Nat) : self.rootD (self.parent x) = self.rootD x := by + simp only [rootD, Array.length_toList, parent_lt] + split + · simp only [parentD, ↓reduceDIte, *] + conv => rhs; rw [root] + split + · rw [root, dif_pos] <;> simp_all + · simp + · simp only [not_false_eq_true, parentD_of_not_lt, *] diff --git a/tests/lean/run/splitOrderIssue.lean b/tests/lean/run/splitOrderIssue.lean new file mode 100644 index 0000000000..457b31a551 --- /dev/null +++ b/tests/lean/run/splitOrderIssue.lean @@ -0,0 +1,10 @@ +example (b : Bool) : (if (if b then true else true) then 1 else 2) = 1 := by + split + next h => + guard_target =ₛ (if true = true then 1 else 2) = 1 + guard_hyp h : b = true + simp + next h => + guard_target =ₛ (if true = true then 1 else 2) = 1 + guard_hyp h : ¬b = true + simp