feat: track permutation simp lemmas

src/Lean/Meta/Tactic/Simp/SimpLemmas.lean

@@ -5,22 +5,28 @@ Authors: Leonardo de Moura
 -/
 import Lean.ScopedEnvExtension
 import Lean.Util.Recognizers
-import Lean.Meta.Basic
+import Lean.Meta.LevelDefEq
 import Lean.Meta.DiscrTree
 
 namespace Lean.Meta
 
 structure SimpLemma where
-  keys        : Array DiscrTree.Key
-  val         : Expr
-  priority    : Nat
-  globalName? : Option Name := none
+  keys     : Array DiscrTree.Key
+  val      : Expr
+  priority : Nat
+  perm     : Bool -- true is lhs and rhs are identical modulo permutation of variables
+  name?    : Option Name := none -- for debugging and tracing purposes
   deriving Inhabited
 
 instance : ToFormat SimpLemma where
-  format s := match s.globalName? with
-    | some n => fmt n
-    | none   => "<local>"
+  format s :=
+    let perm := if s.perm then ":perm" else ""
+    let name :=
+      match s.name? with
+      | some n => fmt n
+      | none   => "<unknown>"
+    let prio := f!":{s.priority}"
+    name ++ prio ++ perm
 
 instance : BEq SimpLemma where
   beq e₁ e₂ := e₁.val == e₂.val
@@ -39,31 +45,45 @@ builtin_initialize simpExtension : SimpleScopedEnvExtension SimpLemma SimpLemmas
     addEntry := addSimpLemmaEntry
   }
 
-private def mkSimpLemmaKey (e : Expr) : MetaM (Array DiscrTree.Key) := do
+private partial def isPerm : Expr → Expr → MetaM Bool
+  | Expr.app f₁ a₁ _, Expr.app f₂ a₂ _ => isPerm f₁ f₂ <&&> isPerm a₁ a₂
+  | Expr.mdata _ s _, t => isPerm s t
+  | s, Expr.mdata _ t _ => isPerm s t
+  | s@(Expr.mvar ..), t@(Expr.mvar ..) => isDefEq s t
+  | Expr.forallE n₁ d₁ b₁ _, Expr.forallE n₂ d₂ b₂ _ => isPerm d₁ d₂ <&&> withLocalDeclD n₁ d₁ fun x => isPerm (b₁.instantiate1 x) (b₂.instantiate1 x)
+  | Expr.lam n₁ d₁ b₁ _, Expr.lam n₂ d₂ b₂ _ => isPerm d₁ d₂ <&&> withLocalDeclD n₁ d₁ fun x => isPerm (b₁.instantiate1 x) (b₂.instantiate1 x)
+  | Expr.letE n₁ t₁ v₁ b₁ _, Expr.letE n₂ t₂ v₂ b₂ _ =>
+    isPerm t₁ t₂ <&&> isPerm v₁ v₂ <&&> withLetDecl n₁ t₁ v₁ fun x => isPerm (b₁.instantiate1 x) (b₂.instantiate1 x)
+  | Expr.proj _ i₁ b₁ _, Expr.proj _ i₂ b₂ _ => i₁ == i₂ <&&> isPerm b₁ b₂
+  | s, t => s == t
+
+def mkSimpLemmaCore (e : Expr) (val : Expr) (prio : Nat) (name? : Option Name) : MetaM SimpLemma := do
   let type ← inferType e
   unless (← isProp type) do
     throwError! "invalid 'simp', proposition expected{indentExpr type}"
   withNewMCtxDepth do
     let (xs, _, type) ← forallMetaTelescopeReducing type
-    match type.eq? with
-    | some (_, lhs, _) => DiscrTree.mkPath lhs
-    | none =>
-    match type.iff? with
-    | some (lhs, _) => DiscrTree.mkPath lhs
-    | none =>
-      if type.isConstOf `False then
-        if xs.size == 0 then
-          throwError! "invalid 'simp', unexpected type{indentExpr type}"
+    let (keys, perm) ←
+      match type.eq? with
+      | some (_, lhs, rhs) => pure (← DiscrTree.mkPath lhs, ← isPerm lhs rhs)
+      | none =>
+      match type.iff? with
+      | some (lhs, rhs) => pure (← DiscrTree.mkPath lhs, ← isPerm lhs rhs)
+      | none =>
+        if type.isConstOf `False then
+          if xs.size == 0 then
+            throwError! "invalid 'simp', unexpected type{indentExpr type}"
+          else
+            pure (← DiscrTree.mkPath (← inferType xs.back), false)
         else
-          DiscrTree.mkPath (← inferType xs.back)
-      else
-        DiscrTree.mkPath type
+          pure (← DiscrTree.mkPath type, false)
+    return { keys := keys, perm := perm, val := val, name? := name?, priority := prio }
 
 def addSimpLemma (declName : Name) (attrKind : AttributeKind) (prio : Nat) : MetaM Unit := do
   let cinfo ← getConstInfo declName
-  let c := mkConst declName (cinfo.lparams.map mkLevelParam)
-  let keys ← mkSimpLemmaKey c
-  simpExtension.add { keys := keys, val := c, priority := prio, globalName? := declName } attrKind
+  /- The `simp` tactic uses fresh universe metavariables when using a global simp lemma. -/
+  let lemma ← mkSimpLemmaCore (mkConst declName (cinfo.lparams.map mkLevelParam)) (mkConst declName) prio declName
+  simpExtension.add lemma attrKind
   pure ()
 
 builtin_initialize
@@ -78,4 +98,13 @@ builtin_initialize
 def getSimpLemmas : MetaM (DiscrTree SimpLemma) :=
   return simpExtension.getState (← getEnv) |>.discrTree
 
+/- Auxiliary method for creating a local simp lemma. -/
+def mkSimpLemma (e : Expr) (prio : Nat := evalPrio! default) (name? : Option Name := none) : MetaM SimpLemma := do
+  mkSimpLemmaCore e e prio name?
+
+/- Auxiliary method for adding a local simp lemma to a `SimpLemmas` datastructure. -/
+def SimpLemmas.add (s : SimpLemmas) (e : Expr) (prio : Nat := evalPrio! default) (name? : Option Name := none) : MetaM SimpLemmas := do
+  let lemma ← mkSimpLemma e prio name?
+  return addSimpLemmaEntry s lemma
+
 end Lean.Meta

tests/lean/run/simp1.lean

@@ -15,6 +15,12 @@ import Lean
 @[simp] theorem ex4 (xs : List α) : ¬(x :: xs = []) :=
   sorry
 
+@[simp] theorem ex6 (p q : Prop) : p ∨ q ↔ q ∨ p:=
+  sorry
+
+@[simp] theorem ex7 [Add α] (a b : α) : a + b = b + a :=
+  sorry
+
 axiom aux {α} (f : List α → List α) (xs ys : List α) : f (xs ++ ys) ++ [] = f (xs ++ ys)
 
 open Lean