perf: mkSplitterProof

The equation lemmas were not using the standard representation for literals.

src/Lean/Elab/Match.lean

@@ -473,7 +473,7 @@ partial def normalize (e : Expr) : M Expr := do
         let p ← normalize p
         addVar h
         return mkApp4 e.getAppFn (e.getArg! 0) x p h
-      else if isMatchValue e then
+      else if (← isMatchValue e) then
         return e
       else if e.isFVar then
         if (← isExplicitPatternVar e) then
@@ -571,8 +571,8 @@ private partial def toPattern (e : Expr) : MetaM Pattern := do
         match e.getArg! 1, e.getArg! 3 with
         | Expr.fvar x, Expr.fvar h => return Pattern.as x p h
         | _,           _           => throwError "unexpected occurrence of auxiliary declaration 'namedPattern'"
-      else if isMatchValue e then
-        return Pattern.val e
+      else if (← isMatchValue e) then
+        return Pattern.val (← normLitValue e)
       else if e.isFVar then
         return Pattern.var e.fvarId!
       else

src/Lean/Meta.lean

@@ -46,3 +46,4 @@ import Lean.Meta.Eval
 import Lean.Meta.CoeAttr
 import Lean.Meta.Iterator
 import Lean.Meta.LazyDiscrTree
+import Lean.Meta.LitValues

src/Lean/Meta/LitValues.lean

@@ -0,0 +1,121 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Basic
+
+namespace Lean.Meta
+
+/-!
+Helper functions for recognizing builtin literal values.
+This module focus on recognizing the standard representation used in Lean for these literals.
+It also provides support for the following exceptional cases.
+- Raw natural numbers (i.e., natural numbers which are not encoded using `OfNat.ofNat`).
+- Bit-vectors encoded using `OfNat.ofNat` and `BitVec.ofNat`.
+- Negative integers encoded using raw natural numbers.
+- Characters encoded `Char.ofNat n` where `n` can be a raw natural number or an `OfNat.ofNat`.
+- Nested `Expr.mdata`.
+-/
+
+/-- Returns `some n` if `e` is a raw natural number, i.e., it is of the form `.lit (.natVal n)`. -/
+def getRawNatValue? (e : Expr) : Option Nat :=
+  match e with
+  | .lit (.natVal n) => some n
+  | _ => none
+
+/-- Return `some (n, type)` if `e` is an `OfNat.ofNat`-application encoding `n` for a type with name `typeDeclName`. -/
+def getOfNatValue? (e : Expr) (typeDeclName : Name) : MetaM (Option (Nat × Expr)) := OptionT.run do
+  guard <| e.isAppOfArity' ``OfNat.ofNat 3
+  let type ← whnfD e.appFn!.appFn!.appArg!
+  guard <| type.getAppFn.isConstOf typeDeclName
+  let .lit (.natVal n) := e.appFn!.appArg! | failure
+  return (n, type)
+
+/-- Return `some n` if `e` is a raw natural number or an `OfNat.ofNat`-application encoding `n`. -/
+def getNatValue? (e : Expr) : MetaM (Option Nat) := do
+  if let some n := getRawNatValue? e then
+    return some n
+  let some (n, _) ← getOfNatValue? e ``Nat | return none
+  return some n
+
+/-- Return `some i` if `e` `OfNat.ofNat`-application encoding an integer, or `Neg.neg`-application of one. -/
+def getIntValue? (e : Expr) : MetaM (Option Int) := do
+  if let some (n, _) ← getOfNatValue? e ``Int then
+    return some n
+  if e.isAppOfArity' ``Neg.neg 3 then
+    let some (n, _) ← getOfNatValue? e.appArg!.consumeMData ``Int | return none
+    return some (-n)
+  return none
+
+/-- Return `some c` if `e` is a `Char.ofNat`-application encoding character `c`. -/
+def getCharValue? (e : Expr) : MetaM (Option Char) := OptionT.run do
+  guard <| e.isAppOfArity' ``Char.ofNat 1
+  let n ← getNatValue? e.appArg!.consumeMData
+  return Char.ofNat n
+
+/-- Return `some s` if `e` is of the form `.lit (.strVal s)`. -/
+def getStringValue? (e : Expr) : (Option String) :=
+  match e with
+  | .lit (.strVal s) => some s
+  | _ => none
+
+/-- Return `some ⟨n, v⟩` if `e` is af `OfNat.ofNat` application encoding a `Fin n` with value `v` -/
+def getFinValue? (e : Expr) : MetaM (Option ((n : Nat) × Fin n)) := OptionT.run do
+  let (v, type) ← getOfNatValue? e ``Fin
+  let n ← getNatValue? (← whnfD type.appArg!)
+  match n with
+  | 0 => failure
+  | m+1 => return ⟨m+1, Fin.ofNat v⟩
+
+/-- Return `some ⟨n, v⟩` if `e` is af `OfNat.ofNat` application encoding a `BitVec n` with value `v` -/
+def getBitVecValue? (e : Expr) : MetaM (Option ((n : Nat) × BitVec n)) := OptionT.run do
+  if e.isAppOfArity' ``BitVec.ofNat 2 then
+    let n ← getNatValue? e.appFn!.appArg!.consumeMData
+    let v ← getNatValue? e.appArg!.consumeMData
+    return ⟨n, BitVec.ofNat n v⟩
+  let (v, type) ← getOfNatValue? e ``BitVec
+  IO.println v
+  let n ← getNatValue? (← whnfD type.appArg!)
+  return ⟨n, BitVec.ofNat n v⟩
+
+/-- Return `some n` if `e` is an `OfNat.ofNat`-application encoding the `UInt8` with value `n`. -/
+def getUInt8Value? (e : Expr) : MetaM (Option UInt8) := OptionT.run do
+  let (n, _) ← getOfNatValue? e ``UInt8
+  return UInt8.ofNat n
+
+/-- Return `some n` if `e` is an `OfNat.ofNat`-application encoding the `UInt16` with value `n`. -/
+def getUInt16Value? (e : Expr) : MetaM (Option UInt16) := OptionT.run do
+  let (n, _) ← getOfNatValue? e ``UInt16
+  return UInt16.ofNat n
+
+/-- Return `some n` if `e` is an `OfNat.ofNat`-application encoding the `UInt32` with value `n`. -/
+def getUInt32Value? (e : Expr) : MetaM (Option UInt32) := OptionT.run do
+  let (n, _) ← getOfNatValue? e ``UInt32
+  return UInt32.ofNat n
+
+/-- Return `some n` if `e` is an `OfNat.ofNat`-application encoding the `UInt64` with value `n`. -/
+def getUInt64Value? (e : Expr) : MetaM (Option UInt64) := OptionT.run do
+  let (n, _) ← getOfNatValue? e ``UInt64
+  return UInt64.ofNat n
+
+/--
+If `e` is literal value, ensure it is encoded using the standard representation.
+Otherwise, just return `e`.
+-/
+def normLitValue (e : Expr) : MetaM Expr := do
+  let e ← instantiateMVars e
+  if let some n ← getNatValue? e then return toExpr n
+  if let some n ← getIntValue? e then return toExpr n
+  if let some ⟨_, n⟩ ← getFinValue? e then return toExpr n
+  if let some ⟨_, n⟩ ← getBitVecValue? e then return toExpr n
+  if let some s := getStringValue? e then return toExpr s
+  if let some c ← getCharValue? e then return toExpr c
+  if let some n ← getUInt8Value? e then return toExpr n
+  if let some n ← getUInt16Value? e then return toExpr n
+  if let some n ← getUInt32Value? e then return toExpr n
+  if let some n ← getUInt64Value? e then return toExpr n
+  return e
+
+end Lean.Meta

