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>
structure Context where
  ref         : Syntax
   
  m           : Syntax
   
  returnType  : Syntax
  mutableVars : VarSet := {}
  insideFor   : Bool := false

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

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

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

def wp (c : m α) (post : α -> l) : l := liftM (n := Cont l) c post

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

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

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

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

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 => let p : Set τ := p; ⨅ a ∈ (p : Set τ), wp (f a) post

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

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

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

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

structure WPGen (x : m α) where
  get : Cont l α
  
  prop : ∀ post, get post <= wp x post

def WPGen.bind {x : m α} {f : α -> m β} (wpg : WPGen x) (wpgf : ∀ a, WPGen (f a)) :
  WPGen (x >>= f) where
  get := fun post => wpg.get (fun a => (wpgf a).get post)
  prop := by admit /- proof elided -/

noncomputable def LE.pure {l : Type u} [inst: LE l] [OrderTop l] [OrderBot l] : Prop -> l := fun p =>
  if p then ⊤ else ⊥

macro "⌜" p:term "⌝" : term => `(LE.pure $p)

class MAlg [Monad m] (l : outParam (Type v)) where
  μ : m l -> l
  pure : ∀ l, μ (pure l) = l
  bind : ∀ {α : Type v} (x : m α) (f g : α -> m l),
    μ ∘ f = μ ∘ g ->
    μ (x >>= f) = μ (x >>= g)

abbrev MAlg.lift {m : Type u -> Type v} {l : Type u} [Monad m] [MAlg m l] :
  {α : Type u} -> m α -> Cont l α := fun x f => μ $ f <$> x

class MAlgOrdered (l : outParam (Type v)) [Monad m] [CompleteLattice l] where
  μ : m l -> l
  μ_ord_pure : ∀ l, μ (pure l) = l
  μ_ord_bind {α : Type v} :
    ∀ (f g : α -> m l), μ ∘ f ≤ μ ∘ g ->
      ∀ x : m α, μ (x >>= f) ≤ μ (x >>= g)

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)

class MAlgPartial (m : Type u -> Type v) [Monad m] [∀ α, Lean.Order.CCPO (m α)]
  [CompleteLattice l] [MAlgOrdered m l] where
  csup_lift {α : Type u} (xc : Set (m α)) (post : α -> l) :
    Lean.Order.chain xc ->
    ⨅ x ∈ xc, MAlg.lift x post <= MAlg.lift (Lean.Order.CCPO.csup xc) 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) => ⊥) = ⊥

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

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

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

inductive NonDetT (m : Type u -> Type v) : (α : Type u) -> Type _ where
  | pure {α} (ret : α) : NonDetT m α
  | vis {α} {β} (x : m β) (f : β → NonDetT m α) : NonDetT m α
  | pickCont {α} (τ : Type u) (p : τ -> Prop) [Findable p] (f : τ → NonDetT m α) : NonDetT m α
  | repeatCont {α} {β} (init : β) (f : β -> NonDetT m (ForInStep β)) (cont : β -> NonDetT m α) : NonDetT m α

def NonDetT.bind (x : NonDetT m α) (f : α → NonDetT m β) : NonDetT m β :=
  match x with
  | pure ret => f ret
  | vis x f' => vis x fun y => bind (f' y) f
  | pickCont τ p f' => pickCont τ p fun t => bind (f' t) f
  | repeatCont init f' cont => repeatCont init f' fun t => bind (cont t) 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 α

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

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

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

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

ForInStep.yield in Init.Core

partial def Handle.readLineSkip (h : IO.FS.Handle) (skipLine : String := "\n") : IO String := do
  let rec loop := do
    let line ← h.getLine
    if line.isEmpty then
      return line
    if line == skipLine then
      loop
    else
      return line
  loop

MonadExcept in Init.Prelude

Finset.range in Mathlib.Data.Finset.Range

Lean.Order.CCPO.csup in Init.Internal.Order.Basic

node in Test.SmtTranslation.Inductive

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

Lean.Order.bot in Init.Internal.Order.Basic

PUnit in Init.Prelude

Lean.SimpleScopedEnvExtension in Lean.ScopedEnvExtension

abbrev doSeqItem := TSyntax ``Term.doSeqItem

instance [Monad m] [inst : ∀ α, Lean.Order.CCPO (m α)] : Lean.Order.CCPO (ReaderT ε m α) :=

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

Auto.Monomorphization.monomorphize in Auto.Translation.Monomorphization

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})"

Lean.setEnv in Lean.MonadEnv

Lake.logInfo in Lake.Util.Log

Lean.BinderInfo in Lean.Expr

scoped instance TotalHandler {ε} : IsHandler (ε := ε) fun _ => False where

Lean.Name.mkStr in Init.Prelude

Top.top in Mathlib.Order.Notation

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 }

elab "type_with_name_prefix" lit:name inv:term : term => do
  let ⟨maxId, _, _, cntr⟩ <- loomAssertionsMap.get
  let newMaxId := maxId + 1
  let coreName := match (← Term.getDeclName?) with
    | some res => res
    | none => `nameless
  let localName := (Lean.Name.mkSimple (lit.getName.toString ++ "_" ++ coreName.toString))
  let cntrElem := match cntr.get? localName with
    | some resId => resId
    | none => 0
  let maxIdLocal := 1 + cntrElem
  let invName := lit.getName.toString ++ "_" ++ toString maxIdLocal.toNat |>.toName
  loomAssertionsMap.modify (fun res => {
      syntaxStore := res.syntaxStore.insert newMaxId inv
      nameStore := res.nameStore.insert invName newMaxId
      maxId := newMaxId
      nameCounter := res.nameCounter.insert localName maxIdLocal
      })
  Term.elabTerm (<- ``(typeWithName $inv $(Lean.quoteNameMk invName))) none

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

