From bc9b814858c934f4f8b14f373825cce93ecd832d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 18 Dec 2024 07:19:29 +0100 Subject: [PATCH] feat: reserved names for congruence theorems (#6412) This PR adds reserved names for congruence theorems used in the simplifier and `grind` tactics. The idea is prevent the same congruence theorems to be generated over and over again. After update stage0, we must use the new API in the simplifier. --- src/Lean/Meta/CongrTheorems.lean | 90 ++++++++++++++++++++++++++++++- tests/lean/run/congrReserved.lean | 40 ++++++++++++++ 2 files changed, 129 insertions(+), 1 deletion(-) create mode 100644 tests/lean/run/congrReserved.lean diff --git a/src/Lean/Meta/CongrTheorems.lean b/src/Lean/Meta/CongrTheorems.lean index e517f9a64d..bd38f0911a 100644 --- a/src/Lean/Meta/CongrTheorems.lean +++ b/src/Lean/Meta/CongrTheorems.lean @@ -4,6 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude +import Lean.AddDecl +import Lean.ReservedNameAction +import Lean.ResolveName import Lean.Meta.AppBuilder import Lean.Class @@ -32,7 +35,7 @@ inductive CongrArgKind where For congr-simp theorems only. Indicates a decidable instance argument. The lemma contains two arguments [a_i : Decidable ...] [b_i : Decidable ...] -/ | subsingletonInst - deriving Inhabited, Repr + deriving Inhabited, Repr, BEq structure CongrTheorem where type : Expr @@ -352,4 +355,89 @@ def mkCongrSimp? (f : Expr) (subsingletonInstImplicitRhs : Bool := true) : MetaM let info ← getFunInfo f mkCongrSimpCore? f info (← getCongrSimpKinds f info) (subsingletonInstImplicitRhs := subsingletonInstImplicitRhs) +def hcongrThmSuffixBase := "hcongr" +def hcongrThmSuffixBasePrefix := hcongrThmSuffixBase ++ "_" + +/-- Returns `true` if `s` is of the form `hcongr_` -/ +def isHCongrReservedNameSuffix (s : String) : Bool := + hcongrThmSuffixBasePrefix.isPrefixOf s && (s.drop 7).isNat + +def congrSimpSuffix := "congr_simp" + +builtin_initialize congrKindsExt : MapDeclarationExtension (Array CongrArgKind) ← mkMapDeclarationExtension + +builtin_initialize registerReservedNamePredicate fun env n => + match n with + | .str p s => (isHCongrReservedNameSuffix s || s == congrSimpSuffix) && env.isSafeDefinition p + | _ => false + +builtin_initialize + registerReservedNameAction fun name => do + let .str p s := name | return false + unless (← getEnv).isSafeDefinition p do return false + if isHCongrReservedNameSuffix s then + let numArgs := (s.drop 7).toNat! + try MetaM.run' do + let info ← getConstInfo p + let f := mkConst p (info.levelParams.map mkLevelParam) + let congrThm ← mkHCongrWithArity f numArgs + addDecl <| Declaration.thmDecl { + name, type := congrThm.type, value := congrThm.proof + levelParams := info.levelParams + } + modifyEnv fun env => congrKindsExt.insert env name congrThm.argKinds + return true + catch _ => return false + else if s == congrSimpSuffix then + try MetaM.run' do + let cinfo ← getConstInfo p + let f := mkConst p (cinfo.levelParams.map mkLevelParam) + let info ← getFunInfo f + let some congrThm ← mkCongrSimpCore? f info (← getCongrSimpKinds f info) + | return false + addDecl <| Declaration.thmDecl { + name, type := congrThm.type, value := congrThm.proof + levelParams := cinfo.levelParams + } + modifyEnv fun env => congrKindsExt.insert env name congrThm.argKinds + return true + catch _ => return false + else + return false + +/-- +Similar to `mkHCongrWithArity`, but uses reserved names to ensure we don't keep creating the +same congruence theorem over and over again. +-/ +def mkHCongrWithArityForConst? (declName : Name) (levels : List Level) (numArgs : Nat) : MetaM (Option CongrTheorem) := do + try + let suffix := hcongrThmSuffixBasePrefix ++ toString numArgs + let thmName := Name.str declName suffix + unless (← getEnv).contains thmName do + executeReservedNameAction thmName + let proof := mkConst thmName levels + let type ← inferType proof + let some argKinds := congrKindsExt.getState (← getEnv) |>.find? thmName + | unreachable! + return some { proof, type, argKinds } + catch _ => + return none + +/-- +Similar to `mkCongrSimp?`, but uses reserved names to ensure we don't keep creating the +same congruence theorem over and over again. +-/ +def mkCongrSimpForConst? (declName : Name) (levels : List Level) : MetaM (Option CongrTheorem) := do + try + let thmName := Name.str declName congrSimpSuffix + unless (← getEnv).contains thmName do + executeReservedNameAction thmName + let proof := mkConst thmName levels + let type ← inferType proof + let some argKinds := congrKindsExt.getState (← getEnv) |>.find? thmName + | unreachable! + return some { proof, type, argKinds } + catch _ => + return none + end Lean.Meta diff --git a/tests/lean/run/congrReserved.lean b/tests/lean/run/congrReserved.lean new file mode 100644 index 0000000000..563d80786e --- /dev/null +++ b/tests/lean/run/congrReserved.lean @@ -0,0 +1,40 @@ +import Lean + +/-- +info: Vector.extract.hcongr_5.{u_1} (α α' : Type u_1) (e_1 : α = α') (n n' : Nat) (e_2 : n = n') (v : Vector α n) + (v' : Vector α' n') (e_3 : HEq v v') (start start' : Nat) (e_4 : start = start') (stop stop' : Nat) + (e_5 : stop = stop') : HEq (v.extract start stop) (v'.extract start' stop') +-/ +#guard_msgs in +#check Vector.extract.hcongr_5 + +/-- +info: Vector.extract.congr_simp.{u_1} {α : Type u_1} {n : Nat} (v v✝ : Vector α n) (e_v : v = v✝) (start stop : Nat) : + v.extract start stop = v✝.extract start stop +-/ +#guard_msgs in +#check Vector.extract.congr_simp + +open Lean Meta + +/-- +info: @Vector.extract.congr_simp +-/ +#guard_msgs in +run_meta do + let some thm1 ← mkCongrSimpForConst? ``Vector.extract [0] | unreachable! + IO.println (← ppExpr thm1.proof) + let some thm2 ← mkCongrSimp? (mkConst ``Vector.extract [0]) | unreachable! + assert! thm1.type == thm2.type + assert! thm1.argKinds == thm2.argKinds + +/-- +info: Vector.extract.hcongr_5 +-/ +#guard_msgs in +run_meta do + let some thm1 ← mkHCongrWithArityForConst? ``Vector.extract [0] 5 | unreachable! + IO.println (← ppExpr thm1.proof) + let thm2 ← mkHCongrWithArity (mkConst ``Vector.extract [0]) 5 + assert! thm1.type == thm2.type + assert! thm1.argKinds == thm2.argKinds