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>
@[heapSimp]
def protect (x : α) := x

def hProp := heap -> Prop

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

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

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

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

AList.entries in Mathlib.Data.List.AList

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

def xsimp_step_lr (xsimp : XSimpR) : TacticM Unit := do
  trace[xsimp] "LHS/RHS step"
  match xsimp.hrg with
  | `(hempty) =>
    match xsimp.hra with
    | `(@HStar.hStar hProp hProp $_ $_ $h1 hempty) =>
      if h1.isMVarStx then
        withAssignableSyntheticOpaque {| hsimp; apply himpl_lr_refl |}
        return ( )
      match h1 with
      | `(@HWand.hWand hProp hProp $_ $_ $h1 $_) =>
        match h1 with
        | `(hpure False) => {| apply xsimp_lr_hwand_hfalse |}
        | _ =>   xsimp_flip_acc_lr xsimp.hla xsimp.hra ; {| apply xsimp_lr_hwand |}
      | `(@HWand.hWand $_   $_    $_ $_ $h1 $_) =>
        xsimp_flip_acc_lr xsimp.hla xsimp.hra ;
        try
          let .true := h1.isMVarStx | failure
          {| apply himpl_lr_qwand_unify |}
        catch _ =>
          {| first | apply xsimpl_lr_qwand_unit
                   | apply xsimpl_lr_qwand; unhygienic intro
             try simp only [qstar_simp] |}
      | `(@hforall $_ fun ($x : $_) => $_) =>  
        {| xsimp_flip_acc_l $xsimp.hla ; apply xsimpl_lr_hforall; intro $x:term |}
      | _ =>   xsimp_flip_acc_lr xsimp.hla xsimp.hra ; {| apply xsimp_lr_exit |}
    | `(hempty) => {| first | apply himpl_lr_refl | apply xsimp_lr_exit |}
    | _ =>   xsimp_flip_acc_lr xsimp.hla xsimp.hra ; {| apply xsimp_lr_exit |}
  | `(@HStar.hStar hProp hProp $_ $_ htop hempty) => {| first | apply himpl_lr_htop | apply xsimp_lr_exit |}
  | _ =>   xsimp_flip_acc_lr xsimp.hla xsimp.hra ; {| apply xsimp_lr_exit |}

@[app_unexpander hforall] def unexpandHForall : Lean.PrettyPrinter.Unexpander
  | `($(_) fun $x:ident => h∀ $xs:binderIdent*, $b) => `(h∀ $x:ident $xs:binderIdent*, $b)
  | `($(_) fun $x:ident => $b)                     => `(h∀ $x:ident, $b)
  | `($(_) fun ($x:ident : $t) => $b)              => `(h∀ ($x:ident : $t), $b)
  | t                                              => pure t

Lean.Meta.mkForallFVars in Lean.Meta.Basic

sby in Ssreflect.Done

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

def purepostin (s : state) (P : val → Prop) (Q : val → state → Prop) : Prop :=
  
  forall v, P v → Q v s

Lean.levelOne in Lean.Level

srw in Ssreflect.Rewrite

Lean.Name in Init.Prelude

Finmap.foldl in Mathlib.Data.Finmap

def val_fixs (f:var) (xs:List var) (t:trm) : val :=
  match xs with
  | .nil => val_uninit
  | x1::xs' => val_fix f x1 (trm_funs xs' t)

L in Archive.Hairer

String in Init.Prelude