Lean.Core.Context in Lean.CoreM

def mkForInBody  (_ : Syntax) (forInBody : CodeBlock) : M ToForInTermResult := do
  let ctx ← read
  let uvars := forInBody.uvars
  let uvars := varSetToArray uvars
  let term ← liftMacroM <| ToTerm.run forInBody.code ctx.m ctx.returnType uvars (if hasReturn forInBody.code then ToTerm.Kind.forInWithReturn else ToTerm.Kind.forIn)
  return ⟨uvars, term⟩

let firstMonadArgPos := 1 + matcherInfo.numParams + implicitArgs.size
  pure <| .some {
    lvls := newLvls,
    wpgenExpr := wpgen,
    matcherInfo := matcherInfo,
    monadRetTypePos := 0,
    monadArgPos := 1 + matcherInfo.numParams,
    monadInstPos := 1 + matcherInfo.numParams + 1,
    omaTypePos := 1 + matcherInfo.numParams + 2,
    firstMonadArgPos := firstMonadArgPos,
    
    
  }

List.cons in Init.Prelude

Array.count in Init.Data.Array.Basic

def WPGen.assert {l : Type u} {m : Type u -> Type v} [Monad m] [LawfulMonad m] [CompleteBooleanAlgebra l] [MAlgOrdered m l] (h : l) : WPGen (assertGadget (m := m) h) where
  get := fun post => h ⊓ (h ⇨ post .unit)
  prop := by admit /- proof elided -/

throwThe in Init.Prelude

def DivM.run {α : Type u} [Inhabited α] : DivM α -> α
  | DivM.res x => x
  | DivM.div => default

MonadReaderOf.read in Init.Prelude

Except.ok in Init.Prelude

f in Test.SmtTranslation.Trigger

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

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

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

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

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

def MAlgLift.mk_rep  (m : semiOutParam (Type u -> Type v)) (l : semiOutParam (Type u)) [Monad m] [CompleteLattice l] [MAlgOrdered m l]
  (n : (Type u -> Type w)) (σ : Type u) [LawfulMonad m] [Monad n] [LawfulMonad n] [CompleteLattice k] [MAlgOrdered n (σ -> l)]
  [MonadLiftT m n] [LawfulMonadLiftT m n]
  (μ_lift : ∀ (x : m (σ → l)),
    MAlgOrdered.μ (liftM (n := n) x) =
    fun s => MAlgOrdered.μ ((· s) <$> x)) : MAlgLift m l n (σ → l) :=

Lean.Parser.Term.letDecl in Lean.Parser.Term

def dependencyFile := "dependencies.toml"

def VelvetM.extract {α : Type} (x : VelvetM α)
  [∀ α, Lean.Order.CCPO (DivM α)] [Lean.Order.MonoBind DivM] [Inhabited α] : α :=
  x.run.run

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

Lean.Meta.withTransparency in Lean.Meta.Basic

abbrev GlobalMutVarsCtx := Std.HashMap Name LocMutVarsCtx

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

Lean.MessageData.ofSyntax in Lean.Message

Lean.HygieneInfo.mkIdent in Init.Meta.Defs

def cvc5Path := buildDir / "cvc5"

