chore: cleanup superposeAC?

This PR ensures `superposeAC?` and `superpose?` have similar signatures.

src/Init/Grind/AC.lean

@@ -485,26 +485,26 @@ theorem diseq_simp_rhs_ac {α} (ctx : Context α) {inst₁ : Std.Associative ctx
     : simp_ac_cert c lhs₁ rhs₁ rhs₂ rhs₂' → lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx ≠ rhs₂.denote ctx → lhs₂.denote ctx ≠ rhs₂'.denote ctx := by
   simp [simp_ac_cert]; intros; subst rhs₂ rhs₂'; simp_all
 
-noncomputable def superpose_ac_cert (a b c lhs₁ rhs₁ lhs₂ rhs₂ lhs rhs : Seq) : Bool :=
-  lhs₁.beq' (c.union_k a) |>.and'
-  (lhs₂.beq' (c.union_k b)) |>.and'
-  (lhs.beq' (b.union_k rhs₁)) |>.and'
-  (rhs.beq' (a.union_k rhs₂))
+noncomputable def superpose_ac_cert (r₁ c r₂ lhs₁ rhs₁ lhs₂ rhs₂ lhs rhs : Seq) : Bool :=
+  lhs₁.beq' (c.union_k r₁) |>.and'
+  (lhs₂.beq' (c.union_k r₂)) |>.and'
+  (lhs.beq' (r₂.union_k rhs₁)) |>.and'
+  (rhs.beq' (r₁.union_k rhs₂))
 
 /--
-Given `lhs₁ = rhs₁` and `lhs₂ = rhs₂` where `lhs₁ := union c a` and `lhs₂ := union c b`,
-`lhs = rhs` where `lhs := union b rhs₁` and `rhs := union a rhs₂`
+Given `lhs₁ = rhs₁` and `lhs₂ = rhs₂` where `lhs₁ := union c r₁` and `lhs₂ := union c r₂`,
+`lhs = rhs` where `lhs := union r₂ rhs₁` and `rhs := union r₁ rhs₂`
 -/
-theorem superpose_ac {α} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op}  (a b c lhs₁ rhs₁ lhs₂ rhs₂ lhs rhs : Seq)
-    : superpose_ac_cert a b c lhs₁ rhs₁ lhs₂ rhs₂ lhs rhs → lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx = rhs₂.denote ctx
+theorem superpose_ac {α} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op}  (r₁ c r₂ lhs₁ rhs₁ lhs₂ rhs₂ lhs rhs : Seq)
+    : superpose_ac_cert r₁ c r₂ lhs₁ rhs₁ lhs₂ rhs₂ lhs rhs → lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx = rhs₂.denote ctx
       → lhs.denote ctx = rhs.denote ctx := by
   simp [superpose_ac_cert]; intro _ _ _ _; subst lhs₁ lhs₂ lhs rhs; simp
   intro h₁ h₂; simp [← h₁, ← h₂]
-  rw [← Std.Associative.assoc (self := inst₁), Std.Commutative.comm (self := inst₂) (b.denote ctx)]
-  rw [← Std.Associative.assoc (self := inst₁), Std.Commutative.comm (self := inst₂) (a.denote ctx)]
+  rw [← Std.Associative.assoc (self := inst₁), Std.Commutative.comm (self := inst₂) (r₂.denote ctx)]
+  rw [← Std.Associative.assoc (self := inst₁), Std.Commutative.comm (self := inst₂) (r₁.denote ctx)]
   simp [Std.Associative.assoc (self := inst₁)]
   apply congrArg (ctx.op (c.denote ctx))
-  rw [Std.Commutative.comm (self := inst₂) (b.denote ctx)]
+  rw [Std.Commutative.comm (self := inst₂) (r₂.denote ctx)]
 
 noncomputable def eq_norm_a_cert (lhs rhs : Expr) (lhs' rhs' : Seq) : Bool :=
   lhs.toSeq.beq' lhs' |>.and' (rhs.toSeq.beq' rhs')

src/Lean/Meta/Tactic/Grind/AC/Eq.lean

@@ -227,11 +227,11 @@ private def EqCnstr.superposeWithAC (c₁ : EqCnstr) : ACM Unit := do
     trace[grind.debug.ac.superpose] "[{lhs₁.sharesVar lhs₂}]: {← lhs₁.denoteExpr}, {← lhs₂.denoteExpr}"
     if lhs₁.sharesVar lhs₂ then
       assert! lhs₁ != lhs₂
-      let (some s, some s₁, some s₂) := lhs₁.superposeAC lhs₂ | unreachable!
+      let some (r₁, c, r₂) := lhs₁.superposeAC? lhs₂ | unreachable!
       if grind.debug.get (← getOptions) then
-        assert! lhs₁ == s₂.union s
-        assert! lhs₂ == s₁.union s
-      let c ← mkEqCnstr (c₁.rhs.union s₁) (c₂.rhs.union s₂) (.superpose_ac s s₁ s₂ c₁ c₂)
+        assert! lhs₁ == r₁.union c
+        assert! lhs₂ == r₂.union c
+      let c ← mkEqCnstr (c₁.rhs.union r₂) (c₂.rhs.union r₁) (.superpose_ac r₁ c r₂ c₁ c₂)
       c.addToQueue
 
 private def EqCnstr.superposeA (c₁ c₂ : EqCnstr) : ACM Unit := do

src/Lean/Meta/Tactic/Grind/AC/Proof.lean

@@ -163,9 +163,9 @@ partial def EqCnstr.toExprProof (c : EqCnstr) : ProofM Expr := do caching c do
   | .swap c =>
     let h ← mkPrefix ``AC.eq_orient
     return mkApp3 h (← mkSeqDecl c.lhs) (← mkSeqDecl c.rhs) (← c.toExprProof)
-  | .superpose_ac s s₁ s₂ c₁ c₂  =>
+  | .superpose_ac r₁ common r₂ c₁ c₂  =>
     let h ← mkACPrefix ``AC.superpose_ac
-    let h := mkApp9 h (← mkSeqDecl s₂) (← mkSeqDecl s₁) (← mkSeqDecl s) (← mkSeqDecl c₁.lhs) (← mkSeqDecl c₁.rhs)
+    let h := mkApp9 h (← mkSeqDecl r₁) (← mkSeqDecl common) (← mkSeqDecl r₂) (← mkSeqDecl c₁.lhs) (← mkSeqDecl c₁.rhs)
         (← mkSeqDecl c₂.lhs) (← mkSeqDecl c₂.rhs) (← mkSeqDecl c.lhs) (← mkSeqDecl c.rhs)
     return mkApp3 h eagerReflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
   | .superpose p common s c₁ c₂ =>

src/Lean/Meta/Tactic/Grind/AC/Seq.lean

@@ -262,25 +262,36 @@ private def app (s? : Option Seq) (s' : Seq) : Option Seq :=
   | none   => some s'
   | some s => some (s ++ s')
 
-def Seq.superposeAC (s₁ s₂ : Seq) : Option Seq × Option Seq × Option Seq :=
+/--
+Returns `some (r₁, c, r₂)` if `s₁ == r₁.union c` and `s₂ == r₂.union c`
+
+It assumes `s₁` and `s₂` are sorted
+-/
+def Seq.superposeAC? (s₁ s₂ : Seq) : Option (Seq × Seq × Seq) :=
   go s₁ s₂ none none none
 where
-  go (s₁ s₂ : Seq) (c r₁ r₂ : Option Seq) : Option Seq × Option Seq × Option Seq :=
+  mkResult (r₁ c r₂ : Option Seq) : Option (Seq × Seq × Seq) :=
+    match r₁, c, r₂ with
+    | some r₁, some c, some r₂ => some (r₁, c, r₂)
+    | _, _, _ => none
+
+  go (s₁ s₂ : Seq) (r₁ c r₂ : Option Seq) : Option (Seq × Seq × Seq) :=
     match s₁, s₂ with
     | .var x, .var y =>
-      if x == y then (push c x |> rev, rev r₁, rev r₂) else (rev c, push r₁ y |> rev, push r₂ x |> rev)
+      if x == y then mkResult (rev r₁) (rev (push c x)) (rev r₂)
+      else mkResult (rev (push r₁ x)) (rev c) (rev (push r₂ y))
     | .var x, .cons y s₂ =>
-      if x == y then (push c x |> rev, app (rev r₁) s₂, rev r₂)
-      else if x < y then (rev c, app (push r₁ y |> rev) s₂, push r₂ x |> rev)
-      else go (.var x) s₂ c (push r₁ y) r₂
+      if x == y then mkResult (rev r₁) (rev (push c x)) (app (rev r₂) s₂)
+      else if x < y then mkResult (rev (push r₁ x)) (rev c) (app (rev r₂) (.cons y s₂))
+      else go (.var x) s₂ r₁ c (push r₂ y)
     | .cons x s₁, .var y =>
-      if x == y then (push c x |> rev, rev r₁, app (rev r₂) s₁)
-      else if x < y then go s₁ (.var y) c r₁ (push r₂ x)
-      else (rev c, push r₁ y |> rev, app (push r₂ x |> rev) s₁)
+      if x == y then mkResult (app (rev r₁) s₁) (rev (push c x)) (rev r₂)
+      else if x < y then go s₁ (.var y) (push r₁ x) c r₂
+      else mkResult (app (rev r₁) (.cons x s₁)) (rev c) (rev (push r₂ y))
     | .cons x s₁, .cons y s₂ =>
-      if x == y then go s₁ s₂ (push c x) r₁ r₂
-      else if x < y then go s₁ (.cons y s₂) c r₁ (push r₂ x)
-      else go (.cons x s₁) s₂ c (push r₁ y) r₂
+      if x == y then go s₁ s₂ r₁ (push c x) r₂
+      else if x < y then go s₁ (.cons y s₂) (push r₁ x) c r₂
+      else go (.cons x s₁) s₂ r₁ c (push r₂ y)
 
 /--
 Returns `some (p, c, s)` if `s₁ == p ++ c` and `s₂ == c ++ s`

src/Lean/Meta/Tactic/Grind/AC/Types.lean

@@ -35,7 +35,7 @@ inductive EqCnstrProof where
   | simp_suffix (lhs : Bool) (s : AC.Seq) (c₁ : EqCnstr) (c₂ : EqCnstr)
   | simp_prefix (lhs : Bool) (s : AC.Seq) (c₁ : EqCnstr) (c₂ : EqCnstr)
   | simp_middle (lhs : Bool) (s₁ s₂ : AC.Seq) (c₁ : EqCnstr) (c₂ : EqCnstr)
-  | superpose_ac (c s₁ s₂ : AC.Seq) (c₁ : EqCnstr) (c₂ : EqCnstr)
+  | superpose_ac (r₁ c r₂ : AC.Seq) (c₁ : EqCnstr) (c₂ : EqCnstr)
   | superpose (p s c : AC.Seq) (c₁ : EqCnstr) (c₂ : EqCnstr)
 end