Using grind helps

Author: nomeata

src/Lean/Meta/Match/MatchEqs.lean

@@ -19,6 +19,7 @@ import Lean.Meta.Match.NamedPatterns
 import Lean.Meta.Tactic.Rewrite
 import Lean.Meta.Constructions.SparseCasesOn
 import Lean.Meta.Constructions.SparseCasesOnEq
+import Lean.Meta.Tactic.Grind.Main
 
 public section
 
@@ -165,6 +166,10 @@ where
       <|>
       (substSomeVar mvarId)
       <|>
+      (do let r ← Grind.main mvarId (← Grind.mkParams {})
+          if r.hasFailed then throwError "grind failed"
+          return #[])
+      <|>
       (throwError "failed to generate equality theorem {thmName} for `match` expression `{matchDeclName}`\n{MessageData.ofGoal mvarId}")
     subgoals.forM (go · (depth+1))
 

tests/lean/run/issue11342.lean

@@ -1,33 +1,27 @@
+opaque double (n : Nat) : Nat
+
 inductive Parity : Nat -> Type
-| even (n) : Parity (n + n)
-| odd  (n) : Parity (Nat.succ (n + n))
+| even (n) : Parity (double n)
+| odd  (n) : Parity (Nat.succ (double n))
 
-set_option trace.Meta.Match.matchEqs true
+-- set_option trace.Meta.Match.matchEqs true
 
 partial def natToBin3 : (n : Nat) → Parity n →  List Bool
 | 0, _             => []
 | _, Parity.even j => [false, false]
 | _, Parity.odd  j => [true, true]
 
--- #guard_msgs in
--- #print sig natToBin3.match_1.splitter
-
 /--
-error: Failed to realize constant natToBin3.match_1.congr_eq_1:
-  failed to generate equality theorem _private.lean.run.issue11342.0.natToBin3.match_1.congr_eq_2 for `match` expression `natToBin3.match_1`
-  case else.even
-  motive✝ : (x : Nat) → Parity x → Sort u_1
-  h_1✝ : (x : Parity 0) → motive✝ 0 x
-  h_2✝ : (j : Nat) → motive✝ (j + j) (Parity.even j)
-  h_3✝ : (j : Nat) → motive✝ (j + j).succ (Parity.odd j)
-  j✝ n✝ : Nat
-  h✝ : Nat.hasNotBit 1 (n✝ + n✝).ctorIdx
-  heq_1✝ : n✝ + n✝ = j✝ + j✝
-  heq_2✝ : Parity.even n✝ ≍ Parity.even j✝
-  x✝ : ∀ (x : Parity 0), n✝ + n✝ = 0 → Parity.even n✝ ≍ x → False
-  ⊢ h_2✝ n✝ ≍ h_2✝ j✝
----
-error: Unknown constant `natToBin3.match_1.congr_eq_1`
+info: private theorem natToBin3.match_1.congr_eq_1.{u_1} : ∀ (motive : (x : Nat) → Parity x → Sort u_1) (x : Nat)
+  (x_1 : Parity x) (h_1 : (x : Parity 0) → motive 0 x) (h_2 : (j : Nat) → motive (double j) (Parity.even j))
+  (h_3 : (j : Nat) → motive (double j).succ (Parity.odd j)) (x_2 : Parity 0),
+  x = 0 →
+    x_1 ≍ x_2 →
+      (match x, x_1 with
+        | 0, x => h_1 x
+        | .(double j), Parity.even j => h_2 j
+        | .((double j).succ), Parity.odd j => h_3 j) ≍
+        h_1 x_2
 -/
 #guard_msgs(pass trace, all) in
 #print sig natToBin3.match_1.congr_eq_1