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>
abbrev loc := Nat

abbrev var := String

abbrev Heap.heap (val : Type) := Finmap (λ _ : loc ↦ val)

inductive prim where
  
  | val_get : prim
  | val_set : prim
  
  | val_neg : prim
  | val_opp : prim
  | val_eq : prim
  | val_add : prim
  | val_neq : prim
  | val_sub : prim
  | val_mul : prim
  | val_div : prim
  | val_mod : prim
  
  | val_le : prim
  | val_lt : prim
  | val_ge : prim
  | val_gt : prim
  | val_ptr_add : prim

inductive val : Type where
    | val_unit   : val
    | val_bool   : Bool → val
    | val_int    : Int → val
    | val_real   : ℝ → val
    | val_loc    : loc → val
    | val_prim   : prim → val
    | val_fun    : var -> trm -> val
    | val_fix    : var -> var -> trm -> val
    | val_uninit : val
    | val_error : val

inductive trm : Type where
    | trm_val   : val -> trm
    | trm_var   : var -> trm
    | trm_fun   : var -> trm -> trm
    | trm_fix   : var -> var -> trm -> trm
    | trm_app   : trm -> trm -> trm
    | trm_seq   : trm -> trm -> trm
    | trm_let   : var -> trm -> trm -> trm
    | trm_if    : trm -> trm -> trm -> trm
    | trm_for   : var -> trm -> trm -> trm -> trm
    | trm_while : trm -> trm -> trm
    | trm_ref   : var → trm → trm → trm
    | trm_alloc : var → trm → trm → trm

abbrev heap := Heap.heap val

Finset.Icc in Mathlib.Order.Interval.Finset.Defs

def formula_sound (t : trm) (F : formula) : Prop :=
  forall Q, F Q ==> wp t Q

def test2 : Finmap (fun _ : ℕ ↦ ℕ) := Finmap.singleton 1 2

Coe in Init.Coe

ident in Ssreflect.IntroPats

local instance : HWand (hProp) (heap → Prop) hProp where
  hWand := hwand

local instance : HAdd ℤ ℕ val := ⟨fun x y => (x + (y : Int))⟩

def trm_funs (xs:List var) (t:trm) : trm :=
  match xs with
  | [] => t
  | x1::xs' => trm_fun x1 (trm_funs xs' t)

inductive evalunop : prim → val → (val → Prop) → Prop where
  | evalunop_neg : forall b1,
      evalunop val_neg (val_bool b1) (fun v => v = val_bool (¬ b1))
  | evalunop_opp : forall n1,
      evalunop val_opp (val_int n1) (fun v => v = val_int (- n1))
  | evalunop_oppr : forall r1,
      evalunop val_opp (val_real r1) (fun v => v = val_real (- r1))

partial def elabSDo (n : Nat) (tac : Lean.Elab.Tactic.TacticM Unit) : Lean.Elab.Tactic.TacticM Unit := do
  if n == 0 then
    return ()
  else
    tryGoal tac
    allGoal $ elabSDo (n - 1) tac

List in Init.Prelude

def trm_fixs (f:var) (xs:List var) (t:trm) : trm :=
  match xs with
  | [] => t
  | x1::xs' => trm_fix f x1 (trm_funs xs' t)

instance (α : Type) : HWand (α → hProp) (α → hProp) hProp where
  hWand := qwand

Lean.levelOne in Lean.Level

def qstar {A} (Q : A → hProp) (H : hProp) : A → hProp :=
  fun x => hstar (Q x) H

Add in Init.Prelude

example (L : List val) (i : Int) (_ : i.natAbs < L.length) :
  L[i.natAbs]! = L[i]! :=

def hexists {A} (J : A → hProp) : hProp :=
  fun h => exists x, J x h

def wpgen_fix (Fof : val → val → formula) : formula :=
  fun Q ↦ h∀ vf, ⌜forall vx Q', Fof vf vx Q' ==>
    wp (trm_app vf vx) Q'⌝ -∗ Q vf

@[app_unexpander triple] def unexpandTriple : Lean.PrettyPrinter.Unexpander
  | `($(_) [lang| $t] $P fun $v ↦ $Q) => `({ $P }[$t:lang]{$v, $Q})
  | _ => throw ( )

def notstuck (s : state) (t : trm) : Prop :=
  trm_is_val t \/ reducible s t

impl in Mathlib.Deprecated.MLList.BestFirst

@[app_unexpander val_fun] def unexpandVFun : Lean.PrettyPrinter.Unexpander
  | `($(_) $x:str [lang| fun $xs* => $t]) =>
    let str := x.getString
    let name := Lean.mkIdent $ Lean.Name.mkSimple str
    `([lang| fun $name $xs* => $t])
  | `($(_) $x:str [lang| $t]) =>
    let str := x.getString
    let name := Lean.mkIdent $ Lean.Name.mkSimple str
    `([lang| fun $name => $t])
  | _ => throw ( )

GetElem in Init.GetElem

def wpgen_fail : formula :=
  fun _ ↦ ⌜false⌝

partial def xsimp_step_r (xsimp : XSimpR) : TacticM Unit := do
  trace[xsimp] "RHS step"
  trace[xsimp] "hrt: {xsimp.hrt}"
  match xsimp.hlw, xsimp.hlt, xsimp.hrt with
  | `(hempty), `(hempty), `(@HStar.hStar hProp hProp $_ $_ $h $_) =>
     
    try
      trace[xsimp] "xsimp_r deals with: {h}"
      match h with
      | `(hempty) => {| apply xsimp_r_hempty |}
      | `(hpure $_) => {| apply xsimp_r_hpure |}
      | `(@HStar.hStar hProp hProp $_ $_ $h1 $h2) =>
        {| erw [@hstar_assoc $h1 $h2];
           simpNums |} 
                       
          
        xsimp_step_r (<- XSimpRIni)
      | `(@HWand.hWand hProp hProp $_ $_ $h1 $_) =>
        match h1 with
        | `(hpure $_) => {| apply xsimp_r_keep |}
        | _ => {| apply xsimp_r_hwand_same |}
      | `(htop) =>
        match xsimp.hrg with
        | `(hempty) =>
          {| apply xsimpl_r_hgc_or_htop |}
          repeat'' do
            xsimp_pick_same h xsimp.hla
            {| apply xsimp_lr_cancel_same |}
        | `(@HStar.hStar hProp hProp $_ $_ htop hempty) => {| apply xsimpl_r_htop_drop |}
        | _ => throwError "xsimp_step_r: @ unreachable"
      | `(@hexists $_ fun ($x:ident : $_) => $_) => xsimp_r_hexists_apply_hints x
      | `(protect $_) => {| apply xsimp_r_keep |}
      | `(hsingle $x $_) =>
        
        if x.isMVarStx then
          {| apply xsimp_r_keep |}
        else
          xsimp_pick_same_pointer x xsimp.hla
          
          
          {| apply xsimpl_lr_cancel_same_hsingle <;>
             xsimp_hsingle_discharge |}
      | _ =>
        if h.isMVarStx then
          {| apply xsimp_r_keep |}
        else
        xsimp_pick_same h xsimp.hla
        {| apply xsimp_lr_cancel_same |}
    catch ex =>
      trace[xsimp] ex.toMessageData
      {| apply xsimp_r_keep |}
  | _, _, _ => throwError "not implemented"

Lean.pp.universes in Lean.PrettyPrinter.Delaborator.Options

@[default_instance]
instance : HStar hProp hProp hProp where
  hStar := hstar

CoeFun in Init.Coe

abbrev himpl (H1 H2 : hProp) : Prop :=
  forall h, H1 h -> H2 h

DecidableEq in Init.Prelude

def hpure (P : Prop) : hProp :=
  hexists (fun (_ : P) => emp)

AList in Mathlib.Data.List.AList

Option.merge in Init.Data.Option.Basic

def val.is_loc : val -> Prop
  | val_loc _ => True
  | _ => False

class PartialCommMonoid (α : Type) extends AddCommSemigroup α where
  valid : α -> Prop
  valid_add : ∀ x, valid (x + y) -> valid x
  add_valid : ∀ x y, valid x -> valid y -> valid (x + y)

