Experiments with grind

Author: nomeata

src/Lean/Meta/Match/MatchEqs.lean

@@ -20,6 +20,7 @@ import Lean.Meta.Tactic.Rewrite
 import Lean.Meta.Constructions.SparseCasesOn
 import Lean.Meta.Constructions.SparseCasesOnEq
 import Lean.Meta.Tactic.Grind.Main
+import Lean.Meta.HasNotBit
 
 public section
 
@@ -29,6 +30,32 @@ private def rewriteGoalUsingEq (goal : MVarId) (eq : Expr) (symm : Bool := false
   let rewriteResult ← goal.rewrite (←goal.getType) eq symm
   goal.replaceTargetEq rewriteResult.eNew rewriteResult.eqProof
 
+private def reduceSparseCasesOn (mvarId : MVarId) : MetaM (Array MVarId) := do
+  let some (_, lhs) ← matchEqHEqLHS? (← mvarId.getType) | throwError "Target not an equality"
+  lhs.withApp fun f xs => do
+  let .const matchDeclName _  := f | throwError "Not a const application"
+  let some sparseCasesOnInfo ← getSparseCasesOnInfo matchDeclName | throwError "Not a sparse casesOn application"
+  withTraceNode `Meta.Match.matchEqs (msg := (return m!"{exceptEmoji ·} splitSparseCasesOn")) do
+  if xs.size < sparseCasesOnInfo.arity then
+    throwError "Not enough arguments for sparse casesOn application"
+  let majorIdx := sparseCasesOnInfo.majorPos
+  let major := xs[majorIdx]!
+  let some ctorInfo  ← isConstructorApp'? major
+    | throwError "Major premise is not a constructor application:{indentExpr major}"
+  if sparseCasesOnInfo.insterestingCtors.contains ctorInfo.name then
+    let mvarId' ← mvarId.modifyTargetEqLHS fun lhs =>
+      unfoldDefinition lhs
+    return #[mvarId']
+  else
+    let sparseCasesOnEqName ← getSparseCasesOnEq matchDeclName
+    let eqProof := mkConst sparseCasesOnEqName lhs.getAppFn.constLevels!
+    let eqProof := mkAppN eqProof lhs.getAppArgs[:sparseCasesOnInfo.arity]
+    let eqProof := mkApp eqProof (← mkHasNotBitProof (mkRawNatLit ctorInfo.cidx) (←  sparseCasesOnInfo.insterestingCtors.mapM (fun n => return (← getConstInfoCtor n).cidx)))
+    let mvarId' ← rewriteGoalUsingEq mvarId eqProof
+    return #[mvarId']
+
+
+
 private def splitSparseCasesOn (mvarId : MVarId) : MetaM (Array MVarId) := do
   let some (_, lhs) ← matchEqHEqLHS? (← mvarId.getType) | throwError "Target not an equality"
   lhs.withApp fun f xs => do
@@ -57,7 +84,6 @@ private def splitSparseCasesOn (mvarId : MVarId) : MetaM (Array MVarId) := do
       else
         s.mvarId.modifyTargetEqLHS fun lhs =>
           unfoldDefinition lhs
-
   catch e =>
     trace[Meta.Match.matchEqs] "splitSparseCasesOn failed{indentD e.toMessageData}"
     throw e
@@ -148,6 +174,8 @@ where
       <|>
       (casesOnStuckLHS mvarId)
       <|>
+      (reduceSparseCasesOn mvarId)
+      <|>
       (splitSparseCasesOn mvarId)
       <|>
       (do let mvarId' ← simpIfTarget mvarId (useDecide := true) (useNewSemantics := true)
@@ -586,7 +614,11 @@ where go baseName := withConfig (fun c => { c with etaStruct := .none }) do
           let mut hs := #[]
           for overlappedBy in matchInfo.overlaps.overlapping i do
             let notAlt := notAlts[overlappedBy]!
-            let h ← instantiateForall notAlt discrs -- We want these to be general during the proof
+            -- We want these assumptions to be general during the proof (discrs)
+            -- so that contradiction can recognize them,
+            -- but specific in the final theorem (patterns)
+            -- so that they match the splitter
+            let h ← instantiateForall notAlt discrs
             -- if let some h ← simpH? h patterns.size then
               -- hs := hs.push h
             -- TODO: We still should simplify them before creating the declaration

tests/lean/run/issue11342.lean

@@ -25,3 +25,46 @@ info: private theorem natToBin3.match_1.congr_eq_1.{u_1} : ∀ (motive : (x : Na
 -/
 #guard_msgs(pass trace, all) in
 #print sig natToBin3.match_1.congr_eq_1
+
+
+def f : List Nat → List Nat → Nat
+  | _, 1 :: _ :: _ => 1
+  | _, a :: _ => if a > 1 then 2 else 3
+  | _, _  => 0
+
+/--
+info: private theorem f.match_1.eq_2.{u_1} : ∀ (motive : List Nat → List Nat → Sort u_1) (x : List Nat) (a : Nat)
+  (tail : List Nat) (h_1 : (x : List Nat) → (head : Nat) → (tail : List Nat) → motive x (1 :: head :: tail))
+  (h_2 : (x : List Nat) → (a : Nat) → (tail : List Nat) → motive x (a :: tail))
+  (h_3 : (x x_1 : List Nat) → motive x x_1),
+  (∀ (head : Nat) (tail_1 : List Nat), a = 1 → tail = head :: tail_1 → False) →
+    (match x, a :: tail with
+      | x, 1 :: head :: tail => h_1 x head tail
+      | x, a :: tail => h_2 x a tail
+      | x, x_2 => h_3 x x_2) =
+      h_2 x a tail
+-/
+#guard_msgs in
+#print sig f.match_1.eq_2
+
+/--
+error: Failed to realize constant f.match_1.congr_eq_2:
+  failed to generate equality theorem _private.lean.run.issue11342.0.f.match_1.congr_eq_2 for `match` expression `f.match_1`
+  case cons.isTrue.cons
+  motive✝ : List Nat → List Nat → Sort u_1
+  h_1✝ : (x : List Nat) → (head : Nat) → (tail : List Nat) → motive✝ x (1 :: head :: tail)
+  h_2✝ : (x : List Nat) → (a : Nat) → (tail : List Nat) → motive✝ x (a :: tail)
+  h_3✝ : (x x_1 : List Nat) → motive✝ x x_1
+  x✝¹ : List Nat
+  a✝ : Nat
+  tail✝¹ : List Nat
+  x✝ : ∀ (x : List Nat) (head : Nat) (tail : List Nat), x✝¹ = x → a✝ :: tail✝¹ = 1 :: head :: tail → False
+  head✝ : Nat
+  tail✝ : List Nat
+  heq_2✝ : 1 :: head✝ :: tail✝ = a✝ :: tail✝¹
+  ⊢ h_1✝ x✝¹ head✝ tail✝ ≍ h_2✝ x✝¹ a✝ tail✝¹
+---
+error: Unknown constant `f.match_1.congr_eq_2`
+-/
+#guard_msgs in
+#print sig f.match_1.congr_eq_2

tests/lean/run/issue9846.lean

@@ -4,7 +4,7 @@ def testMatch : Array α → Unit
 
 /--
 error: Failed to realize constant testMatch.match_1.eq_1:
-  failed to generate equality theorems for `match` expression `testMatch.match_1`
+  failed to generate equality theorem _private.lean.run.issue9846.0.testMatch.match_1.eq_2 for `match` expression `testMatch.match_1`
   case isTrue
   α✝ : Type u_1
   motive✝ : Array α✝ → Sort u_2