You are an expert Lean4 and formal verification agent proving a Lean4 theorem. Your output **must** strictly adhere to the specified format.

### Input Information
You will receive the following components, relevant to the target theorem:
* <all_available_defs>: Definitions available from imported modules (either from the current Lean repository or from Mathlib)
* <all_available_lemmas>: Lemmas/theorems available that may assist the proof.
* <local_ctx>...</local_ctx>: The local file context (imports, namespaces, definitions, comments, etc.) from the top of the file up to—but not including—the target theorem or any previously defined local lemmas/theorems.
* <target_theorem>...</target_theorem>: The target theorem statement, ending with `:=`.

**Notes**
1. Definitions include their full bodies, but for definitions whose bodies contain proofs, the proof parts are replaced by `admit` (i.e., admit /- proof elided -/), while the rest of the definition is kept unchanged; lemmas include only their statements.
2. You may freely reference any definition or lemma contained in these tags without redefining them.
3. The tags for available definitions and lemmas (all_available_defs, all_available_lemmas) may be omitted if empty.

### Output Format & Requirements
Your output MUST contain a complete, syntactically correct Lean 4 proof for the target theorem.

**Strict Output Structure:**
<reasoning> 
...
</reasoning> 

<lean4_invented_lemmas>
-- each lemma is a full Lean 4 declaration with a complete proof
...
</lean4_invented_lemmas>

<lean4_proof>
-- Lean 4 proof body of the target theorem
...
</lean4_proof>

**Requirements:**
1. <reasoning> and <lean4_invented_lemmas> are OPTIONAL. Include them only if they aid proof construction.
2. <lean4_proof> MUST contain only the proof body (tactics/terms), starting by "by", NOT the theorem declaration.
3. <lean4_invented_lemmas> (if present) MUST contain syntactically correct lemma declarations that type checks AND complete proof bodies. Defining a lemma using `axiom` is NOT allowed.
4. <reasoning> contains high-level proof planning.
5. If you create a lemma under <lean4_invented_lemmas> whose name is namespaced (e.g., X.Y.Z), you MUST always refer to it using its fully qualified name. Do NOT rely on shortened names. For example, write rw [X.Y.Z], not rw [Z] for invented lemmas.
6. All Lean 4 code MUST be syntactically correct. No `sorry`, `admit`, or non-Lean text. Comments allowed using `--` or `/- ... -/`.
7. Follow the tags and structure EXACTLY. No extra text before, between, or after the sections.
8. Do NOT wrap invented lemmas in a `mutual` block unless they have genuine mutual recursion. Declare each lemma independently.

### Examples are provided here (example input are under "User Prompt", and example assistant response are under "Agent Response"):
Example 1 ------------------- 
User Prompt:
<all_available_defs>
structure BitVec (w : Nat) where
  /-- Construct a `BitVec w` from a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  ofFin ::

  /-- Interpret a bitvector as a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  toFin : Fin (hPow 2 w)
</all_available_defs>

<all_available_lemmas>
theorem List.getElem_append_left{α : Type u_1} {l₁ l₂ : List α} {i : Nat} (hn : i < l₁.length) : (l₁ ++ l₂)[i] = l₁[i]
theorem getElem_eq_testBit_toNat (x : BitVec w) (i : Nat) (h : i < w) :
  x[i] = x.toNat.testBit i := rfl
@[simp, grind =] theorem toNat_cons (b : Bool) (x : BitVec w) :
    (cons b x).toNat = (b.toNat <<< w) ||| x.toNat
@[simp, grind =] theorem getLsbD_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getLsbD x i = false
theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsbD i
</all_available_lemmas>

<local_ctx>
import Mathlib.Computability.NFA
import Mathlib.Data.FinEnum
import Mathlib.Data.Rel
import Mathlib.Data.Vector.Basic
import Blase.AutoStructs.ForLean

open Set
open Mathlib
open SetRel

-- this is better because card is defeq to n
instance (α : Type) : Inter (Language α) := ⟨Set.inter⟩
instance (α : Type) : Union (Language α) := ⟨Set.union⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width.
-/
structure BitVecs (n : Nat) where
  w : Nat
  bvs : List.Vector (BitVec w) n

