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

@@ -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_<idx>` -/
+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

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