partial def doForToCode (doFor : Syntax) (doElems : List Syntax) : M CodeBlock := do
    let doForDecls := doFor[1].getSepArgs
    if h : doForDecls.size > 1 then
       
      
      let doForDecl := doForDecls[1]!
      unless doForDecl[0].isNone do
        throwErrorAt doForDecl[0] "the proof annotation here has not been implemented yet"
      let y  := doForDecl[1]
      let ys := doForDecl[3]
      let doForDecls := doForDecls.eraseIdx 1
      let body := doFor[3]
      withFreshMacroScope do
         
        let toStreamApp ← withRef ys `(@toStream _ _ _ $ys)
        let auxDo ←
          `(do let mut s := $toStreamApp:term
               for $doForDecls:doForDecl,* do
                 match @Stream.next? _ _ _ s with
                 | none => break
                 | some ($y, s') =>
                   s := s'
                   do $body)
        doSeqToCode (getDoSeqElems (getDoSeq auxDo) ++ doElems)
    else withRef doFor do
      let h?        := if doForDecls[0]![0].isNone then none else some doForDecls[0]![0][0]
      let x         := doForDecls[0]![1]
      withRef x <| checkNotShadowingMutable (← getPatternVarsEx x)
      let xs        := doForDecls[0]![3]
      let forElems  := getDoSeqElems doFor[3]
      let forInBodyCodeBlock ← withFor (doSeqToCode forElems)
      let ⟨uvars, forInBody⟩ ← mkForInBody x forInBodyCodeBlock
      let ctx ← read
      
      
      
      let uvars := uvars.map fun v => ctx.mutableVars.getD v.getId v
      let uvarsTuple ← liftMacroM do mkTuple uvars
      let uvarsTuplePat ← liftMacroM do mkTuplePat uvars

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

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 getMutTypes (stx : Array (TSyntax `leafny_binder)) : MetaM (Array (TSyntax `term)) := do
  let mut types := #[]
  for b in stx do
    match b with
    | `(leafny_binder| (mut $_:ident : $tp:term)) => do
      types := types.push tp
    | _ => pure ()
  return types

Lean.Parser.Term.letId in Lean.Parser.Term

def withNewMutableVars {α} (newVars : Array Var) (mutable : Bool) (x : M α) : M α :=
  withReader (fun ctx => if mutable then { ctx with mutableVars := insertVars ctx.mutableVars newVars } else ctx) x

private def elabSimpArg (indexConfig : Meta.ConfigWithKey) (eraseLocal : Bool) (kind : SimpKind)
    (arg : Syntax) : TermElabM ElabSimpArgResult := withRef arg do
  try
     
    if arg.getKind == ``Lean.Parser.Tactic.simpErase then
      let fvar? ← if eraseLocal then Term.isLocalIdent? arg[1] else pure none
      if let some fvar := fvar? then
        
        return .erase (.fvar fvar.fvarId!)
      else
        let id := arg[1]
        if let .ok declName ← observing (realizeGlobalConstNoOverloadWithInfo id) then
          if (← Simp.isSimproc declName) then
            return .eraseSimproc declName
          else
            return .erase (.decl declName)
        else
          
          
          let name := id.getId.eraseMacroScopes
          if (← Simp.isBuiltinSimproc name) then
            return .eraseSimproc name
          else
            throwUnknownConstantAt id name
    else if arg.getKind == ``Lean.Parser.Tactic.simpLemma then
      let post :=
        if arg[0].isNone then
          true
        else
          arg[0][0].getKind == ``Parser.Tactic.simpPost
      let inv  := !arg[1].isNone
      let term := arg[2]
      match (← resolveSimpIdTheorem? ⟨term⟩) with
      | .expr e  =>
        let name ← mkFreshId
        elabDeclToUnfoldOrTheorem indexConfig (.stx name arg) e post inv kind
      | .simproc declName =>
        return .addSimproc declName post
      | .ext ext₁? ext₂? h =>
        return .ext ext₁? ext₂? h
      | .none    =>
        let name ← mkFreshId
        elabSimpTheorem indexConfig (.stx name arg) term post inv
    else if arg.getKind == ``Lean.Parser.Tactic.simpStar then
      return .star
    else
      throwUnsupportedSyntax
  catch ex =>
    throw ex

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

Lean.Parser.Term.doLetRec in Lean.Parser.Do

Lean.Loop.mk in Init.While

MonadStateOf in Init.Prelude

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

Lean.Expr.mvar in Lean.Expr

abbrev VelvetM α := NonDetT DivM α

ExceptT.map in Init.Control.Except

def Extractable.liftM (x : m α) : Extractable (liftM (n := NonDetT m) x) :=

def atomicAssertion {α : Type u} (n : Name) (a : α) := a

Lean.Parser.Term.bracketedBinder in Lean.Parser.Term.Basic

instance MAlgLiftTTrans
  [Monad m] [CompleteLattice l] [LawfulMonad m] [MAlgOrdered m l]
  [Monad n] [CompleteLattice k] [LawfulMonad n] [MAlgOrdered n k] [MonadLiftT m n]
  [Monad p] [CompleteLattice q] [LawfulMonad p] [MAlgOrdered p q] [MonadLift n p]
  [inst': MAlgLiftT m l n k] [inst: MAlgLift n k p q] :
  MAlgLiftT m l p q where
    cl := by admit /- proof elided -/

partial def expandLeafnyDoSeq (modIds : Array Ident) (stx : doSeq) : TermElabM (Array doSeqItem) :=
  match stx with
  | `(doSeq| $doS:doSeqItem*) => return Array.flatten $ ← doS.mapM (expandLeafnyDoSeqItem modIds)
  | _ => throwErrorAt stx s!"unexpected syntax of Velvet `do`-notation sequence {stx}"

Lean.Parser.Tactic.simpErase in Init.Tactics

def findSpec (prog : Expr) : TacticM (Array (Ident × Loom.SpecType)) := do
  let specs ← specAttr.find? prog
  let grts := specs.qsort (compare · · |>.isGT) |>.map
    fun ⟨specType, specName, _⟩ => (mkIdent specName, specType)
  return grts

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

abbrev M := ReaderT Context TermElabM

@[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

def MAlgExcept (ε : Type u) (df : ε -> Prop) (l : Type u) (m : Type u -> Type v)
  [CompleteLattice l]
  [Monad m] [LawfulMonad m] [inst: MAlgOrdered m l] : MAlgOrdered (ExceptT ε m) l where
  μ := fun e => inst.μ $ Except.getD (⌜df ·⌝) <$> e
  μ_ord_pure := by admit /- proof elided -/

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

instance [NoFailure m] : NoFailure (NonDetT m) where
  noFailure := by admit /- proof elided -/

Lean.Parser.mkIdent in Lean.Parser.Types

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

Lean.AttributeImpl in Lean.Attributes

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]
  }