@[app_unexpander trm_fixs] def unexpandTFixs : Lean.PrettyPrinter.Unexpander
  | `($(_) $f:str [ $xs:str,* ] [lang| $t]) =>
    let xs := xs.getElems.map (Lean.mkIdent $ Lean.Name.mkSimple ·.getString)
    let f := Lean.mkIdent $ Lean.Name.mkSimple f.getString
    `([lang| fix $f $xs* => $t])
  | _ => throw ( )

List.zipWith in Init.Data.List.Basic

Lean.Meta.mkForallFVars in Lean.Meta.Basic

def xsimp_flip_acc_lr (hla hra : Term) : TacticM Unit :=
  {| xsimp_flip_acc_l $hla ; xsimp_flip_acc_r $hra |}

move in Ssreflect.Basic

abbrev trm_is_val : trm → Prop
  | trm_val _ => true
  | _         => false

Lean.Syntax in Init.Prelude

scase in Ssreflect.Elim

def hsingle (p : loc) (v : val) : hProp :=
  fun h => (h = Finmap.singleton p v)

scoped instance (priority := low) : AddCommSemigroup val where
  add := add
  add_assoc := by admit /- proof elided -/

def wpgen_if (t : trm) (F1 F2 : formula) : formula :=
  fun Q ↦ ∃ʰ (b : Bool),
    ⌜t = trm_val (val_bool b)⌝ ∗ (if b then F1 Q else F2 Q)

def haffine (_ : hProp) :=
  True

Finset.sum in Mathlib.Algebra.BigOperators.Group.Finset.Defs

List.nil in Init.Prelude

macro "lang_def" n:ident ":=" l:lang : command => do
  `(def $n:ident : val := [lang| $l])

Qq.checkTypeQ in Qq.MetaM

Option in Init.Prelude

def qimpl {A} (Q1 Q2 : A → hProp) : Prop :=
  forall (v:A), Q1 v ==> Q2 v

noncomputable def is_true (P : Prop) : Bool :=
  if P then true else false

def getPrim (t :Expr) : Expr :=
  let_expr val_prim v := t | t
  v

@[app_unexpander trm_app] def unexpandApp : Lean.PrettyPrinter.Unexpander := fun x => do
  
  match x with
  | `($(_) [uop|$uop] [lang| $t]) => `([lang| $uop:uop$t])
  | `($(_) $app [lang| $t2]) =>
    
    match app with
    | `([bop| $bop].trm_app [lang| $t1]) => `([lang| $t1 $bop $t2])
    | `([lang| $t1]) => `([lang| $t1 $t2])
    | `(val_array_get) => return x
    | `(trm_app val_array_get [lang| $t1]) => `([lang| $t1[$t2] ])
    | `(val_array_set) => return x
    | `(trm_app val_array_set [lang| $_]) => return x
    | `(trm_app $app [lang| $t1]) =>
      match app with
      | `(trm_app val_array_set [lang| $t0]) => `([lang| $t0[$t1] := $t2])
      
      
      
      
      
      | _ => throw ( )
    | _ => throw ( )
  | `($(_) [bop| $bop] [lang| $t1]) => return x
  
  
  
  
  | _ => throw ( )

AList.entries in Mathlib.Data.List.AList

def xsimp_pick (i : Nat) (last? : Bool) : TacticM Unit :=
   {| apply xsimp_pick_lemma
      · apply $(hstar_pick_lemma i last?) |}

def hstars_simp_post :=
  {| hsimp ; try apply himpl_refl |}

def xsimp_pick_applied (h hla : Term) : TacticM Unit := do
  let h <- Term.elabTerm h  none
  hstar_search hla fun i h' last? => do
    let h' <- Term.elabTerm h' none
    let numArgs + 1 := h'.getAppNumArgs' | throwError "not equal"
    let h' := h'.consumeMData.getAppPrefix numArgs
    let .true <-
      withAssignableSyntheticOpaque <| isDefEq h h' | throwError "not equal"
    xsimp_pick i last?

Lean.trace in Lean.Util.Trace

@[app_unexpander trm_for] def unexpandFor : Lean.PrettyPrinter.Unexpander
  | `($(_) $x:str [lang| $n1] [lang| $n2] [lang| $t]) =>
    let str := x.getString
    let name := Lean.mkIdent $ Lean.Name.mkSimple str
    `([lang| for $name in [$n1 : $n2] { $t } ])
  | _ => throw ( )

scoped instance inst : PartialCommMonoidWRT val add valid where
  validE := by admit /- proof elided -/

optParam in Init.Prelude

Lean.Meta.inferType in Lean.Meta.Basic

def val_funs (xs:List var) (t:trm) : val :=
  match xs with
  | [] => panic! "function with zero argumets!"
  | x1::xs' => val_fun x1 (trm_funs xs' t)

abbrev sP h t :=fun v => h∀ (Q : val -> hProp), ⌜eval h t Q⌝ -∗ Q v

def hforall {A} (J : A → hProp) : hProp :=
  fun h => forall x, J x h

AddCommMonoid in Mathlib.Algebra.Group.Defs

tryGoal in Ssreflect.Utils

Lean.Meta.unhygienic in Batteries.Lean.Meta.Basic

@[app_unexpander val_unit] def unexpandUnitL : Lean.PrettyPrinter.Unexpander
  | `($(_)) => `([lang| ()])

def htop : hProp :=
  hexists (fun (H : hProp) => H)

def subst (y : var) (v' : val) (t : trm) : trm :=
  
  let if_y_eq x t1 t2 := if x = y then t1 else t2
  match t with
  | trm_val v          => trm_val v
  | trm_var x          => if_y_eq x (trm_val v') t
  | trm_fun x t1       => trm_fun x (if_y_eq x t1 (subst y v' t1))
  | trm_fix f x t1     => trm_fix f x (if_y_eq f t1 (if_y_eq x t1 (subst y v' t1)))
  | trm_app t1 t2      => trm_app (subst y v' t1) (subst y v' t2)
  | trm_seq t1 t2      => trm_seq (subst y v' t1) (subst y v' t2)
  | trm_let x t1 t2    => trm_let x (subst y v' t1) (if_y_eq x t2 (subst y v' t2))
  | trm_if t0 t1 t2    => trm_if (subst y v' t0) (subst y v' t1) (subst y v' t2)
  | trm_for x t1 t2 t3 => trm_for x (subst y v' t1) (subst y v' t2) (if_y_eq x t3 (subst y v' t3))
  | trm_while t1 t2    => trm_while (subst y v' t1) (subst y v' t2)
  | trm_ref x t1 t2    => trm_ref x (subst y v' t1) (if_y_eq x t2 (subst y v' t2))
  | trm_alloc x t1 t2  => trm_alloc x (subst y v' t1) (if_y_eq x t2 (subst y v' t2))

HAdd in Init.Prelude

@[app_unexpander trm_fix] def unexpandTFix : Lean.PrettyPrinter.Unexpander
  | `($(_) $f:str $x:str [lang| fun $xs* => $t]) =>
    let f := f.getString
    let x := x.getString
    let nameF := Lean.mkIdent $ Lean.Name.mkSimple f
    let nameX := Lean.mkIdent $ Lean.Name.mkSimple x
    `([lang| fix $nameF $nameX $xs* => $t])
  | `($(_) $f:str $x:str [lang| $t]) =>
    let f := f.getString
    let x := x.getString
    let nameF := Lean.mkIdent $ Lean.Name.mkSimple f
    let nameX := Lean.mkIdent $ Lean.Name.mkSimple x
    `([lang| fix $nameF $nameX => $t])
  | _ => throw ( )

partial def getNestedApp (t :Expr) : Expr :=
  let_expr trm_app t _ := t | getVal t
  getNestedApp t

instance AddHProp [PartialCommMonoid val] : Add hProp := ⟨hadd⟩

Prod in Init.Prelude

def purepost (s : state) (P : val → Prop) : val → state → Prop :=
  fun v s' => P v ∧ s' = s

def make_list {A} (n : Nat) (v : A) : List A :=
  match n with
  | 0      => []
  | n' + 1 => v :: make_list n' v

def wpgen_ref (x : var) (t1 t2 : trm) : formula :=
  fun Q ↦ ∃ʰ v, ⌜t1 = trm_val v⌝ ∗
    h∀ p, (p ~~> v) -∗ protect (wp (subst x p t2) (fun hv ↦ Q hv ∗ ∃ʰ u, p ~~> u))

Set in Mathlib.Data.Set.Defs

Int.toNat in Init.Data.Int.Basic

def _root_.List.mkAlist [DecidableEq α] (xs : List α) (vs : List β) :=
  ((xs.zip vs).map fun (x, y) => ⟨x, y⟩).toAList

def XSimpRIni : TacticM XSimpR := withMainContext do
  (<- getMainGoal).setTag `xsimp_goal
  let goal <- getGoalStxNN
  let `(XSimp $hl $hr) := goal | throwError "not a XSimp goal"
  let `(@Prod.mk hProp $_ $hla $hlwt) := hl | throwError "not a XSimp goal"
  let `(@Prod.mk hProp hProp $hlw $hlt) := hlwt | throwError "not a XSimp goal"
  let `(@Prod.mk hProp $_ $hra $hrgt) := hr | throwError "not a XSimp goal"
  let `(@Prod.mk hProp hProp $hrg $hrt) := hrgt | throwError "not a XSimp goal"
  return { hla := hla, hlw := hlw, hlt := hlt, hra := hra, hrg := hrg, hrt := hrt }

local instance : HAdd ℤ ℤ val := ⟨fun x y => val.val_int (x + y)⟩

List.kinsert in Mathlib.Data.List.Sigma

instHAdd in Init.Prelude

noncomputable def sP' (h : heap) (t : trm) : (val → hProp) :=
  if ex : ∃ Q, evalExact h t Q then choose ex else fun _ _ ↦ False

@[app_unexpander trm_if] def unexpandIf : Lean.PrettyPrinter.Unexpander
  | `($(_) [lang| $t1] [lang| $t2] [lang| $t3]) => `([lang| if $t1 then $t2 else $t3])
  | _ => throw ( )

def validLoc (l : loc) (h : heap) : Prop := (h.lookup l).any (valid (α := val))

@[app_unexpander incr] def unexpandIncr : Lean.PrettyPrinter.Unexpander := fun _ => `([uop| ++])

