fix: simp: check permutation based on theorem statement

This reverts commit 98922b878a.

src/Lean/Meta/ACLt.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 import Lean.Meta.Basic
 import Lean.Meta.FunInfo
-import Lean.Meta.DiscrTree
 
 namespace Lean
 
@@ -26,11 +25,6 @@ def Expr.ctorWeight : Expr → UInt8
 namespace Meta
 namespace ACLt
 
-inductive ReduceMode where
-  | reduce
-  | reduceSimpleOnly
-  | none
-
 mutual
 
 /--
@@ -49,26 +43,17 @@ mutual
    - We ignore metadata.
    - We ignore universe parameterst at constants.
 -/
-unsafe def main (a b : Expr) (mode : ReduceMode := .none) : MetaM Bool :=
-  lt a b
+unsafe def lt (a b : Expr) : MetaM Bool :=
+  if ptrAddrUnsafe a == ptrAddrUnsafe b then
+    return false
+  -- We ignore metadata
+  else if a.isMData then
+    lt a.mdataExpr! b
+  else if b.isMData then
+    lt a b.mdataExpr!
+  else
+    lpo a b
 where
-  reduce (e : Expr) : MetaM Expr :=
-    match mode with
-    | .reduce => DiscrTree.reduce e (simpleReduce := false)
-    | .reduceSimpleOnly => DiscrTree.reduce e (simpleReduce := true)
-    | .none => return e
-
-  lt (a b : Expr) : MetaM Bool := do
-    if ptrAddrUnsafe a == ptrAddrUnsafe b then
-      return false
-    -- We ignore metadata
-    else if a.isMData then
-      lt a.mdataExpr! b
-    else if b.isMData then
-      lt a b.mdataExpr!
-    else
-      lpo (← reduce a) (← reduce b)
-
   ltPair (a₁ a₂ b₁ b₂ : Expr) : MetaM Bool := do
     if (← lt a₁ b₁) then
       return true
@@ -110,25 +95,25 @@ where
   lexSameCtor (a b : Expr) : MetaM Bool :=
     match a with
     -- Atomic
-    | .bvar i ..    => return i < b.bvarIdx!
-    | .fvar id ..   => return Name.lt id.name b.fvarId!.name
-    | .mvar id ..   => return Name.lt id.name b.mvarId!.name
-    | .sort u ..    => return Level.normLt u b.sortLevel!
-    | .const n ..   => return Name.lt n b.constName! -- We igore the levels
-    | .lit v ..     => return Literal.lt v b.litValue!
+    | Expr.bvar i ..    => return i < b.bvarIdx!
+    | Expr.fvar id ..   => return Name.lt id.name b.fvarId!.name
+    | Expr.mvar id ..   => return Name.lt id.name b.mvarId!.name
+    | Expr.sort u ..    => return Level.normLt u b.sortLevel!
+    | Expr.const n ..   => return Name.lt n b.constName! -- We igore the levels
+    | Expr.lit v ..     => return Literal.lt v b.litValue!
     -- Composite
-    | .proj _ i e ..    => if i != b.projIdx! then return i < b.projIdx! else lt e b.projExpr!
-    | .app ..           => ltApp a b
-    | .lam _ d e ..     => ltPair d e b.bindingDomain! b.bindingBody!
-    | .forallE _ d e .. => ltPair d e b.bindingDomain! b.bindingBody!
-    | .letE _ _ v e ..  => ltPair v e b.letValue! b.letBody!
+    | Expr.proj _ i e ..    => if i != b.projIdx! then return i < b.projIdx! else lt e b.projExpr!
+    | Expr.app ..           => ltApp a b
+    | Expr.lam _ d e ..     => ltPair d e b.bindingDomain! b.bindingBody!
+    | Expr.forallE _ d e .. => ltPair d e b.bindingDomain! b.bindingBody!
+    | Expr.letE _ _ v e ..  => ltPair v e b.letValue! b.letBody!
     -- See main function
-    | .mdata ..         => unreachable!
+    | Expr.mdata ..         => unreachable!
 
   allChildrenLt (a b : Expr) : MetaM Bool :=
     match a with
-    | .proj _ _ e ..    => lt e b
-    | .app ..           =>
+    | Expr.proj _ _ e ..    => lt e b
+    | Expr.app ..           =>
       a.withApp fun f args => do
         let infos := (← getFunInfoNArgs f args.size).paramInfo
         for i in [:infos.size] do
@@ -140,9 +125,9 @@ where
           if !(← lt args[i]! b) then
             return false
         return true
-    | .lam _ d e ..     => lt d b <&&> lt e b
-    | .forallE _ d e .. => lt d b <&&> lt e b
-    | .letE _ _ v e ..  => lt v b <&&> lt e b
+    | Expr.lam _ d e ..     => lt d b <&&> lt e b
+    | Expr.forallE _ d e .. => lt d b <&&> lt e b
+    | Expr.letE _ _ v e ..  => lt v b <&&> lt e b
     | _ => return true
 
   someChildGe (a b : Expr) : MetaM Bool :=
@@ -169,7 +154,7 @@ end
 
 end ACLt
 
-@[implemented_by ACLt.main, inherit_doc ACLt.main]
-opaque Expr.acLt : Expr → Expr → (mode : ACLt.ReduceMode := .none) → MetaM Bool
+@[implemented_by ACLt.lt]
+opaque Expr.acLt : Expr → Expr → MetaM Bool
 
 end Lean.Meta

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

@@ -69,12 +69,9 @@ private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInf
       if e == rhs then
         return none
       if thm.perm then
-        /-
-        We use `.reduceSimpleOnly` because this is how we indexed the discrimination tree.
-        See issue #1815
-        -/
-        if !(← Expr.acLt rhs e .reduceSimpleOnly) then
-          trace[Meta.Tactic.simp.rewrite] "{← ppSimpTheorem thm}, perm rejected {e} ==> {rhs}"
+        let lhs ← instantiateMVars lhs
+        if !(← Expr.acLt rhs lhs) then
+          trace[Meta.Tactic.simp.rewrite] "{← ppSimpTheorem thm}, perm rejected {lhs} ==> {rhs}"
           return none
       trace[Meta.Tactic.simp.rewrite] "{← ppSimpTheorem thm}, {e} ==> {rhs}"
       recordSimpTheorem thm.origin

tests/lean/run/1842.lean

@@ -0,0 +1,16 @@
+variable (R : α → α → Prop)
+
+inductive List.Pairwise : List α → Prop
+  | nil : Pairwise []
+  | cons : ∀ {a : α} {l : List α}, (∀ {a} (_ : a' ∈ l), R a a') → Pairwise l → Pairwise (a :: l)
+
+theorem and_assoc : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) :=
+  ⟨fun ⟨⟨ha, hb⟩, hc⟩ => ⟨ha, hb, hc⟩, fun ⟨ha, hb, hc⟩ => ⟨⟨ha, hb⟩, hc⟩⟩
+
+theorem and_left_comm : a ∧ (b ∧ c) ↔ b ∧ (a ∧ c) := by
+  rw [← and_assoc, ← and_assoc, @And.comm a b]
+  exact Iff.rfl
+
+theorem pairwise_append {l₁ l₂ : List α} :
+    (l₁ ++ l₂).Pairwise R ↔ l₁.Pairwise R ∧ l₂.Pairwise R ∧ ∀ {a} (_ : a ∈ l₁), ∀ {b} (_ : b ∈ l₂), R a b := by
+  induction l₁ <;> simp [*, and_left_comm] <;> sorry