src/Lean/Meta/Match/Basic.lean

@@ -343,7 +343,7 @@ partial def toPattern (e : Expr) : MetaM Pattern := do
         match e.getArg! 1, e.getArg! 3 with
         | Expr.fvar x, Expr.fvar h => return Pattern.as x p h
         | _,           _   => throwError "unexpected occurrence of auxiliary declaration 'namedPattern'"
-      else if isMatchValue e then
+      else if (← isMatchValue e) then
         return Pattern.val e
       else if e.isFVar then
         return Pattern.var e.fvarId!

src/Lean/Meta/Match/CaseValues.lean

@@ -30,7 +30,7 @@ private def caseValueAux (mvarId : MVarId) (fvarId : FVarId) (value : Expr) (hNa
     let tag ← mvarId.getTag
     mvarId.checkNotAssigned `caseValue
     let target ← mvarId.getType
-    let xEqValue ← mkEq (mkFVar fvarId) (foldPatValue value)
+    let xEqValue ← mkEq (mkFVar fvarId) (← normLitValue value)
     let xNeqValue := mkApp (mkConst `Not) xEqValue
     let thenTarget := Lean.mkForall hName BinderInfo.default xEqValue  target
     let elseTarget := Lean.mkForall hName BinderInfo.default xNeqValue target

src/Lean/Meta/Match/Match.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.Meta.LitValues
 import Lean.Meta.Check
 import Lean.Meta.Closure
 import Lean.Meta.Tactic.Cases
@@ -94,10 +95,11 @@ private def hasValPattern (p : Problem) : Bool :=
     | .val _ :: _ => true
     | _           => false
 
-private def hasNatValPattern (p : Problem) : Bool :=
-  p.alts.any fun alt => match alt.patterns with
-    | .val v :: _ => v.isRawNatLit -- TODO: support `OfNat.ofNat`?
-    | _           => false
+private def hasNatValPattern (p : Problem) : MetaM Bool :=
+  p.alts.anyM fun alt => do
+    match alt.patterns with
+    | .val v :: _ => return (← getNatValue? v).isSome
+    | _           => return false
 
 private def hasVarPattern (p : Problem) : Bool :=
   p.alts.any fun alt => match alt.patterns with
@@ -130,6 +132,15 @@ private def isValueTransition (p : Problem) : Bool :=
      | .var _ :: _ => true
      | _           => false
 
+private def isFinValueTransition (p : Problem) : MetaM Bool := do
+  if hasVarPattern p then return false
+  if !hasValPattern p then return false
+  p.alts.allM fun alt => do
+     match alt.patterns with
+     | .val v :: _   => return (← getFinValue? v).isSome
+     | .ctor .. :: _ => return true
+     | _             => return false
+
 private def isArrayLitTransition (p : Problem) : Bool :=
   hasArrayLitPattern p && hasVarPattern p
   && p.alts.all fun alt => match alt.patterns with
@@ -137,13 +148,13 @@ private def isArrayLitTransition (p : Problem) : Bool :=
      | .var _ :: _       => true
      | _                 => false
 
-private def isNatValueTransition (p : Problem) : Bool :=
-  hasNatValPattern p
-  && (!isNextVar p ||
+private def isNatValueTransition (p : Problem) : MetaM Bool := do
+  unless (← hasNatValPattern p) do return false
+  return !isNextVar p ||
       p.alts.any fun alt => match alt.patterns with
       | .ctor .. :: _        => true
       | .inaccessible _ :: _ => true
-      | _                    => false)
+      | _                    => false
 
 private def processSkipInaccessible (p : Problem) : Problem := Id.run do
   let x :: xs := p.vars | unreachable!
@@ -584,12 +595,29 @@ private def processArrayLit (p : Problem) : MetaM (Array Problem) := do
       let newAlts := p.alts.filter isFirstPatternVar
       return { p with mvarId := subgoal.mvarId, alts := newAlts, vars := x::xs }
 
