From 84f72b938936a1286f7c8138e259796c970c4e7a Mon Sep 17 00:00:00 2001
From: Daniel Fabian <daniel.fabian@integral-it.ch>
Date: Fri, 4 Mar 2022 15:18:36 +0000
Subject: [PATCH] test: add further ac_refl tests.

---
 src/Lean/Meta/Tactic/AC/Main.lean | 25 +++++++++++++++++--------
 tests/lean/run/ac_refl.lean       | 22 +++++++++++-----------
 2 files changed, 28 insertions(+), 19 deletions(-)

diff --git a/src/Lean/Meta/Tactic/AC/Main.lean b/src/Lean/Meta/Tactic/AC/Main.lean
index 3916d118f6..53372cdfc5 100644
--- a/src/Lean/Meta/Tactic/AC/Main.lean
+++ b/src/Lean/Meta/Tactic/AC/Main.lean
@@ -272,18 +272,24 @@ where
     | maybeNormalized _ l r => do mkAppM' op #[←convertType op l, ←convertType op r]
 
 inductive ProofStrategy
-  | rfl (lhs rhs : NormalizedExpr)
+  | ac_rfl (lhs rhs : NormalizedExpr)
+  | rfl (tgt : Expr)
   | norm (e : NormalizedExpr)
 
 def pickStrategy (e : Expr) : M ProofStrategy := do
   match e with
-  | eq lhs rhs =>
-    match ←findUnnormalizedOperator lhs with
+  | eq l r =>
+    match ←findUnnormalizedOperator l with
     | lhs@(unnormalized _ _) => return ProofStrategy.norm lhs
-    | lhs =>
-      match ←findUnnormalizedOperator rhs with
+    | lhs@(maybeNormalized _ _ _) =>
+      match ←findUnnormalizedOperator r with
       | rhs@(unnormalized _ _) => return ProofStrategy.norm rhs
-      | rhs => return ProofStrategy.rfl lhs rhs
+      | rhs => return ProofStrategy.ac_rfl lhs rhs
+    | lhs@(definitelyNormalized _) =>
+      match ←findUnnormalizedOperator r with
+      | rhs@(unnormalized _ _) => return ProofStrategy.norm rhs
+      | rhs@(maybeNormalized _ _ _) => return ProofStrategy.ac_rfl lhs rhs
+      | rhs@(definitelyNormalized _) => return ProofStrategy.rfl l
   | e => return ProofStrategy.norm $ ←findUnnormalizedOperator e
 
 def addAcEq (mvarId : MVarId) (e : NormalizedExpr) (target : Expr) : M MVarId := do
@@ -298,14 +304,17 @@ partial def rewriteUnnormalized (mvarId : MVarId) : M Unit :=
   withMVarContext mvarId do
   let target ← getMVarType mvarId
   match ←pickStrategy target with
-  | ProofStrategy.rfl lhs rhs =>
-    trace[Meta.AC] "picking rfl strategy {MessageData.ofGoal mvarId}"
+  | ProofStrategy.ac_rfl lhs rhs =>
+    trace[Meta.AC] "picking ac_rfl strategy {MessageData.ofGoal mvarId}"
     try
       let (proof, ty) ← buildProof lhs rhs
       if ←isDefEq target ty then
         assignExprMVar mvarId proof
       else throwError ""
     catch _ => throwError "cannot synthesize proof:\n{MessageData.ofGoal mvarId}"
+  | ProofStrategy.rfl tgt =>
+    trace[Meta.AC] "picking rfl strategy {MessageData.ofGoal mvarId}"
+    assignExprMVar mvarId (←mkAppM ``Eq.refl #[tgt])
   | ProofStrategy.norm (definitelyNormalized _) => throwError "no unnormalized operators found"
   | ProofStrategy.norm e =>
     trace[Meta.AC] "picking norm strategy {MessageData.ofGoal mvarId}"
diff --git a/tests/lean/run/ac_refl.lean b/tests/lean/run/ac_refl.lean
index ed051af284..4d977dcd55 100644
--- a/tests/lean/run/ac_refl.lean
+++ b/tests/lean/run/ac_refl.lean
@@ -21,7 +21,7 @@ theorem max_comm (n m : Nat) : max n m = max m n := by
   case inr h₁ h₂ => simp [Nat.not_lt_eq] at *; apply Nat.le_antisymm <;> assumption
 
 theorem max_idem (n : Nat) : max n n = n := by
-  simp [max]; split <;> rfl
+  simp [max]
 
 theorem Nat.zero_max (n : Nat) : max 0 n = n := by
   simp [max]; rfl
@@ -34,17 +34,17 @@ instance : IsCommutative (α := Nat) max := ⟨max_comm⟩
 instance : IsIdempotent (α := Nat) max := ⟨max_idem⟩
 instance : IsNeutral max 0 := ⟨Nat.zero_max, Nat.max_zero⟩
 
-example (x y z : Nat) : x + y + 0 + z = z + (x + y) := by
-  ac_refl
+example (x y z : Nat) : x + y + 0 + z = z + (x + y) := by ac_refl
 
-example (x y z : Nat) : (x + y) * (0 + z) = (x + y) * z:= by
-  ac_refl
+example (x y z : Nat) : (x + y) * (0 + z) = (x + y) * z:= by ac_refl
 
-example (x y z : Nat) : (x + y) * (0 + z) = 1 * z * (y + 0 + x) := by
-  ac_refl
+example (x y z : Nat) : (x + y) * (0 + z) = 1 * z * (y + 0 + x) := by ac_refl
 
-example (x y z : Nat) : max (0 + (max x (max z (max (0 + 0) ((max 1 0) + 0 + 0) * y)))) y = max (max x y) z := by
-  ac_refl
+example (x y z : Nat) : max (0 + (max x (max z (max (0 + 0) ((max 1 0) + 0 + 0) * y)))) y = max (max x y) z := by ac_refl
+
+example (x y : Nat) : 1 + 0 + 0 = 0 + 1 := by ac_refl
+
+example (x y : Nat) : (x + y = 42) = (y + x = 42) := by ac_refl
+
+example (x y : Nat) (P : Prop) : (x + y = 42 → P) = (y + x = 42 → P) := by ac_refl
 
-example (x y : Nat) : 1 + 0 + 0 = 0 + 1 := by
-  ac_refl