class AddCommMonoidWRT (α : Type) (add' : semiOutParam $ α -> α -> α) extends AddCommMonoid α where
  addE : (· + ·) = add'

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

def haffine (_ : hProp) :=
  True

abbrev ctx := AList (fun _ : var ↦ val)

macro "∃ʰ" xs:Lean.explicitBinders ", " b:term : term => Lean.expandExplicitBinders ``hexists xs b

def delabAll :=
  (withOptions (fun _ => KVMap.empty.insert `pp.funBinderTypes true) $ PrettyPrinter.delab ·)

def val_abs : val := [lang|
  fun i =>
    let c := i < 0 in
    let m := 0 - 1 in
    let j := m * i in
    if c then j else i ]

def toHimp (e : Expr) : MetaM Expr := do
  let eTy <- inferType e
  trace[xchange] "type of give hypothesis {eTy}"
  forallTelescope eTy fun xs eTy => do
    let himpl <- match_expr eTy with
      | himpl _ _ => return e
      | qimpl _ _ _ => return e
      | Eq _ _ _  =>
        mkAppOptM `himpl_of_eq #[.none, .none, eTy]
      | _        => throwError "Expected a heap entailment or an equality"
    mkForallFVars xs himpl

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

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

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

Lean.MVarId in Lean.Expr

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

List.zipWith in Init.Data.List.Basic

Disjoint in Mathlib.Order.Disjoint

Lean.Meta.withAssignableSyntheticOpaque in Lean.Meta.Basic

instHAdd in Init.Prelude

noncomputable def Heap.add (h₁ h₂ : heap) : heap :=
  Finmap.liftOn₂ h₁ h₂ (fun h₁ h₂ => (h₁.merge h₂).toFinmap) (by admit /- proof elided -/
    )

| step_neg : forall s b,
      step s (trm_app val_neg (val_bool b)) s (val_bool (¬ b))
  | step_opp : forall s n,
      step s (trm_app val_opp (val_int n)) s (val_int (- n))

| 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')

Inhabited in Init.Prelude

Add.add in Init.Prelude

def hstar_pick_lemma (i : Nat) (pickLast : Bool) : Ident :=
  if pickLast then
    mkIdent s!"hstar_pick_last_{i}".toName
  else
    mkIdent s!"hstar_pick_{i}".toName

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

Nat in Init.Prelude

AList in Mathlib.Data.List.AList

Lean.RBMap in Lean.Data.RBMap

@[simp]
def wpgen_app (t : trm) : formula :=
  fun Q ↦ ∃ʰ H, H ∗ ⌜triple t H Q⌝

elab "#hint_xapp" thm:ident : command => do
  Command.runTermElabM fun _ => do
    let thm := (<- Term.elabTerm thm none)
    let .some thmName := thm.getAppFn.constName? | throwError "invalid theorem"
    let thm <- Meta.inferType thm
    let thmFun <- Meta.forallTelescope thm fun _ thm => do
      getTripleFun thm
    xappExtension.add (thmFun, thmName)

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

Lean.binderIdent in Init.Notation

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

def harray_int (L : List Int) : loc → hProp :=
  harray (L.map val_int)

Lean.explicitBinders in Init.NotationExtra

instance (priority := low) : Zero hProp := ⟨emp⟩

AddCommMonoid in Mathlib.Algebra.Group.Defs

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

AList.lookup in Mathlib.Data.List.AList

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

Finset.Ioo in Mathlib.Order.Interval.Finset.Defs

Finset in Mathlib.Data.Finset.Defs

AList.insert in Mathlib.Data.List.AList

partial def hstar_search (hs : Term) (test : Nat -> Term -> optParam Bool false -> TacticM Unit) :=
  let rec loop (i : Nat) (hs : Term)  : TacticM Unit := do
    match hs with
    | `(@HStar.hStar hProp hProp $_ $_ $h1 $h2) => do
      try
        test i h1
      catch _ => loop (i+1) h2
    | _ => test i hs true
  loop 1 hs

def xsimp_pick_same_pointer (p hla : Term) : TacticM Unit := withMainContext do
  let p  <- Tactic.elabTerm p none
  hstar_search hla fun i h' last? => do
    match h' with
      | `(hsingle $p' $_) =>
        if p'.isMVarStx then throwError "not equal" else
        let p' <- Tactic.elabTerm p' none
        let .true <-
          withAssignableSyntheticOpaque <| isDefEq p' p | throwError "not equal"
      | _ => throwError "not equal"
    xsimp_pick i last?

def hstars_simp_pick (i : Nat) (_ : Bool) : TacticM Unit :=
  let L := hstar_pick_lemma i false
  {| eapply hstars_simp_pick_lemma ; apply $(L) |}

Option.any in Init.Data.Option.Basic

List.foldl in Init.Prelude

Int in Init.Data.Int.Basic

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

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

def mkstruct (F : formula) :=
  fun (Q : val -> hProp) ↦ ∃ʰ Q', F Q' ∗ (Q' -∗ Q)

macro "h∀" xs:Lean.explicitBinders ", " b:term : term => Lean.expandExplicitBinders ``hforall xs b

Lean.Syntax in Init.Prelude

Lean.Meta.isDefEq in Lean.Meta.Basic

Sigma in Init.Core

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

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

def conseq {B : Type} (vs : List B) (l : Nat) : Finmap (fun _ : Nat ↦ B) :=
  match vs with
  | [] => ∅
  | v :: vs' => (Finmap.singleton l v) ∪ (conseq vs' (l + 1))

| step_fun : forall s x t1,
      step s (trm_fun x t1) s (val_fun x t1)
  | step_fix : forall s f x t1,
      step s (trm_fix f x t1) s (val_fix f x t1)
  | step_app_fun : forall s v1 v2 x t1,
      v1 = val_fun x t1 →
      v2 = trm_val v2' →
      step s (trm_app v1 v2) s (subst x v2' t1)
  | step_app_fix : forall s v1 v2 f x t1,
      v1 = val_fix f x t1 →
      v2 = trm_val v2' →
      step s (trm_app v1 v2) s (subst x v2' (subst f v1 t1))
  | step_if : forall s b t1 t2,
      step s (trm_if (val_bool b) t1 t2) s (if b then t1 else t2)
  | step_seq : forall s t2 v1,
      step s (trm_seq v1 t2) s t2
  | step_let : forall s x t2 v1,
      v1 = trm_val v1' →
      step s (trm_let x v1 t2) s (subst x v1' t2)

HAdd in Init.Prelude

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

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

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

ident in Ssreflect.IntroPats

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

inductive evalExact : state → trm → (val → state → Prop) -> Prop where
  | val : forall s v,
      evalExact s (trm_val v) (fun v' s' ↦ v' = v ∧ s' = s)
  | fun : forall s x t1,
      evalExact s (trm_fun x t1) (fun v' s' ↦ v' = val_fun x t1 ∧ s' = s)
  | fix : forall s f x t1,
      evalExact s (trm_fix f x t1) (fun v' s' ↦ v' = val_fix f x t1 ∧ s' = s)
  | app_arg1 : forall s1 t1 t2 Q1 Q,
      ¬ trm_is_val t1 ->
      evalExact s1 t1 Q1 ->
      (forall v1 s2, Q1 v1 s2 -> evalExact s2 (trm_app v1 t2) Q) ->
      evalExact s1 (trm_app t1 t2) Q
  | app_arg2 : forall s1 (v1 : val) t2 Q1 Q,
      ¬ trm_is_val t2 ->
      evalExact s1 t2 Q1 ->
      (forall v2 s2, Q1 v2 s2 -> evalExact s2 (trm_app v1 v2) Q) ->
      evalExact s1 (trm_app v1 t2) Q
  | app_fun : forall s1 v1 (v2 :val) x t1 Q,
      v1 = val_fun x t1 ->
      evalExact s1 (subst x v2 t1) Q ->
      evalExact s1 (trm_app v1 v2) Q
  | app_fix : forall s (v1 v2 : val) f x t1 Q,
      v1 = val_fix f x t1 ->
      evalExact s (subst x v2 (subst f v1 t1)) Q ->
      evalExact s (trm_app v1 v2) Q
  | seq : forall Q1 s t1 t2 Q,
      evalExact s t1 Q1 ->
      (forall v1 s2, Q1 v1 s2 -> evalExact s2 t2 Q) ->
      evalExact s (trm_seq t1 t2) Q
  | let : forall Q1 s x t1 t2 Q,
      evalExact s t1 Q1 ->
      (forall v1 s2, Q1 v1 s2 -> evalExact s2 (subst x v1 t2) Q) ->
      evalExact s (trm_let x t1 t2) Q
  | if : forall s (b : Bool) t1 t2 Q,
      evalExact s (if b then t1 else t2) Q ->
      evalExact s (trm_if (val_bool b) t1 t2) Q
  | unop : forall op s v1 P,
      evalunop op v1 P ->
      evalExact s (trm_app op v1) (purepost s P)
  | binop : forall op s (v1 v2 : val) P,
      evalbinop op v1 v2 P ->
      evalExact s (trm_app (trm_app op v1) v2) (purepost s P)
  | ref : forall s x t1 t2 Q Q₁,
    evalExact s t1 Q₁ →
    (∀ v1 s1, Q₁ v1 s1 → ∀ p ∉ s1,
     evalExact (s1.insert p v1) (subst x p t2) fun v s ↦ Q v (s.erase p)) →
      evalExact s (trm_ref x t1 t2) Q
  | get : forall s p,
      p ∈ s ->
      evalExact s (trm_app val_get (val_loc p))
        (fun v' s' ↦ v' = read_state p s ∧ s' = s)
  | set : forall s p v,
      v = trm_val v' ->
      p ∈ s ->
      evalExact s (trm_app (trm_app val_set (val_loc p)) v)
        (fun v'' s' ↦ v'' = val_unit ∧ s' = s.insert p v')
  | alloc_arg : forall s Q₁ Q,
    ¬ trm_is_val t1 →
    evalExact s t1 Q₁ →
    (∀ v' s', Q₁ v' s' → evalExact s' (trm_alloc x v' t2) Q) →
    evalExact s (trm_alloc x t1 t2) Q
  | alloc : forall (sa : state) (n : ℤ) Q,
    n ≥ 0 →
    (∀ (p : loc) (sb : state),
      sb = conseq (make_list n.natAbs val_uninit) p →
      p ≠ null →
      Finmap.Disjoint sa sb →
      evalExact (sb ∪ sa) (subst x p t2) fun v s ↦ Q v (s \ sb)) →
    evalExact sa (trm_alloc x n t2) Q
  
  
  
  
  
  
  | for (n₁ n₂ : Int) (Q : val -> state -> Prop) :
    evalExact s (if (n₁ < n₂) then
               (trm_seq (subst x n₁ t₁) (trm_for x (val_int (n₁ + 1)) n₂ t₁))
            else val_unit) Q ->
    evalExact s (trm_for x n₁ n₂ t₁) Q
  | while (t₁ t₂ : trm) (Q Q₁ : val -> state -> Prop) :
    evalExact s t₁ Q₁ ->
    (∀ s v, Q₁ v s -> evalExact s (trm_if v (trm_seq t₂ (trm_while t₁ t₂)) val_unit) Q) ->
    evalExact s (trm_while t₁ t₂) Q

@[simp]
def trms_vals (vs : List var) : List trm :=
  vs.map trm_var

@[app_unexpander trm_alloc] def unexpandAlloc : Lean.PrettyPrinter.Unexpander
  | `($(_) $x:str [lang| $t1] [lang| $t2]) =>
    let str := x.getString
    let name := Lean.mkIdent $ Lean.Name.mkSimple str
    `([lang| alloc $t1 as $name in $t2])
  | _ => throw ( )

def evalExact_ref_nonpositive s x t1 t2 (Q : val → state → Prop) :=
  ∃ Q₁, evalExact s t1 Q₁ ∧
  (∀ v1 s1, Q₁ v1 s1 → ∀ p ∉ s1,
    (evalExact (s1.insert p v1) (subst x p t2) (fun v s ↦ Q v (s.erase p))))

GetElem in Init.GetElem

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

def hstar_flip_lemma (i : Nat) : Ident :=
  mkIdent s!"hstar_flip_{i}".toName

def reducible (s : state) (t : trm) : Prop :=
  exists s' t', step s t s' t'

def intersect (s1 s2 : state) := s1 \ (s1 \ s2)

@[app_unexpander val_prim] def unexpandPrim : Lean.PrettyPrinter.Unexpander
  
  | `($(_) val_free) => `([uop| free])
  | `($(_) val_not) => `([uop| not])
  | `($(_) val_opp) => `([uop| -])
  | `($(_) val_get) => `([uop| !])
  | `($(_) val_add) => `([bop| +])
  | `($(_) val_mul) => `([bop| *])
  | `($(_) val_sub) => `([bop| -])
  | `($(_) val_div) => `([bop| /])
  | `($(_) val_lt) => `([bop| <])
  | `($(_) val_gt) => `([bop| >])
  | `($(_) val_le) => `([bop| <=])
  | `($(_) val_ge) => `([bop| >=])
  | `($(_) val_eq) => `([bop| =])
  | `($(_) val_neq) => `([bop| !=])
  | `($(_) val_mod) => `([bop| mod])
  | `($(_) val_set) => `([bop| :=])
  | `($(_) val_ptr_add) => `([bop| ++])
  | _ => throw ( )

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

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

OfNat.ofNat in Init.Prelude

scoped instance (priority := 1) EPCM : PartialCommMonoid val where
  valid := valid
  valid_add := by admit /- proof elided -/

abbrev tohProp (h : heap -> Prop) : hProp := h

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

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

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

inductive steps : state → trm → state → trm → Prop :=
  | steps_refl : forall s t,
      steps s t s t
  | steps_step : forall s1 s2 s3 t1 t2 t3,
      step s1 t1 s2 t2 →
      steps s2 t2 s3 t3 →
      steps s1 t1 s3 t3

Lean.PrettyPrinter.delab in Lean.PrettyPrinter.Delaborator.Basic

List.length in Init.Prelude

instance : Coe (List var) (List trm) where
  coe := trms_vals

Finmap.insert in Mathlib.Data.Finmap

scoped instance (priority := 0) EPCM' : PartialCommMonoidWRT val add valid where
  addE := by admit /- proof elided -/

@[simp]
abbrev valid : val -> Prop
  | .val_bool _ => True
  | _ => False

def wpgen_let (F1 : formula) (F2of : val → formula) : formula :=
  fun Q ↦ F1 (fun v ↦ F2of v Q)

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

impl in Mathlib.Deprecated.MLList.BestFirst

instance : Coe loc val where
  coe l := val.val_loc l

def getTripleFun (g : Expr) : MetaM Name := do
  let_expr triple t _ _ := g | throwError "goal is not a triple"
  let_expr trm_app t _ := t | throwError "triple term is not an application"
  let .some n := (getNestedApp t).constName? | throwError "nested application is not a constant"
  return n

elim in Ssreflect.Elim

scase! in Ssreflect.Elim

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 val_bool] def unexpandBool : Lean.PrettyPrinter.Unexpander
  | `($(_) $n:ident) => `($n:ident)
  | `($(_) $n:term) => `(lang|⟨$n:term⟩)
  | _ => throw ( )

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

def wpgen_seq (F1 F2 : formula) : formula :=
  fun Q ↦ F1 (fun _ ↦ F2 Q)

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"

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

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

List.map in Init.Prelude

def structural_pred (S : α -> formula) :=
  ∀ x, structural $ S x

inductive step : state → trm → state → trm → Prop where

Int.toNat in Init.Data.Int.Basic

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

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

instance: GetElem (List α) Int α (fun L i => i.natAbs < L.length) :=
  ⟨fun xs i _ => xs[i.natAbs]⟩

Lean.pp.funBinderTypes in Lean.PrettyPrinter.Delaborator.Options

def hcell (v : val) (p : loc) (i : Int) : hProp :=
  ((p + 1 + (Int.natAbs i)) ~~> v) ∗ ⌜i >= 0⌝

Prod.mk in Init.Prelude

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

Lean.pp.all in Lean.PrettyPrinter.Delaborator.Options

def null : loc := 0

List.Perm in Init.Data.List.Basic

propext in Init.Core

abbrev default_get' := default_get (val_int 0)

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

instance : Coe ℝ val := ⟨val_real⟩

CoeFun in Init.Coe
</all_available_defs>

<all_available_lemmas>
lemma himpl_trans H2 H1 H3 :
  (H1 ==> H2) → (H2 ==> H3) → (H1 ==> H3)

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

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

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 himpl_hwand_r H1 H2 H3 :
  H2 ∗ H1 ==> H3 →
  H1 ==> (H2 -∗ H3)

lemma haffine_hpure P :
  haffine ⌜P⌝

lemma set_keep_length (L : List val) i v :
  L.length = (L.set i v).length

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

lemma wp_app_fix f x v1 v2 t1 Q :
  v1 = val_fix f x t1 →
  wp (subst x v2 (subst f v1 t1)) Q ==> wp (trm_app v1 v2) Q

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

lemma triple_gt n1 n2 :
  triple (trm_app val_gt (val_int n1) (val_int n2))
    emp
    (fun r ↦ ⌜r = val_bool (n1 > n2)⌝)

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

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

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

lemma qwand_specialize A (x : A) (Q1 Q2 : A → hProp) :
  (Q1 -∗ Q2) ==> (Q1 x -∗ Q2 x)

@[simp]
lemma star_post_empty (Q : α -> hProp) :
  Q ∗ emp = Q

@[xapp] -- Another way to add a triple lemma to a hint database
lemma incr_spec (p : loc) (n : Int) :
  { p ~~> n }
  [ ++p ]
  { p ~~> val_int (n + 1) }

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

lemma hstar_pick_last_7 :
  h1 ∗ h2 ∗ h3 ∗ h4 ∗ h5 ∗ h6 ∗ h7 = h7 ∗ h1 ∗ h2 ∗ h3 ∗ h4 ∗ h5 ∗ h6

lemma haffine_hexists A (J : A → hProp) :
  (forall x, haffine (J x)) →
  haffine (hexists J)

lemma evalExact_frame_get :
  s.Disjoint h2 →
  p ∈ s →
  evalExact (s ∪ h2) t (fun v' s' ↦ v' = read_state p (s ∪ h2) ∧ s' = s ∪ h2 ) →
  evalExact (s ∪ h2) t
    (qstar (fun v' s' ↦ v' = read_state p s ∧ s' = s) (tohProp fun h ↦ h = h2))

lemma xapp_lemma : forall t Q1 H1 H Q,
  triple t H1 Q1 ->
  H ==> H1 ∗ (Q1 -∗ protect Q) ->
  H ==> wpgen_app t Q

lemma triple_of_wpgen t H Q :
  H ==> wpgen t Q →
  triple t H Q

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

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 xval_lemma v H Q :
  H ==> Q v →
  H ==> wpgen_val v Q

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

lemma frame_eq_rw :
  s.Disjoint h2 →
  (fun v' s' ↦ v' = v ∧ s' = s ∪ h2) =
  (qstar (fun v' s' ↦ v' = v ∧ s' = s) (tohProp (fun h ↦ h = h2)))

lemma himpl_hforall_l A (x : A) (J : A → hProp) H :
  (J x ==> H) →
  (hforall J) ==> H

lemma himpl_refl H : H ==> H

lemma insert_same (h1 h2 : state) :
  p ∉ h1 → p ∉ h2 →
  (h1.insert p v).keys = (h2.insert p v').keys →
  h1.keys = h2.keys

lemma hstar_flip_1 :
  h1 ∗ emp = h1 ∗ emp

lemma hstar_hempty_l H :
  emp ∗ H = H

lemma mkstruct_erase Q F :
  F Q ==> mkstruct F Q

lemma hstar_pick_last_3 :
  h1 ∗ h2 ∗ h3 = h3 ∗ h1 ∗ h2

lemma htop_intro h :
  ⊤ h

lemma triple_mulr r1 r2 :
  triple (trm_app val_mul (val_real r1) (val_real r2))
    emp
    (fun r ↦ ⌜r = val_real (r1 * r2)⌝)

lemma finite_state' n (s : state) :
  ∃ p, p ≠ null ∧
    Finmap.Disjoint s (conseq (make_list n val_uninit) p)

lemma hempty_eq_hpure_true :
  emp = ⌜True⌝

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

lemma haffine_hany : forall H,
  haffine H

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

lemma hseg_focus (i j : Int) L p (v : 0 <= i - j ∧ i - j < L.length) :
  0 <= i - j ∧ i - j < L.length →
  hseg L p j ==>
  hcell L[(i - j).natAbs]! p i
    ∗ (h∀ w, hcell w p i -∗ hseg (L.set (i - j).natAbs w) p j)

lemma triple_addr r1 r2 :
  triple (trm_app val_add (val_real r1) (val_real r2))
    emp
    (fun r ↦ ⌜r = val_real (r1 + r2)⌝)

lemma natabs_nonneg (p : Nat) (n : Int) :
  n ≥ 0 → (p + n).natAbs = p + n.natAbs

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 erase_of_non_mem (h : state) :
  p ∉ h →
  h.erase p = h

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

lemma triple_le n1 n2 :
  triple (trm_app val_le (val_int n1) (val_int n2))
    emp
    (fun r ↦ ⌜r = val_bool (n1 <= n2)⌝)

lemma triple_eq v1 v2 :
  triple (trm_app val_eq (trm_val v1) (trm_val v2))
    emp
    (fun r ↦ ⌜r = is_true (v1 = v2)⌝)

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

lemma triple_lt n1 n2 :
  triple (trm_app val_lt (val_int n1) (val_int n2))
    emp
    (fun r ↦ ⌜r = val_bool (n1 < n2)⌝)

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

lemma hadd_single (v v' : Bool) :
  (p ~~> v) + (p ~~> v') = p ~~> (v || v')

lemma triple_let x t1 t2 Q1 H Q :
  triple t1 H Q1 →
  (forall v1, triple (subst x v1 t2) (Q1 v1) Q) →
  triple (trm_let x t1 t2) H Q

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

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

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

lemma union_monotone_r (s₃ s₁ s₂ : state) :
  s₁ = s₂ →
  s₁ ∪ s₃ = s₂ ∪ s₃

lemma wpgen_app_sound t :
  formula_sound t (wpgen_app t)

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

lemma hstar_hsingle_same_loc p v1 v2 :
  (p ~~> v1) ∗ (p ~~> v2) ==> ⌜False⌝

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

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

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₄

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

lemma himpl_lr_refl :
  XSimp (hla, emp, emp) (hla, emp, emp)

lemma Int.Ico_insert_succ_left (h : i < j) : insert i ⟦i+1, j⟧ = ⟦i, j⟧

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

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

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

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 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 wpgen_let_sound F1 F2of x t1 t2 :
  formula_sound t1 F1 →
  (forall v, formula_sound (subst x v t2) (F2of v)) →
  formula_sound (trm_let x t1 t2) (wpgen_let F1 F2of)

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

lemma triple_conseq t H' Q' H Q :
  triple t H' Q' →
  H ==> H'→
  Q' ===> Q →
  triple t H Q

lemma conseq_cons B (l : Nat) (v : B) (vs : List B) :
  conseq (v :: vs) l = (Finmap.singleton l v) ∪ (conseq vs (l + 1))

lemma haffine_hgc : haffine /GC

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

lemma triple_named_heap t H Q :
  (forall h, H h → triple t (fun h' ↦ h' = h) Q) →
  triple t H Q

lemma himpl_qwand_r A (Q1 Q2 : A → hProp) H :
  Q1 ∗ H ===> Q2 →
  H ==> (Q1 -∗ Q2)

lemma list_nil_length (A : Type) :
  ([] : List A).length = 0

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

lemma mkstruct_conseq F Q1 Q2 :
  Q1 ===> Q2 →
  mkstruct F Q1 ==> mkstruct F Q2

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

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

lemma findIdx_spec (arr : loc) (f : ℤ -> ℝ) (target : ℝ)
  (z n : ℤ) (_ : z <= n) (_ : 0 <= z) (N : ℕ) (_ : n <= N) :
  Set.InjOn f ⟦z, n⟧ ->
  target ∈ f '' ⟦z, n⟧ ->
  { arr(arr, i in N => f i) }
  [ findIdx arr target z n ]
  { v, ⌜ v = f.invFunOn ⟦z, n⟧ target ⌝ ∗ arr(arr, i in N => f i) }

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

lemma union_singleton_eq_insert (h : state) :
  Finmap.singleton p v ∪ h = h.insert p v

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

lemma hseg_cons v p j L :
  hseg (v :: L) p j = hcell v p j ∗ hseg L p (j + 1)

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 xsimp_flip_acc_l_lemma :
  hla = hla' →
  XSimp (hla', emp, emp) (hra, hrg, emp) →
  XSimp (hla, emp, emp) (hra, hrg, emp)

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

lemma hadd_disjoint_hstar [PartialCommMonoid val] (H₁ H₂ : hProp) :
  H₁.Disjoint H₂ ->  H₁ + H₂ = H₁ ∗ H₂

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

lemma xsimp_r_hwand_same :
  XSimp hl (hra, hrg, hrt) ->
  XSimp hl (hra, hrg, (h -∗ h) ∗ hrt)

lemma himpl_htop_r H :
  H ==> ⊤

lemma xsimp_r_hpure :
  XSimp hl (hra, hrg, hrt) -> p ->
  XSimp hl (hra, hrg, hpure p ∗ hrt)

lemma triple_array_set_hcell (p : loc) (i : Int) (v w : val) :
  triple (trm_app val_array_set p i v)
    (hcell w p i)
    (fun _ ↦ hcell v p i)

lemma remove_disjoint_union_l (h1 h2 : state) (x : loc) :
  x ∈ h1 → Finmap.Disjoint h1 h2 →
  Finmap.erase x (h1 ∪ h2) = Finmap.erase x h1 ∪ h2

lemma hstar_pick_1 :
  h1 ∗ h = h1 ∗ h

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

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

lemma triple_mod n1 n2 :
  n2 ≠ 0 →
  triple (trm_app val_mod (val_int n1) (val_int n2))
    emp
    (fun r ↦ ⌜r = val_int (n1 % n2)⌝)

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

lemma wp_of_wpgen :
  H ==> wpgen t Q →
  H ==> wp t Q

lemma xsimpl_lr_qwand_unit (Q1 Q2 : Unit -> hProp) :
  XSimp (emp, emp, (Q1 ( ) ∗ Hla)) (emp, emp, (Q2 ( ) ∗ emp)) ->
  XSimp (Hla, emp, emp) ((Q1 -∗ Q2) ∗ emp, emp, 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 insert_disjoint_l (h1 h2 : state) (x : loc) (v : val) :
  h2.Disjoint (h1.insert x v) →
  x ∉ h2 ∧ h2.Disjoint h1

lemma xsimp_l_hpure :
  (p -> XSimp (hla, hlw, hlt) hr) ->
  XSimp (hla, hlw, ⌜p⌝ ∗ hlt) hr

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

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

lemma hpure_intro_hempty P h :
  emp h → P → ⌜P⌝ h

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

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

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

lemma mem_erase_right (s : state) :
  p ∈ s.erase x → p ∈ s

lemma triple_array_get_hseg L (p : loc) (i j : Int) (_ : 0 <= i - j ∧ i - j < L.length) :
  triple [lang| val_array_get p i]
    (hseg L p j)
    (fun r ↦ ⌜r = L[(i - j).natAbs]!⌝ ∗ hseg L p j)

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

@[simp]
lemma labSet_mem :
  x ∈ ⟪l, s⟫ ↔ x.lab = l ∧ x.val ∈ s

@[simp]
lemma Heap.add_mem (h₁ h₂ : heap) : (l ∈  h₁ +ʰ h₂) = (l ∈ h₁ ∨ l ∈ h₂)

lemma make_list_len (n : Int) (v : val) :
  (make_list n.natAbs v).length = n.natAbs

lemma Int.Ico_succ_right_eq_insert_Ico (h : i ≤ j) : ⟦i, j+1⟧ = insert j ⟦i, j⟧

lemma triple_hexists t A (J : A → hProp) Q :
  (forall x, triple t (J x) Q) →
  triple t (hexists J) Q

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 himpl_frame_r H1 H2 H2' :
  H2 ==> H2' →
  (H1 ∗ H2) ==> (H1 ∗ H2')

lemma himpl_hforall A (J1 J2 : A → hProp) :
  J1 ===> J2 →
  hforall J1 ==> hforall J2

lemma xsimp_l_cancel_qwand α (Q1 Q2 : α -> hProp) x :
  XSimp (emp, Hlw, (Hla ∗ Q2 x ∗ Hlt)) HR ->
  XSimp ((Q1 x ∗ Hla), ((Q1 -∗ Q2) ∗ Hlw), Hlt) HR

lemma xsimpl_lr_hforall :
  (forall x, XSimp (emp, emp, Hla) (emp, emp, J x ∗ emp)) ->
  XSimp (Hla, emp, emp) ((hforall J) ∗ emp, emp, emp)

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

lemma hstar_comm H1 H2 :
  H1 ∗ H2 = H2 ∗ H1

lemma read_state_frame :
  s.Disjoint h2 →
  p ∈ s →
  (fun v' s' ↦ v' = read_state p (s ∪ h2) ∧ s' = s ∪ h2 ) =
  (qstar (fun v' s' ↦ v' = read_state p s ∧ s' = s) (tohProp fun h ↦ h = h2))

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

lemma disjoint_remove_l (h1 h2 : state) (x : loc) :
  Finmap.Disjoint h1 h2 →
  Finmap.Disjoint (Finmap.erase x h1) h2

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

lemma hseg_nil p j :
  hseg [] p j = emp

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

lemma hstar_assoc H1 H2 H3 :
  (H1 ∗ H2) ∗ H3 = H1 ∗ (H2 ∗ H3)

lemma hwandE :
  H1 -∗ H2 = hexists (fun H0 => H0 ∗ hpure ((H1 ∗ H0) ==> H2))

@[simp]
lemma disjoint_add_eq (h₁ h₂ h₃ : heap) :
  (h₁ +ʰ h₂).Disjoint h₃ = (h₁.Disjoint h₃ ∧ h₂.Disjoint h₃)

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

lemma hwand_equiv H0 H1 H2 :
  (H0 ==> H1 -∗ H2) ↔ (H1 ∗ H0 ==> H2)

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

@[simp]
lemma Heap.add_single (v v' : val) [PartialCommMonoid val] :
  (Finmap.singleton p v) +ʰ (Finmap.singleton p v') = (Finmap.singleton p (v + v'))

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

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

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

lemma xref_lemma x v t2 H Q :
  H ==> (h∀ p, (p ~~> v) -∗
    protect (wp (subst x p t2) (fun hv ↦ Q hv ∗ ∃ʰ u, p ~~> u))) →
  H ==> wpgen_ref x (trm_val v) t2 Q

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

lemma wp_sound t :
  formula_sound t (wp t)

lemma hstar_pick_last_2 :
  h1 ∗ h2 = h2 ∗ h1

lemma diff_insert_intersect_id (s₁ s₂ : state) :
  (s₁ \ s₂) ∪ (intersect s₁ s₂) = s₁

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

lemma insert_union (h1 h2 : state) (p : loc) (v : val) :
  p ∉ h1 ∪ h2 →
  (h1 ∪ h2).insert p v = (h1.insert p v) ∪ h2

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

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 xsimp_r_keep :
  XSimp hl (h ∗ hra, hrg, hrt) ->
  XSimp hl (hra, hrg, h ∗ hrt)

lemma insert_eq_union_single (h : state) :
  p ∉ h →
  h.insert p v = h ∪ (Finmap.singleton p v)

lemma hstar_htop_htop :
  ⊤ ∗ ⊤ = ⊤

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

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

lemma triple_neg (b1 : Bool) :
  triple (trm_app val_neg b1)
    emp
    (fun r ↦ ⌜r = val_bool (¬b1)⌝)

lemma sum_disjoint_hstar (H : β -> hProp) (fs : Finset β) [inst : PartialCommMonoid val] :
  (∀ᵉ (i ∈ fs) (j ∈ fs), i ≠ j -> (H i).Disjoint (H j)) ->
  (∑ b in fs, H b) =
  (@Finset.sum β hProp (@instAddCommMonoidHPropOfPartialCommMonoidVal (PartialCommMonoidWRT.toPartialCommMonoid add valid)) fs H)

@[simp]
lemma Heap.add_lookup (h₁ h₂ : heap) (l : loc) :
  (h₁ +ʰ h₂).lookup l = Option.merge (·+·) (h₁.lookup l) (h₂.lookup l)

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 wp_equiv t H Q :
  (H ==> wp t Q) ↔ triple t H Q

lemma hseg_start_eq L p j1 j2 :
  j1 = j2 →
  hseg L p j1 ==> hseg L p j2

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 hpure_intro P :
  P → ⌜P⌝  ∅

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

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

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

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

lemma list_cons_length (A : Type) (x : A) (L : List A) :
  (x :: L).length = 1 + L.length

lemma in_read_union_l (h1 h2 : state) (x : loc) :
  x ∈ h1 → read_state x (h1 ∪ h2) = read_state x h1

lemma harray_focus_read i L p :
  0 <= i ∧ i < L.length →
  harray L p ==>
  hcell L[Int.natAbs i]! p i ∗ (hcell L[Int.natAbs i]! p i -∗ harray L p)

lemma hstar_comm_assoc (H1 H2 H3 : hProp) :
  H1 ∗ H2 ∗ H3 = H2 ∗ H1 ∗ H3

lemma int_index_eq {_ : Inhabited α} (L : List α) (i : Int) :
  L[i.natAbs]! = L[i]!

lemma himpl_trans_r H2 H1 H3:
  H2 ==> H3 → H1 ==> H2 → H1 ==> H3

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

lemma hpure_inv_hempty P h :
  ⌜P⌝ h →
  P ∧ emp h

lemma xwp_lemma_fun v1 v2 x t H Q :
  v1 = val_fun x t →
  H ==> wpgen (subst x v2 t) Q →
  triple (trm_app v1 v2) H Q

lemma xtriple_lemma t H (Q:val → hProp) :
  H ==> mkstruct (wpgen_app t) Q →
  triple t H Q

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

lemma xsimp_lr_exit :
  Hla ==> Hra ∗ Hrg ->
  XSimp (Hla, emp, emp) (Hra, Hrg, emp)

lemma wp_conseq_frame t H (Q1 Q2 : val -> hProp) :
  Q1 ∗ H ===> Q2 →
  (wp t Q1) ∗ H ==> (wp t Q2)

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

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

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

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

lemma eval_conseq s t Q1 Q2 :
  eval s t Q1 →
  Q1 ===> Q2 →
  eval s t Q2

lemma haffine_hempty : haffine emp
</all_available_lemmas>

<local_ctx>
import Lean

import Mathlib.Data.Finmap

import Mathlib.Data.List.Indexes

import SPLean.Common.State

import SPLean.Common.Util

import SPLean.Theories.HProp

import SPLean.Theories.XSimp

import SPLean.Theories.XChange

import SPLean.Theories.SepLog

import SPLean.Theories.WPUtil

open trm val prim

namespace Theories

abbrev formula := (val → hProp) → hProp

section tactics

open Lean Elab Tactic
</local_ctx>

<target_theorem>
lemma xapp_simpl_lemma (F : formula) :
  H ==> F Q ->
  H ==> F Q ∗ (Q -∗ protect Q) :=
</target_theorem>