-private def expandNatValuePattern (p : Problem) : Problem :=
-  let alts := p.alts.map fun alt => match alt.patterns with
-    | .val (.lit (.natVal 0)) :: ps     => { alt with patterns := .ctor ``Nat.zero [] [] [] :: ps }
-    | .val (.lit (.natVal (n+1))) :: ps => { alt with patterns := .ctor ``Nat.succ [] [] [.val (mkRawNatLit n)] :: ps }
-    | _                                 => alt
-  { p with alts := alts }
+private def expandNatValuePattern (p : Problem) : MetaM Problem := do
+  let alts ← p.alts.mapM fun alt => do
+    match alt.patterns with
+    | .val n :: ps =>
+      match (← getNatValue? n) with
+      | some 0     => return { alt with patterns := .ctor ``Nat.zero [] [] [] :: ps }
+      | some (n+1) => return { alt with patterns := .ctor ``Nat.succ [] [] [.val (toExpr n)] :: ps }
+      | _ => return alt
+    | _ => return alt
+  return { p with alts := alts }
+
+private def expandFinValuePattern (p : Problem) : MetaM Problem := do
+  let alts ← p.alts.mapM fun alt => do
+    match alt.patterns with
+    | .val n :: ps =>
+      match (← getFinValue? n) with
+      | some ⟨n, v⟩ =>
+        let p ← mkLt (toExpr v.val) (toExpr n)
+        let h ← mkDecideProof p
+        return { alt with patterns := .ctor ``Fin.mk [] [toExpr n] [.val (toExpr v.val), .inaccessible h] :: ps }
+      | _ => return alt
+    | _ => return alt
+  return { p with alts := alts }
 
 private def traceStep (msg : String) : StateRefT State MetaM Unit := do
   trace[Meta.Match.match] "{msg} step"
@@ -634,9 +662,12 @@ private partial def process (p : Problem) : StateRefT State MetaM Unit := do
     traceStep ("as-pattern")
     let p ← processAsPattern p
     process p
-  else if isNatValueTransition p then
+  else if (← isNatValueTransition p) then
     traceStep ("nat value to constructor")
-    process (expandNatValuePattern p)
+    process (← expandNatValuePattern p)
+  else if (← isFinValueTransition p) then
+    traceStep ("fin value to constructor")
+    process (← expandFinValuePattern p)
   else if !isNextVar p then
     traceStep ("non variable")
     let p ← processNonVariable p
@@ -654,11 +685,11 @@ private partial def process (p : Problem) : StateRefT State MetaM Unit := do
   else if isArrayLitTransition p then
     let ps ← processArrayLit p
     ps.forM process
-  else if hasNatValPattern p then
+  else if (← hasNatValPattern p) then
     -- This branch is reachable when `p`, for example, is just values without an else-alternative.
     -- We added it just to get better error messages.
     traceStep ("nat value to constructor")
-    process (expandNatValuePattern p)
+    process (← expandNatValuePattern p)
   else
     checkNextPatternTypes p
     throwNonSupported p

src/Lean/Meta/Match/MatchEqs.lean

@@ -15,6 +15,35 @@ import Lean.Meta.Tactic.Contradiction
 
 namespace Lean.Meta
 
+/--
+A custom, approximated, and quick `contradiction` tactic.
+It only finds contradictions of the form `(h₁ : p)` and `(h₂ : ¬ p)` where
+`p`s are structurally equal. The procedure is not quadratic like `contradiction`.
+
+We use it to improve the performance of `proveSubgoalLoop` at `mkSplitterProof`.
+We will eventually have to write more efficient proof automation for this module.
+The new proof automation should exploit the structure of the generated goals and avoid general purpose tactics
+such as `contradiction`.
+-/
+private def _root_.Lean.MVarId.contradictionQuick (mvarId : MVarId) : MetaM Bool := do
+  mvarId.withContext do
+    let mut posMap : HashMap Expr FVarId := {}
+    let mut negMap : HashMap Expr FVarId := {}
+    for localDecl in (← getLCtx) do
+      unless localDecl.isImplementationDetail do
+        if let some p ← matchNot? localDecl.type then
+          if let some pFVarId := posMap.find? p then
+            mvarId.assign (← mkAbsurd (← mvarId.getType) (mkFVar pFVarId) localDecl.toExpr)
+            return true
+          negMap := negMap.insert p localDecl.fvarId
+        if (← isProp localDecl.type) then
+          if let some nFVarId := negMap.find? localDecl.type then
+            mvarId.assign (← mkAbsurd (← mvarId.getType) localDecl.toExpr (mkFVar nFVarId))
+            return true
+          posMap := posMap.insert localDecl.type localDecl.fvarId
+      pure ()
+    return false
+
 /--
   Helper method for `proveCondEqThm`. Given a goal of the form `C.rec ... xMajor = rhs`,
   apply `cases xMajor`. -/
@@ -567,6 +596,8 @@ where
 
   proveSubgoalLoop (mvarId : MVarId) : MetaM Unit := do
     trace[Meta.Match.matchEqs] "proveSubgoalLoop\n{mvarId}"
+    if (← mvarId.contradictionQuick) then
+      return ()
     match (← injectionAny mvarId) with
     | InjectionAnyResult.solved => return ()
     | InjectionAnyResult.failed =>

src/Lean/Meta/Match/Value.lean

@@ -4,46 +4,24 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.Meta.LitValues
 import Lean.Expr
 
 namespace Lean.Meta