def BitVecs.cast (bvs : BitVecs n) (h : n = n') : BitVecs n' :=
  { w := bvs.w, bvs := h ▸ bvs.bvs }

abbrev BitVecs.empty : BitVecs n := ⟨0, List.Vector.replicate n .nil⟩
abbrev BitVecs.singleton {w : Nat} (bv : BitVec w) : BitVecs 1 := ⟨w, bv ::ᵥ .nil⟩
abbrev BitVecs.pair {w : Nat} (bv1 bv2 : BitVec w) : BitVecs 2 := ⟨w, bv1 ::ᵥ bv2 ::ᵥ .nil⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width, encoded as a list of
bit vectors of width `n`. The width of the encoded bit vectors is the length of
the list.
-/
abbrev BitVecs' (n : Nat) := List (BitVec n)

@[simps]
def dec (bvs' : BitVecs' n) : BitVecs n where
  w := bvs'.length
  bvs := List.Vector.ofFn fun k => BitVec.ofFn fun i => bvs'[i].getLsbD k

@[simp]
</local_ctx>

<target_theorem>
lemma dec_snoc n (bvs' : BitVecs' n) (a : BitVec n) :
  dec (bvs' ++ [a]) =
    { w := bvs'.length + 1
      bvs := List.Vector.ofFn fun k =>
        BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k) } :=
</target_theorem>

Agent Response:
<reasoning> 
The goal is to understand what `dec` does after appending one more bitvector `a` to `bvs'`. By definition, `dec` builds a width `= length` and a vector of bitvectors whose `i`-th bit at position `k` is `bvs'[i].getLsbD k`. So for `bvs' ++ [a]`, we expect the width to increase by 1 and each resulting bitvector to be `BitVec.cons` of the new bit coming from `a`.

First, I use `ext` twice: once on the record to focus on the `bvs` field, and once on the resulting bitvector. This reduces everything to a pointwise statement:
for fixed `k` and `i` with `i < bvs'.length + 1`,
the bit `(bvs' ++ [a])[i].getLsbD k` should match the bit at index `i` of `BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k)`.

At this point I need a clean description of indexing into `BitVec.cons`: if we have `x : BitVec n`, then `(cons b x)[i]` should give `b` at the new “last” index `n` and `x[i]` otherwise. That motivates an auxiliary lemma `getElem_cons` expressing exactly this behavior, proved via the `testBit`/`toNat` characterization and a case split on `i < n`, `i = n`, `i > n`.

Using `getElem_cons`, the RHS becomes an `if` on whether `i = bvs'.length`. So I split into cases:
- If `i = bvs'.length`, then `(bvs' ++ [a])[i]` is the appended `a`, so both sides reduce to `a.getLsbD k`.
- If `i ≠ bvs'.length`, the bound `i < bvs'.length + 1` forces `i < bvs'.length`. Then `(bvs' ++ [a])[i] = bvs'[i]` by `List.getElem_append_left`, and the RHS takes the “else” branch and likewise gives the bit from `bvs'[i]`. In both subcases, `simp` (plus the definition of `dec`) finishes.

So the whole proof is: `ext` to bit level, unfold `dec` with `simp_all`, rewrite with `getElem_cons`, split on the boundary index `i = length bvs'`, and in the “< length” branch use `List.getElem_append_left` and bounds to line up both sides.
</reasoning> 

<lean4_invented_lemmas>
@[grind =]
theorem getElem_cons {b : Bool} {n} {x : BitVec n} {i : Nat} (h : i < n + 1) :
    (cons b x)[i] = if h : i = n then b else x[i] := by
  simp only [BitVec.getElem_eq_testBit_toNat, BitVec.toNat_cons, Nat.testBit_or]
  rw [Nat.testBit_shiftLeft]
  rcases Nat.lt_trichotomy i n with i_lt_n | i_eq_n | n_lt_i
  · have p1 : ¬(n ≤ i) := by omega
    have p2 : i ≠ n := by omega
    simp [p1, p2]
  · simp only [i_eq_n, ge_iff_le, Nat.le_refl, decide_true, Nat.sub_self, Nat.testBit_zero,
    Bool.true_and, BitVec.testBit_toNat, BitVec.getLsbD_of_ge, Bool.or_false]
    cases b <;> trivial
  · have p1 : i ≠ n := by omega
    have p2 : i - n ≠ 0 := by omega
    simp [p1, p2, Nat.testBit_bool_toNat]
</lean4_invented_lemmas>

<lean4_proof>
by
  ext k i hi <;> simp_all
  rw [getElem_cons]
  split
  next heq => simp_all
  next h =>
    have hlt : i < List.length bvs' := by simp at hi; omega
    rw [List.getElem_append_left hlt]
    simp
</lean4_proof>

### Your task:
<all_available_defs>
def wp (c : m α) (post : α -> l) : l := liftM (n := Cont l) c post

def triple (pre : l) (c : m α) (post : α -> l) : Prop :=
  pre ≤ wp c post

class LogicLift (l : outParam (Type u)) ( k : Type u) [CompleteLattice l] [CompleteLattice k] where
  [lift : MonadLift (Cont l) (Cont k)]
  lift_top {α : Type u} :
    monadLift (m := Cont l) (n := Cont k) (fun (_ : α -> l) => ⊤) = ⊤
  lift_bot {α : Type u} :
    monadLift (m := Cont l) (n := Cont k) (fun (_ : α -> l) => ⊥) = ⊥

def cvc5Path := buildDir / "cvc5"

@[app_unexpander LE.pure] def unexpandPure : Lean.PrettyPrinter.Unexpander
  | `($(_) $p:term) => `(⌜$p:term⌝)
  | _ => throw ()

@[instance high]
instance [md : Monad m] [ccpo : ∀ α, CCPO (m α)] [mono : MonoBind m] : ForIn m Lean.Loop Unit where
  forIn {β} _ := @Loop.forIn m β md ccpo mono

Min in Init.Prelude

Lean.Parser.Term.doFor in Lean.Parser.Do

Lean.Elab.Term.elabTermEnsuringType in Lean.Elab.Term.TermElabM

def hasExitPoint (c : Code) : Bool :=
  hasExitPointPred c fun _ => true

def mkUVarTuple : M Syntax := do
  let ctx ← read
  mkTuple ctx.uvars

def decodeStrLeanList (encoded_str: List Encoding) : List Char :=
  match encoded_str with
  | List.nil => List.nil
  | List.cons hd tl => (List.replicate hd.cnt hd.c) ++ (decodeStrLeanList tl)

def annotate [Monad m] [MonadRef m] [MonadQuotation m] (ref : Syntax) (term : Syntax) : m Syntax :=
  withRef term <| `(with_annotate_term $ref $term)

Lean.Elab.Term.expandMatchAlt in Lean.Elab.BindersUtil

iSup in Mathlib.Order.SetNotation

Lean.mkLevelSucc in Lean.Level

prove_correct maxElem by
  loom_solve

Lean.ReducibilityHints.regular in Lean.Declaration

partial def toTerm (c : Code) : M Syntax := do
  let term ← go c
  if let some ref := c.getRef? then
    annotate ref term
  else
    return term
where
  go (c : Code) : M Syntax := do
    match c with
    | .return ref val     => withRef ref <| returnToTerm val
    | .continue ref       => withRef ref continueToTerm
    | .break ref          => withRef ref breakToTerm
    | .action e           => actionTerminalToTerm e
    | .joinpoint j ps b k => mkJoinPoint j ps (← toTerm b) (← toTerm k)
    | .jmp ref j args     => return mkJmp ref j args
    | .decl _ stx k       => declToTerm stx (← toTerm k)
    | .reassign _ stx k   => reassignToTerm stx (← toTerm k)
    | .seq stx k          => seqToTerm stx (← toTerm k)
    | .ite ref _ o c t e  => withRef ref <| do mkIte o c (← toTerm t) (← toTerm e)
    | .match ref genParam discrs optMotive alts =>
      let mut termAlts := #[]
      for alt in alts do
        let rhs ← toTerm alt.rhs
        let termAlt := mkNode ``Parser.Term.matchAlt #[mkAtomFrom alt.ref "|", mkNullNode #[alt.patterns], mkAtomFrom alt.ref "=>", rhs]
        termAlts := termAlts.push termAlt
      let termMatchAlts := mkNode ``Parser.Term.matchAlts #[mkNullNode termAlts]
      return mkNode ``Parser.Term.«match» #[mkAtomFrom ref "match", genParam, optMotive, discrs, mkAtomFrom ref "with", termMatchAlts]
    | .matchExpr ref «meta» d alts elseBranch => withFreshMacroScope do
      let d' ← `(discr)
      let mut termAlts := #[]
      for alt in alts do
        let rhs ← `(($(← toTerm alt.rhs) : $((← read).m) _))
        let optVar := if let some var := alt.var? then mkNullNode #[var, mkAtomFrom var "@"] else mkNullNode #[]
        let pat := mkNode ``Parser.Term.matchExprPat #[optVar, alt.funName, mkNullNode alt.pvars]
        let termAlt := mkNode ``Parser.Term.matchExprAlt #[mkAtomFrom alt.ref "|", pat, mkAtomFrom alt.ref "=>", rhs]
        termAlts := termAlts.push termAlt
      let elseBranch := mkNode ``Parser.Term.matchExprElseAlt #[mkAtomFrom ref "|", mkHole ref, mkAtomFrom ref "=>", (← toTerm elseBranch)]
      let termMatchExprAlts := mkNode ``Parser.Term.matchExprAlts #[mkNullNode termAlts, elseBranch]
      let body := mkNode ``Parser.Term.matchExpr #[mkAtomFrom ref "match_expr", d', mkAtomFrom ref "with", termMatchExprAlts]
      if «meta» then
        `(Bind.bind (instantiateMVarsIfMVarApp $d) fun discr => $body)
      else
        `(let discr := $d; $body)

private def _root_.Lean.EnvExtension.set (ext : EnvExtension σ) (s : σ)
  [Monad m] [MonadEnv m] : m Unit := do
  Lean.setEnv $ ext.setState (<- getEnv) s

List.range in Init.Data.List.Basic

Lean.instantiateMVars in Lean.MetavarContext

method LeftmostMaximalDigit (input: Array Char)
  return (result: Array Char)
  ensures result.size > 0 → ∀ pos, appearsAt input result pos →
    ∀ pos', pos' < pos →
      ¬(pos' + result.size ≤ input.size ∧
        (∀ i, i < result.size → isDigit input[pos' + i]!) ∧
        (pos' = 0 ∨ ¬isDigit input[pos' - 1]!) ∧
        (pos' + result.size = input.size ∨ ¬isDigit input[pos' + result.size]!))
  do
  let mut i: Nat := 0
  let mut currentStart: Nat := 0
  let mut currentLen: Nat := 0
  let mut bestStart: Nat := 0
  let mut bestLen: Nat := 0
  let mut inDigitSubstring: Bool := false

def NonDetT.assume (as : Prop) [Decidable as] : NonDetT m PUnit :=
  NonDetT.pickCont PUnit (fun _ => as) fun _ => pure .unit

instance : ToString SmtResult where
  toString
    | SmtResult.Sat none => "sat"
    | SmtResult.Sat (some m) => s!"sat\n{m}"
    | SmtResult.Unsat => s!"unsat"
    | SmtResult.Unknown none => s!"unknown"
    | SmtResult.Unknown (some r) => s!"unknown ({r})"
    | SmtResult.Failure none => "failure"
    | SmtResult.Failure (some r) => s!"failure ({r})"

private def _root_.Lean.SimplePersistentEnvExtension.get [Inhabited σ] (ext : SimplePersistentEnvExtension α σ)
  [Monad m] [MonadEnv m] : m σ := do
  return ext.getState (<- getEnv)

abbrev WithName (α : Sort u) (name : Lean.Name := default) := α

MonadExceptOf in Init.Prelude

Nat in Init.Prelude

abbrev MProdWithNames.mk' {α β : Type u} (a : α) (b : β)
  (αName : Lean.Name := default) : MProdWithNames α β αName :=
  @MProdWithNames.mk _ _ αName a b

def Lean.Expr.getName (e : Expr) : MetaM Name := do
  match_expr e with
  | Name.mkStr _ n =>
    match n with
    | .lit (.strVal n) => return n.toName
    | _                => throwError "expected a string literal1"
  | _ => throwError "expected a string literal3"

Lean.hygieneInfoKind in Init.Prelude

structure ToForInTermResult where
  uvars      : Array Var
  term       : Syntax

tryFinally in Init.Control.Except

class MonadOrder extends Monad w, PreOrderFunctor w where
  bind_le {α : Type u} {β : Type u} (x y : w α) (f g : α -> w β) :
    x ≤ y → (∀ a, f a ≤ g a) → bind x f ≤ bind y g

def WPGen.recProd {l : Type u} {m : Type u -> Type v} [Monad m] [LawfulMonad m] [CompleteBooleanAlgebra l] [MAlgOrdered m l]
  {pr: Prod α₁ α₂}
  {mkp : α₁ → α₂ → m β}
  (wpgf : ∀ (a: α₁) (b: α₂), WPGen (mkp a b)):
  WPGen (Prod.recOn pr mkp : m β) where
  get := fun post =>
    (⨅ a, ⨅ b, (wpgf a b).get post)
  prop := by admit /- proof elided -/

def mkTerminalAction (action : Syntax) : CodeBlock :=
  { code := .action action }

private def liftMethodDelimiter (k : SyntaxNodeKind) : Bool :=
  k == ``Parser.Term.do ||
  k == ``Parser.Term.doSeqIndent ||
  k == ``Parser.Term.doSeqBracketed ||
  k == ``Parser.Term.termReturn ||
  k == ``Parser.Term.termUnless ||
  k == ``Parser.Term.termTry ||
  k == ``Parser.Term.termFor

def spv_dot (spv1 spv2: SpV Int) (pnt1 pnt2: ℕ): Int :=
  if (spv1.size) ≤ pnt1 ∨ (spv2.size) ≤ pnt2 then
    0
  else
    if (spv1.ind)[pnt1]! = (spv2.ind)[pnt2]! then
      (spv1.val)[pnt1]! * (spv2.val)[pnt2]! + spv_dot spv1 spv2 (pnt1 + 1) (pnt2 + 1)
    else
      if (spv1.ind)[pnt1]! < (spv2.ind)[pnt2]! then
        spv_dot spv1 spv2 (pnt1 + 1) pnt2
      else
        spv_dot spv1 spv2 pnt1 (pnt2 + 1)
  termination_by ((spv1.size) + (spv2.size) - pnt1 - pnt2)

def concat (terminal : CodeBlock) (kRef : Syntax) (y? : Option Var) (k : CodeBlock) : TermElabM CodeBlock := do
  unless hasTerminalAction terminal.code do
    throwErrorAt kRef "`do` element is unreachable"
  let (terminal, k) ← homogenize terminal k
  let xs := varSetToArray k.uvars
  let y ← match y? with | some y => pure y | none => `(y)
  let ps := xs.map fun x => (x, true)
  let ps := ps.push (y, false)
  let jpDecl ← mkFreshJP ps k.code
  let jp := jpDecl.name
  let terminal ← liftMacroM <| convertTerminalActionIntoJmp terminal.code jp xs
  return { code  := attachJP jpDecl terminal, uvars := k.uvars }

def getLetIdDeclVars (letIdDecl : Syntax) : Array Var :=
  assert! letIdDecl.isOfKind ``Parser.Term.letIdDecl
  
  
  getLetIdVars letIdDecl[0]

let wpgenTypeBuilder x : MetaM Expr :=
    
    mkAppOptM ``WPGen #[.some mExpr, .some monadInstExpr, .some αExpr, .some lExpr, .none, .some omaInstExpr, .some x]
  let branchConds ← do
    pure <| Array.map (fun x => (x.1, x.2.1)) <| List.toArray <| getForallPremises partialMatcher
  let subMonadArgsWithInfo ← branchConds.mapM fun (nm, br) => do
    
    
    
    
    forallTelescope br fun xs body => do
      if xs.isEmpty then
        return ((0, MatcherArgCase.normal), (nm, mαExpr))
      let (case, xs') :=
        if xs[0]!.occurs body
        then (MatcherArgCase.normal, xs)
        else (MatcherArgCase.dropFirst, xs.drop 1)
      pure ((xs'.size, case), (nm, ← mkForallFVars xs' mαExpr))
  let (subMonadArgsInfo, subMonadArgs) := subMonadArgsWithInfo.unzip
  trace[Loom.debug] "subMonadArgs: {subMonadArgs.map Prod.snd}"
  withLocalDecls (← subMonadArgs.mapM fun (nm, t) => do
      let nm' ← mkFreshUserName nm
      pure (nm', BinderInfo.implicit, fun _ => pure t)) fun subMonadArgsFVars => do

instance : Monad (NonDetT m) where
  pure := NonDetT.pure
  bind := NonDetT.bind

class IsHandler {ε : Type*} (handler : outParam (ε -> Prop)) where

def cvc5.arch := if System.Platform.target.startsWith "x86_64" then "x86_64" else "arm64"

def mkMatch (ref : Syntax) (genParam : Syntax) (discrs : Syntax) (optMotive : Syntax) (alts : Array (Alt CodeBlock)) : TermElabM CodeBlock := do
  
  let ws := alts.foldl (union · ·.rhs.uvars) {}
  let alts ← alts.mapM fun alt => do
    let rhs ← extendUpdatedVars alt.rhs ws
    return { ref := alt.ref, vars := alt.vars, patterns := alt.patterns, rhs := rhs.code : Alt Code }
  return { code := .match ref genParam discrs optMotive alts, uvars := ws }

IO.FS.removeDirAll in Init.System.IO

Lean.setEnv in Lean.MonadEnv

def NonDetT.μ {l : Type u} [CompleteLattice l] [MAlgOrdered m l] : NonDetT m l -> l := fun x => NonDetT.wp x id

getThe in Init.Prelude

ExceptT.bindCont in Init.Control.Except

Except in Init.Prelude

def WPGen.recMT1 {l : Type u} {m : Type u -> Type v} [Monad m] [LawfulMonad m] [CompleteBooleanAlgebra l] [MAlgOrdered m l]
  {ls: mt1 γ}
  {ll : γ → m β}
  {el : m β}
  {nl : mt1 γ → mt1 γ → γ → m β → m β → m β}
  (wpgl : ∀ (a: γ), WPGen (ll a))
  (wpge : WPGen el)
  (wpgn : ∀ (l r: mt1 γ) (a: γ) (ml mr: m β), WPGen (nl l r a ml mr)):
  WPGen (mt1.recOn ls ll el nl : m β) where
  get := fun post =>
    (⨅ a, (wpgl a).get post) ⊓
    (wpge.get post) ⊓
    (⨅ l, ⨅ r, ⨅ a, ⨅ ml, ⨅ mr, (wpgn l r a ml mr).get post)
  prop := by admit /- proof elided -/

Lean.Parser.Term.num in Lean.Parser.Term

private def _root_.Lean.SimpleScopedEnvExtension.modify
  (ext : SimpleScopedEnvExtension α σ) (s : σ -> σ)
  [Monad m] [MonadEnv m] : m Unit := do
  Lean.modifyEnv (ext.modifyState · s)

private def recordOption (stx : Syntax) : CommandElabM Unit := do
  let options ← Elab.elabSetOption stx[1] stx[3]
  modify fun s => { s with maxRecDepth := maxRecDepth.get options }
  modifyScope fun scope => { scope with opts := options }

method SubstringSearch (s: Array Char) (p: Char -> Bool) return (res: SubstringResult)

partial def querySolver (goalQuery : String) (withTimeout : Nat) (forceSolver : Option SmtSolver := none) (retryOnUnknown : Bool := false) : MetaM (SmtResult × SmtSolver):= do
  let opts ← getOptions
  let solverName :=
    match forceSolver with
    | some s => s
    | none => loom.solver.smt.default.get opts
  try
  trace[loom.smt.debug] "solver: {solverName}"
  let solver ← createSolver solverName withTimeout
  emitCommandStr solver goalQuery
  emitCommand solver .checkSat
  let stdout ← solver.stdout.getLine
  trace[loom.smt.debug] "[checkSat] stdout: {stdout}"
  let (checkSatResponse, _) ← Auto.Solver.SMT.getSexp stdout
  match checkSatResponse with
  | .atom (.symb "sat") =>
    trace[loom.smt.result] "{solverName} says Sat"
    emitCommand solver .getModel
    let (_, solver) ← solver.takeStdin
    let stdout ← solver.stdout.readToEnd
    let stderr ← solver.stderr.readToEnd
    trace[loom.smt.debug] "stdout: {stdout}"
    trace[loom.smt.debug] "stderr: {stderr}"
    let (model, _) ← Auto.Solver.SMT.getSexp stdout
    solver.kill
    return (SmtResult.Sat s!"{model}", solverName)

Lean.getConstVal in Lean.MonadEnv

semiOutParam in Init.Prelude

ReaderT.read in Init.Prelude

Min.min in Init.Prelude

class CCPOBot (m : Type u -> Type v)  where
  compBot {α} : m α

StateT.modifyGet in Init.Control.State

type in Auto.Lib.Rebind

Auto.runAuto in Auto.Tactic

register_option loom.semantics.choice : LoomSemanticsChoice := {
  defValue := .unspecified
  descr :=
  "Option to control the semantics of non-deterministic choice. Right now we support
  - `demonic` semantics. In this case, the specification of the method should be justified for all possible choices.
    Note that, in total correctness semantics, one also has to prove that all choices are feasible.
  - `angelic` semantics. In this case, the specification of the method should be justified for at least one choice.
  Default is `demonic` semantics.
  "
}

def mkUnless (cond : Syntax) (c : CodeBlock) : MacroM CodeBlock := do
  let thenBranch ← mkPureUnitAction
  return { c with code := .ite (← getRef) none mkNullNode cond thenBranch.code c.code }

def matchNestedTermResult (term : Syntax) (uvars : Array Var) (a r bc : Bool) : MacroM (List Syntax) := do
  let toDoElems (auxDo : Syntax) : List Syntax := getDoSeqElems (getDoSeq auxDo)
  let u ← mkTuplePat uvars
  match a, r, bc with
  | true, false, false =>
    if uvars.isEmpty then
      return toDoElems (← `(do $term:term))
    else
      return toDoElems (← `(do let r ← $term:term; $u:term := r.2; pure r.1))
  | false, true, false =>
    if uvars.isEmpty then
      return toDoElems (← `(do let r ← $term:term; return r))
    else
      return toDoElems (← `(do let r ← $term:term; $u:term := r.2; return r.1))
  | false, false, true => toDoElems <$>
    `(do let r ← $term:term;
         match r with
         | .break u => $u:term := u; break
         | .continue u => $u:term := u; continue)
  | true, true, false => toDoElems <$>
    `(do let r ← $term:term;
         match r with
         | .pure a u => $u:term := u; pure a
         | .return b u => $u:term := u; return b)
  | true, false, true => toDoElems <$>
    `(do let r ← $term:term;
         match r with
         | .pureReturn a u => $u:term := u; pure a
         | .break u => $u:term := u; break
         | .continue u => $u:term := u; continue)
  | false, true, true => toDoElems <$>
    `(do let r ← $term:term;
         match r with
         | .pureReturn a u => $u:term := u; return a
         | .break u => $u:term := u; break
         | .continue u => $u:term := u; continue)
  | true, true, true => toDoElems <$>
    `(do let r ← $term:term;
         match r with
         | .pure a u => $u:term := u; pure a
         | .return a u => $u:term := u; return a
         | .break u => $u:term := u; break
         | .continue u => $u:term := u; continue)
  | false, false, false => unreachable!

structure AltExpr (σ : Type) where
  ref     : Syntax
  var?    : Option Var
  funName : Syntax
  pvars   : Array Syntax
  rhs     : σ
  deriving Inhabited

private def elabSimpTheorem (config : Meta.ConfigWithKey) (id : Origin) (stx : Syntax)
    (post : Bool) (inv : Bool) : TermElabM ElabSimpArgResult := do
  let thm? ← Term.withoutModifyingElabMetaStateWithInfo <| withRef stx do
    let e ← Term.elabTerm stx .none
    Term.synthesizeSyntheticMVars (postpone := .no) (ignoreStuckTC := true)
    let e ← instantiateMVars e
    if e.hasSyntheticSorry then
      return .none
    let e := e.eta
    if e.hasMVar then
      let r ← abstractMVars e
      return some (r.paramNames, r.expr)
    else
      return some (#[], e)
  if let some (levelParams, proof) := thm? then
    let thms ← mkSimpTheoremFromExpr id levelParams proof (post := post) (inv := inv) (config := config)
    return .addEntries <| thms.map (SimpEntry.thm ·)
  else
    return .none

def simpleAddThm (n : Name) (tp : Expr) (pf : Expr)
  (attr : Array Attribute := #[]) : TermElabM Unit := do
  addDecl <|
    Declaration.thmDecl <|
      mkTheoremValEx n [] tp pf []
  applyAttributes n attr

Lean.Parser.Term.doTry in Lean.Parser.Do

structure Context where
  ref         : Syntax
   
  m           : Syntax
   
  returnType  : Syntax
  mutableVars : VarSet := {}
  insideFor   : Bool := false

class PreOrderFunctor where preord : (α : Type u) -> Preorder (w α)

DoResultPRBC in Init.Core

Array.foldlM in Init.Data.Array.Basic

def NonDetT.μ  {l : Type u} [CompleteLattice l] [MAlgOrdered m l] : NonDetT m l -> l := fun x => NonDetT.wp x id

def NonDetT.pick (τ : Type u) : NonDetT m τ :=
  NonDetT.pickCont _ (fun _ => True) pure

Lean.mkNode in Init.Prelude

Top in Mathlib.Order.Notation

def partiallyInstantiateWPGen (outerArgs : Array Expr) (a : MatcherWPGen) (b : MatcherApp) : MetaM Expr := do
  let wpgen := a.wpgenExpr.instantiateLevelParams a.lvls.toList (← mkFreshLevelMVars a.lvls.size)
  try
    
    let fma := a.firstMonadArgPos
    let alts' ← do
      lambdaBoundedTelescope wpgen (fma + a.matcherInfo.numAlts) fun xs _ => do
      b.alts.mapIdxM fun i alt => do
        let numArgRequired ← Expr.getNumHeadForalls <$> inferType xs[fma + i]!
        let numArgs := alt.getNumHeadLambdas
        
        if numArgRequired + 1 == numArgs then
          return mkApp alt (mkConst ``Unit.unit)
        pure alt
    let args : Array (Option Expr) := Array.replicate fma none
     
    
    let args := args.set! a.monadRetTypePos (some outerArgs[0]!)
    let args := args.set! a.monadArgPos (some outerArgs[1]!)
    let args := args.set! a.monadInstPos (some outerArgs[2]!)
    let args := args.set! a.omaTypePos (some outerArgs[3]!)
    
    
     
    let partialwpgen ← args.foldlM (init := wpgen) fun e arg => do
      match arg with
      | .some v => pure <| mkApp e v
      | .none => pure <| mkApp e (← mkFreshExprMVar none)
    let res := mkAppN partialwpgen alts'
    check res   
    pure res
  catch ex =>
    trace[Loom.debug] m!"Error in [{decl_name%}]: {ex.toMessageData}"
    return wpgen

private def _root_.Lean.SimpleScopedEnvExtension.modify
  (ext : SimpleScopedEnvExtension α σ) (s : σ -> σ)
  [Monad m] [MonadEnv m] : m Unit := do
  Lean.modifyEnv (ext.modifyState · s)

ReaderT.bind in Init.Prelude

def cvc5.target := s!"{os}-{arch}-static"

Lean.mkStrLit in Lean.Expr

method SpMSpV
  (mut out: Array Int)
  (spm: Array (SpV Int))
  (spv: SpV Int) return (u: Unit)
  ensures out.size = spm.size
  ensures ∀ i < spm.size, out[i]! = spv_dot spm[i]! spv 0 0
  do
    out := Array.replicate spm.size 0
    let mut spmInd := Array.replicate spm.size 0
    let mut spvInd := Array.replicate spm.size 0
    while_some i :| i < spm.size ∧ spmInd[i]! < spm[i]!.size ∧ spvInd[i]! < spv.size
    invariant spvInd.size = spm.size
    invariant spmInd.size = spm.size
    invariant out.size = spm.size
    invariant ∀ i < spmInd.size, spmInd[i]! <= spm[i]!.size
    invariant ∀ i < spvInd.size, spvInd[i]! <= spv.size
    invariant ∀ i < spm.size, out[i]! + spv_dot spm[i]! spv spmInd[i]! spvInd[i]! = spv_dot spm[i]! spv 0 0
    done_with ∀ i < spm.size, spmInd[i]! = spm[i]!.size ∨ spvInd[i]! = spv.size
    do
      let ind_m := spmInd[i]!
      let ind_v := spvInd[i]!
      if spm[i]!.ind[ind_m]! = spv.ind[ind_v]! then
        out[i] += spm[i]!.val[ind_m]! * spv.val[ind_v]!
        spmInd[i] += 1
        spvInd[i] += 1
      else
        if spm[i]!.ind[ind_m]! < spv.ind[ind_v]! then
          spmInd[i] += 1
        else
          spvInd[i] += 1
    return

private def getDoSeq (doStx : Syntax) : Syntax :=
  doStx[1]

Array.filter in Init.Data.Array.Basic

def Lake.unzip (file : FilePath) (dir : FilePath) : LogIO PUnit := do
  IO.FS.createDirAll dir
  proc (quiet := true) {
    cmd := "unzip"
    args := #["-d", dir.toString, file.toString]
  }

Std.TreeMap in Std.Data.TreeMap.Basic

Lean.Meta.withTrackingZetaDeltaSet in Lean.Meta.Basic

@[inline]
def Loop.forIn {β : Type u} [Monad m] [∀ α, CCPO (m α)] [MonoBind m]
  (_ : Lean.Loop) (init : β) (f : Unit → β → m (ForInStep β)) : m β :=
  Loop.forIn.loop f init

private def _root_.Lean.EnvExtension.get [Inhabited σ] (ext : EnvExtension σ)
  [Monad m] [MonadEnv m] : m σ := do
  return ext.getState (<- getEnv)

PUnit in Init.Prelude

lamEVarTy in Auto.Parser.TPTP

Lean.Loop in Init.While

inductive SmtResult
   
  | Sat (modelString : Option String)
  | Unsat
  | Unknown (reason : Option String)
  | Failure (reason : Option String)
deriving Inhabited

Lean.Elab.Term.expandOptType in Lean.Elab.BindersUtil

instance [MonadNonDet m] : ForIn m Lean.Loop Unit where
  forIn {β} _ _ init f := @MonadNonDet.rep m _ β init (f ())

Lean.Meta.Simp.getSimprocs in Lean.Meta.Tactic.Simp.Simproc

Lean.mkArrow in Lean.CoreM

def termBeforeReqEnsDo := withForbidden "require" (withForbidden "ensures" Term.termBeforeDo)

def WPGen.forWithInvariantLoop {β}
  {init : β} {f : Unit -> β → NonDetT m (ForInStep β)}
  (inv : β → List l) (on_done' : β → l)
  (measure : β → Option ℕ)
  (wpg : ∀ b, WPGen (f () b)) :
    WPGen (forIn Lean.Loop.mk init (fun u b => do
        invariantGadget (inv b)
        onDoneGadget (on_done' b)
        decreasingGadget (measure b)
        f u b)) where
    get := ⌜∀ b, invariantSeq (inv b) <= (wpg b).get fun
      | .yield b' => invariantSeq <| inv b'
      | .done b'  => invariantSeq (inv b') ⊓ on_done' b'⌝
      ⊓ spec
      ((inv init).foldr (·⊓·) ⊤)
      (fun b => (inv b).foldr (·⊓·) ⊤ ⊓ on_done' b)
    prop := by admit /- proof elided -/

def chain_le (a : Array Int) (h_adjacent : ∀ k, 0 ≤ k ∧ k < a.size - 1 → a[k]! ≤ a[k+1]!)
    (i j : Nat) (h_i_ge : 0 ≤ i) (h_i_lt_j : i < j) (h_j_lt_size : j < a.size) : a[i]! ≤ a[j]! :=
  if h : j = i + 1 then by
    
    rw [h]
    exact h_adjacent i ⟨h_i_ge, by admit /- proof elided -/
    ⟩
  else by
    
    have h_next : i + 1 < j := by admit /- proof elided -/

Lean.Meta.mkFreshExprSyntheticOpaqueMVar in Lean.Meta.Tactic.Util

instance : MonadLift m (NonDetT m) where
  monadLift x := NonDetT.vis x pure

instance [Monad m] [LawfulMonad m] : LawfulMonadLiftT m (ReaderT σ m) where
  monadLift_pure := by admit /- proof elided -/

Lean.Parser.skip in Lean.Parser.Basic

Lean.Parser.Term.termUnless in Lean.Parser.Do

private def expandDoLetExpr? (stx : Syntax) (doElems : List Syntax) : MacroM (Option Syntax) := match stx with
  | `(doElem| let_expr $pat:matchExprPat := $discr:term | $elseBranch:doSeq) =>
    return some (← `(doElem| match_expr (meta := false) $discr:term with
                             | $pat:matchExprPat => $(mkDoSeq doElems.toArray)
                             | _ => $elseBranch))
  | `(doElem| let_expr $pat:matchExprPat ← $discr:term | $elseBranch:doSeq) =>
    return some (← `(doElem| match_expr $discr:term with
                             | $pat:matchExprPat => $(mkDoSeq doElems.toArray)
                             | _ => $elseBranch))
  | _ => return none

List.head! in Init.Data.List.BasicAux

def cvc5.os :=
  if System.Platform.isWindows then "Win64"
  else if System.Platform.isOSX then "macOS"
  else "Linux"

def getSpecKey (ty : Expr) : MetaM (Expr × Loom.SpecType) := do
  let (_xs, _bis, body) ← forallMetaTelescope ty
  let x <- match_expr body with
  | triple _m _mInst _α _l _lInst _mPropInst _pre x _post => pure (x, .triple)
  | WPGen _m _mInst _α _l _lInst _mPropInst x => pure (x, .wpgen)
  | _ => throwError s!"not a triple: {body}"
  
  
  
  
  return x

ForIn.forIn in Init.Core

Lean.Meta.getPropHyps in Lean.Meta.Tactic.Util

def getDoPatDeclVars (doPatDecl : Syntax) : TermElabM (Array Var) := do
  let pattern := doPatDecl[0]
  getPatternVarsEx pattern

f in Test.SmtTranslation.Trigger

leaf in Test.SmtTranslation.Inductive

class MAlgLiftT
  (m : (Type u -> Type v)) (l : (Type u)) [Monad m] [CompleteLattice l] [MAlgOrdered m l]
  (n : (Type u -> Type w)) (k : outParam (Type u)) [Monad n] [CompleteLattice k] [MAlgOrdered n k]
  [MonadLiftT m n]
  where
    [cl : LogicLiftT l k]
    μ_lift (x : m α) : MAlg.lift (liftM (n := n) x) f = liftM (n := Cont k) (MAlg.lift x) f

class MonadNonDet (m : Type u → Type v) where
  pick : (τ : Type u) → [Inhabited τ] → m τ
  
  pickSuchThat : (τ : Type u) → (p : τ → Prop) → [Findable p] → m τ
  assume : (as : Prop) → [Decidable as] → m PUnit.{u+1}
  
  rep {α : Type u} : α → (α → m (ForInStep α)) → m α

Lean.Elab.liftMacroM in Lean.Elab.Util

instance {p : α -> Prop} [Encodable α] [DecidablePred p] : Findable p where
  find := fun _ => find p
  find_none := find_none p
  find_some_p := find_some_p p _

System.Platform.isOSX in Init.System.Platform

instance : Inhabited (SpV Int) where
  default :=
  { ind := #[],
    val := #[],
    size := 0,
    size_eq := (by admit /- proof elided -/
    ),
    inc := (fun i j h_i h_j i_lt_j => by admit /- proof elided -/
    ) }

Lake.JobM in Lake.Build.Job.Monad

class CCPOBotLawful (m : Type u -> Type v) [∀ α, Lean.Order.CCPO (m α)] [CCPOBot m] where
  prop {α} : CCPOBot.compBot (m := m) (α := α) = Lean.Order.bot

Auto.Reif.ReifM in Auto.Translation.ReifM

instance : MonadNonDet (NonDetT m) where
  pick   := .pick
  assume := .assume
  pickSuchThat := .pickSuchThat
  rep := .repeat

Lean.Parser.Term.doExpr in Lean.Parser.Do

abbrev M := ReaderT Context TermElabM

Except.bind in Init.Control.Except

Lean.Meta.Simp.Context in Lean.Meta.Tactic.Simp.Types

let wpgenPost ← do
    let motive ← do
      
      let (_, discrsBuilder) ← discrs.foldlM (init := (#[], #[])) fun (xspre, res) x => do
        let nm ← mkFreshUserName (← x.fvarId!.getUserName)
        let xty ← inferType x
        let ty xspre' := pure <| xty.replaceFVars xspre xspre'
        pure (xspre.push x, res.push (nm, ty))
      
      let lhs ← instantiateLambda wpgenGet #[postExpr]
      let rhs ← mkAppOptM ``wp
        #[.some mExpr, .some monadInstExpr, .some αExpr, .some lExpr, .none,
          .some omaInstExpr, .some targetMatcher, .some postExpr]
      withLocalDeclsD discrsBuilder fun discrs' => do
        let rhs' := rhs.replaceFVars discrs discrs'
        let eqs ← discrs'.mapIdxM fun i lhs => mkEq discrs[i]! lhs
        let le ← mkAppM ``LE.le #[lhs, rhs']
        let tmp ← mkArrowN eqs le
        mkLambdaFVars discrs' tmp
    trace[Loom.debug] "motive for the splitter in proof: {motive}"
    let paramsAndDiscrs' := paramsAndDiscrs.set! matcherInfo.getMotivePos motive
    let partialSplitter := mkAppN splitter paramsAndDiscrs'
    let partialSplitterType ← inferType partialSplitter
    let numBranches := matcherInfo.numAlts    
    let branchConds ← do
      pure <| List.map (fun x => x.2.1) <| List.take numBranches <| getForallPremises partialSplitterType
    let wpgenPostSubProofs ← branchConds.toArray.mapIdxM fun i br => do
      trace[Loom.debug] "subgoal {i}: {br}"
      
      let res ← forallTelescope br fun xs body => do
        
        
        
        let body ← whnf body
        forallTelescope body fun eqs body => do

Lean.Parser.Term.doLet in Lean.Parser.Do

Lean.binderIdent in Init.Notation

inductive LoomSolver : Type where
  | cvc5
  | smt (smtSolver : SmtSolver)
  | grind
  | custom

def WPGen.recOption {l : Type u} {m : Type u -> Type v} [Monad m] [LawfulMonad m] [CompleteBooleanAlgebra l] [MAlgOrdered m l]
   {x : m β} {y : α → m β} {val: Option α}
  (wpgx : WPGen x) (wpgy : ∀ a, WPGen (y a)) :
  WPGen (Option.recOn val x y : m β) where
  get := fun post =>
    (wpgx.get post) ⊓ (⨅ a, (wpgy a).get post)
  prop := by admit /- proof elided -/

instance MAlgExceptHdDet (hd : ε -> Prop)
  [CompleteLattice l] [inst: MAlgOrdered m l] [IsHandler hd]
  [inst': MAlgDet m l] : MAlgDet (ExceptT ε m) l where
  angelic := by admit /- proof elided -/

Lean.MessageData.joinSep in Lean.Message

private def List.foldldM.{u, v, w} {m : Type u → Type v} [Monad m] {s : Type u} {α : Type w} (f : s → α → m s)
  (g : α → m s) (init : s) (l : List α) : m s :=
  match l with
  | [] => pure init
  | a :: l' => do
    let init' ← g a
    List.foldlM f init' l'

class MAlgDet (l : outParam (Type v)) [Monad m] [CompleteLattice l] [MAlgOrdered m l] where
   
  demonic {α ι : Type v} (c : m α) (p : ι -> α -> l) [Nonempty ι] :
    ⨅ i, MAlg.lift c (p i) ≤ MAlg.lift c (fun x => ⨅ i, p i x)
   
  angelic {α ι : Type v} (c : m α) (p : ι -> α -> l) [Nonempty ι] :
    ⨆ i, MAlg.lift c (p i) ≥ MAlg.lift c (fun x => ⨆ i, p i x)

Lean.MessageData in Lean.Message

Functor in Init.Prelude

def WPGen.default (x : m α) : WPGen x where
  get := wp x
  prop := by admit /- proof elided -/

Lean.Parser.Term.optIdent in Lean.Parser.Term.Basic

abbrev Except.bind' {m : Type u -> Type v} {ε α β} [Monad m] : Except ε α -> (α -> ExceptT ε m β) -> ExceptT ε m β :=
  fun x f => bind (m := ExceptT ε m) (pure (f := m) x) f

def z3.baseUrl := "https://github.com/Z3Prover/z3/releases/download"

def failureGoalStr (solver : Option SmtSolver := none) : String := s!"{solverStr solver}solver invocation failed"

Lean.Elab.Term.Quotation.getPatternVars in Lean.Elab.Quotation.Util

cmd in Auto.Parser.TPTP

def anyGoalsWithTag (tactic : MVarId → TacticM (Option (Name × α))) : TacticM (Array α) := do
  let mvarIds ← getGoals
  let mut res : Array α := #[]
  let mut mvarIdsNew : Array MVarId := #[]
  for mvarId in mvarIds do
    unless (← mvarId.isAssigned) do
      setGoals [mvarId]
      try
        let r ← tactic mvarId
        let goals <- getUnsolvedGoals
        if let some ⟨n, r⟩ := r then
          for goal in goals do
            goal.setTag n
          res := res.push r
          mvarIdsNew := mvarIdsNew ++ goals
      catch _ =>
        mvarIdsNew := mvarIdsNew.push mvarId
  setGoals mvarIdsNew.toList
  pure res

instance : CCPOBotLawful DivM where
  prop := by admit /- proof elided -/

Lean.Parser.Term.doReassign in Lean.Parser.Do

Lean.Parser.Term.app in Lean.Parser.Term

Stream.next? in Init.Data.Stream

def Array.sumUpTo [Inhabited α] [AddCommMonoid β] (a : Array α) (f : ℕ -> α -> β) (bound : ℕ) : β :=
  ∑ i ∈ Finset.range bound, f i a[i]!

Except.ok in Init.Prelude

private def Array.andListWithName (ts : Array (TSyntax `term)) (name_prefix : TSyntax `name) : TermElabM (TSyntax `term) := do
  if ts.size = 0 then `(term| True) else
    let mut t <- `(term| with_name_prefix $name_prefix:name $(ts[0]!))
    for t' in ts[1:] do
      t <- `(term| (with_name_prefix $name_prefix:name $t') ∧ $t)
    return t

if hasReturn forInBodyCodeBlock.code then
        let forInBody ← liftMacroM <| destructTuple uvars (← `(r)) forInBody
        let optType ← `(Option $((← read).returnType))
        let forInTerm ← if let some h := h? then
          annotate doFor
            (← `(for_in'% $(xs) (MProdWithNames.mk (none : $optType) $uvarsTuple) fun $x $h (r : MProdWithNames $optType _) => let r := r.2; $forInBody))
        else
          annotate doFor
            (← `(for_in% $(xs) (MProdWithNames.mk (none : $optType) $uvarsTuple) fun $x (r : MProdWithNames $optType _) => let r := r.2; $forInBody))
        let auxDo ← `(do let r ← $forInTerm:term;
                         $uvarsTuplePat:term := r.2;
                         match r.1 with
                         | none => Pure.pure (ensure_expected_type% "type mismatch, `for`" PUnit.unit)
                         | some a => return ensure_expected_type% "type mismatch, `for`" a)
        doSeqToCode (getDoSeqElems (getDoSeq auxDo) ++ doElems)
      else
        let forInBody ← liftMacroM <| destructTuple uvars (← `(r)) forInBody
        let forInTerm ← if let some h := h? then
          annotate doFor (← `(for_in'% $(xs) $uvarsTuple fun $x $h r => $forInBody))
        else
          annotate doFor (← `(for_in% $(xs) $uvarsTuple fun $x r => $forInBody))
        if doElems.isEmpty then
          let auxDo ← `(do let r ← $forInTerm:term;
                           $uvarsTuplePat:term := r;
                           Pure.pure (ensure_expected_type% "type mismatch, `for`" PUnit.unit))
          doSeqToCode <| getDoSeqElems (getDoSeq auxDo)
        else
          let auxDo ← `(do let r ← $forInTerm:term; $uvarsTuplePat:term := r)
          doSeqToCode <| getDoSeqElems (getDoSeq auxDo) ++ doElems

private def _root_.Lean.SimpleScopedEnvExtension.get [Inhabited σ] (ext : SimpleScopedEnvExtension α σ)
  [Monad m] [MonadEnv m] : m σ := do
  return ext.getState (<- getEnv)

DecidablePred in Init.Prelude

List.map in Init.Prelude

Lean.Name.mkStr in Init.Prelude

def satGoalStr (solver : Option SmtSolver := none) : String := s!"{solverStr solver}the goal is false"

def findNat (p : Nat -> Prop) [DecidablePred p] : Option Nat :=
  let rec aux i :=
    if p i then
      some i
    else
      aux (i + 1)
  partial_fixpoint
  aux 0

List.replicate in Init.Data.List.Basic

Lean.Meta.ConfigWithKey in Lean.Meta.Basic

Lean.indentExpr in Lean.Message

method SpVSpV
  (mut out: Array Int)
  (spv1: SpV Int)
  (spv2: SpV Int) return (u: Unit)
  ensures out.size = 1
  ensures out[0]! = spv_dot spv1 spv2 0 0
  do
    out := Array.replicate 1 0
    let mut pnt1 := 0
    let mut pnt2 := 0
    while pnt1 ≠ spv1.size ∧ pnt2 ≠ spv2.size
    invariant out.size = 1
    invariant pnt1 ≤ spv1.size ∧ pnt2 ≤ spv2.size
    invariant out[0]! + spv_dot spv1 spv2 pnt1 pnt2 = spv_dot spv1 spv2 0 0
    done_with pnt1 = spv1.size ∨ pnt2 = spv2.size
    do
      if (spv1.ind)[pnt1]! = (spv2.ind)[pnt2]! then
        out[0] += (spv1.val)[pnt1]! * (spv2.val)[pnt2]!
        pnt1 := pnt1 + 1
        pnt2 := pnt2 + 1
      else
        if (spv1.ind)[pnt1]! < (spv2.ind)[pnt2]! then
          pnt1 := pnt1 + 1
        else
          pnt2 := pnt2 + 1
    return

StateT.run in Init.Control.State

Int in Init.Data.Int.Basic

structure VelvetObligation where
  binderIdents : TSyntaxArray `Lean.Parser.Term.bracketedBinder
  modIds : Array Ident
  ids : Array Ident
  retId : Ident
  ret : Term
  pre : Term
  post : Term
deriving Inhabited

And in Init.Prelude

structure JPDecl where
  name : Name
  params : Array (Var × Bool)
  body : Code

instance (σ : Type u) (l : Type u) (m : Type u -> Type v)
  [CompleteLattice l]
  [Monad m] [LawfulMonad m] [inst: MAlgOrdered m l] : MAlgOrdered (ReaderT σ m) (σ -> l) where
  μ := fun rp r => inst.μ $ (· r) <$> rp r
  μ_ord_pure := by admit /- proof elided -/

instance (l : Type u) {m : Type u -> Type v} [Monad m] [MAlg m l] : MonadLiftT m (Cont l) where
  monadLift := MAlg.lift

partial def extendUpdatedVarsAux (c : Code) (ws : VarSet) : TermElabM Code :=
  let rec update (c : Code) : TermElabM Code := do
    match c with
    | .joinpoint j ps b k    => return .joinpoint j ps (← update b) (← update k)
    | .seq e k               => return .seq e (← update k)
    | .match ref g ds t alts =>
      if alts.any fun alt => alt.vars.any fun x => ws.contains x.getId then
        
        pullExitPoints c
      else
        return .match ref g ds t (← alts.mapM fun alt => do pure { alt with rhs := (← update alt.rhs) })
    | .matchExpr ref «meta» d alts e =>
      if alts.any fun alt => alt.vars.any fun x => ws.contains x.getId then
        
        pullExitPoints c
      else
        let alts ← alts.mapM fun alt => do pure { alt with rhs := (← update alt.rhs) }
        let e ← update e
        return .matchExpr ref «meta» d alts e
    | .ite ref none o c t e => return .ite ref none o c (← update t) (← update e)
    | .ite ref (some h) o cond t e =>
      if ws.contains h.getId then
        
        pullExitPoints c
      else
        return Code.ite ref (some h) o cond (← update t) (← update e)
    | .reassign xs stx k => return .reassign xs stx (← update k)
    | .decl xs stx k => do
      if xs.any fun x => ws.contains x.getId then
        
        pullExitPoints c
      else
        return .decl xs stx (← update k)
    | c => return  c
  update c

iInf in Mathlib.Order.SetNotation

private def _root_.Lean.SimpleScopedEnvExtension.get [Inhabited σ] (ext : SimpleScopedEnvExtension α σ)
  [Monad m] [MonadEnv m] : m σ := do
  return ext.getState (<- getEnv)

def deriveDecidableNatUpperBound (tms : List <| TSyntax `term)
  : MacroM (TSyntax `Lean.Parser.Tactic.tacticSeq) := do
  match tms with
  | [] => `(Lean.Parser.Tactic.tacticSeq| (infer_instance) )
  | tm :: tms' =>
    let res ← deriveDecidableNatUpperBound tms'
    let h := mkIdent `h
    `(Lean.Parser.Tactic.tacticSeq|
      refine @$(mkIdent ``Decidable.Nat.decidableBallLT') _ ($tm) ?_ ?_
      on_goal 1=> intro _
      on_goal 1=>
        $res
      constructor
      next => (intro $h:ident ; intros ; apply $h:ident <;> (try split_ands) <;> (solve
          | omega
          | grind))
      next => grind)

Lean.Meta.mkAppM in Lean.Meta.AppBuilder

Lean.Meta.mkFreshExprMVar in Lean.Meta.Basic

def mkReassignCore (xs : Array Var) (stx : Syntax) (c : CodeBlock) : TermElabM CodeBlock := do
  let us := c.uvars
  let ws := insertVars us xs
  
  
  let code ← if xs.any fun x => !us.contains x.getId then extendUpdatedVarsAux c.code ws else pure c.code
  pure { code := .reassign xs stx code, uvars := ws }

abbrev NonDetT.prop {α : Type u} : (s : NonDetT m α) -> Cont l α
  | .pure x => Pure.pure x
  | .vis x f => fun post => wlp x fun y => NonDetT.prop (f y) post
  | .pickCont _ p f => fun post =>
    (⨅ t, ⌜p t⌝ ⇨ NonDetT.prop (f t) post) ⊓ (⨆ t, ⌜p t⌝)

Lean.registerSimplePersistentEnvExtension in Lean.EnvExtension

List.toArray in Init.Prelude

Lean.Parser.Term.matchAlt in Lean.Parser.Term

def renameOld (n : Name) : TacticM Unit := withMainContext do
  (<- getMainGoal).modifyLCtx fun hyps => Id.run do
    let mut hypsNew := hyps
    for hyp in hyps.decls.toArray.reverse do
      if hyp.isSome then
        let n' := hyp.get!.userName
        if n' == n then
          hypsNew := hyps.renameUserName n' (n'.toString ++ "Old" |>.toName)
    return hypsNew

def   NonDetT.wp {l : Type u} {α : Type u} [CompleteLattice l] [MAlgOrdered m l] : NonDetT m α -> Cont l α
  | .pure ret => pure ret
  | .vis x f => fun post => _root_.wp x fun a => wp (f a) post
  | .pickCont _ p f => fun post => ⨆ a, ⌜p a⌝ ⊓ wp (f a) post

private def mkUnit : MacroM Syntax :=
  ``((⟨⟩ : PUnit))

instance: GetElem (SpV Int) Nat Int fun _ _ => True where
  getElem inst i _ :=
    match (List.zip (inst.ind.toList) (inst.val.toList)).find? fun (j, _) => j = i with
    | some pr => pr.2
    | none => 0

Membership.mem in Init.Prelude

private def _root_.Lean.EnvExtension.modify (ext : EnvExtension σ) (s : σ -> σ)
  [Monad m] [MonadEnv m] : m Unit := do
  Lean.modifyEnv (ext.modifyState · s)

private def letDeclArgHasBinders (letDeclArg : Syntax) : Bool :=
  let k := letDeclArg.getKind
  if k == ``Parser.Term.letPatDecl then
    false
  else if k == ``Parser.Term.letEqnsDecl then
    true
  else if k == ``Parser.Term.letIdDecl then
    
    let binders := letDeclArg[1]
    binders.getNumArgs > 0
  else
    false

abbrev SolverHints := Array Name

def CaseStudiesRoot : Array Glob :=
  #[`CaseStudies.Extension,
    `CaseStudies.Macro,
    `CaseStudies.Tactic,
    `CaseStudies.TestingUtil,
    `CaseStudies.Theory]

Lake.Job.collectArray in Lake.Build.Job.Monad

Lean.Elab.Term.exprToSyntax in Lean.Elab.Term.TermElabM

structure MatcherWPGen where
  lvls : Array Name
  wpgenExpr : Expr
  matcherInfo : MatcherInfo
  monadRetTypePos : Nat
  monadArgPos : Nat
  monadInstPos : Nat
  omaTypePos : Nat
  firstMonadArgPos : Nat

Lean.Meta.SimpTheorems in Lean.Meta.Tactic.Simp.SimpTheorems

noncomputable
</all_available_defs>

<all_available_lemmas>
lemma wp_cons (x : m α) (post post' : α -> l) :
  (∀ y, post y ≤ post' y) ->
  wp x post ≤ wp x post'

@[simp]
lemma wp_bot :
  wp (bot : m α) = fun _ => (⊥ : l)

lemma get_cnt_sum_append l1 l2:  get_cnt_sum (l1 ++ l2) = get_cnt_sum l1 + get_cnt_sum l2

lemma NonDetT.wp_lift (c : m α) post :
  _root_.wp (liftM (n := NonDetT m) c) post = _root_.wp c post

lemma VelvetM.total_decompose_triple {α : Type} {pre : Prop} {post : α -> Prop}
  (x y z: VelvetM α) (termination: [totl| triple pre x fun _ => True]) (postcondition: [part| triple pre y post]) {eqx: x = z} {eqy: y = z}:
  [totl| triple pre z post]

lemma triple_pure (pre : l) (x : α) (post : α -> l) :
  triple pre (pure (f := m) x) post <-> pre ≤ (post x)

lemma findNat_none (p : Nat -> Prop) [DecidablePred p] :
  (findNat p).isNone -> ∀ i, ¬ p i

theorem triple_forIn_range'_aux {β}
  {xstart : ℕ} {step : ℕ} (n : ℕ) (init : β) {f : ℕ → β → m (ForInStep β)}
  (inv : ℕ → β → l)
  (hstep : ∀ i b,
    triple
      (inv i b)
      (f i b)
      (fun | .yield b' => inv (i + step) b' | .done b' => inv (xstart + n * step) b')) :
  i <= n ->
  triple (inv (xstart + (n - i) * step) init) (forIn (List.range' (xstart + (n - i) * step) i step) init f) (inv (xstart + n * step))

lemma MonadNonDet.wp_forIn {β : Type u} (init : β) (f : Unit -> β -> NonDetT m (ForInStep β))
  (inv : β -> l) (on_done' : β -> l) :
  (∀ b, inv b <= wp (f () b) (fun | .yield b' => inv b' | .done b' => inv b' ⊓ on_done' b')) ->
  triple (inv init) (forIn (m := NonDetT m) Lean.Loop.mk init f) (fun b => inv b ⊓ on_done' b)

@[solverHint]
lemma spv_dot_eq
  (spv1 spv2: SpV Int) (pnt1 pnt2: ℕ) (prev: Int):
  prev + spv_dot spv1 spv2 pnt1 pnt2 = spv_dot spv1 spv2 0 0 →
    spv1.ind[pnt1]! = spv2.ind[pnt2]! →
    pnt1 < spv1.size →
    pnt2 < spv2.size →
    prev + spv1.val[pnt1]! * spv2.val[pnt2]! + spv_dot spv1 spv2 (pnt1 + 1) (pnt2 + 1) = spv_dot spv1 spv2 0 0

lemma repeat_inv_split (f : Unit -> β -> m (ForInStep β))
  (inv : β -> l) (doneWith : β -> l)
  init  (measure: β -> Nat):
    (∀ b, triple (inv b) (f () b) (fun | .yield b' => inv b' ⊓ ⌜ measure b' < measure b ⌝ | .done b' => inv b' ⊓ doneWith b')) ->
    triple (inv init) (Loop.forIn.loop f init) (fun b => inv b ⊓ doneWith b)

theorem triple_forIn_range' {β}
  {xstart : ℕ} {step : ℕ} (n : ℕ) {init : β} {f : ℕ → β → m (ForInStep β)}
  (inv : ℕ → β → l)
  (hstep : ∀ i b,
    triple
      (inv i b)
      (f i b)
      (fun | .yield b' => inv (i + step) b' | .done b' => inv (xstart + n * step) b')) :
  triple (inv xstart init) (forIn (List.range' xstart n step) init f) (inv (xstart + n * step))

lemma MonadNonDet.wp_pick {τ : Type u} [Inhabited τ] post :
  _root_.wp (MonadNonDet.pick (m := NonDetT m) τ) post = iInf post

lemma p_findNat_some (p : Nat -> Prop) [DecidablePred p] (i : Nat) :
  p i -> ∃ j, p j ∧ j <= i ∧ findNat p = some j

omit [MAlgDet m l] in
lemma wlp_cons (c : m α) (post post' : α -> l) :
  post <= post' ->
  wlp c post <= wlp c post'

omit [MonoBind m] [LawfulMonad m] in
lemma wp_csup (xc : Set (m α)) (post : α -> l) :
  Lean.Order.chain xc ->
  ⨅ c ∈ xc, wp c post ≤ wp (Lean.Order.CCPO.csup xc) post

lemma findNat_some_p (p : Nat -> Prop) [DecidablePred p] (i : Nat) :
  findNat p = some i -> p i

@[loomLogicSimp]
lemma infE (l : Type u) [CompleteLattice l] (a b : α -> l) : (a ⊓ b) = fun x => a x ⊓ b x

lemma wp_pure (x : α) (post : α -> l) : wp (m := m) (pure x) post = post x

@[loomLogicSimp]
lemma himpPureE (a b : Prop) :
  (a ⇨ b) = (a -> b)

lemma MonadNonDet.wp_assume {as : Prop} post : _root_.wp (MonadNonDet.assume (m := NonDetT m) as) post = ⌜as⌝ ⊓ post .unit

lemma ExtractNonDet.extract_refines (pre : l) (s : NonDetT m α) (inst : ExtractNonDet Findable s) :
  triple pre s post ->
  pre <= s.prop ⊤ ->
  triple pre s.extract post

lemma array_extract_split_i_j_k (arr : Array α) (i j k: Nat) :
    i < j -> j < k -> k ≤ arr.size →
    arr.extract i k = (arr.extract i j) ++ (arr.extract j k)

lemma NonDetT.wp_mono [LawfulMonad m] {α : Type u} {l : Type u} [CompleteLattice l] [MAlgOrdered m l] (x : NonDetT m α) (f g : α -> l) :
  (∀ a, f a <= g a) ->
  NonDetT.wp x f <= NonDetT.wp x g

private lemma le_coml_sup (x y z : l) :
  y <= x ⊔ z -> xᶜ <= yᶜ ⊔ z

@[aesop unsafe]
theorem non_zero_length (q: List Nat) (hnemp: q.nonEmpty): 0 < q.length

omit [CCPOBot m] [MAlgDet m l] [LawfulMonad m] in
lemma wp_csup (xc : Set (m α)) (post : α -> l) [∀ α, CCPO (m α)] [MAlgPartial m]:
  Lean.Order.chain xc ->
  ⨅ c ∈ xc, wp c post ≤ wp (Lean.Order.CCPO.csup xc) post

omit [MAlgOrdered m l] in
lemma spec_mono {α : Type u}  {l : Type u} [CompleteLattice l] (pre : l) (post : α -> l) (f g : α -> l) :
  (∀ a, f a <= g a) ->
  spec pre post f <= spec pre post g

@[simp]
lemma NonDetT.wp_pure (x : α) post :
  _root_.wp (NonDetT.pure (m := m) x) post = post x

lemma ExtractNonDet.extract_refines_wp (s : NonDetT m α) :
  wp s post <= wp s.run post

lemma MonadNonDet.wp_forIn {β : Type u} (init : β) (f : Unit -> β -> NonDetT m (ForInStep β))
  (inv : β -> l) (on_done' : β -> l) (measure: β → Nat):
  (∀ b, inv b <= wp (f () b) (fun | .yield b' => inv b' ⊓ ⌜ measure b' < measure b ⌝ | .done b' => inv b' ⊓ on_done' b')) ->
  triple (inv init) (forIn (m := NonDetT m) Lean.Loop.mk init f) (fun b => inv b ⊓ on_done' b)

theorem triple_forIn_deacreasing {β} {measure : β -> ℕ}
  {init : β} {f : β → m (ForInStep β)}
  (inv : β → l)
  (hstep : ∀ b,
    measure b <= measure init ->
    triple
      (inv b)
      (f b)
      (fun | .yield b' => inv b' ⊓ ⌜measure b' < measure b⌝ | .done b' => ⌜ measure b' = 0 ⌝ ⊓ inv b')) :
  triple (inv init) (forIn [0:measure init] init (fun _ => f)) (fun b => inv b ⊓ ⌜measure b = 0⌝)

theorem Array.get_set_c [Inhabited α] (i j: Nat) (val: α) (arr: Array α):
  i < arr.size → (arr.set! j val)[i]! = if i = j then val else arr[i]!

lemma wlp_bind {β} (x : m α) (f : α -> m β) (post : β -> l) :
  wlp (x >>= f) post = wlp x (fun x => wlp (f x) post)

omit [MAlgOrdered m l] in
lemma spec_mono {α : Type u}  {l : Type u} [CompleteLattice l] (pre : l) (post : α -> l) (f g : α -> l) :
  (∀ a, f a <= g a) ->
  spec pre post f <= spec pre post g

lemma NonDetT.wp_bind  {l : Type u} [CompleteLattice l] [MAlgOrdered m l] [LawfulMonad m] {α β : Type u} (x : NonDetT m α) (f : α -> NonDetT m β)
  (post : β -> l):
  NonDetT.wp (x.bind f) post = NonDetT.wp x (fun x => NonDetT.wp (f x) post)

lemma NonDetT.wp_iInf {ι : Type u} {α : Type u} {l : Type u} [CompleteBooleanAlgebra l] [MAlgOrdered m l] [MAlgDet m l] [Nonempty ι]
  (x : NonDetT m α) (post : ι -> α -> l) :
  _root_.wp x (fun a => iInf post a) = ⨅ i, _root_.wp x (post i)

lemma wp_bind {β} (x : m α) (f : α -> m β) (post : β -> l) :
    wp (x >>= f) post = wp x (fun x => wp (f x) post)

@[simp]
lemma falseE (l : Type v) [inst: LE l] [OrderTop l] [OrderBot l] : ⌜False⌝ = (⊥ : l)

omit [MAlgDet m l] in
lemma ExtractNonDet.extract_refines_wp_weak (s : NonDetT m α) (inst : ExtractNonDet WeakFindable s) :
  wp s.extractWeak post <= wp s post

lemma NonDetT.wp_mono [LawfulMonad m] {α : Type u} {l : Type u} [CompleteLattice l] [MAlgOrdered m l] (x : NonDetT m α) (f g : α -> l) :
  (∀ a, f a <= g a) ->
  NonDetT.wp x f <= NonDetT.wp x g

lemma Gen.wp_rand {α : Type} (c : Gen α) :
  triple ⊤ c (fun _ => ⊤)

lemma MonadNonDet.wp_pick {τ : Type u} post :
  _root_.wp (MonadNonDet.pick (m := NonDetT m) τ) post = iSup post

lemma TotalCorrectness.DivM.wp_eq (α : Type) (x : DivM α) (post : α -> Prop) :
  wp x post =
    match x with

lemma NonDetT.wp_mono [LawfulMonad m] {α : Type u} {l : Type u} [CompleteLattice l] [MAlgOrdered m l] (x : NonDetT m α) (f g : α -> l) :
  (∀ a, f a <= g a) ->
  NonDetT.wp x f <= NonDetT.wp x g

theorem finalCorrectnessTheorem (s : Array Char) (p : Char → Bool) :
  let res := SubstringSearch s p |>.extract
  (res.flag = false → ∀ i < s.size, p s[i]! = false) ∧
  (res.flag = true →
    (∀ l₁ r₁, CorrectSubstring s p l₁ r₁ →
  r₁ - l₁ + 1 = res.r - res.l + 1 ∧ res.r ≤ r₁ ∨
  r₁ - l₁ + 1 < res.r - res.l + 1)) ∧
  (res.flag = true → CorrectSubstring s p res.l res.r) ∧
  (0 < s.size → res.r < s.size) ∧
  (res.l ≤ res.r)

@[grind, solverHint]
lemma sumUpToSucc
  (spv : SpV Int)
  (v : Array Int) (bound : ℕ) :
  sumUpTo spv v (bound + 1) = (sumUpTo spv v bound) +
    ((spv.val)[bound]! * v[(spv.ind)[bound]!]!)

theorem VSpV_correct_triple (out: Array Int) (arr: Array Int) (spv: SpV Int):
  triple
    (∀ i < spv.size, spv.ind[i]! < arr.size)
    (VSpV out arr spv)
    fun ⟨_, outNew⟩ =>
      outNew[0]! = ∑ i ∈ Finset.range (arr.size), spv[i] * arr[i]!

lemma MonadNonDet.wp_repeat {α : Type u} (init : α) (f : α -> NonDetT m (ForInStep α)) post :
  _root_.wp (MonadNonDet.rep (m := NonDetT m) init f) post = ⨆ (inv : ForInStep _ -> l),
    ⌜ ∀ b, (inv (ForInStep.yield b)) <= wp (f b) inv⌝ ⊓
    spec (inv (.yield init)) (fun b => inv (.done b)) post

lemma decodeStrLean_append : forall arr1 arr2,
  decodeStrLean (arr1 ++ arr2) = ( decodeStrLean arr1 ) ++ ( decodeStrLean arr2 )

@[solverHint]
lemma spv_dot_eq
  (spv1 spv2: SpV Int) (pnt1 pnt2: ℕ) (prev: Int):
  prev + spv_dot spv1 spv2 pnt1 pnt2 = spv_dot spv1 spv2 0 0 →
    spv1.ind[pnt1]! = spv2.ind[pnt2]! →
    pnt1 < spv1.size →
    pnt2 < spv2.size →
    prev + spv1.val[pnt1]! * spv2.val[pnt2]! + spv_dot spv1 spv2 (pnt1 + 1) (pnt2 + 1) = spv_dot spv1 spv2 0 0

@[local simp]
lemma wp_mono_part (x : NonDetT DivM α) (post₁ post₂ : α -> Prop) :
  (post₁ ≤ post₂) → ([totl|wp x post₁]) ≤ ([part| wp x post₂])

lemma NonDetT.wp_eq_wp {α : Type u} (x : NonDetT m α) (post : α -> l) :
  _root_.wp x post = NonDetT.wp x post

@[simp]
lemma NonDetT.wp_pure (x : α) post :
  _root_.wp (NonDetT.pure (m := m) x) post = post x
</all_available_lemmas>

<local_ctx>
import Auto

import Lean

import Mathlib.Algebra.BigOperators.Intervals

import Mathlib.Algebra.Ring.Int.Defs

import Loom.MonadAlgebras.NonDetT.Extract

import Loom.MonadAlgebras.WP.Tactic

import Loom.MonadAlgebras.WP.DoNames'

import CaseStudies.Velvet.Std

section SpMV

structure SpV (valTyp : Type) where
  ind: Array Nat
  val: Array valTyp
  size: ℕ
  size_eq: ind.size = size ∧ val.size = size
  inc: ∀ (i j: Nat), i < size → j < size →  i < j → ind[i]! < ind[j]!

def sumUpTo
  (spv : SpV Int)
  (v : Array Int) (bound : ℕ) : Int := ∑ i ∈ Finset.range bound, ((spv.val)[i]! * v[(spv.ind)[i]!]!)
</local_ctx>

<target_theorem>
theorem spmv_correct_triple (out: Array Int) (arr: Array Int) (spm: Array (SpV Int)):
  triple
    (∀ i < spm.size, ∀ j < spm[i]!.size, spm[i]!.ind[j]! < arr.size)
    (spmv out arr spv spm)
    fun ⟨_, outNew⟩ =>
      (∀ j < outNew.size, outNew[j]! = ∑ i ∈ Finset.range (arr.size), spm[j]![i] * arr[i]!) :=
</target_theorem>