default
  else
    
    x

def NonDetT.pickSuchThat (τ : Type u) (p : τ → Prop) [Findable p] : NonDetT m τ :=
  NonDetT.pickCont τ p pure

Auto.Reif.ReifM in Auto.Translation.ReifM

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)

method spmv
  (mut out: Array Int)
  (arr: Array Int) (spv: SpV Int)
  (spm : Array (SpV Int)) return (u : Unit)
  ensures spm.size = out.size
  ensures ∀ i < spm.size, out[i]! = sumUpTo spm[i]! arr spm[i]!.size
  do
    out := Array.replicate spm.size 0
    let mut arrInd : Array Nat := Array.replicate spm.size 0
    let mut spmInd : Array Nat := Array.replicate spm.size 0
    while_some i :| i < arrInd.size ∧ arrInd[i]! < spm[i]!.size
    invariant arrInd.size = spm.size
    invariant out.size = spm.size
    invariant ∀ i < arrInd.size, arrInd[i]! <= spm[i]!.size
    invariant ∀ i < arrInd.size, out[i]! = sumUpTo spm[i]! arr arrInd[i]!
    done_with ∀ i < arrInd.size, arrInd[i]! = spm[i]!.size
    do
      let ind := arrInd[i]!
      let vInd := (spm[i]!.ind)[ind]!
      let mVal := (spm[i]!.val)[ind]!
      let val := mVal * arr[vInd]!
      out[i] += val
      arrInd[i] += 1
    return

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)

Lean.instantiateMVars in Lean.MetavarContext

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 -/

Lean.Order.MonoBind in Init.Internal.Order.Basic

Monad in Init.Prelude

MonadReaderOf in Init.Prelude

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

instance [Monad m] [LawfulMonad m] [_root_.CompleteLattice l]
  [inst: MAlgOrdered m l] :
  MAlgLift m l (NonDetT m) l where
    cl := by admit /- proof elided -/

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!

def wlp (c : m α) (post : α -> l) : l := iwp c post ⊔ wp c post

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

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 }

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

List.sum in Init.Data.List.Basic

PUnit.unit in Init.Prelude

instance : NoFailure DivM where
  noFailure := by admit /- proof elided -/

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 -/
    ) }