--- TODO: produce error for `USize` because `USize.decEq` depends on an opaque value: `System.Platform.numBits`.
-
--- TODO: move?
-private def UIntTypeNames : Array Name :=
-  #[``UInt8, ``UInt16, ``UInt32, ``UInt64, ``USize]
-
-private def isUIntTypeName (n : Name) : Bool :=
-  UIntTypeNames.contains n
-
-def isFinPatLit (e : Expr) : Bool :=
-  e.isAppOfArity `Fin.ofNat 2 && e.appArg!.isRawNatLit
-
-/-- Return `some (typeName, numLit)` if `v` is of the form `UInt*.mk (Fin.ofNat _ numLit)` -/
-def isUIntPatLit? (v : Expr) : Option (Name × Expr) :=
-  match v with
-  | Expr.app (Expr.const (Name.str typeName "mk" ..) ..) val .. =>
-    if isUIntTypeName typeName && isFinPatLit val then
-      some (typeName, val.appArg!)
-    else
-      none
-  | _ => none
-
-def isUIntPatLit (v : Expr) : Bool :=
-  isUIntPatLit? v |>.isSome
-
-/--
-  The frontend expands uint numerals occurring in patterns into `UInt*.mk ..` constructor applications.
-  This method convert them back into `UInt*.ofNat ..` applications.
--/
-def foldPatValue (v : Expr) : Expr :=
-  match isUIntPatLit? v with
-  | some (typeName, numLit) => mkApp (mkConst (Name.mkStr typeName "ofNat")) numLit
-  | _ => v
-
 
 /-- Return true is `e` is a term that should be processed by the `match`-compiler using `casesValues` -/
-def isMatchValue (e : Expr) : Bool :=
-  e.isRawNatLit || e.isCharLit || e.isStringLit || isFinPatLit e || isUIntPatLit e
+def isMatchValue (e : Expr) : MetaM Bool := do
+  let e ← instantiateMVars e
+  if (← getNatValue? e).isSome then return true
+  if (← getIntValue? e).isSome then return true
+  if (← getFinValue? e).isSome then return true
+  if (← getBitVecValue? e).isSome then return true
+  if (getStringValue? e).isSome then return true
+  if (← getCharValue? e).isSome then return true
+  if (← getUInt8Value? e).isSome then return true
+  if (← getUInt16Value? e).isSome then return true
+  if (← getUInt32Value? e).isSome then return true
+  if (← getUInt64Value? e).isSome then return true
+  return false
 
 end Lean.Meta

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.Meta.LitValues
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
 import Init.Data.BitVec.Basic
@@ -18,39 +19,13 @@ structure Literal where
   /-- Actual value. -/
   value : BitVec n
 
-/--
-Try to convert an `OfNat.ofNat`-application into a bitvector literal.
--/
-private def fromOfNatExpr? (e : Expr) : SimpM (Option Literal) := OptionT.run do
-  guard (e.isAppOfArity ``OfNat.ofNat 3)
-  let type ← whnf e.appFn!.appFn!.appArg!
-  guard (type.isAppOfArity ``BitVec 1)
-  let n ← Nat.fromExpr? type.appArg!
-  let v ← Nat.fromExpr? e.appFn!.appArg!
-  return { n, value := BitVec.ofNat n v }
-
-/--
-Try to convert an `BitVec.ofNat`-application into a bitvector literal.
--/
-private def fromBitVecExpr? (e : Expr) : SimpM (Option Literal) := OptionT.run do
-  guard (e.isAppOfArity ``BitVec.ofNat 2)
-  let n ← Nat.fromExpr? e.appFn!.appArg!
-  let v ← Nat.fromExpr? e.appArg!
-  return { n, value := BitVec.ofNat n v }
-
 /--
 Try to convert `OfNat.ofNat`/`BitVec.OfNat` application into a
 bitvector literal.
 -/
-def fromExpr? (e : Expr) : SimpM (Option Literal) := OptionT.run do
-  fromBitVecExpr? e <|> fromOfNatExpr? e
-
-/--
-Convert a bitvector literal into an expression.
--/
--- Using `BitVec.ofNat` because it is being used in `simp` theorems
-def Literal.toExpr (lit : Literal) : Expr :=
-  mkApp2 (mkConst ``BitVec.ofNat) (mkNatLit lit.n) (mkNatLit lit.value.toNat)
+def fromExpr? (e : Expr) : SimpM (Option Literal) := do
+  let some ⟨n, value⟩ ← getBitVecValue? e | return none
+  return some { n, value }
 
 /--
 Helper function for reducing homogenous unary bitvector operators.
@@ -59,8 +34,7 @@ Helper function for reducing homogenous unary bitvector operators.
     (op : {n : Nat} → BitVec n → BitVec n) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some v ← fromExpr? e.appArg! | return .continue
-  let v := { v with value := op v.value }
-  return .done { expr := v.toExpr }
+  return .done { expr := toExpr (op v.value) }
 
 /--
 Helper function for reducing homogenous binary bitvector operators.
@@ -72,8 +46,7 @@ Helper function for reducing homogenous binary bitvector operators.
   let some v₂ ← fromExpr? e.appArg! | return .continue
   if h : v₁.n = v₂.n then
     trace[Meta.debug] "reduce [{declName}] {v₁.value}, {v₂.value}"
-    let v := { v₁ with value := op v₁.value (h ▸ v₂.value) }
-    return .done { expr := v.toExpr }
+    return .done { expr := toExpr (op v₁.value (h ▸ v₂.value)) }
   else
     return .continue
 
@@ -83,8 +56,7 @@ Helper function for reducing homogenous binary bitvector operators.
   unless e.isAppOfArity declName 3 do return .continue
   let some v ← fromExpr? e.appArg! | return .continue
   let some n ← Nat.fromExpr? e.appFn!.appArg! | return .continue
-  let lit : Literal := { n, value := op n v.value }
-  return .done { expr := lit.toExpr }
+  return .done { expr := toExpr (op n v.value) }
 
 /--
 Helper function for reducing bitvector functions such as `getLsb` and `getMsb`.
@@ -105,8 +77,7 @@ Helper function for reducing bitvector functions such as `shiftLeft` and `rotate
   unless e.isAppOfArity declName arity do return .continue
   let some v ← fromExpr? e.appFn!.appArg! | return .continue
   let some i ← Nat.fromExpr? e.appArg! | return .continue
-  let v := { v with value := op v.value i }
-  return .done { expr := v.toExpr }
+  return .done { expr := toExpr (op v.value i) }
 
 /--
 Helper function for reducing bitvector predicates.
@@ -194,16 +165,14 @@ builtin_simproc [simp, seval] reduceAppend ((_ ++ _ : BitVec _)) := fun e => do
   unless e.isAppOfArity ``HAppend.hAppend 6 do return .continue
   let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
   let some v₂ ← fromExpr? e.appArg! | return .continue
-  let v : Literal := { n := v₁.n + v₂.n, value := v₁.value ++ v₂.value }
-  return .done { expr := v.toExpr }
+  return .done { expr := toExpr (v₁.value ++ v₂.value) }
 
 /-- Simplification procedure for casting `BitVec`s along an equality of the size. -/
 builtin_simproc [simp, seval] reduceCast (cast _ _) := fun e => do
   unless e.isAppOfArity ``cast 4 do return .continue
   let some v ← fromExpr? e.appArg! | return .continue
   let some m ← Nat.fromExpr? e.appFn!.appFn!.appArg! | return .continue