def hstars_simp_step : TacticM Unit := withMainContext do
  let goal <- getGoalStxNN
  match goal with
    | `(himpl $Hl $Hr) =>
        match Hr with
          | `(@HStar.hStar hProp hProp $_ $_ $_ $hs) =>
              match hs with
              | `(@HStar.hStar hProp hProp $_ $_ $H $_) =>
                    try
                      xsimp_pick_same H Hl hstars_simp_pick ;
                      {| apply hstars_simp_cancel_lemma |}
                    catch ex =>
                      let s <- ex.toMessageData.toString
                      if s == "not equal" then
                        {| apply hstars_simp_keep_lemma |}
                      else
                        throw ex
              | _ => throwError "cannot simplify"
          | _ => throwError "cannot simplify"
    | _ => throwError "cannot simplify"

| step_eq : forall s v1 v2,
      step s (trm_app (trm_app val_eq v1) v2) s (val_bool (is_true (v1 = v2)))
  | step_neq : forall s v1 v2,
      step s (trm_app (trm_app val_neq v1) v2) s (val_bool (is_true (v1 ≠ v2)))
  | step_add : forall s n1 n2,
      step s (trm_app (trm_app val_add (val_int n1)) (val_int n2)) s
        (val_int (n1 + n2))
  | step_sub : forall s n1 n2,
      step s (trm_app (trm_app val_sub (val_int n1)) (val_int n2)) s
        (val_int (n1 - n2))
  | step_mul : forall s n1 n2,
      step s (trm_app (trm_app val_mul (val_int n1)) (val_int n2)) s
        (val_int (n1 * n2))
  | step_div : forall s n1 n2,
      n2 ≠ 0 →
      step s (trm_app (trm_app val_div (val_int n1)) (val_int n2)) s
        (n1 / n2)
  | step_mod : forall s n1 n2,
      n2 ≠ 0 →
      step s (trm_app (trm_app val_mod (val_int n1)) (val_int n2)) s
        (n1 % n2)
  | step_le : forall s n1 n2,
      step s (trm_app (trm_app val_le (val_int n1)) (val_int n2)) s
        (val_bool (n1 <= n2))
  | step_lt : forall s n1 n2,
      step s (trm_app (trm_app val_lt (val_int n1)) (val_int n2)) s
        (val_bool (n1 < n2))
  | step_ge : forall s n1 n2,
      step s (trm_app (trm_app val_ge (val_int n1)) (val_int n2)) s
        (val_bool (n1 >= n2))
  | step_gt : forall s n1 n2,
      step s (trm_app (trm_app val_gt (val_int n1)) (val_int n2)) s
        (val_bool (n1 > n2))
  | step_ptr_add : forall s p1 p2 n,
      (p2:ℤ) = (p1:loc) + n →
      step s (trm_app (trm_app val_ptr_add (val_loc p1)) (val_int n)) s
        (val_loc (Int.toNat p2))

@[app_unexpander hexists] def unexpandHExists : Lean.PrettyPrinter.Unexpander
  | `($(_) fun $x:ident => ∃ʰ $xs:binderIdent*, $b) => `(∃ʰ $x:ident $xs:binderIdent*, $b)
  | `($(_) fun $x:ident => $b)                     => `(∃ʰ $x:ident, $b)
  | `($(_) fun ($x:ident : $t) => $b)              => `(∃ʰ ($x:ident : $t), $b)
  | t                                              => pure t

| step_seq_ctx : forall s1 s2 t1 t1' t2,
      step s1 t1 s2 t1' →
      step s1 (trm_seq t1 t2) s2 (trm_seq t1' t2)
  | step_let_ctx : forall s1 s2 x t1 t1' t2,
      step s1 t1 s2 t1' →
      step s1 (trm_let x t1 t2) s2 (trm_let x t1' t2)
  | step_app_arg_1 : forall s1 s2 t1 t1' t2,
      step s1 t1 s2 t1' →
      step s1 (trm_app t1 t2) s2 (trm_app t1' t2)
  | step_app_arg2 : forall s1 s2 v1 t2 t2',
      step s1 t2 s2 t2' →
      step s1 (trm_app v1 t2) s2 (trm_app v1 t2')

def wpgen_alloc (x : var) (t1 t2 : trm) : formula :=
  fun Q ↦ ∃ʰ n : ℤ,
    ⌜n ≥ 0 ∧ t1 = trm_val n⌝ ∗
    h∀ p,
      (hrange (make_list n.natAbs val_uninit) p) -∗
      protect wp (subst x p t2) (Q ∗ ⌜p ≠ null⌝ ∗ ∃ʰ L, ⌜L.length = n⌝ ∗ hrange L p)

Lean.Name in Init.Prelude

def validInter (h₁ h₂ : heap) : Prop :=
  ∀ l ∈ h₁, l ∈ h₂ -> ((h₁ +ʰ h₂).lookup l).any (valid (α := val))

@[simp]
abbrev add : val -> val -> val
  | .val_int i, .val_int j => val.val_int (i + j)
  | _, _ => val.val_unit

allGoal in Ssreflect.Utils

Lean.Elab.Tactic.getMainTarget in Lean.Elab.Tactic.Basic

def trm_apps (f:trm) (ts:List trm) : trm :=
  match ts with
  | [] => f
  | ti::ts' => trm_apps (trm_app f ti) ts'

L in Archive.Hairer

Lean.Meta.isDefEq in Lean.Meta.Basic

skip in Talk.DemoLeanSSR

def test1 : Finmap (fun _ : ℕ ↦ ℕ) := Finmap.singleton 0 1

instance : Inhabited val where
  default := val.val_unit

List.NodupKeys in Mathlib.Data.List.Sigma

@[app_unexpander val_fixs] def unexpandVFixs : Lean.PrettyPrinter.Unexpander
  | `($(_) $f:str [ $xs:str,* ] [lang| $t]) =>
    let xs := xs.getElems.map (Lean.mkIdent $ Lean.Name.mkSimple ·.getString)
    let f := Lean.mkIdent $ Lean.Name.mkSimple f.getString
    `([lang| fix $f $xs* => $t])
  | _ => throw ( )

Finmap.lookup in Mathlib.Data.Finmap

def structural (F : formula) :=
  forall Q, mkstruct F Q ==> F Q

abbrev default_get' := default_get (val_int 0)

def xsimp_r_hexists_apply_hints (x : Ident) : TacticM Unit := do
  let hints <- hintExt.getSSR
  match hints with
  | [] =>
    trace[xsimp] "no hints"
    eApplyAndName `xsimp_r_hexists $ `xsimp ++ x.getId
  | h :: hs =>
    hintExt.setSSR hs
    match h with
    | `(hint| ?)       => eApplyAndName `xsimp_r_hexists $ `xsimp ++ x.getId
    | `(hint| $t:term) => {| apply (@xsimp_r_hexists _ $t) |}
    | _ => throwError "xsimp_r_hexists_apply_hints: @ unreachable"

String in Init.Prelude

abbrev HintExtState := List Syntax

def hseg (L : List val) (p : loc) (j : Int) : hProp :=
  match L with
  | []      => emp
  | x :: L' => (hcell x p j) ∗ (hseg L' p (j + 1))

local instance : Coe val trm where
  coe v := trm.trm_val v

instance : CoeFun trm (fun _ => trm -> trm) where
  coe x := trm.trm_app x

OfNat in Init.Prelude

def hwand (H1 H2 : hProp) : hProp :=
  hexists (fun (H0 : hProp) => H0 ∗ hpure ((H1 ∗ H0) ==> H2))

abbrev add : val -> val -> val := fun _ _ => default

List.length in Init.Prelude

Zero in Init.Prelude

instance : Coe Bool val where
  coe b := val.val_bool b

def st1 : state := (Finmap.singleton 0 1).insert 1 1

Lean.Name.mkSimple in Init.Prelude

def val_array_length : val := [lang|
  fun p => !p ]

Eq in Init.Prelude

@[app_unexpander val_real] def unexpandReal : Lean.PrettyPrinter.Unexpander
  | `($(_) $n:num) => `($n:num)
  | `($(_) $n:ident) => `($n:ident)
  | `($(_) $n:term) => `(lang|⟨$n:term⟩)
  | _ => throw ( )

Finmap.instSDiff in Mathlib.Data.Finmap

local instance : HAdd ℕ ℤ val := ⟨fun x y => ((x : Int) + y)⟩

def val_array_set : val := [lang|
  fun p i v =>
    let p1 := p ++ 1 in
    let q := p1 ++ i in
    q := v ]

Or in Init.Prelude

Finmap.erase in Mathlib.Data.Finmap

And in Init.Prelude
</all_available_defs>

<all_available_lemmas>
lemma hforall_specialize A (x : A) (J : A → hProp) :
  (hforall J) ==> (J x)

lemma hstar_pick_last_8 :
  h1 ∗ h2 ∗ h3 ∗ h4 ∗ h5 ∗ h6 ∗ h7 ∗ h8 = h8 ∗ h1 ∗ h2 ∗ h3 ∗ h4 ∗ h5 ∗ h6 ∗ h7

lemma triple_app_fun x v1 v2 t1 H Q :
  v1 = val_fun x t1 →
  triple (subst x v2 t1) H Q →
  triple (trm_app v1 v2) H Q

lemma xwhile_inv_basic_lemmaQ (I : Bool -> α -> hProp) R:
  WellFounded R ->
  (H ==> H' ∗ ∃ʰ b a, I b a) ->
  (∀ b X, I b X ==> wp F1 (fun bv => I b X ∗ ⌜bv = b⌝)) ->
  (∀ X, I true X ==> wp F2 (fun _ => ∃ʰ b X', ⌜R X' X⌝ ∗ I b X')) ->
  ((fun _ => H' ∗ ∃ʰ a, I false a) ===> Q) ->
  H ==> wp (trm_while F1 F2) Q

lemma kmerge_assoc_perm (l₁ l₂ l₃ : List (Sigma (fun _ : loc => val))) (nd₁ : l₁.NodupKeys) (nd₂ : l₂.NodupKeys) (nd₃ : l₃.NodupKeys) :
  (kmerge (kmerge l₁ l₂) l₃).Perm $ (kmerge l₁ (kmerge l₂ l₃))

lemma triple_sub n1 n2 :
  triple (trm_app val_sub (val_int n1) (val_int n2))
    emp
    (fun r ↦ ⌜r = val_int (n1 - n2)⌝)

@[simp]
lemma labSet_inter (l : ℕ) (s s' : Set α) :
  ⟪l, s⟫ ∩ ⟪l, s'⟫ = ⟪l, s ∩ s'⟫

lemma xfun_nospec_lemma  H Q Fof :
(forall (vf : val),
    (forall (vx : val) H' Q', (H' ==> Fof vx Q') → triple (trm_app vf vx) H' Q') →
    (H ==> Q vf)) →
H ==> wpgen_fun Fof Q

lemma validInter_empty_r (h : heap) : h ⊥ʰ ∅

lemma eval_divr s r1 r2 Q :
  r2 ≠ 0 ->
  Q (val_real (r1 / r2)) s ->
  eval s (trm_app (trm_app val_div (val_real r1)) (val_real r2)) Q

lemma lookup_intersect (s₁ s₂ : state) :
  p ∈ s₁ ∧ p ∈ s₂ →
  (intersect s₁ s₂).lookup p = s₁.lookup p

lemma xsimp_r_hempty :
  XSimp hl (hra, hrg, hrt) ->
  XSimp hl (hra, hrg, emp ∗ hrt)

lemma getElem!_nil_intint (n : Int) :
  ([] : List Int)[n]! = default

lemma hseg_eq_hrange L p (k : Nat) :
  hseg L p k = hrange L (p + 1 + k)

lemma triple_app_fix_direct v2 f x t1 H Q :
  f ≠ x →
  triple (subst x v2 (subst f (val_fix f x t1) t1)) H Q →
  triple (trm_app (val_fix f x t1) v2) H Q

lemma intersect_disjoint_cancel (s₁ s₂ s₃ : state) :
  s₁.Disjoint s₃ →
  (s₁ ∪ intersect s₂ s₃) \ s₃ = s₁

lemma wpgen_val_sound v :
  formula_sound (trm_val v) (wpgen_val v)

lemma wpgen_ref_sound x t1 t2 :
  formula_sound (trm_ref x t1 t2) (wpgen_ref x t1 t2)

lemma hwand_curry_eq H1 H2 H3 :
  (H1 ∗ H2) -∗ H3 = H1 -∗ (H2 -∗ H3)

lemma triple_set w p (v : val) :
  triple (trm_app val_set (val_loc p) v)
    (p ~~> w)
    (fun r ↦ ⌜r = val_unit⌝ ∗ (p ~~> v))

lemma wp_ramified t (Q1 Q2 : val -> hProp) :
  (wp t Q1) ∗ (Q1 -∗ Q2) ==> (wp t Q2)

lemma himpl_refl H : H ==> H

lemma xif_lemma b H F1 F2 Q :
  (b = true -> H ==> F1 Q) →
  (b = false -> H ==> F2 Q) →
  H ==> wpgen_if b F1 F2 Q

@[heapSimp]
lemma foo' : (@OfNat.ofNat ℤ n _) = (n : ℤ)

lemma mkstruct_frame F H Q :
  (mkstruct F Q) ∗ H ==> mkstruct F (Q ∗ H)

lemma hstar_flip_6 :
  h1 ∗ h2 ∗ h3 ∗ h4 ∗ h5 ∗ h6 ∗ emp =
  h6 ∗ h5 ∗ h4 ∗ h3 ∗ h2 ∗ h1 ∗ emp

lemma hpure_intr :
  (P -> H s) -> (⌜P⌝ -∗ H) s

lemma wp_seq t1 t2 Q :
  wp t1 (fun _ ↦ wp t2 Q) ==> wp (trm_seq t1 t2) Q

lemma hstar_pick_4 :
  h1 ∗ h2 ∗ h3 ∗ h4 ∗ h = h4 ∗ h1 ∗ h2 ∗ h3 ∗ h

lemma triple_subr r1 r2 :
  triple (trm_app val_sub (val_real r1) (val_real r2))
    emp
    (fun r ↦ ⌜r = val_real (r1 - r2)⌝)

lemma triple_ptr_add_nonneg (p : loc) (n : Int) :
  n >= 0 →
  triple [lang| p ++ n]
    emp
    (fun r ↦ ⌜r = val_loc (p + Int.natAbs n)⌝)

lemma xpull_protect (h : H1 ==> protect H2) : H1 ==> H2

lemma wp_let x t1 t2 Q :
  wp t1 (fun v ↦ wp (subst x v t2) Q) ==> wp (trm_let x t1 t2) Q

lemma triple_array_length L (p : loc) :
  triple (trm_app val_array_length p)
    (harray L p)
    (fun r ↦ ⌜r = val_int L.length⌝ ∗ harray L p)

lemma triple_neq v1 v2 :
  triple (trm_app val_neq (trm_val v1) (trm_val v2))
    emp
    (fun r ↦ ⌜r = is_true (v1 ≠ v2)⌝)

lemma xsimp_l_cancel_hwand_hempty :
  XSimp (hla, hlw, h ∗ hlt) hr ->
  XSimp (hla, (emp -∗ h) ∗ hlw, hlt) hr

lemma wp_fix f x t Q :
  Q (val_fix f x t) ==> wp (trm_fix f x t) Q

lemma triple_add n1 n2 :
  triple (trm_app val_add (val_int n1) (val_int n2))
    emp
    (fun r ↦ ⌜r = val_int (n1 + n2)⌝)

lemma finite_state (s : state) :
  ∃ p, p ∉ s

lemma validInter_disjoint (h₁ h₂ : Heap.heap val) :
  h₁ ⊥ʰ h₂ = h₁.Disjoint h₂

@[simp]
lemma Heap.add_union_validInter (h₁ h₂ : Heap.heap val) {h : h₁ ⊥ʰ h₂} :
  h₁ +ʰ h₂ = h₁ ∪ h₂

@[heapSimp]
lemma foo'' : (@OfNat.ofNat val n _) = val.val_int (n : ℤ)

lemma himpl_frame_lr H1 H1' H2 H2' :
  H1 ==> H1' →
  H2 ==> H2' →
  (H1 ∗ H2) ==> (H1' ∗ H2')

lemma hstar_pick_last_5 :
  h1 ∗ h2 ∗ h3 ∗ h4 ∗ h5 = h5 ∗ h1 ∗ h2 ∗ h3 ∗ h4

@[heapSimp]
lemma foo : (@OfNat.ofNat ℕ n _) = (n : ℤ)

lemma triple_for_raw (x:var) (n1 n2: Int) t3 H (Q:val->hProp) :
  triple (
    if (n1 < n2)
      then (trm_seq (subst x n1 t3) (trm_for x (val_int $ n1+1) n2 t3))
      else val_unit) H Q ->
  triple (trm_for x n1 n2 t3) H Q

lemma wpgen_fix_sound f x t1 Fof :
  (forall vf vx, formula_sound (subst x vx (subst f vf t1)) (Fof vf vx)) →
  formula_sound (trm_fix f x t1) (wpgen_fix Fof)

lemma hexists_inv A (J : A → hProp) h :
  (hexists J) h → exists x, J x h

lemma xsimp_l_hwand_reorder :
  h1 = h1' ->
  XSimp (hla, ((h1' -∗ h2) ∗ hlw), hlt) hr ->
  XSimp (hla, (h1 -∗ h2) ∗ hlw, hlt) hr

lemma hstar_pick_last_6 :
  h1 ∗ h2 ∗ h3 ∗ h4 ∗ h5 ∗ h6 = h6 ∗ h1 ∗ h2 ∗ h3 ∗ h4 ∗ h5

lemma state_eq_not_mem (p : loc) (h1 h2 : state) :
  h1 = h2 →
  p ∉ h1 →
  p ∉ h2

lemma AList_erase_entries (l : @AList loc (fun _ ↦ val)) :
  (l.erase p).entries = (l.entries).kerase p

lemma hstar_flip_2 :
  h1 ∗ h2 ∗ emp = h2 ∗ h1 ∗ emp

lemma triple_ler r1 r2 :
  triple (trm_app val_le (val_real r1) (val_real r2))
    emp
    (fun r ↦ ⌜r = val_bool (r1 <= r2)⌝)

lemma wp_sound t :
  formula_sound t (wp t)

lemma triple_hwand_hpure_l t (P : Prop) H Q :
  P →
  triple t H Q →
  triple t (⌜P⌝ -∗ H) Q

lemma isubst_single x v t : isubst (List.mkAlist [x] [v]) t = subst x v t

lemma himpl_hwand_r H1 H2 H3 :
  H2 ∗ H1 ==> H3 →
  H1 ==> (H2 -∗ H3)

lemma wp_app_fun x v1 v2 t1 Q :
  v1 = val_fun x t1 →
  wp (subst x v2 t1) Q ==> wp (trm_app v1 v2) Q

lemma wp_equiv t H Q :
  (H ==> wp t Q) ↔ triple t H Q

lemma Heap.add_comm (h₁ h₂ : heap) : h₁ +ʰ h₂ = h₂ +ʰ h₁

lemma wpgen_fail_sound t :
  formula_sound t wpgen_fail

lemma xsimpl_l_cancel_hwand_hstar_hempty :
  XSimp (Hla, Hlw, ((H2 -∗ H3) ∗ Hlt)) HR ->
  XSimp (Hla, (((emp ∗ H2) -∗ H3) ∗ Hlw), Hlt) HR

lemma triple_conseq_frame H2 H1 Q1 t H Q :
  triple t H1 Q1 →
  H ==> H1 ∗ H2 →
  Q1 ∗ H2 ===> Q →
  triple t H Q

lemma wp_frame t H Q :
  (wp t Q) ∗ H ==> wp t (Q ∗ H)

lemma kmerge_dlookup (l₁ l₂ : List (Sigma (fun _ : loc => val))) (nd₁ : l₁.NodupKeys) (nd₂ : l₂.NodupKeys)
    (a : loc) : (kmerge l₁ l₂).dlookup a = Option.merge (· + ·) (l₁.dlookup a) (l₂.dlookup a)

lemma wpgen_if_sound F1 F2 t0 t1 t2 :
  formula_sound t1 F1 →
  formula_sound t2 F2 →
  formula_sound (trm_if t0 t1 t2) (wpgen_if t0 F1 F2)

lemma triple_get v (p : loc) :
  triple (trm_app val_get p)
    (p ~~> v)
    (fun r ↦ ⌜r = v⌝ ∗ (p ~~> v))

lemma hstar_pick_8 :
  h1 ∗ h2 ∗ h3 ∗ h4 ∗ h5 ∗ h6 ∗ h7 ∗ h8 ∗ h = h8 ∗ h1 ∗ h2 ∗ h3 ∗ h4 ∗ h5 ∗ h6 ∗ h7 ∗ h

@[simp]
lemma himpl_refl_resolve  H : (H ==> H) = True

lemma triple_seq t1 t2 H Q H1 :
  triple t1 H (fun _ ↦ H1) →
  triple t2 H1 Q →
  triple (trm_seq t1 t2) H Q

lemma triple_app_fix v1 v2 f x t1 H Q :
  v1 = val_fix f x t1 →
  triple (subst x v2 (subst f v1 t1)) H Q →
  triple (trm_app v1 v2) H Q

lemma himpl_wpgen_wp t Q :
  wpgen t Q ==> wp t Q

lemma wp_structural : structural (wp t)

lemma non_mem_diff_helper1 (h₁ : state) (l : @AList loc fun _ ↦ val) :
  a ∉ l →
  p ∈ List.foldl (fun d s ↦ Finmap.erase s.fst d) (Finmap.erase a h₁) l.entries →
  p ≠ a

@[simp]
lemma kmerge_empty_r (l : List (Sigma (fun _ : loc => val))) : kmerge l [] = l

lemma himpl_lr_htop :
  XSimp (emp, emp, emp) (emp, Hrg, emp) ->
  XSimp (Hla, emp, emp) (emp, (⊤ ∗ Hrg), emp)

lemma reinsert_erase_union (h1 h2 h3 : state) :
  h3.lookup p = some v →
  p ∉ h2 →
  h3.erase p = h1 ∪ h2 →
  h3 = (h1.insert p v) ∪ h2

lemma validInter_empty_l (h : heap) : ∅ ⊥ʰ h

lemma Option.merge_comm (h : Commutative f) (a b : Option α) :
  Option.merge f a b = Option.merge f b a

lemma triple_fun x t1 H Q :
  H ==> Q (val_fun x t1) →
  triple (trm_fun x t1) H Q

lemma xsimp_l_acc_other :
  XSimp (h ∗ hla, hlw, hlt) hr ->
  XSimp (hla, hlw, h ∗ hlt) hr

lemma hstars_simp_start_lemma :
  H1 ∗ emp ==> emp ∗ H2 ∗ emp →
  H1 ==> H2

lemma triple_gtr r1 r2 :
  triple (trm_app val_gt (val_real r1) (val_real r2))
    emp
    (fun r ↦ ⌜r = val_bool (r1 > r2)⌝)

lemma xwp_lemma_funs (xs : List _) (vs : List val) :
  t = trm_apps v0 ts ->
  v0 = val_funs xs t1 ->
  trms_to_vals ts = vs ->
  var_funs xs vs.length ->
  H ==> wpgen (isubst (xs.mkAlist vs) t1) Q ->
  triple t H Q

lemma hstars_simp_keep_lemma :
  H1 ==> (H ∗ Ha) ∗ Ht →
  H1 ==> Ha ∗ H ∗ Ht

lemma remove_not_in_r (h1 h2 : state) (p : loc) :
  p ∉ h2 →
  (h1 ∪ h2).erase p = h1.erase p ∪ h2

lemma trm_apps1 :
  trm_app t1 t2 = trm_apps t1 [t2]

lemma hstar_pick_10 :
  h1 ∗ h2 ∗ h3 ∗ h4 ∗ h5 ∗ h6 ∗ h7 ∗ h8 ∗ h9 ∗ h10 ∗ h = h10 ∗ h1 ∗ h2 ∗ h3 ∗ h4 ∗ h5 ∗ h6 ∗ h7 ∗ h8 ∗ h9 ∗ h

lemma hrange_of_conseq :
  (hrange L p) (conseq L p)

lemma eval_frame (h1 h2 : state) t (Q : val -> hProp) :
  eval h1 t (ofhProp Q) →
  Finmap.Disjoint h1 h2 →
  eval (h1 ∪ h2) t (Q ∗ (tohProp (fun h ↦ h = h2)))

lemma xsimp_flip_acc_l_lemma :
  hla = hla' →
  XSimp (hla', emp, emp) (hra, hrg, emp) →
  XSimp (hla, emp, emp) (hra, hrg, emp)

lemma xsimp_lr_hwand_hfalse :
  XSimp (Hla, emp, emp) ((⌜False⌝ -∗ H1) ∗ emp, emp, emp)

lemma triple_array_get L (p : loc) (i : Int) : --(v : 0 <= i ∧ i < L.length) :
   0 <= i ∧ i < L.length →
   triple (trm_app val_array_get p i)
    (harray L p)
    (fun r ↦ ⌜r = L[i.natAbs]!⌝ ∗ harray L p)

lemma remove_not_in_l (h1 h2 : state) (p : loc) :
  p ∉ h1 →
  (h1 ∪ h2).erase p = h1 ∪ h2.erase p

lemma neg_mul_abs (n : Int) :
  n < 0 → -1 * n = n.natAbs

lemma himpl_hstar_hpure_r P H H' :
   P →
   (H ==> H') →
   H ==> ⌜P⌝ ∗ H'

lemma triple_array_get_hcell (p : loc) (i : Int) (v : val) :
  triple [lang| val_array_get p i]
    (hcell v p i)
    (fun r ↦ ⌜r = v⌝ ∗ hcell v p i)

lemma hfalse_hstar_any H :
  ⌜False⌝ ∗ H = ⌜False⌝

lemma diff_disjoint (h₁ h₂ : state) :
  h₂.Disjoint (h₁ \ h₂)

lemma nth_app_r {A : Type} (_ : Inhabited A) n (l1 l2 : List A) :
  n ≥ l1.length →
  (l1 ++ l2)[n]! = l2[n - l1.length]!

lemma mem_diff_helper (h₁ : state) (l : @AList loc fun _ ↦ val) :
  a ∉ l →
  (p ∈ List.foldl (fun d s ↦ Finmap.erase s.fst d) h₁ l.entries → p ∈ h₁) →
  p ∈ List.foldl (fun d s ↦ Finmap.erase s.fst d) (Finmap.erase a h₁) l.entries →
  p ∈ h₁

lemma triple_hpure' t (P : Prop) Q :
  (P → triple t emp Q) →
  triple t ⌜P⌝ Q

lemma xfor_lemma (z n : ℤ) (x : var) (I : ℤ -> hProp) :
  z <= n ->
  (H ==> H' ∗ I z) ->
  (∀ i, z <= i -> i < n -> I i ==> wp (subst x i F1) (fun _ => I (i + 1))) ->
  ((fun _ => I n ∗ H') ===> Q) ->
  H ==> wp (trm_for x z n F1) Q

lemma evalExact_frame (h1 h2 : state) t (Q : val → hProp) :
  evalExact h1 t (ofhProp Q) →
  Finmap.Disjoint h1 h2 →
  evalExact (h1 ∪ h2) t (Q ∗ (tohProp (fun h ↦ h = h2)))

lemma int_eq_sub (l m n : ℤ) :
  l + m = n → l = n - m

lemma triple_val v H Q :
  H ==> Q v →
  triple (trm_val v) H Q

lemma triple_array_set L (p : loc) (i : Int) (v : val) :
  0 <= i ∧ i < L.length →
  triple (trm_app val_array_set p i v)
    (harray L p)
    (fun _ ↦ harray (L.set (Int.natAbs i) v) p)

lemma getElem!_nil_intval (n : Int) :
  ([] : List val)[n]! = default

@[simp]
lemma validLocE : validLoc (val := val) l h = False

lemma qstar_simp (Q1 : α -> hProp) :
  (Q1 ∗ H) x = Q1 x ∗ H

lemma Int.Ico_succ_left : ⟦i+1, j⟧ = Finset.Ioo (α := ℤ) i j

lemma hstar_flip_9 :
  h1 ∗ h2 ∗ h3 ∗ h4 ∗ h5 ∗ h6 ∗ h7 ∗ h8 ∗ h9 ∗ emp =
  h9 ∗ h8 ∗ h7 ∗ h6 ∗ h5 ∗ h4 ∗ h3 ∗ h2 ∗ h1 ∗ emp

lemma hstar_pick_last_10 :
  h1 ∗ h2 ∗ h3 ∗ h4 ∗ h5 ∗ h6 ∗ h7 ∗ h8 ∗ h9 ∗ h10 = h10 ∗ h1 ∗ h2 ∗ h3 ∗ h4 ∗ h5 ∗ h6 ∗ h7 ∗ h8 ∗ h9

lemma xsimp_l_cancel_hwand :
  XSimp (emp, Hlw, Hla ∗ H2 ∗ Hlt) HR →
  XSimp ((H1 ∗ Hla), ((H1 -∗ H2) ∗ Hlw), Hlt) HR

lemma insert_mem_keys (s : state) :
  p ∈ s →
  (s.insert p v).keys = s.keys

lemma hstar_pick_2  :
  h1 ∗ h2 ∗ h = h2 ∗ h1 ∗ h

lemma triple_arrayFun_length (p : loc) :
  triple (trm_app val_array_length p)
    (harrayFun f n p)
    (fun r ↦ ⌜r = val_int n⌝ ∗ harrayFun f n p)

lemma eval_like_val_fun_trm_fun_app_left (x : var) (t1 t2 : trm) :
  eval_like (trm_app (val_fun x t1) t2) (trm_app (trm_fun x t1) t2)

lemma hforall_inv A (J : A → hProp) h :
  (hforall J) h → forall x, J x h

lemma triple_unop op v1 (P : val → Prop) :
  evalunop op v1 P →
  triple (trm_app op v1) emp (fun r ↦ ⌜P r⌝)

lemma triple_array_length_hheader (n : Int) (p : loc) :
  triple (trm_app val_array_length p)
    (hheader n p)
    (fun r ↦ ⌜r = n⌝ ∗ hheader n p)

lemma purepost_frame :
  s.Disjoint h2 →
  (purepost (s ∪ h2) P) =
  (qstar (purepost s P) (tohProp fun h ↦ h = h2))

lemma himpl_lr_qwand_unify (Q : α -> hProp):
  XSimp (Hla, emp, emp) ((Q -∗ (Q ∗ Hla)) ∗ emp, emp, emp)

lemma hrange_eq_conseq (L : List val) (n : ℤ) (p : loc) (s : state) :
  L.length = n →
  hrange L p s →
  s.keys = (conseq (make_list n.natAbs val_uninit) p).keys

lemma hstar_flip_8 :
  h1 ∗ h2 ∗ h3 ∗ h4 ∗ h5 ∗ h6 ∗ h7 ∗ h8 ∗ emp =
  h8 ∗ h7 ∗ h6 ∗ h5 ∗ h4 ∗ h3 ∗ h2 ∗ h1 ∗ emp

theorem mem_diff_r (h₁ h₂ : state) :
  p ∈ h₁ \ h₂ → p ∉ h₂

lemma Heap.addE_of_disjoint (h₁ h₂ : heap) :
  h₁.Disjoint h₂ ->  h₁ +ʰ h₂ = h₁ ∪ h₂

lemma hcell_eq v p i :
  (hcell v p i) = ((p + 1 + (Int.natAbs i)) ~~> v) ∗ ⌜i >= 0⌝

lemma hstar_pick_7 :
  h1 ∗ h2 ∗ h3 ∗ h4 ∗ h5 ∗ h6 ∗ h7 ∗ h = h7 ∗ h1 ∗ h2 ∗ h3 ∗ h4 ∗ h5 ∗ h6 ∗ h

lemma nat_abs_succ (n : Int) :
  n ≥ 0 → (n + 1).natAbs = n.natAbs + 1

lemma validInter_hop_distr_l (h₁ h₂ h₃ : heap) :
  (h₁ +ʰ h₂) ⊥ʰ h₃ -> (h₁ ⊥ʰ h₃ ∧ h₂ ⊥ʰ h₃)

lemma cons_app {A : Type} (l1 l2 : List A) (x : A) :
  x :: l1 ++ l2 = x :: (l1 ++ l2)

lemma eval_like_trm_fun_val_fun_app_left (x : var) (t1 t2 : trm) :
  eval_like (trm_app (trm_fun x t1) t2) (trm_app (val_fun x t1) t2)

lemma sP_strongest :
  eval h t Q -> sP h t ===> Q

lemma xsimp_pick_lemma :
  hla2 = hla1 ->
  XSimp (hla1, hlw, hlt) hr ->
  XSimp (hla2, hlw, hlt) hr

lemma wp_conseq t Q1 Q2 :
  Q1 ===> Q2 →
  wp t Q1 ==> wp t Q2

lemma xlet_lemma H F1 F2of Q :
  H ==> F1 (fun v => F2of v Q) →
  H ==> wpgen_let F1 F2of Q

lemma xsimp_l_hempty :
  XSimp (hla, hlw, hlt) hr ->
  XSimp (hla, hlw, emp ∗ hlt) hr

lemma validInter_hop_distr_r (h₁ h₂ h₃ : heap) :
  h₁ ⊥ʰ (h₂ +ʰ h₃) -> (h₁ ⊥ʰ h₂ ∧ h₁ ⊥ʰ h₃)

lemma mkstruct_monotone F1 F2 Q :
  (forall Q, F1 Q ==> F2 Q) →
  mkstruct F1 Q ==> mkstruct F2 Q

lemma evalExact_sat :
  evalExact s t Q → ∃ v s, Q v s

lemma Option.merge_assoc (h : Associative f) (a b c : Option α) :
  Option.merge f (Option.merge f a b) c = Option.merge f a (Option.merge f b c)

lemma hstar_flip_5 :
  h1 ∗ h2 ∗ h3 ∗ h4 ∗ h5 ∗ emp = h5 ∗ h4 ∗ h3 ∗ h2 ∗ h1 ∗ emp

lemma natabs_eq (a : Nat) :
  a = (Int.ofNat a).natAbs

lemma validInter_of_disjoint (h₁ h₂ : heap) :
  h₁.Disjoint h₂ ->  h₁ ⊥ʰ h₂

lemma union_same_keys (h₁ h₂ h₃ : state) :
  h₁.Disjoint h₃ → h₂.Disjoint h₃ →
  (h₁ ∪ h₃).keys = (h₂ ∪ h₃).keys →
  h₁.keys = h₂.keys

lemma eval_addr s r1 r2 Q :
  Q (val_real (r1 + r2)) s →
  eval s (trm_app (trm_app val_add (val_real r1)) (val_real r2)) Q

lemma xsimpl_r_hgc_or_htop :
  XSimp HL (Hra, (H ∗ Hrg), Hrt) ->
  XSimp HL (Hra, Hrg, (H ∗ Hrt))

lemma wp_eval_like t1 t2 Q :
  eval_like t1 t2 →
  wp t1 Q ==> wp t2 Q

lemma hstar_intro (H1 H2 : hProp) h1 h2 :
  H1 h1 →
  H2 h2 →
  Finmap.Disjoint h1 h2 →
  (H1 ∗ H2) (h1 ∪ h2)

lemma triple_ref (v : val) :
  (forall (p : loc), triple (subst x p t2) (H ∗ (p ~~> v)) (Q ∗ ∃ʰ v, p ~~> v)) →
  triple (trm_ref x (trm_val v) t2) H Q

lemma sum_Ico_succlr {_ : AddCommMonoid M} (f : Int -> M) (i j : Int) :
  ∑ i in ⟦i, j⟧, f (i+1) = ∑ i in ⟦i+1, j+1⟧, f i

lemma xwhile_inv_measure_lemma_up (Xtop : Int) (I : Bool -> Int -> hProp) :
  (H ==> H' ∗ ∃ʰ b a, I b a) ->
  (∀ b X, I b X ==> wp F1 (fun bv => I b X ∗ ⌜bv = b⌝)) ->
  (∀ X, I true X ==> wp F2 (fun _ => ∃ʰ b X', ⌜X < X' ∧ X' <= Xtop⌝ ∗ I b X')) ->
  ((fun _ => H' ∗ ∃ʰ a, I false a) ===> Q) ->
  H ==> wp (trm_while F1 F2) Q

lemma eval_app_arg2' : forall s1 (v1 : val) t2 Q1 Q,
  eval s1 t2 Q1 ->
  (forall v2 s2, eval s2 (trm_app v1 v2) Q) ->
  eval s1 (trm_app v1 t2) Q

lemma hstar_flip_3 :
  h1 ∗ h2 ∗ h3 ∗ emp = h3 ∗ h2 ∗ h1 ∗ emp

lemma mkstruct_sound t F :
  formula_sound t F →
  formula_sound t (mkstruct F)

lemma Alist_insert_delete_id (l : @AList loc (fun _ ↦ val)) :
  p ∉ l →
  (l.insert p v).erase p = l

lemma keys_eq_not_mem_l (h1 h2 : state) :
  h1.keys = h2.keys →
  p ∉ h1 →
  p ∉ h2

lemma list_middle_inv (A : Type) (n : Nat) (l : List A) :
  n < l.length →
  exists (x : A) (l1 l2 : List A),
    l = l1 ++ x :: l2 ∧ l1.length = n

theorem Perm.kmerge {l₁ l₂ l₃ l₄ : List (Sigma (fun _ : loc => val))} (nd₁ : l₁.NodupKeys) /- nd₁ is necessary -/ (nd₃ : l₃.NodupKeys)
    (p₁₂ : l₁.Perm l₂) (p₃₄ : l₃.Perm l₄) : (kmerge l₁ l₃).Perm $ kmerge l₂ l₄

@[simp]
lemma oneE : OfNat.ofNat 1 = 1

lemma triple_app_fun_direct x v2 t1 H Q :
  triple (subst x v2 t1) H Q →
  triple (trm_app (val_fun x t1) v2) H Q

lemma insert_frame :
  s.Disjoint h2 →
  p ∈ s →
  fun v'' s' ↦ v'' = val_unit ∧ s' = Finmap.insert p v' (s ∪ h2) =
  (qstar (fun v'' s' ↦ v'' = val_unit ∧ s' = Finmap.insert p v' s) (tohProp fun h ↦ h = h2))

lemma List.not_nil_snoc {α : Type u} (l : List α) : l ≠ [] → ∃ l' x, l = l' ++ [x]

lemma insert_disjoint_l (h1 h2 : state) (x : loc) (v : val) :
  h2.Disjoint (h1.insert x v) →
  x ∉ h2 ∧ h2.Disjoint h1

lemma Option.merge_none_r (a : Option α) : Option.merge f a none = a

lemma triple_hpure t P H Q :
  (P → triple t H Q) →
  triple t (⌜P⌝ ∗ H) Q

lemma hwand_hpure_l P H :
  P → (⌜P⌝ -∗ H) = H

lemma hstar_pick_last_4 :
  h1 ∗ h2 ∗ h3 ∗ h4 = h4 ∗ h1 ∗ h2 ∗ h3

lemma himpl_frame_l H1 H1' H2 :
  H1 ==> H1' →
  (H1 ∗ H2) ==> (H1' ∗ H2)

lemma triple_array_set_hseg L (p : loc) (i j : Int) (v : val) :
  0 <= i - j ∧ i - j < L.length →
  triple (trm_app val_array_set p i v)
    (hseg L p j)
    (fun _ ↦ hseg (L.set (Int.natAbs (i - j)) v) p j)

lemma himpl_hempty_hwand_same H :
  emp ==> (H -∗ H)

lemma wp_if (b : Bool) t1 t2 Q :
  wp (if b then t1 else t2) Q ==> wp (trm_if b t1 t2) Q

lemma wpgen_fun_sound x t1 Fof :
  (forall vx, formula_sound (subst x vx t1) (Fof vx)) →
  formula_sound (trm_fun x t1) (wpgen_fun Fof)

lemma xsimp_lr_hwand :
  XSimp (emp, emp, (H1 ∗ Hla)) (emp, emp, H2 ∗ emp) ->
  XSimp (Hla, emp, emp) ((H1 -∗ H2) ∗ emp, emp, emp)

lemma union_difference_id (h₁ h₂ : state) :
  h₁.Disjoint h₂ →
  (h₁ ∪ h₂) \ h₂ = h₁

lemma disjoint_insert_l (h1 h2 : state) (x : loc) (v : val) :
  Finmap.Disjoint h1 h2 →
  x ∈ h1 →
  Finmap.Disjoint (Finmap.insert x v h1) h2

lemma AList.erase_twice {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (l : AList β) :
    (AList.erase a (AList.erase a l)).entries.Perm (AList.erase a l).entries

lemma add_pointer_spec (p q : loc) (n m : Int) (_ : m >= 0) :
  { p ~~> n ∗ q ~~> m }
  [ add_pointer p q ]
  { v, ⌜v = n+m⌝ ∗ ⊤  }

lemma xstruct_lemma F H Q :
  H ==> F Q →
  H ==> mkstruct F Q

lemma xwhile_inv_lemma (I : Bool -> α -> hProp)
  (F1 F2 : formula) :
    WellFounded R ->
    (H ==> ∃ʰ b a, I b a) ->
    (∀ (S: formula) b X, structural S ->
        (∀ b a', R a' X -> (I b a') ==> S fun _ => ∃ʰ a, I false a) ->
        I b X ==> wpgen_if_trm F1 (wpgen_seq F2 S) (wpgen_val val_unit) fun _ => ∃ʰ a, I false a) ->
    H ==> wpgen_while F1 F2 (fun _ => ∃ʰ a, I false a)

lemma non_mem_union (h1 h2 : state) :
  a ∉ h1 ∪ h2 ↔ a ∉ h1 ∧ a ∉ h2

lemma evalunop_unique :
  evalunop op v P → evalunop op v P' → P = P'

lemma triple_abs (i : Int) :
  triple [lang| val_abs i]
    emp
    (fun r ↦ ⌜r = val_int i.natAbs⌝)

lemma hstar_pick_last_2 :
  h1 ∗ h2 = h2 ∗ h1

lemma kmerge_comm_perm (l₁ l₂ : List (Sigma (fun _ : loc => val))) (nd₁ : l₁.NodupKeys) (nd₂ : l₂.NodupKeys) :
  (kmerge l₁ l₂).Perm $ (kmerge l₂ l₁)

lemma eval_val_minimal s v :
  eval s (trm_val v) (fun v' s' => (v' = v) /\ (s' = s))

@[simp]
lemma Heap.add_empty_l (h : heap) : ∅ +ʰ h = h

lemma get_out_of_bounds {_ : Inhabited α} (L : List α) (i : Int) :
  L.length ≤ i.natAbs →
  L[i]! = default

@[disjE]
lemma disjoint_label_set :
  Disjoint ⟪l,s⟫ ⟪l',s'⟫ ↔ l ≠ l' ∨ Disjoint s s'
</all_available_lemmas>

<local_ctx>
import Mathlib.Data.Finmap

import Mathlib.Algebra.BigOperators.Group.Finset

import SPLean.Common.Heap

import SPLean.Common.Util

import SPLean.Theories.Lang

open Classical

def hProp := heap -> Prop

abbrev himpl (H1 H2 : hProp) : Prop :=
  forall h, H1 h -> H2 h

infixr:51 " ==> " => himpl

def qimpl {A} (Q1 Q2 : A → hProp) : Prop :=
  forall (v:A), Q1 v ==> Q2 v

infixr:51 " ===> " => qimpl

def hempty : hProp :=
  fun h => (h = ∅)

def hstar (H1 H2 : hProp) : hProp :=
  fun h => exists h1 h2,
    H1 h1 ∧ H2 h2 ∧ Finmap.Disjoint h1 h2 ∧ h = h1 ∪ h2

def hexists {A} (J : A → hProp) : hProp :=
  fun h => exists x, J x h

def hforall {A} (J : A → hProp) : hProp :=
  fun h => forall x, J x h

notation:max "emp" => hempty

infixr:60 " ~~> " => hsingle

class HStar (α : Type u) (β : Type v) (γ : outParam (Type w)) where
   
  hStar : α → β → γ

infixr:55 " ∗ " => HStar.hStar

@[default_instance]
instance : HStar hProp hProp hProp where
  hStar := hstar

section

open Lean.TSyntax.Compat

end

def hpure (P : Prop) : hProp :=
  hexists (fun (_ : P) => emp)

def hwand (H1 H2 : hProp) : hProp :=
  hexists (fun (H0 : hProp) => H0 ∗ hpure ((H1 ∗ H0) ==> H2))

def qwand {A} (Q1 Q2 : A → hProp) : hProp :=
  hforall (fun (x : A) => hwand (Q1 x) (Q2 x))

notation:max "⌜" P "⌝" => hpure P

notation (priority := high) "⊤" => htop

def qstar {A} (Q : A → hProp) (H : hProp) : A → hProp :=
  fun x => hstar (Q x) H

instance (A : Type) : HStar (A → hProp) hProp (A → hProp) where
  hStar := qstar

class HWand (α : Type u) (β : Type v) (γ : outParam (Type w)) where
   
  hWand : α → β → γ

infixr:55 " -∗ " => HWand.hWand

@[default_instance]
instance : HWand hProp hProp hProp where
  hWand := hwand

instance (α : Type) : HWand (α → hProp) (α → hProp) hProp where
  hWand := qwand
</local_ctx>

<target_theorem>
lemma qwand_equiv H A (Q1 Q2 : A → hProp) :
  H ==> (Q1 -∗ Q2) ↔ (Q1 ∗ H) ===> Q2 :=
</target_theorem>

