Another test

src/Lean/Meta/Match/MatchEqs.lean

@@ -496,6 +496,16 @@ where
    else
      k altsNew
 
+/--
+Does this matcher need a dedicated splitter?
+We generate a splitter only if during match compilation, we (conservatively) detected that some
+alternativs are overlapped or if the matcher type contains named patterns.
+-/
+def needsSplitter (matchDeclName : Name) : MetaM Bool := do
+  let some matchInfo ← getMatcherInfo? matchDeclName | throwError "`{matchDeclName}` is not a matcher function"
+  let constInfo ← getConstVal matchDeclName
+  return !matchInfo.overlaps.isEmpty || (constInfo.type.find? isNamedPattern).isSome
+
 /-
 Creates conditional equations and splitter for the given match auxiliary declaration.
 
@@ -503,6 +513,13 @@ See also `getEquationsFor`.
 -/
 @[export lean_get_match_equations_for]
 def getEquationsForImpl (matchDeclName : Name) : MetaM MatchEqns := do
+  let some matchInfo ← getMatcherInfo? matchDeclName | throwError "`{matchDeclName}` is not a matcher function"
+  if matchInfo.numAlts = 0 then
+    -- Special case of no alternatives, do not bother creating anything
+    let result := { eqnNames := #[], splitterName := matchDeclName, splitterMatchInfo := matchInfo }
+    registerMatchEqns matchDeclName result
+    return result
+
   /-
   Remark: users have requested the `split` tactic to be available for writing code.
   Thus, the `splitter` declaration must be a definition instead of a theorem.
@@ -511,13 +528,17 @@ def getEquationsForImpl (matchDeclName : Name) : MetaM MatchEqns := do
   keep `splitter` as a private declaration to prevent import failures.
   -/
   let baseName := mkPrivateName (← getEnv) matchDeclName
-  let splitterName := baseName ++ `splitter
+
+  -- Use the first equation as the key for realizeConst
+  -- (We used to use the splitter, but we are only generating it on demand now)
+  let realizeKey := Name.str baseName eqnThmSuffixBase |>.appendIndexAfter 1
+
   -- NOTE: `go` will generate both splitter and equations but we use the splitter as the "key" for
   -- `realizeConst` as well as for looking up the resultant environment extension state via
   -- `getState`.
-  realizeConst matchDeclName splitterName (go baseName splitterName)
-  return matchEqnsExt.getState (asyncMode := .async .asyncEnv) (asyncDecl := splitterName) (← getEnv) |>.map.find! matchDeclName
-where go baseName splitterName := withConfig (fun c => { c with etaStruct := .none }) do
+  realizeConst matchDeclName realizeKey (go baseName)
+  return matchEqnsExt.getState (asyncMode := .async .asyncEnv) (asyncDecl := realizeKey) (← getEnv) |>.map.find! matchDeclName
+where go baseName := withConfig (fun c => { c with etaStruct := .none }) do
   let constInfo ← getConstInfo matchDeclName
   let us := constInfo.levelParams.map mkLevelParam
   let some matchInfo ← getMatcherInfo? matchDeclName | throwError "`{matchDeclName}` is not a matcher function"
@@ -588,31 +609,39 @@ where go baseName splitterName := withConfig (fun c => { c with etaStruct := .no
       altArgMasks := altArgMasks.push argMask
       trace[Meta.Match.matchEqs] "splitterAltType: {splitterAltType}"
       idx := idx + 1
-    -- Define splitter with conditional/refined alternatives
-    withSplitterAlts splitterAltTypes fun altsNew => do
-      let splitterParams := params.toArray ++ #[motive] ++ discrs.toArray ++ altsNew
-      let splitterType ← mkForallFVars splitterParams matchResultType
-      trace[Meta.Match.matchEqs] "splitterType: {splitterType}"
-      let splitterVal ←
-        if (← isDefEq splitterType constInfo.type) then
-          pure <| mkConst constInfo.name us
-        else
-          let template := mkAppN (mkConst constInfo.name us) (params ++ #[motive] ++ discrs ++ alts)
-          let template ← deltaExpand template (· == constInfo.name)
-          let template := template.headBeta
-          mkLambdaFVars splitterParams (← mkSplitterProof matchDeclName template alts altsNew splitterAltInfos altArgMasks)
-      addAndCompile <| Declaration.defnDecl {
-        name        := splitterName
-        levelParams := constInfo.levelParams
-        type        := splitterType
-        value       := splitterVal
-        hints       := .abbrev
-        safety      := .safe
-      }
-      setInlineAttribute splitterName
-      let splitterMatchInfo := { matchInfo with altInfos := splitterAltInfos }
+    if (← needsSplitter matchDeclName) then
+      let splitterName := baseName ++ `splitter
+      -- Define splitter with conditional/refined alternatives
+      withSplitterAlts splitterAltTypes fun altsNew => do
+        let splitterParams := params.toArray ++ #[motive] ++ discrs.toArray ++ altsNew
+        let splitterType ← mkForallFVars splitterParams matchResultType
+        trace[Meta.Match.matchEqs] "splitterType: {splitterType}"
+        let template := mkAppN (mkConst constInfo.name us) (params ++ #[motive] ++ discrs ++ alts)
+        let template ← deltaExpand template (· == constInfo.name)
+        let template := template.headBeta
+        let splitterVal ←
+          if (← isDefEq splitterType constInfo.type) then
+            pure <| mkConst constInfo.name us
+          else
+            mkLambdaFVars splitterParams (← mkSplitterProof matchDeclName template alts altsNew splitterAltInfos altArgMasks)
+        addAndCompile <| Declaration.defnDecl {
+          name        := splitterName
+          levelParams := constInfo.levelParams
+          type        := splitterType
+          value       := splitterVal
+          hints       := .abbrev
+          safety      := .safe
+        }
+        setInlineAttribute splitterName
+      let splitterMatchInfo := { matchInfo with altInfos := splitterAltInfos, overlaps := {} }
       let result := { eqnNames, splitterName, splitterMatchInfo }
       registerMatchEqns matchDeclName result
+    else
+      -- No dedicated splitter
+      unless splitterAltInfos == matchInfo.altInfos do
+        panic s!"internal error: altNumParams for {matchDeclName} changed from {repr matchInfo.altInfos} to {repr splitterAltInfos} even though no splitter is needed"
+      let result := { eqnNames, splitterName := matchDeclName, splitterMatchInfo := matchInfo }
+      registerMatchEqns matchDeclName result
 
 /- We generate the equations and splitter on demand, and do not save them on .olean files. -/
 builtin_initialize matchCongrEqnsExt : EnvExtension (PHashMap Name (Array Name)) ←

src/Lean/Meta/Match/MatcherInfo.lean

@@ -23,6 +23,9 @@ structure Overlaps where
   map : Std.HashMap Nat (Std.TreeSet Nat) := {}
 deriving Inhabited, Repr
 
+def Overlaps.isEmpty (o : Overlaps) : Bool :=
+  o.map.isEmpty
+
 def Overlaps.insert (o : Overlaps) (overlapping overlapped : Nat) : Overlaps where
   map := o.map.alter overlapped fun s? => some ((s?.getD {}).insert overlapping)
 
@@ -41,7 +44,7 @@ structure AltParamInfo where
   numOverlaps : Nat
   /-- Whether this alternatie has an artifcial `Unit` parameter -/
   hasUnitThunk : Bool
-deriving Inhabited, Repr
+deriving Inhabited, Repr, BEq
 
 /--
 A "matcher" auxiliary declaration has the following structure:

tests/lean/run/1080.lean

@@ -21,4 +21,3 @@ attribute [simp] Bar.check
 #check Bar.check.eq_2
 #check Bar.check.match_1.eq_1
 #check Bar.check.match_1.eq_2
-#check Bar.check.match_1.splitter

tests/lean/run/casesOnSameCtor.lean

@@ -34,22 +34,12 @@ info: Vec.match_on_same_ctor.{u_1, u} {α : Type u}
 #guard_msgs in
 #check Vec.match_on_same_ctor
 
--- Splitter and equations are generated
-/--
-info: Vec.match_on_same_ctor.splitter.{u_1, u} {α : Type u}
-  {motive : {a : Nat} → (t t_1 : Vec α a) → t.ctorIdx = t_1.ctorIdx → Sort u_1} {a✝ : Nat} (t t✝ : Vec α a✝)
-  (h : t.ctorIdx = t✝.ctorIdx) (h_1 : Unit → motive nil nil ⋯)
-  (h_2 : (a : α) → (n : Nat) → (a_1 : Vec α n) → (a' : α) → (a'_1 : Vec α n) → motive (cons a a_1) (cons a' a'_1) ⋯) :
-  motive t t✝ h
--/
+-- Splitter is not generated, because it is equal to the matcher
+/-- error: Unknown constant `Vec.match_on_same_ctor.splitter` -/
 #guard_msgs in
-#check Vec.match_on_same_ctor.splitter
+#print sig Vec.match_on_same_ctor.splitter
 
--- After #11211 this is no longer true. Should we thunk the same-ctor-construction?
-
--- -- Since there is no overlap, the splitter is equal to the matcher
--- -- (I wonder if we should use this in general in MatchEq)
--- example : @Vec.match_on_same_ctor = @Vec.match_on_same_ctor.splitter := by rfl
+-- But equations are generated
 
 /--
 info: Vec.match_on_same_ctor.eq_2.{u_1, u} {α : Type u}

tests/lean/run/issue11211.lean

@@ -68,13 +68,10 @@ info: def Option_map.match_1.{u_1, u_2} : {α : Type u_1} →
 #guard_msgs in
 #print sig Option_map.match_1
 
-/--
-info: private def Option_map.match_1.splitter.{u_1, u_2} : {α : Type u_1} →
-  (motive : Option α → Sort u_2) → (x : Option α) → ((x : α) → motive (some x)) → (Unit → motive none) → motive x :=
-@Option_map.match_1
--/
+-- No splitter generated now, it is identical to the matcher
+/-- error: Unknown constant `Option_map.match_1.splitter` -/
 #guard_msgs in
-#print Option_map.match_1.splitter
+#print sig Option_map.match_1.splitter
 
 /--
 info: theorem Option_map.fun_cases.{u_1} : ∀ {α : Type u_1} (motive : Option α → Prop),

tests/lean/run/issue11277.lean

@@ -0,0 +1,31 @@
+
+
+inductive F : Nat → Type where
+  | zero : F n
+  | succ : F n → F (n + 1)
+
+def foo : F n → Nat
+  | .zero => 0
+  -- | x@(.succ i) => 1 + foo i
+  | .succ i => 1 + foo i
+
+def bar : F n → Nat
+  | .zero => 0
+  | .succ i => 1 + bar i
+
+theorem baz (xs : F n) : foo xs = bar xs := by
+  unfold foo
+  split
+  next =>
+    simp [bar]
+  next z zs =>
+    rw [bar]
+    have := baz zs
+    grind
+termination_by foo xs
+decreasing_by
+  skip
+  subst ‹n = _›
+  have := eq_of_heq ‹_›
+  subst this
+  grind [foo]

tests/lean/run/issue11277b.lean

@@ -0,0 +1,270 @@
+
+prelude
+
+import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Basic
+import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Var
+
+set_option Elab.async false
+set_option warn.sorry false
+
+@[expose] public section
+
+/-!
+This module contains the implementation of a bitblaster for `BitVec` expressions (`BVExpr`).
+That is, expressions that evaluate to `BitVec` again. Its used as a building block in bitblasting
+general `BitVec` problems with boolean substructure.
+-/
+
+namespace Std.Tactic.BVDecide
+
+open Std.Sat
+
+namespace BVExpr
+
+structure Cache.Key where
+  w : Nat
+  expr : BVExpr w
+  deriving DecidableEq
+
+instance : Hashable Cache.Key where
+  -- The width is already mixed into the hash of `key.expr` which is completely cached.
+  hash key := hash key.expr
+
+structure Cache (aig : AIG BVBit) where
+  map : Std.DHashMap Cache.Key (fun k => Vector AIG.Fanin k.w)
+  hbound : ∀ k (h1 : k ∈ map), ∀ (h2 : i < k.1), (map.get k h1)[i].gate < aig.decls.size
+
+@[inline]
+def Cache.empty : Cache aig :=
+  ⟨{}, by simp⟩
+
+@[inline]
+def Cache.insert (cache : Cache aig) (expr : BVExpr w) (refs : AIG.RefVec aig w) :
+    Cache aig :=
+  let ⟨map, hbound⟩ := cache
+  have := by
+    intro i k hk h2
+    rw [Std.DHashMap.get_insert]
+    split
+    next heq =>
+      rcases k with ⟨w, expr⟩
+      simp only [beq_iff_eq, Key.mk.injEq] at heq
+      rcases heq with ⟨heq1, heq2⟩
+      symm at heq1
+      subst heq1
+      have := refs.hrefs h2
+      rw [getElem_congr_coll]
+      · exact this
+      · simp
+    · apply hbound
+  ⟨map.insert ⟨w, expr⟩ refs.refs, this⟩
+
+@[inline]
+def Cache.get? (cache : Cache aig) (expr : BVExpr w) : Option (AIG.RefVec aig w) :=
+  match h : cache.map.get? ⟨w, expr⟩ with
+  | some refs =>
+    have : ⟨w, expr⟩ ∈ cache.map := by
+      rw [Std.DHashMap.mem_iff_contains, Std.DHashMap.contains_eq_isSome_get?]
+      simp [h]
+    have : cache.map.get ⟨w, expr⟩ this = refs := by
+      rw [Std.DHashMap.get?_eq_some_get (h := this)] at h
+      simpa using h
+    have := by
+      intro i hi
+      rw [← this]
+      apply cache.hbound
+    some ⟨refs, this⟩
+  | none => none
+
+@[inline]
+def Cache.cast (cache : Cache aig1) (h : aig1.decls.size ≤ aig2.decls.size) :
+    Cache aig2 :=
+  let ⟨map, hbound⟩ := cache
+  have := by
+    intro i k hk h2
+    apply Nat.lt_of_lt_of_le
+    · apply hbound
+    · exact h
+  ⟨map, this⟩
+
+structure WithCache (α : Type u) (aig : AIG BVBit) where
+  val : α
+  cache : Cache aig
+
+structure Return (aig : AIG BVBit) (w : Nat) where
+  result : AIG.ExtendingRefVecEntry aig w
+  cache : Cache result.val.aig
+
+set_option maxHeartbeats 400000 in
+def bitblast (aig : AIG BVBit) (input : WithCache (BVExpr w) aig) : Return aig w :=
+  let ⟨expr, cache⟩ := input
+  goCache aig expr cache
+where
+  goCache {w : Nat} (aig : AIG BVBit) (expr : BVExpr w) (cache : Cache aig) : Return aig w :=
+    match cache.get? expr with
+    | some vec => sorry
+    | none =>
+      let ⟨result, cache⟩ := go aig expr cache
+      ⟨result, cache.insert expr result.val.vec⟩
+  termination_by (sizeOf expr, 1)
+
+  go {w : Nat} (aig : AIG BVBit) (expr : BVExpr w) (cache : Cache aig) : Return aig w :=
+    match expr with
+    | x@(.var a) => -- Works
+    -- | (.var a) => -- Doesn't work
+      let res := bitblast.blastVar aig ⟨a⟩
+      have := AIG.LawfulVecOperator.le_size (f := bitblast.blastVar) ..
+      let cache := cache.cast this
+      ⟨⟨res, this⟩, cache⟩
+    | .const val => sorry
+    | .bin lhsExpr op rhsExpr =>
+      let ⟨⟨⟨aig, lhs⟩, hlaig⟩, cache⟩ := goCache aig lhsExpr cache
+      let ⟨⟨⟨aig, rhs⟩, hraig⟩, cache⟩ := goCache aig rhsExpr cache
+      let lhs := lhs.cast <| by
+        dsimp only at hlaig hraig
+        omega
+      match op with
+      | .and => sorry
+      | .or => sorry
+      | .xor => sorry
+      | .add =>
+        ⟨⟨sorry, sorry⟩, cache.cast sorry⟩
+      | .mul => sorry
+      | .udiv => sorry
+      | .umod => sorry
+    | .un op expr =>
+      let ⟨⟨⟨eaig, evec⟩, heaig⟩, cache⟩ := goCache aig expr cache
+      match op with
+      | .not => sorry
+      | .rotateLeft distance => sorry
+      | .rotateRight distance => sorry
+      | .arithShiftRightConst distance => sorry
+      | .reverse => sorry
+      | .clz => sorry
+    | .append lhs rhs h => sorry
+    | .replicate n expr h => sorry
+    | .extract start len expr => sorry
+    | .shiftLeft lhs rhs => sorry
+    | .shiftRight lhs rhs => sorry
+    | .arithShiftRight lhs rhs => sorry
+  termination_by (sizeOf expr, 0)
+
+
+namespace bitblast
+
+mutual
+
+theorem goCache_decl_eq (aig : AIG BVBit) (expr : BVExpr w) (cache : Cache aig) :
+    ∀ (idx : Nat) (h1) (h2), (goCache aig expr cache).result.val.aig.decls[idx]'h2 = aig.decls[idx]'h1 := by
+  sorry
+
+theorem go_decl_eq (aig : AIG BVBit) (expr : BVExpr w) (cache : Cache aig) :
+    ∀ (idx : Nat) (h1) (h2), (go aig expr cache).result.val.aig.decls[idx]'h2 = aig.decls[idx]'h1 := by
+  sorry
+
+end
+
+end bitblast
+
+theorem bitblast_decl_eq (aig : AIG BVBit) (input : WithCache (BVExpr w) aig) :
+    ∀ (idx : Nat) (h1) (h2), (bitblast aig input).result.val.aig.decls[idx]'h2 = aig.decls[idx]'h1 := by
+  sorry
+
+theorem bitblast_le_size (aig : AIG BVBit) (input : WithCache (BVExpr w) aig) :
+    aig.decls.size ≤ (bitblast aig input).result.val.aig.decls.size := by
+  sorry
+
+theorem bitblast_lt_size_of_lt_aig_size (aig : AIG BVBit) (input : WithCache (BVExpr w) aig)
+    (h : x < aig.decls.size) :
+    x < (bitblast aig input).result.val.aig.decls.size := by
+  sorry
+
+end BVExpr
+
+end Std.Tactic.BVDecide
+
+
+/-!
+This module contains the verification of the `BitVec` expressions (`BVExpr`) bitblaster from
+`Impl.Expr`.
+-/
+
+namespace Std.Tactic.BVDecide
+
+open Std.Sat
+open Std.Sat.AIG
+
+namespace BVExpr
+
+namespace Cache
+
+abbrev Inv (assign : Assignment) (aig : AIG BVBit) (cache : Cache aig) : Prop :=
+  ∀ k (h1 : k ∈ cache.map), ∀ (i : Nat) (h2 : i < k.w),
+    ⟦aig, ⟨(cache.map.get k h1)[i].gate, (cache.map.get k h1)[i].invert, cache.hbound ..⟩, assign.toAIGAssignment⟧
+      =
+    (k.expr.eval assign).getLsbD i
+
+theorem Inv_cast (cache : Cache aig1) (hpref : IsPrefix aig1.decls aig2.decls)
+    (hinv : Inv assign aig1 cache):
+    Inv assign aig2 (cache.cast hpref.size_le) := by sorry
+
+theorem Inv_insert (cache : Cache aig) (expr : BVExpr w) (refs : AIG.RefVec aig w)
+    (hinv : Inv assign aig cache)
+    (hrefs : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, refs.get idx hidx, assign.toAIGAssignment⟧ = (expr.eval assign).getLsbD idx) :
+    Inv assign aig (cache.insert expr refs) := by sorry
+
+end Cache
+
+namespace bitblast
+
+set_option maxHeartbeats 400000
+
+mutual
+
+theorem goCache_Inv_of_Inv (cache : Cache aig) (hinv : Cache.Inv assign aig cache) :
+    ∀ (expr : BVExpr w),
+        Cache.Inv assign (goCache aig expr cache).result.val.aig (goCache aig expr cache).cache := by
+  intro expr
+  generalize hres : goCache aig expr cache = res
+  unfold goCache at hres
+  split at hres
+  · sorry
+  · rw [← hres]
+    dsimp only
+    apply Cache.Inv_insert
+    · apply go_Inv_of_Inv
+      sorry
+    · sorry
+termination_by expr => (sizeOf expr, 1, sizeOf aig)
+decreasing_by all_goals decreasing_tactic
+
+theorem go_Inv_of_Inv (cache : Cache aig) (hinv : Cache.Inv assign aig cache) :
+    ∀ (expr : BVExpr w),
+        Cache.Inv assign (go aig expr cache).result.val.aig (go aig expr cache).cache := by
+  intro expr
+  generalize hres : go aig expr cache = res
+  unfold go at hres
+  split at hres
+  · sorry
+  · sorry
+  next op lhsExpr rhsExpr =>
+    dsimp only at hres
+    match (generalizing := false) op, hres with
+    | .add, hres =>
+      dsimp only at hres
+      rw [← hres]
+      apply Cache.Inv_cast
+      · sorry
+      · apply goCache_Inv_of_Inv
+        sorry
+    | _, hres =>
+      sorry
+  all_goals sorry
+termination_by expr => (sizeOf expr, 0, 0)
+decreasing_by
+  skip
+  decreasing_tactic
+
+end
+
+#exit