def   NonDetT.wp {l : Type u} [CompleteLattice l] [MAlgOrdered m l] : {α : Type u} -> NonDetT m α -> Cont l α
  | _, .pure ret => pure ret
  | _, .vis x f => fun post => _root_.wp x fun a => wp (f a) post
  | _, @NonDetT.pickCont _ _ _ p _ f => fun post => ⨆ a, ⌜p a⌝ ⊓ wp (f a) post
  | _, .repeatCont init f cont => fun post => ⨆ (inv : ForInStep _ -> l) (measure : _ -> Nat),
    ⌜ ∀ b, (inv (ForInStep.yield b)) <= wp (f b) (fun | .yield b' => inv (.yield b') ⊓ ⌜ measure b' < measure b ⌝ | .done b' => inv (.done b'))⌝ ⊓
    spec (inv (.yield init)) (fun b => inv (.done b)) (fun b => wp (cont b) post)

Auto.Embedding.Lam.MutualIndInfo in Auto.Embedding.LamInductive

Bind in Init.Prelude

register_option loom.solver : LoomSolver := {
  defValue := .grind
  descr :=
  "Loom solver options. Right now we support
   - `cvc5` and `z3` to use the SMT solvers via `auto` tactic
   - `grind` to use the grind tactic
   - `custom` to use a user-provided solver tactic

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

Lean.Order.CCPO in Init.Internal.Order.Basic

def mkVarDeclCore (xs : Array Var) (stx : Syntax) (c : CodeBlock) : CodeBlock := {
  code := Code.decl xs stx c.code,
  uvars := eraseVars c.uvars xs
}

IO.Process.spawn in Init.System.IO

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 -/

Lemma.ofConst in Auto.Translation.Assumptions

structure LoomAssertionsMap where
  maxId : Int
  syntaxStore : Std.HashMap Int Term
  nameStore : Std.HashMap Name Int
  nameCounter : Std.HashMap Name Int

Lean.indentD in Lean.Message

MonadLiftT in Init.Prelude

Array.foldlM in Init.Data.Array.Basic

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

instance [CompleteLattice l] [CompleteLattice k] [LogicLift l k] : MonadLift (Cont l) (Cont k) where
  monadLift := LogicLift.lift.monadLift

def hideNonWPGenGoals : TacticM Unit := do
  let goals <- getGoals
  let goals' <- goals.filterM (·.isWPGenGoal)
  setGoals goals'

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 failureGoalStr (solver : Option SmtSolver := none) : String := s!"{solverStr solver}solver invocation failed"

Lake.proc in Lake.Util.Proc

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

partial def expandLeafnyDoSeqItem (modIds : Array Ident) (stx : doSeqItem) : TermElabM (Array doSeqItem) := do
  match stx with
  
  | `(Term.doSeqItem| $stx ;) => expandLeafnyDoSeqItem modIds $ <- `(Term.doSeqItem| $stx:doElem)
  | `(Term.doSeqItem| return) => expandLeafnyDoSeqItem modIds $ <- `(Term.doSeqItem| return ())
  | `(Term.doSeqItem| return $t) =>
    let ret <-
      if modIds.size = 0 then
      `(term| $t)
     else
       `(term| ($t, $[$modIds:term],*))
    return #[<-`(Term.doSeqItem| return $ret)]
  | `(Term.doSeqItem| pure $t) =>
    let ret <-
      if modIds.size = 0 then
      `(term| $t)
     else
       `(term| ($t, $[$modIds:term],*))
    return #[<-`(Term.doSeqItem| pure $ret)]
  | `(Term.doSeqItem| if $h:ident : $t:term then $thn:doSeq else $els:doSeq) =>
    let thn <- expandLeafnyDoSeq modIds thn
    let els <- expandLeafnyDoSeq modIds els
    let ret ← `(Term.doSeqItem| if $h:ident : $t then $thn* else $els*)
    return #[ret]
  | `(Term.doSeqItem| if $h:ident : $t:term then $thn) =>
    expandLeafnyDoSeqItem modIds $ <- `(Term.doSeqItem| if $h:ident : $t:term then $thn else pure ())
  | `(Term.doSeqItem| if $t:term then $thn:doSeq) =>
    expandLeafnyDoSeqItem modIds $ <- `(Term.doSeqItem| if $t then $thn:doSeq else pure ())
  | `(Term.doSeqItem| match $discrs:matchDiscr,* with $[$alts:matchAlt]*) =>
    let alts' ← alts.mapM fun (alt : TSyntax _) => do
      match alt with
      | `(doMatchAltExpr| | $a,* => $rhs:doSeq) =>
        let rhs' ← expandLeafnyDoSeq modIds rhs
        let alt' ← `(doMatchAltExpr| | $a,* => $rhs'*)
        pure ⟨alt'.raw⟩
      | _ =>
        pure alt
    let ret ← `(Term.doSeqItem| match $discrs:matchDiscr,* with $[$alts':matchAlt]*)
    return #[ret]
  | `(Term.doSeqItem| if $t:term then $thn:doSeq else $els:doSeq) =>
    let thn <- expandLeafnyDoSeq modIds thn
    let els <- expandLeafnyDoSeq modIds els
    let ret ← `(Term.doSeqItem| if $t then $thn* else $els*)
    return #[ret]
  | `(Term.doSeqItem| let $id <- $trm:term) | `(Term.doSeqItem| let $id : $_ <- $trm:term) =>
    let `($t:ident $args:term*) := trm | pure #[stx]
    
    let ctx <- globalMutVarsCtx.get
    let .some ids := ctx[t.getId]? | pure #[stx]
    let mut mods := #[]
    let mut modArgs := #[]
    for (pos, a) in ids do
      let .some arg := args[pos]? | throwErrorAt stx s!"{t} is not fully applied"
      
      let argName := arg.raw.getId
      if argName.isAnonymous then throwErrorAt arg s!"mutable argument {arg} is not a name"
      if argName ∈ modArgs then throwErrorAt arg s!"mutable arguments cannot alias"
      modArgs := modArgs.push argName
      mods := mods.push $ <- withRef arg `(Term.doSeqItem| $(mkIdent argName):ident := $a:ident)
    return #[<-`(Term.doSeqItem| let $id <- $trm:term)] ++ mods
  | `(Term.doSeqItem| $trm:term) =>
    let id := mkIdent <| <- mkFreshUserName `ret
    let `($t:ident $args:term*) := trm | pure #[stx]
    
    let ctx <- globalMutVarsCtx.get
    let .some ids := ctx[t.getId]? | pure #[stx]
    let mut mods := #[]
    let mut modArgs := #[]
    for (pos, a) in ids do
      let .some arg := args[pos]? | throwErrorAt stx s!"{t} is not fully applied"
      
      let argName := arg.raw.getId
      if argName.isAnonymous then throwErrorAt arg s!"mutable argument {arg} is not a name"
      if argName ∈ modArgs then throwErrorAt arg s!"mutable arguments cannot alias"
      modArgs := modArgs.push argName
      mods := mods.push $ <- withRef arg `(Term.doSeqItem| $(mkIdent argName):ident := $a:ident)
    let ret <- withRef trm `(Term.doSeqItem| pure $id)
    return #[<- withRef trm `(Term.doSeqItem| let ⟨$id, _⟩ <- $trm:term)] ++ mods.push ret
  | `(Term.doSeqItem| while_some $id :| $p:term $invs* $done do $doSeq:doSeq) =>
    let doSeq <- expandLeafnyDoSeq modIds doSeq
    return #[<-`(Term.doSeqItem| while_some $id :| $p:term $invs* $done do $doSeq*)]
  | stx => pure #[stx]