-  let v : Literal := { n := m, value := BitVec.ofNat m v.value.toNat }
-  return .done { expr := v.toExpr }
+  return .done { expr := toExpr (BitVec.ofNat m v.value.toNat) }
 
 /-- Simplification procedure for `BitVec.toNat`. -/
 builtin_simproc [simp, seval] reduceToNat (BitVec.toNat _) := fun e => do
@@ -215,15 +184,14 @@ builtin_simproc [simp, seval] reduceToNat (BitVec.toNat _) := fun e => do
 builtin_simproc [simp, seval] reduceToInt (BitVec.toInt _) := fun e => do
   unless e.isAppOfArity ``BitVec.toInt 2 do return .continue
   let some v ← fromExpr? e.appArg! | return .continue
-  return .done { expr := Int.toExpr v.value.toInt }
+  return .done { expr := toExpr v.value.toInt }
 
 /-- Simplification procedure for `BitVec.ofInt`. -/
 builtin_simproc [simp, seval] reduceOfInt (BitVec.ofInt _ _) := fun e => do
   unless e.isAppOfArity ``BitVec.ofInt 2 do return .continue
   let some n ← Nat.fromExpr? e.appFn!.appArg! | return .continue
   let some i ← Int.fromExpr? e.appArg! | return .continue
-  let lit : Literal := { n, value := BitVec.ofInt n i }
-  return .done { expr := lit.toExpr }
+  return .done { expr := toExpr (BitVec.ofInt n i) }
 
 /-- Simplification procedure for ensuring `BitVec.ofNat` literals are normalized. -/
 builtin_simproc [simp, seval] reduceOfNat (BitVec.ofNat _ _) := fun e => do
@@ -232,7 +200,7 @@ builtin_simproc [simp, seval] reduceOfNat (BitVec.ofNat _ _) := fun e => do
   let some v ← Nat.fromExpr? e.appArg! | return .continue
   let bv := BitVec.ofNat n v
   if bv.toNat == v then return .continue -- already normalized
-  return .done { expr := { n, value := BitVec.ofNat n v : Literal }.toExpr }
+  return .done { expr := toExpr (BitVec.ofNat n v) }
 
 /-- Simplification procedure for `<` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceLT (( _ : BitVec _) < _)  := reduceBinPred ``LT.lt 4 (· < ·)
@@ -262,8 +230,7 @@ builtin_simproc [simp, seval] reduceZeroExtend' (zeroExtend' _ _) := fun e => do
   let some v ← fromExpr? e.appArg! | return .continue
   let some w ← Nat.fromExpr? e.appFn!.appFn!.appArg! | return .continue
   if h : v.n ≤ w then