instance angelic_exception: MonadExceptOf String CashmereM where
  throw e := liftM (m := ExceptT String (StateT Bal DivM)) (throw e)
  tryCatch := fun x _ => x

def NonDetT.repeat (init : α) (f : α -> NonDetT m (ForInStep α)) : NonDetT m α :=
  NonDetT.repeatCont init f pure

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

lamEVarTy in Auto.Parser.TPTP

abbrev DiscrTreeKey := Array DiscrTree.Key

Lean.KVMap.Value in Lean.Data.KVMap

def assertGadget {l : Type u} (h : l) : m PUnit := pure .unit

instance WeakFindable.of_Findable {α : Type u} (p : α -> Prop) [Findable p] : WeakFindable p where
  find := Findable.find p
  find_some_p := Findable.find_some_p

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

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

Array.filter in Init.Data.Array.Basic

Lean.Parser.Term.doSeqBracketed in Lean.Parser.Do

structure W (t : Type v) [Preorder t] (α : Type u) where
  wp : Cont t α
  wp_montone : wp.monotone

Lean.Meta.Simp.Discharge in Lean.Meta.Tactic.Simp.Rewrite

instance ExtractNonDet.pure' : ExtractNonDet findable (Pure.pure (f := NonDetT m) x) :=

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

Lean.MonadEnv in Lean.Environment

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 -/
    ) }

method SumOfDigits (number: Nat) return (sum: Nat)
    ensures sum = SumDigits number
do
    let mut sum := 0
    let mut n := number
    while n > 0
        invariant sum + SumDigits n = SumDigits number
        invariant 0 ≤ sum
        done_with n = 0
    do
        let digit := n % 10
        sum := sum + digit
        n := n / 10
    return sum

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

instance : Lean.Order.MonoBind DivM where
  bind_mono_left := by admit /- proof elided -/

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

Prod.fst in Init.Prelude

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

inline in Init.Core
</all_available_defs>

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

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

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

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_eq_wp {α : Type u} (x : NonDetT m α) (post : α -> l) :
  _root_.wp x post = NonDetT.wp x post

@[simp]
lemma NonDetT.wp_vis {β : Type u} (x : m β) (f : β → NonDetT m α) post :
  _root_.wp (NonDetT.vis x f) post = _root_.wp x fun a => _root_.wp (f a) post

@[simp]
lemma NonDetT.wp_pickCont {τ : Type u} p (f : τ → NonDetT m α) post :
  _root_.wp (NonDetT.pickCont τ p f) post = ⨅ a, ⌜p a⌝ ⇨ _root_.wp (f a) 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_vis {β : Type u} (x : m β) (f : β → NonDetT m α) post :
  _root_.wp (NonDetT.vis x f) post = _root_.wp x fun a => _root_.wp (f a) post

@[simp]
lemma NonDetT.wp_pickCont {τ : Type u} p (f : τ → NonDetT m α) post :
  _root_.wp (NonDetT.pickCont τ p f) post = ⨆ a, ⌜p a⌝ ⊓ _root_.wp (f a) post

@[simp]
lemma trueE (l : Type v) [inst: LE l] [OrderTop l] [OrderBot l] : ⌜True⌝ = (⊤ : l)

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_eq_wp {α : Type u} (x : NonDetT m α) (post : α -> l) :
  _root_.wp x post = NonDetT.wp x post

@[simp]
lemma NonDetT.wp_vis {β : Type u} (x : m β) (f : β → NonDetT m α) post :
  _root_.wp (NonDetT.vis x f) post = _root_.wp x fun a => _root_.wp (f a) 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_vis {β : Type u} (x : m β) (f : β → NonDetT m α) post :
  _root_.wp (NonDetT.vis x f) post = _root_.wp x fun a => _root_.wp (f a) 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_vis {β : Type u} (x : m β) (f : β → NonDetT m α) post :
  _root_.wp (NonDetT.vis x f) post = _root_.wp x fun a => _root_.wp (f a) 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_vis {β : Type u} (x : m β) (f : β → NonDetT m α) post :
  _root_.wp (NonDetT.vis x f) post = _root_.wp x fun a => _root_.wp (f a) post

lemma MonadNonDet.wp_pickSuchThat {τ : Type u} (p : τ → Prop) [Findable p] post :
  _root_.wp (MonadNonDet.pickSuchThat (m := NonDetT m) τ p) post = ⨆ a, ⌜p a⌝ ⊓ post a

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

lemma ExceptT.wlp_eq (c : ExceptT ε m α) (post : α -> l) :
  [totl| wlp c post] = [part| wlp c post]

lemma MAlg.lift_ExceptT ε (hd : ε -> Prop) [IsHandler hd] [CompleteLattice l] [inst: MAlgOrdered m l]
   (c : ExceptT ε m α) post :
  MAlg.lift c post = MAlg.lift (m := m) c (fun | .ok x => post x | .error e => ⌜hd e⌝)

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 ExtractNonDet.extract_refines_wp (s : NonDetT m α) (inst : ExtractNonDet Findable s) :
  wp s post ⊓ s.prop ⊤ <= wp s.extract post

lemma exists_findNat (p : Nat -> Prop) [DecidablePred p] :
  (∃ x, p x) ↔ (findNat p).isSome