-    let lit : Literal := { n := w, value := v.value.zeroExtend' h }
-    return .done { expr := lit.toExpr }
+    return .done { expr := toExpr (v.value.zeroExtend' h) }
   else
     return .continue
 
@@ -272,8 +239,7 @@ builtin_simproc [simp, seval] reduceShiftLeftZeroExtend (shiftLeftZeroExtend _ _
   unless e.isAppOfArity ``shiftLeftZeroExtend 3 do return .continue
   let some v ← fromExpr? e.appFn!.appArg! | return .continue
   let some m ← Nat.fromExpr? e.appArg! | return .continue
-  let lit : Literal := { n := v.n + m, value := v.value.shiftLeftZeroExtend m }
-  return .done { expr := lit.toExpr }
+  return .done { expr := toExpr (v.value.shiftLeftZeroExtend m) }
 
 /-- Simplification procedure for `extractLsb'` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceExtracLsb' (extractLsb' _ _ _) := fun e => do
@@ -281,16 +247,14 @@ builtin_simproc [simp, seval] reduceExtracLsb' (extractLsb' _ _ _) := fun e => d
   let some v ← fromExpr? e.appArg! | return .continue
   let some start ← Nat.fromExpr? e.appFn!.appFn!.appArg! | return .continue
   let some len ← Nat.fromExpr? e.appFn!.appArg! | return .continue
-  let lit : Literal := { n := len, value := v.value.extractLsb' start len }
-  return .done { expr := lit.toExpr }
+  return .done { expr := toExpr (v.value.extractLsb' start len) }
 
 /-- Simplification procedure for `replicate` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceReplicate (replicate _ _) := fun e => do
   unless e.isAppOfArity ``replicate 3 do return .continue
   let some v ← fromExpr? e.appArg! | return .continue
   let some w ← Nat.fromExpr? e.appFn!.appArg! | return .continue
-  let lit : Literal := { n := v.n * w, value := v.value.replicate w }
-  return .done { expr := lit.toExpr }
+  return .done { expr := toExpr (v.value.replicate w) }
 
 /-- Simplification procedure for `zeroExtend` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceZeroExtend (zeroExtend _ _) := reduceExtend ``zeroExtend zeroExtend
@@ -302,7 +266,6 @@ builtin_simproc [simp, seval] reduceSignExtend (signExtend _ _) := reduceExtend
 builtin_simproc [simp, seval] reduceAllOnes (allOnes _) := fun e => do
   unless e.isAppOfArity ``allOnes 1 do return .continue
   let some n ← Nat.fromExpr? e.appArg! | return .continue
-  let lit : Literal := { n, value := allOnes n }
-  return .done { expr := lit.toExpr }
+  return .done { expr := toExpr (allOnes n) }
 
 end BitVec

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Char.lean

@@ -5,15 +5,14 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.ToExpr
+import Lean.Meta.LitValues
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
 
 namespace Char
 open Lean Meta Simp
 
-def fromExpr? (e : Expr) : SimpM (Option Char) := OptionT.run do
-  guard (e.isAppOfArity ``Char.ofNat 1)
-  let value ← Nat.fromExpr? e.appArg!
-  return Char.ofNat value
+def fromExpr? (e : Expr) : SimpM (Option Char) :=
+  getCharValue? e
 
 @[inline] def reduceUnary [ToExpr α] (declName : Name) (op : Char → α) (arity : Nat := 1) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
@@ -45,7 +44,7 @@ builtin_simproc [simp, seval] reduceToString (toString (_ : Char)) := reduceUnar
 builtin_simproc [simp, seval] reduceVal (Char.val _) := fun e => do
   unless e.isAppOfArity ``Char.val 1 do return .continue
   let some c ← fromExpr? e.appArg! | return .continue
-  return .done { expr := UInt32.toExprCore c.val }
+  return .done { expr := toExpr c.val }
 builtin_simproc [simp, seval] reduceEq  (( _ : Char) = _)  := reduceBinPred ``Eq 3 (. = .)
 builtin_simproc [simp, seval] reduceNe  (( _ : Char) ≠ _)  := reduceBinPred ``Ne 3 (. ≠ .)
 builtin_simproc [simp, seval] reduceBEq  (( _ : Char) == _)  := reduceBoolPred ``BEq.beq 4 (. == .)

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean

@@ -5,37 +5,29 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.ToExpr
+import Lean.Meta.LitValues
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
 
 namespace Fin
 open Lean Meta Simp
 
 structure Value where
-  ofNatFn   : Expr
-  size      : Nat
-  value     : Nat
+  n     : Nat
+  value : Fin n
 
-def fromExpr? (e : Expr) : SimpM (Option Value) := OptionT.run do
-  guard (e.isAppOfArity ``OfNat.ofNat 3)
-  let type ← whnf e.appFn!.appFn!.appArg!
-  guard (type.isAppOfArity ``Fin 1)
-  let size ← Nat.fromExpr? type.appArg!
-  guard (size > 0)
-  let value ← Nat.fromExpr? e.appFn!.appArg!
-  let value := value % size
-  return { size, value, ofNatFn := e.appFn!.appFn! }
+def fromExpr? (e : Expr) : SimpM (Option Value) := do
+  let some ⟨n, value⟩ ← getFinValue? e | return none
+  return some { n, value }
 
-def Value.toExpr (v : Value) : Expr :=
-  let vExpr := mkRawNatLit v.value
-  mkApp2 v.ofNatFn vExpr (mkApp2 (mkConst ``Fin.instOfNat) (Lean.toExpr (v.size - 1)) vExpr)
-
-@[inline] def reduceBin (declName : Name) (arity : Nat) (op : Nat → Nat → Nat) (e : Expr) : SimpM Step := do
+@[inline] def reduceBin (declName : Name) (arity : Nat) (op : {n : Nat} → Fin n → Fin n → Fin n) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
   let some v₂ ← fromExpr? e.appArg! | return .continue
-  unless v₁.size == v₂.size do return .continue
-  let v := { v₁ with value := op v₁.value v₂.value % v₁.size }
-  return .done { expr := v.toExpr }
+  if h : v₁.n = v₂.n then
+    let v := op v₁.value (h ▸ v₂.value)
+    return .done { expr := toExpr v }
+  else
+    return .continue
 
 @[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : Nat → Nat → Bool) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
@@ -71,12 +63,12 @@ builtin_simproc [simp, seval] reduceBNe  (( _ : Fin _) != _)  := reduceBoolPred
 
 /-- Simplification procedure for ensuring `Fin` literals are normalized. -/
 builtin_simproc [simp, seval] isValue ((OfNat.ofNat _ : Fin _)) := fun e => do
-  let some v ← fromExpr? e | return .continue
-  let v' ← Nat.fromExpr? e.appFn!.appArg!
-  if v.value == v' then
+  let some ⟨n, v⟩ ← getFinValue? e | return .continue
+  let some m ← getNatValue? e.appFn!.appArg! | return .continue
+  if n == m then
     -- Design decision: should we return `.continue` instead of `.done` when simplifying.
     -- In the symbolic evaluator, we must return `.done`, otherwise it will unfold the `OfNat.ofNat`
     return .done { expr := e }
-  return .done { expr := v.toExpr }
+  return .done { expr := toExpr v }
 
 end Fin

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean

@@ -5,33 +5,14 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.ToExpr
+import Lean.Meta.LitValues
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
 
 namespace Int
 open Lean Meta Simp
 
-def fromExpr? (e : Expr) : SimpM (Option Int) := OptionT.run do
-  let mut e := e
-  let mut isNeg := false
-  if e.isAppOfArity ``Neg.neg 3 then
-    e := e.appArg!
-    isNeg := true
-  guard (e.isAppOfArity ``OfNat.ofNat 3)
-  let type ← whnf e.appFn!.appFn!.appArg!
-  guard (type.isConstOf ``Int)
-  let value ← Nat.fromExpr? e.appFn!.appArg!
-  let mut value : Int := value
-  if isNeg then value := - value
-  return value
-
-def toExpr (v : Int) : Expr :=
-  let n := v.natAbs
-  let r := mkRawNatLit n
-  let e := mkApp3 (mkConst ``OfNat.ofNat [levelZero]) (mkConst ``Int) r (mkApp (mkConst ``instOfNat) r)
-  if v < 0 then
-    mkAppN (mkConst ``Neg.neg [levelZero]) #[mkConst ``Int, mkConst ``instNegInt, e]
-  else
-    e
+def fromExpr? (e : Expr) : SimpM (Option Int) :=
+  getIntValue? e
 
 @[inline] def reduceUnary (declName : Name) (arity : Nat) (op : Int → Int) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Simproc
+import Lean.Meta.LitValues
 import Lean.Meta.Offset
 import Lean.Meta.Tactic.Simp.Simproc
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Util
@@ -12,20 +13,19 @@ import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Util
 namespace Nat
 open Lean Meta Simp
 
-def fromExpr? (e : Expr) : SimpM (Option Nat) := do
-  let some n ← evalNat e |>.run | return none
-  return n
+def fromExpr? (e : Expr) : SimpM (Option Nat) :=
+  getNatValue? e
 
 @[inline] def reduceUnary (declName : Name) (arity : Nat) (op : Nat → Nat) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← fromExpr? e.appArg! | return .continue
-  return .done { expr := mkNatLit (op n) }
+  return .done { expr := toExpr (op n) }
 
 @[inline] def reduceBin (declName : Name) (arity : Nat) (op : Nat → Nat → Nat) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← fromExpr? e.appFn!.appArg! | return .continue
   let some m ← fromExpr? e.appArg! | return .continue
-  return .done { expr := mkNatLit (op n m) }
+  return .done { expr := toExpr (op n m) }
 
 @[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : Nat → Nat → Bool) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean

@@ -10,9 +10,8 @@ import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
 namespace String
 open Lean Meta Simp
 
-def fromExpr? (e : Expr) : SimpM (Option String) := OptionT.run do
-  let .lit (.strVal s) := e | failure
-  return s
+def fromExpr? (e : Expr) : SimpM (Option String) := do
+  return getStringValue? e
 
 builtin_simproc [simp, seval] reduceAppend ((_ ++ _ : String)) := fun e => do
   unless e.isAppOfArity ``HAppend.hAppend 6 do return .continue

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.Meta.LitValues
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
 
 open Lean Meta Simp
@@ -13,49 +14,30 @@ let ofNat := typeName.getId ++ `ofNat
 let ofNatCore := mkIdent (typeName.getId ++ `ofNatCore)
 let toNat := mkIdent (typeName.getId ++ `toNat)
 let fromExpr := mkIdent `fromExpr
-let toExprCore := mkIdent `toExprCore
-let toExpr := mkIdent `toExpr
 `(
 namespace $typeName
 
-structure Value where
-  ofNatFn : Expr
-  value   : $typeName
-
-def $fromExpr (e : Expr) : OptionT SimpM Value := do
-  guard (e.isAppOfArity ``OfNat.ofNat 3)
-  let type ← whnf e.appFn!.appFn!.appArg!
-  guard (type.isConstOf $(quote typeName.getId))
-  let value ← Nat.fromExpr? e.appFn!.appArg!
-  let value := $(mkIdent ofNat) value
-  return { value, ofNatFn := e.appFn!.appFn! }
-
-def $toExprCore (v : $typeName) : Expr :=
-  let vExpr := mkRawNatLit v.val
-  mkApp3 (mkConst ``OfNat.ofNat [levelZero]) (mkConst $(quote typeName.getId)) vExpr (mkApp (mkConst $(quote (typeName.getId ++ `instOfNat))) vExpr)
-
-def $toExpr (v : Value) : Expr :=
-  let vExpr := mkRawNatLit v.value.val
-  mkApp2 v.ofNatFn vExpr (mkApp (mkConst $(quote (typeName.getId ++ `instOfNat))) vExpr)
+def $fromExpr (e : Expr) : SimpM (Option $typeName) := do
+  let some (n, _) ← getOfNatValue? e $(quote typeName.getId) | return none
+  return $(mkIdent ofNat) n
 
 @[inline] def reduceBin (declName : Name) (arity : Nat) (op : $typeName → $typeName → $typeName) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← ($fromExpr e.appFn!.appArg!) | return .continue
   let some m ← ($fromExpr e.appArg!) | return .continue
-  let r := { n with value := op n.value m.value }
-  return .done { expr := $toExpr r }
+  return .done { expr := toExpr (op n m) }
 
 @[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : $typeName → $typeName → Bool) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← ($fromExpr e.appFn!.appArg!) | return .continue
   let some m ← ($fromExpr e.appArg!) | return .continue
-  evalPropStep e (op n.value m.value)
+  evalPropStep e (op n m)
 
 @[inline] def reduceBoolPred (declName : Name) (arity : Nat) (op : $typeName → $typeName → Bool) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← ($fromExpr e.appFn!.appArg!) | return .continue
   let some m ← ($fromExpr e.appArg!) | return .continue
-  return .done { expr := Lean.toExpr (op n.value m.value) }
+  return .done { expr := toExpr (op n m) }
 
 builtin_simproc [simp, seval] $(mkIdent `reduceAdd):ident ((_ + _ : $typeName)) := reduceBin ``HAdd.hAdd 6 (· + ·)
 builtin_simproc [simp, seval] $(mkIdent `reduceMul):ident ((_ * _ : $typeName)) := reduceBin ``HMul.hMul 6 (· * ·)
@@ -76,14 +58,13 @@ builtin_simproc [simp, seval] $(mkIdent `reduceOfNatCore):ident ($ofNatCore _ _)
   unless e.isAppOfArity $(quote ofNatCore.getId) 2 do return .continue
   let some value ← Nat.fromExpr? e.appFn!.appArg! | return .continue
   let value := $(mkIdent ofNat) value
-  let eNew := $toExprCore value
-  return .done { expr := eNew }
+  return .done { expr := toExpr value }
 
 builtin_simproc [simp, seval] $(mkIdent `reduceToNat):ident ($toNat _) := fun e => do
   unless e.isAppOfArity $(quote toNat.getId) 1 do return .continue
   let some v ← ($fromExpr e.appArg!) | return .continue
-  let n := $toNat v.value
-  return .done { expr := mkNatLit n }
+  let n := $toNat v
+  return .done { expr := toExpr n }
 
 /-- Return `.done` for UInt values. We don't want to unfold in the symbolic evaluator. -/
 builtin_simproc [seval] isValue ((OfNat.ofNat _ : $typeName)) := fun e => do

src/Lean/ToExpr.lean

@@ -48,7 +48,7 @@ instance : ToExpr (Fin n) where
   toExpr a :=
     let r := mkRawNatLit a.val
     mkApp3 (.const ``OfNat.ofNat [0]) (.app (mkConst ``Fin) (toExpr n)) r
-      (mkApp2 (.const ``Fin.instOfNat []) (mkRawNatLit (n-1)) r)
+      (mkApp2 (.const ``Fin.instOfNat []) (mkNatLit (n-1)) r)
 
 instance : ToExpr (BitVec n) where
   toTypeExpr := .app (mkConst ``BitVec) (toExpr n)

tests/lean/lit_values.lean

@@ -0,0 +1,14 @@
+import Lean
+open Lean Meta
+run_meta IO.println (← getNatValue? (toExpr 2))
+run_meta IO.println (← getNatValue? (mkRawNatLit 2))
+run_meta IO.println (← getIntValue? (toExpr (2 : Int)))
+run_meta IO.println (← getIntValue? (toExpr (-2)))
+run_meta IO.println (← getCharValue? (toExpr 'a'))
+#eval getStringValue? (toExpr "hello")
+run_meta IO.println (← getFinValue? (toExpr (3 : Fin 5)))
+run_meta IO.println (← getBitVecValue? (toExpr (3 : BitVec 12)))
+run_meta IO.println (← getUInt8Value? (toExpr (2 : UInt8)))
+run_meta IO.println (← getUInt16Value? (toExpr (2 : UInt16)))
+run_meta IO.println (← getUInt32Value? (toExpr (2 : UInt32)))
+run_meta IO.println (← getUInt64Value? (toExpr (2 : UInt64)))

tests/lean/lit_values.lean.expected.out

@@ -0,0 +1,12 @@
+(some 2)
+(some 2)
+(some 2)
+(some -2)
+(some a)
+(some (⟨5, 3⟩))
+(some (⟨12, 0x003#12⟩))
+(some 2)
+(some 2)
+(some 2)
+(some 2)
+some "hello"

tests/lean/run/bv_math_lit_perf.lean

@@ -16,7 +16,7 @@ def f (x : BitVec 32) : Nat :=
   | 920#32 => 12
   | _      => 1000
 
-set_option maxHeartbeats 500
+set_option maxHeartbeats 2800
 example : f 500#32 = x := by
   simp [f]
   sorry

tests/lean/run/finLit.lean

@@ -22,3 +22,11 @@ def h : Fin 15 → Nat
   | 0 => 5
   | 1 => 45
   | _ => 50
+
+def f' : Fin 2 → Nat
+  | ⟨0, _⟩ => 5
+  | ⟨1, _⟩ => 45
+
+def f'' : Fin 2 → Nat
+  | 0 => 5
+  | ⟨1, _⟩ => 45

tests/lean/run/match_lit_issues.lean

@@ -0,0 +1,88 @@
+@[simp] def f1 (i : Int) (a b : Nat) : Nat :=
+  match i, a with
+  | -1, _  => b
+  | _,  0  => b+1
+  | _, a+1 => f1 (i-1) a (b*2)
+
+#check f1._eq_1
+#check f1._eq_2
+
+example : f1 (-1) a b = b := by simp -- should work
+example : f1 (-2) 0 b = b+1 := by simp
+example : f1 (-2) (a+1) b = f1 (-3) a (b*2) := by simp
+example (h : i ≠ -1) : f1 i (a+1) b = f1 (i-1) a (b*2) := by simp -- should work
+
+@[simp] def f2 (c : Char) (a b : Nat) : Nat :=
+  match c, a with
+  | 'a', _ => b
+  | _,  0  => b+1
+  | _, a+1 => f2 c a (b*2)
+
+example : f2 'a' a b = b   := by simp
+example : f2 'b' 0 b = b+1 := by simp
+example : f2 'b' (a+1) b = f2 'b' a (b*2) := by simp
+example (h : c ≠ 'a') : f2 c (a+1) b = f2 c a (b*2) := by simp
+
+@[simp] def f3 (i : Fin 5) (a b : Nat) : Nat :=
+  match i, a with
+  | 2, _ => b
+  | _,  0  => b+1
+  | _, a+1 => f3 (i+1) a (b*2)
+
+#check f3._eq_1
+#check f3._eq_2
+
+example : f3 2 a b = b   := by simp -- should work
+example : f3 3 0 b = b+1 := by simp
+example : f3 1 (a+1) b = f3 2 a (b*2) := by simp
+example (h : i ≠ 2) : f3 i (a+1) b = f3 (i+1) a (b*2) := by simp; done -- should work
+
+@[simp] def f4 (i : UInt16) (a b : Nat) : Nat :=
+  match i, a with
+  | 2, _ => b
+  | _,  0  => b+1
+  | _, a+1 => f4 (i+1) a (b*2)
+
+#check f4._eq_1
+#check f4._eq_2
+
+example : f4 2 a b = b   := by simp -- should work
+example : f4 3 0 b = b+1 := by simp
+example : f4 1 (a+1) b = f4 2 a (b*2) := by simp
+example (h : i ≠ 2) : f4 i (a+1) b = f4 (i+1) a (b*2) := by simp -- should work
+
+@[simp] def f5 (i : BitVec 8) (a b : Nat) : Nat :=
+  match i, a with
+  | 2, _ => b
+  | _,  0  => b+1
+  | _, a+1 => f5 (i+1) a (b*2)
+
+#check f5._eq_1
+#check f5._eq_2
+
+open BitVec
+
+example : f5 2 a b = b   := by simp -- should work
+example : f5 2#8 a b = b   := by simp -- should work
+example : f5 3 0 b = b+1 := by simp
+example : f5 3#8 0 b = b+1 := by simp
+example : f5 1 (a+1) b = f5 2 a (b*2) := by simp
+example : f5 1#8 (a+1) b = f5 2 a (b*2) := by simp
+example (h : i ≠ 2#8) : f5 i (a+1) b = f5 (i+1) a (b*2) := by simp -- should work
+
+@[simp] def f6 (i : BitVec 8) (a b : Nat) : Nat :=
+  match i, a with
+  | 2#8, _ => b
+  | _,  0  => b+1
+  | _, a+1 => f6 (i+1) a (b*2)
+
+#check f6._eq_1
+#check f6._eq_2
+
+example : f6 2#8 a b = b   := by simp -- should work
+example : f6 2#8 a b = b   := by simp -- should work
+example : f6 3 0 b = b+1 := by simp
+example : f6 3#8 0 b = b+1 := by simp
+example : f6 1 (a+1) b = f6 2 a (b*2) := by simp
+example : f6 1#8 (a+1) b = f6 2 a (b*2) := by simp
+example (h : i ≠ 2#8) : f6 i (a+1) b = f6 (i+1) a (b*2) := by simp -- should work