@[simp]
lemma wlp_true (c : m α) : wlp c (fun _ => ⊤) = ⊤

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]!)

lemma ExceptionAsSuccess.ExceptT.wp_lift (c : m α) (post : α -> l) :
  wp (liftM (n := ExceptT ε m) c) post = wp (m := m) c post

theorem triple_forIn_list {α β}
  {xs : List α} {init : β} {f : α → β → m (ForInStep β)}
  (inv : List α → β → l)
  (hstep : ∀ hd tl b,
    triple
      (inv (hd :: tl) b)
      (f hd b)
      (fun | .yield b' => inv tl b' | .done b' => inv [] b')) :
  triple (inv xs init) (forIn xs init f) (inv [])

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)

lemma StateT.wp_eq (c : StateT σ m α) (post : α -> σ -> l) :
  wp c post = fun s => wp (m := m) (c s) (fun xs => post xs.1 xs.2)

omit [CCPOBot m] [MAlgDet m l] in
lemma NonDetT.prop_mono (x : NonDetT m α) post post' :
  post <= post' -> x.prop post <= x.prop post'

@[ext]
lemma W_ext (t : Type v) (α : Type u) [Preorder t] (w w' : W t α) :
  w.wp = w'.wp → w = w'

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

@[aesop safe]
theorem List.sum_lt (x: Bal) : x < y -> x < ([Int.toNat y]).sum

lemma filter_sum_snoc (arr: Array Nat) (p: Nat → Bool) :
  forall i, i < arr.size →
      (Array.filter p (Array.extract arr 0 i)).sum + (if (p arr[i]!) then arr[i]! else 0)=
      (Array.filter p (Array.extract arr 0 (i + 1))).sum

lemma AccFrom_findNat (p : Nat -> Prop) [DecidablePred p] (i : Nat) :
  AccFrom p i -> (findNat.aux p i).isSome

lemma wlp_join_wp (c : m α) (post post' : α -> l) :
  wlp c post ⊓ wp c post' = wp c (fun x => post x ⊓ post' x)

lemma adjacent_to_global_sorted (a : Array Int) :
    (∀ k, 0 ≤ k ∧ k < a.size - 1 → a[k]! ≤ a[k+1]!) →
    (∀ i j, 0 ≤ i ∧ i < j ∧ j < a.size → a[i]! ≤ a[j]!)

theorem VSpV_correct_pure (out: Array Int) (arr: Array Int)
  (spv: SpV Int)
  (h_b: ∀ i < spv.size, spv.ind[i]! < arr.size):
  out.size = 1 → out[0]! = sumUpTo spv arr spv.size →
    out[0]! = ∑ i ∈ Finset.range (arr.size), spv[i] * arr[i]!

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

@[simp]
lemma NonDetT.wp_repeatCont {α : Type u} (init : α) (f : α -> NonDetT m (ForInStep α)) (cont : α -> NonDetT m β) post :
  _root_.wp (NonDetT.repeatCont init f cont) post = ⨆ (inv : ForInStep _ -> l) (measure : _ → Nat),
    ⌜ ∀ b, (inv (ForInStep.yield b)) <= wp (f b) (fun | .yield b' => inv (.yield b') ⊓ ⌜ measure b' < measure b ⌝ | .done b' => inv (.done b'))⌝ ⊓
    spec (inv (.yield init)) (fun b => inv (.done b)) (fun b => wp (cont b) post)

lemma wp_part_eq ε (c : ExceptT ε m α) post :
  wp c post = wp (m := m) c (fun | .ok x => post x | .error _ => ⊤)

lemma TotalCorrectness.DivM.wlp_eq (α : Type) (x : DivM α) (post : α -> Prop) :
  (open TotalCorrectness in wlp x post) = (open PartialCorrectness in wp x post)

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

@[solverHint]
theorem spv_dot_exh
  (spv1 spv2: SpV Int) (pnt1 pnt2: ℕ):
  pnt1 = spv1.size ∨ pnt2 = spv2.size → spv_dot spv1 spv2 pnt1 pnt2 = 0

lemma wp_top_wlp (c : m α) (post : α -> l) :
  wp c ⊤ ⊓ wlp c post = wp c post

lemma findNat_aux_some_le (p : Nat -> Prop) [DecidablePred p] (i : Nat) :
  findNat.aux p i = some j -> ∀ k, i <= k -> k < j -> ¬ p k

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

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)

theorem spv_dot_pure_gen (spv1: SpV Int) (spv2: SpV Int) (n pnt1 pnt2: ℕ)
  (sz1: ∀ i < spv1.size, spv1.ind[i]! < n)
  (sz2: ∀ i < spv2.size, spv2.ind[i]! < n):
  spv_dot spv1 spv2 pnt1 pnt2 =
    ∑ i ∈ Finset.range n,
      if max
        (if spv1.size ≤ pnt1 then n else spv1.ind[pnt1]!)
        (if spv2.size ≤ pnt2 then n else spv2.ind[pnt2]!) ≤ i then
        spv1[i] * spv2[i]
      else
        0

lemma ReaderT.wp_lift (c : m α) (post : α -> σ -> l) :
  wp (liftM (n := ReaderT σ m) c) post = fun s => wp (m := m) c (post · s)
</all_available_lemmas>

<local_ctx>
import Mathlib.Logic.Function.Basic

import Mathlib.Order.CompleteBooleanAlgebra

import Mathlib.Order.Lattice

import Mathlib.Order.Basic

import Mathlib.Data.W.Basic

import Mathlib.Data.FinEnum

import Loom.MonadAlgebras.WP.Gen

import Loom.MonadAlgebras.WP.Liberal

import Loom.MonadAlgebras.NonDetT'.Basic

open Lean.Order

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

def find [Encodable α] (p : α -> Prop) [DecidablePred p] : Option α :=
  findNat (fun x => (Encodable.decode x).any (p ·)) |>.bind Encodable.decode

class WeakFindable {α : Type u} (p : α -> Prop) where
  find : Unit -> Option α
  find_some_p : find () = some x -> p x

instance WeakFindable.of_Findable {α : Type u} (p : α -> Prop) [Findable p] : WeakFindable p where
  find := Findable.find p
  find_some_p := Findable.find_some_p

inductive ExtractNonDet (findable : {τ : Type u} -> (τ -> Prop) -> Type u) {m} : {α : Type u} -> NonDetT m α -> Type _ where
  | pure {α} : ∀ (x : α), ExtractNonDet findable (NonDetT.pure x)
  | vis {α} {β} (x : m β) (f : β → NonDetT m α) :
      (∀ y, ExtractNonDet findable (f y)) → ExtractNonDet findable (.vis x f)
  | pickSuchThat {α} (τ : Type u) (p : τ -> Prop) (f : τ → NonDetT m α)
    {_ : findable p}
     : (∀ x, ExtractNonDet findable (f x)) → ExtractNonDet findable (.pickCont τ p f)
  | assume {α} (p : PUnit -> Prop) (f : PUnit → NonDetT m α) {_ : Decidable (p .unit)} :
    (∀ x, ExtractNonDet findable (f x)) → ExtractNonDet findable (.pickCont PUnit p f)

instance ExtractNonDet.pure' : ExtractNonDet findable (Pure.pure (f := NonDetT m) x) :=

instance ExtractNonDet.liftM (x : m α) :
  ExtractNonDet findable (liftM (n := NonDetT m) x) :=

instance ExtractNonDet.assume' {p : Prop} [Decidable p] : ExtractNonDet findable (MonadNonDet.assume (m :=  NonDetT m) p) :=

instance ExtractNonDet.pickSuchThat' {τ : Type u} (p : τ -> Prop) [Findable p] :
  ExtractNonDet Findable (MonadNonDet.pickSuchThat (m := NonDetT m) τ p) :=

instance ExtractNonDet.pickSuchThat_weak {τ : Type u} (p : τ -> Prop) [WeakFindable p] :
  ExtractNonDet WeakFindable (MonadNonDet.pickSuchThat (m := NonDetT m) τ p) :=

instance ExtractNonDet.if {p : Prop} {dec : Decidable p} {x y : NonDetT m α}
  (_ : ExtractNonDet findable x) (_ : ExtractNonDet findable y) :
  ExtractNonDet findable (if p then x else y) :=

instance ExtractNonDet.ForIn_list {xs : List α} {init : β} {f : α → β → NonDetT m (ForInStep β)}
  (_ : ∀ a b, ExtractNonDet findable (f a b)) :
  ExtractNonDet findable (forIn xs init f) :=

variable [Monad m] [CCPOBot m] [CompleteBooleanAlgebra l] [MAlgOrdered m l] [MAlgDet m l] [LawfulMonad m]

@[simp, inline]
def NonDetT.extractGen {findable : {τ : Type u} -> (τ -> Prop) -> Type u} {α : Type u}
  (findOf : ∀ {τ : Type u} (p : τ -> Prop), findable p -> Unit -> Option τ)
  : (s : NonDetT m α) -> (ex : ExtractNonDet findable s := by admit /- proof elided -/
  ) -> m α
  | .pure x, _ => Pure.pure x
  | .vis x f, .vis _ _ _ => liftM x >>= (fun x => extractGen findOf (f x))
  | .pickCont _ p f, .pickSuchThat _ _ _ _ =>
    match findOf p ‹_› () with
    | none => CCPOBot.compBot
    | some x =>  extractGen findOf (f x)
  | .pickCont _ p f, .assume _ _ _ =>
    if p .unit then
      extractGen findOf (f .unit)
    else CCPOBot.compBot

def NonDetT.extractWeak {α : Type u} (s : NonDetT m α) (ex : ExtractNonDet WeakFindable s := by admit /- proof elided -/
) : m α :=
  NonDetT.extractGen WeakFindable.find s

namespace DemonicChoice
</local_ctx>

<target_theorem>
omit [MAlgDet m l] in
lemma ExtractNonDet.extract_refines_wp_weak [∀ α, CCPO (m α)] [MAlgPartial m] [CCPOBotLawful m] (s : NonDetT m α) (inst : ExtractNonDet WeakFindable s) :
  wp s post <= wp s.extractWeak post :=
</target_theorem>

