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

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

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

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

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

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

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

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

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

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

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

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

open Set
open Mathlib
open SetRel

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

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

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

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

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

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

@[simp]
</local_ctx>

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

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

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

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

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

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

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

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

### Your task:
<all_available_defs>
def harrayFun (f : ℤ -> val) (n : ℕ) (p : loc) : hProp :=
  harray (@List.ofFn _ n (f ·)) p

def XSimp (hl hr : hProp × hProp × hProp) :=
  let (hla, hlw, hlt) := hl
  let (hra, hrg, hrt) := hr
  hla ∗ hlw ∗ hlt ==> hra ∗ hrg ∗ hrt

@[heapSimp]
def protect (x : α) := x

structure XSimpR where
  hla : Term
  hlw : Term
  hlt : Term
  
  hra : Term
  hrg : Term
  hrt : Term

def getGoalStxNN : Lean.Elab.Tactic.TacticM Syntax := do
  delabNoNotations $ <- getMainTarget

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 }

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

partial def hstar_arity (hs : Term) : TacticM Nat :=
  match hs with
  | `(hempty)      => return (0)
  | `(@HStar.hStar hProp hProp $_ $_ $_ $h2) => do
      let n <- hstar_arity h2
      return (1 + n)
  | _           => throwError "cannot get arity"

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

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

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

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 (h hla : Term) (f : optParam (Nat → Bool → TacticM Unit) xsimp_pick) : TacticM Unit := do
  let h  <- Tactic.elabTerm h none
  hstar_search hla fun i h' last? => do
    let h' <- Tactic.elabTerm h' none
    let .true <-
      withAssignableSyntheticOpaque <| isDefEq h' h | throwError "not equal"
    f i last?

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?

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

def hstars_simp_start : TacticM Unit := withMainContext do
  let goal <- getGoalStxNN
  match goal with
  | `(himpl $_ $_) =>
      {| apply hstars_simp_start_lemma ; try srw ?hstar_assoc |}
  | _          => throwError "hstars_simp_start failure"

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"

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

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 xsimp_hwand_hstars_l (hla hs : Term) :=
  hstar_search hs fun i h last? => do
    
    {| apply xsimp_l_hwand_reorder
       · apply $(hstar_pick_lemma i last?) |}
    match h with
    | `(hempty) => {| apply xsimpl_l_cancel_hwand_hstar_hempty |}
    | _ => xsimp_pick_same h hla; {| apply xsimp_l_cancel_hwand_hstar |}

def xsimp_apply_intro_names (lem : Name) (xs : Syntax) : TacticM Unit :=
  let lem := mkIdent lem
  match xs with
  | `(Lean.explicitBinders| $xs:unbracketedExplicitBinders) =>
    match xs with
    | `(unbracketedExplicitBinders| $[$xs]* : $_)
    | `(unbracketedExplicitBinders| $[$xs]*) =>
      for x in xs do
        match x with
        | `(binderIdent| $x:ident) =>
          {| apply $lem; intro $x:ident |}
        | `(binderIdent| $_:hole) =>
          {| apply $lem; unhygienic intro |}
        | _ => throwError "xsimp_l_exists: @ unreachable 2"
    | _ => throwError "xsimp_l_exists: @ unreachable 3"
  | `(Lean.explicitBinders| $[$xs]*) =>
      for x in xs do
        match x with
        | `(Lean.bracketedExplicitBinders| ($x:ident : $_) ) =>
          {| apply $lem; intro $x:ident |}
        | _ => throwError "xsimp_l_exists: @ unreachable 1"
  | _ => throwError "xsimp_l_exists: @ unreachable 3"

partial def xsimp_step_l (xsimp : XSimpR) (cancelWand := true) : TacticM Unit := do
  trace[xsimp] "LHS step"
  match xsimp.hlt, xsimp.hlw with
  | `(@HStar.hStar hProp hProp $_ $_ $h $_), _ =>
    match h with
    | `(hempty)         => {| apply xsimp_l_hempty |}
    | `(hpure $_)        =>
      let n <- fresh `n
      revExt.modifySSR (n :: ·)
      {| apply xsimp_l_hpure; intro $n:ident |}
    | `(@HStar.hStar hProp hProp $_ $_ $h1 $h2)   =>
      withAssignableSyntheticOpaque {| erw [@hstar_assoc $h1 $h2]; simpNums |}
      
       
      xsimp_step_l (<- XSimpRIni) cancelWand
    | `(@hexists $_ fun ($x:ident : $_) => $_) =>
      revExt.modifySSR (x :: ·)
      {| apply xsimp_l_hexists; intro $x:term |}
    | `(@HWand.hWand hProp hProp $_ $_ $_ $_)    => {| apply xsimp_l_acc_wand |}
    | `(@HWand.hWand $_    $_    $_ $_ $_ $_)   => {| apply xsimp_l_acc_wand |}
    | _              => {| apply xsimp_l_acc_other |}
  | `(hempty), `(@HStar.hStar hProp hProp $_ $_ $h1 $_) =>
    match h1 with
    | `(@HWand.hWand hProp hProp $_ $_ $h1 $_) =>
      match h1 with
      | `(hempty) => {| apply xsimp_l_cancel_hwand_hempty |}
      | `(@HStar.hStar hProp hProp $_ $_ $_ $_) => xsimp_hwand_hstars_l xsimp.hla h1
      | _ => try
          let .true := cancelWand | failure
          xsimp_pick_same h1 xsimp.hla
          {| apply xsimp_l_cancel_hwand |}
        catch _ => {| apply xsimp_l_keep_wand |}
    | `(@HWand.hWand $_ $_ $_ $_ $q1 $_) =>
      try
        let .true := cancelWand | failure
        xsimp_pick_applied q1 xsimp.hla
        {| apply xsimp_l_cancel_qwand |}
      catch _ => {| apply xsimp_l_keep_wand |}
    | _ => throwError "xsimp_step_l: @ unreachable"
  | _, _ => throwError "xsimp_step_l: @ unreachable"

def eApplyAndName (lem : Name) (mvarName : Name) : TacticM Unit := withMainContext do
    let gs <- getUnsolvedGoals
    let [g, ex] <- gs[0]!.applyConst lem | throwError "eApplyAndName: should be two goals"
    let nm <- fresh mvarName
    ex.setTag nm.getId
    ex.setUserName nm.getId
    setGoals $ g :: gs.tail

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"

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"

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

partial def dup (n : Nat) : TacticM Unit := do
  match n with
  | 0 => {|skip|}
  | _ => dup (n-1); {| apply dup_lemma|}

def hProp := heap -> Prop

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 : α → β → γ

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

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

def haffine (_ : hProp) :=
  True

def hgc := htop 

def hind : hProp :=
  hexists (fun b ↦ if b then emp else ⊤)

def hadd [PartialCommMonoid val] (H₁ H₂ : hProp) : hProp :=
  fun h => exists h1 h2, H₁ h1 ∧ H₂ h2 ∧ h1 ⊥ʰ h2 ∧ h = h1 +ʰ h2

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

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

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

instance [PartialCommMonoid val] : AddCommMonoid hProp where
  zero := emp
  add  := hadd
  nsmul := nsmulRec
  add_comm  := by admit /- proof elided -/

instance [PartialCommMonoidWRT val add valid] : AddCommMonoidWRT hProp hadd where
  addE := by admit /- proof elided -/

@[simp]
def haddE : (· + ·) = (· ∗ ·) :=

instance (priority := high) : AddCommMonoidWRT hProp hadd where
  addE := by admit /- proof elided -/

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

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

scoped instance : PartialCommMonoid val where
  add := add
  add_assoc := by admit /- proof elided -/

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

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

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

scoped instance : PartialCommMonoid val where
  add := add
  add_assoc := by admit /- proof elided -/

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

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

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

scoped instance : PartialCommMonoid val where
  add := add
  add_assoc := by admit /- proof elided -/

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

def hProp.Disjoint (H₁ H₂ : hProp) :=
  forall h1 h2, H₁ h1 -> H₂ h2 -> h1.Disjoint h2

local macro "LabType" : term => `(ℕ)

structure Labeled (α : Type*) where
  lab : LabType
  val : α

instance [Inhabited α] : Inhabited (Labeled α) := ⟨⟨0, default⟩⟩

def labSet (l : ℕ) (s : Set α) : Set (Labeled α) := { ⟨l, x⟩ | x ∈ s }

abbrev loc := Nat

abbrev var := String

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

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)

class PartialCommMonoidWRT (α : Type) (add' : semiOutParam (α -> α -> α)) (valid' : semiOutParam (α -> Prop)) extends PartialCommMonoid α where
  addE : (· + ·) = add'
  validE : PartialCommMonoid.valid = valid'

private def kmerge1 (l : loc) (v : val) (l₂ : List (Sigma (fun _ : loc => val))) : val :=
  match l₂.dlookup l with
  | .some v' => v + v'
  | _ => v

@[simp]
def kmerge : List (Sigma (fun _ : loc => val)) → List (Sigma (fun _ : loc => val)) → List (Sigma (fun _ : loc => val))
  | [], l₂ => l₂
  | s :: l₁, l₂ =>
    (if s.1 ∈ l₂.keys then
      ⟨s.1, kmerge1 s.1 s.2 l₂⟩ :: kmerge l₁ (l₂.kerase s.1)
    else s :: kmerge l₁ l₂)

noncomputable def AList.merge (h₁ h₂ : AList (fun _ : loc => val)) :  AList (fun _ : loc => val) :=
  ⟨kmerge h₁.entries h₂.entries, by admit /- proof elided -/
    ⟩

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

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

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

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

abbrev valid : val -> Prop := fun _ => False

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

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

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

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

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

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

partial def getList! (xs : Syntax) : (List Syntax) :=
  match xs with
  | `(List.nil) => []
  | `(List.cons $x $xs) => x::getList! xs
  | _ => panic! "getList!: {xs} is not a list"

private def castToProp (e: Lean.Expr) : Lean.Elab.Tactic.TacticM (Option Q(Prop)) := do
  Qq.checkTypeQ (u := Lean.levelOne) e q(Prop)

def getGoalProp : Lean.Elab.Tactic.TacticM Q(Prop) := do
  let goal ← Lean.Elab.Tactic.getMainTarget
  match ← castToProp goal with
  | some qType => return qType
  | none => throwError "goal is not a proposition"

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

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

def delabNoNotations :=
  (withOptions (fun _ =>
    (((KVMap.empty.insert
      `pp.all true).insert
      `pp.universes false).insert
      `pp.deepTerms true).insert
      `pp.fullNames true) $ PrettyPrinter.delab ·)

def getGoalStxAll : Lean.Elab.Tactic.TacticM Syntax := do
  delabAll $ <- getMainTarget

abbrev HintExtState := List Syntax

abbrev RevExtState := List Ident

partial def repeat'' (tac : TacticM Unit) : TacticM Unit := do
  try
    withMainContext tac
  catch _ => return ()
  repeat'' tac

def _root_.Lean.TSyntax.isMVarStx (x : Term) : Bool :=
  match x with
  | `(?$_) => true
  | _ => false

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

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

#hint_xapp triple_add 

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

abbrev triple (t : trm) (H : hProp) (Q : val → hProp) : Prop :=
  forall s, H s → eval s t Q

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

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

abbrev ofhProp (h : val -> hProp) : val -> heap -> Prop := h

def hheader (n : Int) (p : loc) : hProp :=
  p ~~> (val_int n)

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

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

def harray (L : List val) (p : loc) : hProp :=
  hheader (L.length) p ∗ hseg L p 0

def hrange (L : List val) (p : loc) : hProp :=
  match L with
  | []      => emp
  | x :: L' => (p ~~> x) ∗ (hrange L' (p + 1))

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

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

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

def wp (t : trm) (Q : val → hProp) : hProp :=
  fun s ↦ eval s t Q

abbrev formula := (val → hProp) → hProp

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

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

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

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

def wpgen_val (v : val) : formula :=
  fun Q ↦ Q v

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

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

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

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

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 wpgen_if_trm (F0 F1 F2 : formula) : formula :=
  wpgen_let F0 (fun v ↦ mkstruct (wpgen_if v F1 F2))

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

def wpgen_for (v₁ v₂ : trm) (F1 : val -> formula) : formula :=
  mkstruct fun Q =>
    ∃ʰ n₁ n₂ : Int, ⌜v₁ = n₁⌝ ∗ ⌜v₂ = n₂⌝ ∗
      h∀ (S : Int -> formula),
        (let F i :=
          if i < n₂ then
            wpgen_seq (F1 (val_int i)) (S (i + 1))
          else wpgen_val val_unit
        ⌜structural_pred S /\ ∀ i, F i ===> S i⌝ -∗ S n₁ Q )

def wpgen_while (F1 F2 : formula) : formula := mkstruct fun Q =>
  h∀ R : formula,
    let F := wpgen_if_trm F1 (wpgen_seq F2 R) (wpgen_val val_unit)
    ⌜structural R ∧ F ===> R⌝ -∗ R 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))

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)

def wpgen (t : trm) : formula :=
  mkstruct (match t with
  | trm_val v          => wpgen_val v
  | trm_fun x t1       => wpgen_fun (fun v ↦ wp $ subst x v t1)
  | trm_fix f x t1     => wpgen_fix
      (fun vf v => wp $ subst x v $ subst f vf t1)
  | trm_if t0 t1 t2    => wpgen_if t0 (wp t1) (wp t2)
  | trm_seq t1 t2      => wpgen_seq (wp t1) (wp t2)
  | trm_let x t1 t2    => wpgen_let (wp t1) (fun v ↦ wp $ subst x v t2)
  | trm_app _ _        => wpgen_app t
  
  
  | trm_ref x t1 t2    => wpgen_ref x t1 t2
  | trm_alloc x t1 t2  => wpgen_alloc x t1 t2
  | _ => wp t
  )

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

@[simp]
abbrev var_funs (xs:List var) (n:Nat) : Prop :=
     xs.Nodup
  /\ xs.length = n
  /\ xs != []

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

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

@[simp]
def trms_to_vals (ts:List trm) : Option (List val) := do
  match ts with
  | [] => return []
  | (trm_val v) :: ts' => v :: (<- trms_to_vals ts')
  | _ => failure

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

def isubst (E : ctx) (t : trm) : trm :=
  match t with
  | trm_val v =>
      v
  | trm_var x =>
      match lookup x E with
      | none   => t
      | some v => v
  | trm_fun x t1 =>
      trm_fun x (isubst (erase x E) t1)
  | trm_fix f x t1 =>
      trm_fix f x (isubst (erase x (erase f E)) t1)
  | trm_if t0 t1 t2 =>
      trm_if (isubst E t0) (isubst E t1) (isubst E t2)
  | trm_seq t1 t2 =>
      trm_seq (isubst E t1) (isubst E t2)
  | trm_let x t1 t2 =>
      trm_let x (isubst E t1) (isubst (erase x E) t2)
  | trm_ref x t1 t2 =>
      trm_ref x (isubst E t1) (isubst (erase x E) t2)
  | trm_alloc x t1 t2 =>
      trm_alloc x (isubst E t1) (isubst (erase x E) t2)
  | trm_app t1 t2 =>
      trm_app (isubst E t1) (isubst E t2)
  | trm_for x n1 n2 t =>
      trm_for x (isubst E n1) (isubst E n2) (isubst (erase x E) t)
  | trm_while c t =>
      trm_while (isubst E c) (isubst E t)

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

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

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

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

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

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

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

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

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

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

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

def xchangeApply (l : Expr) : MVarId -> MetaM (List MVarId) := fun goal => do
  let g :: gs <- goal.applyConst `xchange_lemma | throwError "Expected a heap entailment"
  let gs' <- g.apply $ <- toHimp l
  return gs ++ gs'

def xcahngeCore (l : Expr) : MVarId -> MetaM (List MVarId) := fun goal => do
  let goal <-
    match_expr <- goal.getType with
    | himpl _ _ => pure goal
    | qimpl _ _ _ => pure (<- goal.intro1P).2
    | _ => throwError "Expected a heap entailment"
  xchangeApply l goal

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

def null : loc := 0

  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 state := Finmap (λ _ : loc ↦ val)

abbrev heap := Heap.heap val

instance : Inhabited val where
  default := val.val_unit

instance : Inhabited trm where
  default := trm.trm_val (val.val_unit)

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

instance : Coe Int val where
  coe z := val.val_int z

instance : OfNat val n where
  ofNat := val.val_int n

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

instance : Coe prim val where
  coe x := val.val_prim x

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

instance : Coe var trm where
  coe x := trm.trm_var x

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

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

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

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

def read_state (p : loc) (h : state) :=
  match Finmap.lookup p h with
  | some v => v
  | none   => default

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

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

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

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

  
  | step_ref : forall s v p,
      ¬ p ∈ s →
      v = trm_val v' →
      step s (trm_app val_ref v) (Finmap.insert p v' s) (val_loc p)
  | step_get : forall s p,
      p ∈ s →
      step s (trm_app val_get (val_loc p)) s (read_state p s)
  | step_set : forall s p v,
      p ∈ s ->
      v = trm_val v' →
      step s (trm_app (trm_app val_set (val_loc p)) v)
        (Finmap.insert p v' s) val_unit
  | step_free : forall s p,
      p ∈ s →
      step s (trm_app val_free (val_loc p)) (Finmap.erase p s) val_unit

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

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

def notstuck (s : state) (t : trm) : Prop :=
  trm_is_val t \/ reducible s 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))

inductive evalbinop : val → val → val → (val->Prop) → Prop where
  | evalbinop_eq : forall v1 v2,
      evalbinop val_eq v1 v2 (fun v => v = val_bool (is_true (v1 = v2)))
  | evalbinop_neq : forall v1 v2,
      evalbinop val_neq v1 v2 (fun v => v = val_bool (is_true (v1 ≠ v2)))
  | evalbinop_add : forall n1 n2,
      evalbinop val_add (val_int n1) (val_int n2)
        (fun v => v = val_int (n1 + n2))
  | evalbinop_addr : forall r₁ r₂,
      evalbinop val_add (val_real r₁) (val_real r₂)
        (fun v => v = val_real (r₁ + r₂))
  | evalbinop_sub : forall n1 n2,
      evalbinop val_sub (val_int n1) (val_int n2)
        (fun v => v = val_int (n1 - n2))
  | evalbinop_subr : forall r1 r2,
      evalbinop val_sub (val_real r1) (val_real r2)
        (fun v => v = val_real (r1 - r2))
  | evalbinop_mul : forall n1 n2,
      evalbinop val_mul (val_int n1) (val_int n2)
        (fun v => v = val_int (n1 * n2))
  | evalbinop_mulr : forall r1 r2,
      evalbinop val_mul (val_real r1) (val_real r2)
        (fun v => v = val_real (r1 * r2))
  | evalbinop_div : forall n1 n2,
      ¬(n2 = 0) →
      evalbinop val_div (val_int n1) (val_int n2)
        (fun v => v = val_int (n1 / n2))
  | evalbinop_divr : forall r1 r2,
      ¬(r2 = 0) →
      evalbinop val_div (val_real r1) (val_real r2)
        (fun v => v = val_real (r1 / r2))
  | evalbinop_mod : forall n1 n2,
      ¬(n2 = 0) →
      evalbinop val_mod (val_int n1) (val_int n2)
        (fun v => v = val_int (n1 % n2))
  | evalbinop_le : forall n1 n2,
      evalbinop val_le (val_int n1) (val_int n2)
        (fun v => v = val_bool (n1 <= n2))
  | evalbinop_ler : forall r1 r2,
      evalbinop val_le (val_real r1) (val_real r2)
        (fun v => v = val_bool (r1 <= r2))
  | evalbinop_lt : forall n1 n2,
      evalbinop val_lt (val_int n1) (val_int n2)
        (fun v => v = val_bool (n1 < n2))
  | evalbinop_ltr : forall r1 r2,
      evalbinop val_lt (val_real r1) (val_real r2)
        (fun v => v = val_bool (r1 < r2))
  | evalbinop_ge : forall n1 n2,
      evalbinop val_ge (val_int n1) (val_int n2)
        (fun v => v = val_bool (n1 >= n2))
  | evalbinop_ger : forall r1 r2,
      evalbinop val_ge (val_real r1) (val_real r2)
        (fun v => v = val_bool (r1 >= r2))
  | evalbinop_gt : forall n1 n2,
      evalbinop val_gt (val_int n1) (val_int n2)
        (fun v => v = val_bool (n1 > n2))
  | evalbinop_gtr : forall r1 r2,
      evalbinop val_gt (val_real r1) (val_real r2)
        (fun v => v = val_bool (r1 > r2))

  
  
  
  
  | evalbinop_ptr_add : forall (p1 : loc) (p2 : Int) n,
      p2 = p1 + n ->
      evalbinop val_ptr_add (val_loc p1) (val_int n)
        (fun v => v = val_loc (Int.natAbs p2))

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

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

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

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

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

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

inductive eval : state → trm → (val → state → Prop) -> Prop where
  | eval_val : forall s v Q,
      Q v s ->
      eval s (trm_val v) Q
  | eval_fun : forall s x t1 Q,
      Q (val_fun x t1) s ->
      eval s (trm_fun x t1) Q
  | eval_fix : forall s f x t1 Q,
      Q (val_fix f x t1) s ->
      eval s (trm_fix f x t1) Q
  | eval_app_arg1 : forall s1 t1 t2 Q1 Q,
      ¬ trm_is_val t1 ->
      eval s1 t1 Q1 ->
      (forall v1 s2, Q1 v1 s2 -> eval s2 (trm_app v1 t2) Q) ->
      eval s1 (trm_app t1 t2) Q
  | eval_app_arg2 : forall s1 (v1 : val) t2 Q1 Q,
      ¬ trm_is_val t2 ->
      eval s1 t2 Q1 ->
      (forall v2 s2, Q1 v2 s2 -> eval s2 (trm_app v1 v2) Q) ->
      eval s1 (trm_app v1 t2) Q
  | eval_app_fun : forall s1 v1 (v2 :val) x t1 Q,
      v1 = val_fun x t1 ->
      eval s1 (subst x v2 t1) Q ->
      eval s1 (trm_app v1 v2) Q
  | eval_app_fix : forall s (v1 v2 : val) f x t1 Q,
      v1 = val_fix f x t1 ->
      eval s (subst x v2 (subst f v1 t1)) Q ->
      eval s (trm_app v1 v2) Q
  | eval_seq : forall Q1 s t1 t2 Q,
      eval s t1 Q1 ->
      (forall v1 s2, Q1 v1 s2 -> eval s2 t2 Q) ->
      eval s (trm_seq t1 t2) Q
  | eval_let : forall Q1 s x t1 t2 Q,
      eval s t1 Q1 ->
      (forall v1 s2, Q1 v1 s2 -> eval s2 (subst x v1 t2) Q) ->
      eval s (trm_let x t1 t2) Q
  | eval_if : forall s (b : Bool) t1 t2 Q,
      eval s (if b then t1 else t2) Q ->
      eval s (trm_if (val_bool b) t1 t2) Q
  | eval_unop : forall op s v1 P Q,
      evalunop op v1 P ->
      purepostin s P Q ->
      eval s (trm_app op v1) Q
  | eval_binop : forall op s (v1 v2 : val) P Q,
      evalbinop op v1 v2 P ->
      purepostin s P Q ->
      eval s (trm_app (trm_app op v1) v2) Q
  | eval_ref : forall s x t1 t2 (Q Q₁ : val → state → Prop),
    eval s t1 Q₁ →
    (∀ v1 s1, Q₁ v1 s1 → ∀ p ∉ s1,
     eval (s1.insert p v1) (subst x p t2) fun v s ↦ Q v (s.erase p)) →
    eval s (trm_ref x t1 t2) Q
  | eval_get : forall s p Q,
      p ∈ s ->
      Q (read_state p s) s ->
      eval s (trm_app val_get (val_loc p)) Q
  | eval_set : forall s p v Q,
      v = trm_val v' ->
      p ∈ s ->
      Q val_unit (Finmap.insert p v' s) ->
      eval s (trm_app (trm_app val_set (val_loc p)) v) Q
  | eval_alloc_arg : forall s Q₁ Q,
    ¬ trm_is_val t1 →
    eval s t1 Q₁ →
    (∀ v' s', Q₁ v' s' → eval s' (trm_alloc x v' t2) Q) →
    eval s (trm_alloc x t1 t2) Q
  | eval_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 →
      eval (sb ∪ sa) (subst x p t2) fun v s ↦ Q v (s \ sb)) →
    eval sa (trm_alloc x n t2) Q
  
  
  
  
  
  
  
  
  | eval_for (n₁ n₂ : Int) (Q : val -> state -> Prop) :
    eval s (if (n₁ < n₂) then
               (trm_seq (subst x n₁ t₁) (trm_for x (val_int (n₁ + 1)) n₂ t₁))
            else val_unit) Q ->
    eval s (trm_for x n₁ n₂ t₁) Q
  | eval_while (t₁ t₂ : trm) (Q : val -> state -> Prop) :
    eval s t₁ Q₁ ->
    (∀ s v, Q₁ v s -> eval s (trm_if v (trm_seq t₂ (trm_while t₁ t₂)) val_unit) Q) ->
    eval s (trm_while t₁ t₂) Q

def eval_like (t1 t2:trm) : Prop :=
  forall s Q, eval s t1 Q -> eval s t2 Q

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

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

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

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

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

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)

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)

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)

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

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

def default_get d := [lang|
  fun p i =>
    let n := val_abs i in
    let l := val_array_length p in
    let b := n < l in
    if b then
      val_array_get p n
    else
      d ]

def default_set : val := [lang|
  fun p i v =>
      let i := val_abs i in
      let L := val_array_length p in
      let b := i < L in
      if b then
        val_array_set p i v
      else
        () ]

def val_array_fill : val := [lang|
  fix f p i n v =>
    let b := n > 0 in
    if b then
      ((val_array_set p) i) v ;
      let m := n - 1 in
      let j := i + 1 in
      f p j m v
    end ]

def val_array_make : val := [lang|
  fun n v =>
    let m := n + 1 in
    alloc m as p in
    (val_set p) n ;
    (((val_array_fill p) 0) n) v ;
    p ]

abbrev default_get' := default_get (val_int 0)

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

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

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

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

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

@[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_val] def unexpandVal : Lean.PrettyPrinter.Unexpander := fun x =>
  match x with
  | `($(_) $x:ident) =>
    match x with
    | `(val_array_get) => `($x)
    | `(val_array_set) => `($x)
    | `(val_unit) => `([lang| ()])
    | `(val_array_make) => `([uop| mkarr])
    | _ => `([lang| $x:ident])
  | `($(_) $x) =>
    match x with
    | `($n:num) => `([lang| $n:num])
    | `($n:ident) => `([lang| $n:ident])
    | `(lang|⟨$n:term⟩) => `([lang| ⟨$n⟩])
    | `([lang| $_]) => return x
    | `([uop| $_]) => return x
    | `([bop| $_]) => return x
    | t => `([lang| ⟨$t⟩])
  | _ => throw ( )

instance : Coe ℝ val := ⟨val_real⟩

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

@[app_unexpander trm_var] def unexpandVar : Lean.PrettyPrinter.Unexpander
  | `($(_) $x:str) =>
    let str := x.getString
    let name := Lean.mkIdent $ Lean.Name.mkSimple str
    `([lang| $name:ident])
  | _ => throw ( )

@[app_unexpander trm_seq] def unexpandSeq : Lean.PrettyPrinter.Unexpander
  | `($(_) [lang| $t1] [lang| $t2]) => `([lang| $t1 ; $t2])
  | _ => throw ( )

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

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

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

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

@[app_unexpander trm_while] def unexpandWhile : Lean.PrettyPrinter.Unexpander
  | `($(_) [lang| $c] [lang| $t]) => do
    `([lang| while $c { $t:lang } ])
  | _ => throw ( )

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

@[app_unexpander trm_fun] def unexpandTFun : 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 ( )

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

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

@[app_unexpander val_fix] def unexpandVFix : 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 ( )

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

@[app_unexpander val_funs] def unexpandVFuns : Lean.PrettyPrinter.Unexpander := fun x =>
  match x with
  | `($(_) [ $xs:str,* ] [lang| $f]) =>
    let xs := xs.getElems.map (Lean.mkIdent $ Lean.Name.mkSimple ·.getString)
    `([lang| fun $xs* => $f])
  | _ => 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 ( )

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

abbrev XAppExtState := RBMap Name Name Name.cmp

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

def getVal (t :Expr) : Expr :=
  let_expr trm_val v := t | t
  getPrim v

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

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

def pickTripleLemma : TacticM Name := do
  let n <- getTripleFun (<- getMainTarget)
  let .some thm := (xappExtension.getState (← getEnv)).find? n | throwError "no triple lemma found"
  return thm

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)

Lean.PrettyPrinter.Unexpander in Init.Prelude

Int in Init.Data.Int.Basic

move in Ssreflect.Basic

Finset.Ico in Mathlib.Order.Interval.Finset.Defs

Set in Mathlib.Data.Set.Defs

Set.InjOn in Mathlib.Data.Set.Operations

scase in Ssreflect.Elim

srw in Ssreflect.Rewrite

Lean.Name.cmp in Lean.Data.Name

Lean.RBMap in Lean.Data.RBMap

Lean.Expr in Lean.Expr

Lean.Name in Init.Prelude

t in Ssreflect.IntroPats

Lean.throwError in Lean.Exception

Bool in Init.Prelude

Finmap in Mathlib.Data.Finmap

Inhabited in Init.Prelude

Coe in Init.Coe

OfNat in Init.Prelude

CoeFun in Init.Coe

Finmap.lookup in Mathlib.Data.Finmap

Finmap.erase in Mathlib.Data.Finmap

Finmap.insert in Mathlib.Data.Finmap

Int.toNat in Init.Data.Int.Basic

sby in Ssreflect.Done

elim in Ssreflect.Elim

Int.natAbs in Init.Data.Int.Basic

List in Init.Prelude

Nat in Init.Prelude

Finmap.singleton in Mathlib.Data.Finmap

sdone in Ssreflect.Done

Finmap.Disjoint in Mathlib.Data.Finmap

L in Archive.Hairer

Not in Init.Prelude

seq in Talk.DemoLeanSSR

Lean.Name.mkSimple in Init.Prelude

Lean.mkIdent in Init.Meta.Defs

Finset in Mathlib.Data.Finset.Defs

sapply in Ssreflect.ApplyIn

Iff in Init.Core

propext in Init.Core

Int.ofNat in Init.Data.Int.Basic

Lean.Meta.MetaM in Lean.Meta.Basic

Lean.Meta.forallTelescope in Lean.Meta.Basic

Lean.Meta.inferType in Lean.Meta.Basic

Lean.trace in Lean.Util.Trace

Eq in Init.Prelude

Lean.Meta.mkAppOptM in Lean.Meta.AppBuilder

Lean.Meta.mkForallFVars in Lean.Meta.Basic

impl in Mathlib.Deprecated.MLList.BestFirst

Lean.MVarId in Lean.Expr

outParam in Init.Prelude

And in Init.Prelude

scase! in Ssreflect.Elim

AddCommMonoid in Mathlib.Algebra.Group.Defs

semiOutParam in Init.Prelude

Zero in Init.Prelude

Add in Init.Prelude

nsmulRec in Init.Data.Zero

HAdd in Init.Prelude

HAdd.hAdd in Init.Prelude

instHAdd in Init.Prelude

Add.add in Init.Prelude

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

OfNat.ofNat in Init.Prelude

Lean.Elab.Tactic.TacticM in Lean.Elab.Tactic.Basic

Lean.Syntax in Init.Prelude

Prod in Init.Prelude

Prod.mk in Init.Prelude

Unit in Init.Prelude

optParam in Init.Prelude

Lean.Meta.isDefEq in Lean.Meta.Basic

Lean.Meta.withAssignableSyntheticOpaque in Lean.Meta.Basic

Lean.Expr.equal in Lean.Expr

Lean.Meta.subst in Lean.Meta.Tactic.Subst

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

Lean.binderIdent in Init.Notation

Lean.bracketedExplicitBinders in Init.NotationExtra

Lean.explicitBinders in Init.NotationExtra

Lean.unbracketedExplicitBinders in Init.NotationExtra

ident in Ssreflect.IntroPats

fresh in Ssreflect.Utils

skip in Talk.DemoLeanSSR

scase_if in Ssreflect.Elim

Option in Init.Prelude

AList in Mathlib.Data.List.AList

AList.erase in Mathlib.Data.List.AList

AList.lookup in Mathlib.Data.List.AList

DecidableEq in Init.Prelude

Sigma in Init.Core

AList.entries in Mathlib.Data.List.AList

List.NodupKeys in Mathlib.Data.List.Sigma

List.keys in Mathlib.Data.List.Sigma

List.map in Init.Prelude

List.zip in Init.Data.List.Basic

List.zipWith in Init.Data.List.Basic

AList.insert in Mathlib.Data.List.AList

List.kerase in Mathlib.Data.List.Sigma

List.kinsert in Mathlib.Data.List.Sigma

AList.keys in Mathlib.Data.List.AList

List.length in Init.Prelude

instOfNat in Init.Data.Int.Basic

instOfNatNat in Init.Prelude

shave in Ssreflect.Have

WellFounded in Init.WF

GetElem in Init.GetElem

List.ofFn in Init.Data.List.OfFn

Function.update in Mathlib.Logic.Function.Basic

List.cons in Init.Prelude

List.nil in Init.Prelude

Lean.levelOne in Lean.Level

Qq.checkTypeQ in Qq.MetaM

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

Lean.KVMap in Lean.Data.KVMap

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

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

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

Lean.pp.deepTerms in Lean.PrettyPrinter.Delaborator.Options

Lean.pp.fullNames in Lean.PrettyPrinter.Delaborator.Options

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

allGoal in Ssreflect.Utils

tryGoal in Ssreflect.Utils

Nonempty in Init.Prelude

Or in Init.Prelude

Disjoint in Mathlib.Order.Disjoint

List.foldl in Init.Prelude

Finmap.foldl in Mathlib.Data.Finmap

Finmap.instSDiff in Mathlib.Data.Finmap

Finmap.sdiff in Mathlib.Data.Finmap

String in Init.Prelude

Option.merge in Init.Data.Option.Basic

AddCommSemigroup in Mathlib.Algebra.Group.Defs

List.Perm in Init.Data.List.Basic

Finmap.liftOn₂ in Mathlib.Data.Finmap

Option.any in Init.Data.Option.Basic

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

Finset.Icc in Mathlib.Order.Interval.Finset.Defs
</all_available_defs>

<all_available_lemmas>
lemma triple_harrayFun_get (p : loc) (i : Int) :
   0 <= i ∧ i < (n : ℕ) →
   triple (trm_app val_array_get p i)
    (harrayFun f n p)
    (fun r ↦ ⌜r = f i⌝ ∗ harrayFun f n p)

lemma triple_harrayFun_set (f : ℤ -> val) (p : loc) (i : Int) (v : val) :
   0 <= i ∧ i < (n : ℕ) →
   triple (trm_app val_array_set p i v)
    (harrayFun f n p)
    (fun _ => harrayFun (Function.update f i v) n p)

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 himpl_of_eq H1 H2 : H1 = H2 -> H1 ==> H2

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

lemma qimpl_refl (Q : α -> hProp) : Q ===> Q

@[simp]
lemma qimpl_refl_resolve (Q : α -> hProp) : (Q ===> Q) = True

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

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

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

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

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

lemma foo''' (n : ℕ) : (@OfNat.ofNat ℕ n _) = n

lemma hstar_flip_0 :
  emp = emp

lemma hstar_flip_1 :
  h1 ∗ emp = h1 ∗ emp

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

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

lemma hstar_flip_4 :
  h1 ∗ h2 ∗ h3 ∗ h4 ∗ emp = h4 ∗ h3 ∗ h2 ∗ h1 ∗ emp

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

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

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

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

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_flip_10 :
  h1 ∗ h2 ∗ h3 ∗ h4 ∗ h5 ∗ h6 ∗ h7 ∗ h8 ∗ h9 ∗ h10 ∗ emp =
  h10 ∗ h9 ∗ h8 ∗ h7 ∗ h6 ∗ h5 ∗ h4 ∗ h3 ∗ h2 ∗ h1 ∗ emp

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

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

lemma hstar_pick_1 :
  h1 ∗ h = h1 ∗ h

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

lemma hstar_pick_3 :
  h1 ∗ h2 ∗ h3 ∗ h = h3 ∗ h1 ∗ h2 ∗ h

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

lemma hstar_pick_5 :
  h1 ∗ h2 ∗ h3 ∗ h4 ∗ h5 ∗ h = h5 ∗ h1 ∗ h2 ∗ h3 ∗ h4 ∗ h

lemma hstar_pick_6 :
  h1 ∗ h2 ∗ h3 ∗ h4 ∗ h5 ∗ h6 ∗ h = h6 ∗ h1 ∗ h2 ∗ h3 ∗ h4 ∗ h5 ∗ h

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

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

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 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 hstar_pick_last_1 :
  h1 = h1

lemma hstar_pick_last_2 :
  h1 ∗ h2 = h2 ∗ h1

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

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

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

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

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

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

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

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_pick_lemma :
  hla2 = hla1 ->
  XSimp (hla1, hlw, hlt) hr ->
  XSimp (hla2, hlw, hlt) hr

lemma xsimp_start_lemma :
  XSimp (emp, emp, h1 ∗ emp) (emp, emp, h2 ∗ emp) ->
  h1 ==> h2

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

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

lemma hstars_simp_cancel_lemma :
  H1 ==> Ha ∗ Ht →
  H ∗ H1 ==> Ha ∗ H ∗ Ht

lemma hstars_simp_pick_lemma :
  H1 = H1' →
  H1' ==> H2 →
  H1 ==> H2

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

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

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

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

lemma xsimp_l_hexists :
  (∀ x, XSimp (hla, hlw, j x ∗ hlt) hr) ->
  XSimp (hla, hlw, (hexists j) ∗ hlt) hr

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

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

lemma xsimp_l_keep_wand :
  XSimp (H ∗ Hla, Hlw, Hlt) HR →
  XSimp (Hla, H ∗ Hlw, Hlt) HR

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

lemma xsimp_l_cancel_hwand_hstar :
  XSimp (Hla, Hlw, (H2 -∗ H3) ∗ Hlt) HR →
  XSimp ((H1 ∗ Hla), (((H1 ∗ H2) -∗ H3) ∗ Hlw), Hlt) HR

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

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 xpull_protect (h : H1 ==> protect H2) : H1 ==> H2

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

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

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

lemma xsimp_r_hexists α (x : α) hl hra hrg hrt j :
  XSimp hl (hra, hrg, j x ∗ hrt) ->
  XSimp hl (hra, hrg, (hexists j) ∗ hrt)

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

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

lemma xsimpl_r_htop_drop :
  XSimp HL (Hra, Hrg, Hrt) ->
  XSimp HL (Hra, Hrg, (⊤ ∗ Hrt))

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

lemma xsimp_lr_cancel_same :
  XSimp (hla, hlw, hlt) (hra, hrg, hrt) ->
  XSimp (h ∗ hla, hlw, hlt) (hra, hrg, h ∗ hrt)

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

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

lemma xsimpl_lr_qwand α (Q1 Q2 : α -> hProp) :
  (forall x, XSimp (emp, emp, (Q1 x ∗ Hla)) (emp, emp, (Q2 x ∗ emp))) ->
  XSimp (Hla, emp, emp) (((Q1 -∗ Q2) ∗ emp), emp, emp)

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 himpl_lr_qwand_unify (Q : α -> hProp):
  XSimp (Hla, emp, emp) ((Q -∗ (Q ∗ Hla)) ∗ emp, emp, emp)

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

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 xsimpl_lr_cancel_htop :
  XSimp (Hla, Hlw, Hlt) (Hra, (⊤ ∗ Hrg), Hrt) ->
  XSimp ((H ∗ Hla), Hlw, Hlt) (Hra, (⊤ ∗ Hrg), Hrt)

lemma xsimpl_lr_cancel_same_hsingle :
  XSimp (Hla, Hlw, Hlt) (Hra, Hrg, Hrt) →
  v1 = v2 →
  XSimp (p ~~> v1 ∗ Hla, Hlw, Hlt) (Hra, Hrg, p ~~> v2 ∗ Hrt)

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

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

lemma val_int_congr :
  n1 = n2 →
  val.val_int n1 = val.val_int n2

lemma val_loc_congr :
  n1 = n2 →
  val.val_loc n1 = val.val_loc n2

lemma dup_lemma (p : Prop) : p -> p -> p

@[ext]
lemma hProp.ext (H1 H2 : hProp) :
  (∀ h, H1 h ↔ H2 h) → H1 = H2

lemma himpl_refl H : H ==> H

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

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

lemma himpl_antisym H1 H2:
  (H1 ==> H2) → (H2 ==> H1) → (H1 = H2)

lemma hprop_op_comm (op : hProp → hProp → hProp) :
  (forall H1 H2, op H1 H2 ==> op H2 H1) →
  (forall H1 H2, op H1 H2 = op H2 H1)

lemma hempty_intro : emp ∅

lemma hempty_inv h :
  emp h → h = ∅

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

lemma hstar_inv (H1 H2 : hProp) h:
  (H1 ∗ H2) h →
  exists h1 h2, H1 h1 ∧ H2 h2 ∧ Finmap.Disjoint h1 h2 ∧ h = h1 ∪ h2

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

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

lemma hstar_hempty_l H :
  emp ∗ H = H

lemma hstar_hempty_r H :
  H ∗ emp = H

lemma hstar_hexists A (J : A → hProp) H :
  (hexists J) ∗ H = hexists (fun x => (J x) ∗ H)

lemma hstar_hforall A (J : A → hProp) H :
  (hforall J) ∗ H ==> hforall (J ∗ H)

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

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

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

lemma himpl_hstar_trans_l H1 H2 H3 H4 :
  H1 ==> H2 →
  H2 ∗ H3 ==> H4 →
  H1 ∗ H3 ==> H4

lemma himpl_hstar_trans_r H1 H2 H3 H4 :
  H1 ==> H2 →
  H3 ∗ H2 ==> H4 →
  H3 ∗ H1 ==> H4

lemma hpure_intro P :
  P → ⌜P⌝  ∅

lemma hpure_inv P h :
  ⌜P⌝ h →
  P ∧ h = ∅

lemma hstar_hpure_l P H h :
  (⌜P⌝ ∗ H) h = (P ∧ H h)

lemma hstar_hpure_r P H h :
  (H ∗ ⌜P⌝) h = (H h ∧ P)

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

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

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

lemma himpl_hempty_hpure P :
  P → emp ==> ⌜P⌝

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

lemma hempty_eq_hpure_true :
  emp = ⌜True⌝

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

lemma hexists_intro A (x : A) (J : A → hProp) h :
  J x h → (hexists J) h

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

lemma himpl_hexists_l A H (J : A → hProp) :
  (forall x, J x ==> H) → (hexists J) ==> H

lemma himpl_hexists_r A (x : A) H (J : A → hProp) :
  (H ==> J x) →
  H ==> (hexists J)

lemma himpl_hexists A (J1 J2 : A → hProp) :
  J1 ===> J2 →
  hexists J1 ==> hexists J2

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

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

lemma himpl_hforall_r A (J : A → hProp) H :
  (forall x, H ==> J x) →
  H ==> (hforall J)

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

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

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

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

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

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

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

lemma hwand_cancel H1 H2 :
  H1 ∗ (H1 -∗ H2) ==> H2

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

lemma hwand_hempty_l H :
  (emp -∗ H) = H

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

lemma hwand_curry H1 H2 H3 :
  (H1 ∗ H2) -∗ H3 ==> H1 -∗ (H2 -∗ H3)

lemma hwand_uncurry H1 H2 H3 :
  H1 -∗ (H2 -∗ H3) ==> (H1 ∗ H2) -∗ H3

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

lemma hwand_inv h1 h2 H1 H2 :
  (H1 -∗ H2) h2 →
  H1 h1 →
  Finmap.Disjoint h1 h2 →
  H2 (h1 ∪ h2)

lemma qwandE α (Q1 Q2 : α → hProp) :
  Q1 -∗ Q2 = hforall (fun x => (Q1 x) -∗ (Q2 x))

lemma qstarE α (Q1 : α → hProp)  (H : hProp):
  Q1 ∗ H = fun x => Q1 x ∗ H

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

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

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

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

lemma htop_intro h :
  ⊤ h

lemma himpl_htop_r H :
  H ==> ⊤

lemma htop_eq :
  ⊤ = ∃ʰ H, H

lemma hstar_htop_htop :
  ⊤ ∗ ⊤ = ⊤

lemma hsingle_intro p v :
  (p ~~> v) (Finmap.singleton p v)

lemma hsingl_inv p v h :
  (p ~~> v) h →
  h = Finmap.singleton p v

lemma disjoint_single_same_inv {α : Type u} {β : α → Type v}
  (p : α) (v1 v2 : β p) :
  Finmap.Disjoint (Finmap.singleton p v1) (Finmap.singleton p v2) →
  False

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

lemma haffine_hany : forall H,
  haffine H

lemma haffine_hempty : haffine emp

lemma haffine_hgc : haffine /GC

lemma himpl_hgc_r : forall H,
  haffine H →
  H ==> /GC

lemma hstar_hgc_hgc : /GC ∗ /GC = /GC

lemma haffine_hpure P :
  haffine ⌜P⌝

lemma haffine_hstar H1 H2 :
  haffine H1 → haffine H2 → haffine (H1 ∗ H2)

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

lemma haffine_hforall A {_ : Inhabited A} (J : A → hProp) :
  (forall x, haffine (J x)) →
  haffine (hforall J)

lemma haffine_hastar_hpure (P : Prop) H :
  (P → haffine H) →
  haffine (⌜P⌝ ∗ H)

lemma hind_any h : ⊤⊤ h

lemma hind_hstar_hempty :
  ⊤⊤ ∗ emp ==> ⊤⊤

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

lemma hadd_single_gen (v v' : val) [PartialCommMonoid val] :
  PartialCommMonoid.valid v ->
  PartialCommMonoid.valid v' ->
  (p ~~> v) + (p ~~> v') = p ~~> (v + v')

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

lemma sum_single (v : β -> Int) (fs : Finset β) :
  (p ~~> 0) + ∑ i in fs, (p ~~> v i) = p ~~> val.val_int (∑ i in fs, v i)

lemma sum_single' (v : β -> Int) (fs : Finset β) (x : ℤ) :
  (p ~~> x) + ∑ i in fs, (p ~~> v i) = p ~~> val.val_int (x + ∑ i in fs, v i)

lemma sum_single'' (v : β -> Int) (fs : Finset β)  :
  fs.Nonempty ->
  ∑ i in fs, (p ~~> v i) = p ~~> val.val_int (∑ i in fs, v i)

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

lemma sum_single (v : β -> Bool) (fs : Finset β) :
  (p ~~> false) + ∑ i in fs, (p ~~> v i) =
  p ~~> val.val_bool (∃ i ∈ fs, v i)

lemma hadd_single (v v' : ℝ) :
  (p ~~> val.val_real v) + (p ~~> val.val_real v') = p ~~> val.val_real (v + v')

lemma sum_single (v : β -> ℝ) (fs : Finset β) :
  (p ~~> val.val_real 0) + ∑ i in fs, (p ~~> val.val_real (v i)) = p ~~> val.val_real (∑ i in fs, v i)

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

lemma hProp.disjoint_hstar (H₁ H₂ H₃ : hProp) :
  (H₃.Disjoint H₁ ∧ H₃.Disjoint H₂) -> H₃.Disjoint (H₁ ∗ H₂)

lemma hProp.disjoint_sum (H : hProp) (fs : Finset β) :
  (∀ i ∈ fs, H.Disjoint (H' i)) ->
    H.Disjoint (fs.sum H')

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)

lemma single_disjoint :
  p ≠ p' ->
  (p ~~> v).Disjoint (p' ~~> v')

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

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

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

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

lemma List.kerase_noterased {α : Type u} {β : α → Type v} [DecidableEq α] (l : List (Sigma β))
  (a a' : α) (hneq : a ≠ a') (b : β a) : ⟨a, b⟩ ∈ l ↔ ⟨a, b⟩ ∈ List.kerase a' l

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

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

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

@[simp]
lemma kmerge_mem (l₁ : List (Sigma (fun _ : loc => val))) : l ∈ (kmerge l₁ l₂).keys ↔ l ∈ l₁.keys ∨ l ∈ l₂.keys

lemma kmerge_mem2 (l₁ l₂ : List (Sigma (fun _ : loc => val))) (nd₁ : l₁.NodupKeys) (nd₂ : l₂.NodupKeys) -- necessary
    (a : Sigma (fun _ : loc => val)) : a ∈ (kmerge l₁ l₂) ↔
      if a.1 ∈ l₁.keys
      then (if a.1 ∈ l₂.keys then Option.merge (· + ·) (l₁.dlookup a.1) (l₂.dlookup a.1) = .some a.2 else a ∈ l₁)
      else a ∈ l₂

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 kmerge_NodupKeys (l₁ l₂ : List (Sigma (fun _ : loc => val))) (nd₁ : l₁.NodupKeys) (nd₂ : l₂.NodupKeys) : (kmerge l₁ l₂).NodupKeys

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

@[simp]
lemma AList.merge_empty_r (h : AList (fun _ : loc => val)) : AList.merge h ∅ = h

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 Heap.add_lookup (h₁ h₂ : heap) (l : loc) :
  (h₁ +ʰ h₂).lookup l = Option.merge (·+·) (h₁.lookup l) (h₂.lookup l)

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

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

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

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

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

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

lemma validInter_comm (h₁ h₂ : heap) :
  h₁ ⊥ʰ h₂ = h₂ ⊥ʰ h₁

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

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

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

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

lemma nonneg_eq_abs (n : Int) :
  0 ≤ n → n.natAbs = n

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

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

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

lemma hseg_one v p j :
  hseg (v :: []) p j = hcell v p j

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

lemma hseg_app L1 L2 p j :
  hseg (L1 ++ L2) p j =
  hseg L1 p j ∗ hseg L2 p (j + L1.length)

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

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

lemma ofnat_plusone (n : Nat) :
  Int.ofNat (n + 1) = (Int.ofNat n) + 1

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

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

lemma nth_middle (A : Type) (IA : Inhabited A) (n : Nat)
  (l1 l2 : List A) (x : A) :
  n = l1.length → (l1 ++ x :: l2)[n]! = x

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

lemma update_app_r {A : Type} (l1 l2 : List A) n v :
  n ≥ l1.length →
  (l1 ++ l2).set n v = l1 ++ l2.set (n - l1.length) v

lemma update_middle (A : Type) (_ : Inhabited A) (n : Nat)
  (l1 l2 : List A) (x v : A) :
  n = l1.length → (l1 ++ x :: l2).set n v = (l1.concat v) ++ l2

lemma hseg_focus_relative (k : Nat) L p j (v : 0 <= k ∧ k < L.length):
  hseg L p j ==>
  hcell L[k]! p (j + k)
    ∗ (h∀ w, hcell w p (j + k) -∗ hseg (L.set k w) p j)

lemma add_Int.natAbs i j :
  0 <= i - j → j + Int.natAbs (i - j) = i

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 harray_focus i L p (v : 0 <= i ∧ i < L.length) :
  0 <= i ∧ i < L.length →
  harray L p ==>
  hcell L[Int.natAbs i]! p i
    ∗ (h∀ w, hcell w p i -∗ harray (L.set (Int.natAbs i) w) p)

lemma set_nth_same (A : Type) (IA : Inhabited A) (n : Nat) (l : List A) :
  n < l.length → l.set n l[n]! = l

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 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 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_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 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 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 hseg_eq_hrange L p (k : Nat) :
  hseg L p k = hrange L (p + 1 + k)

lemma of_nat_nat n :
  OfNat.ofNat n = n

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

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

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 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 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 int_index_eq {_ : Inhabited α} (L : List α) (i : Int) :
  L[i.natAbs]! = L[i]!

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

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

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

lemma set_out_of_bounds (L : List val) i v :
  i < 0 ∨ i ≥ L.length →
  L.set i v = L

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

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

@[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 add_pointer_spec (p q : loc) (n m : Int) (_ : m >= 0) :
  { p ~~> n ∗ q ~~> m }
  [ add_pointer p q ]
  { v, ⌜v = n+m⌝ ∗ ⊤  }

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 findIdx_spec' (arr : loc) (f : Int -> ℝ)
  (z n : ℤ) (_ : z <= n) (_ : 0 <= z) (N : ℕ) (_ : n <= N) :
  Set.InjOn f ⟦z, n⟧ ->
  i ∈ ⟦z, n⟧ ->
  { arr(arr, x in N => f x) }
  [ findIdx arr ⟨f i⟩ z n ]
  { v, ⌜ v = i ⌝ ∗ arr(arr, x in N => f x) }

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

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

lemma conseq_ind (n : ℕ) (v : val) (p : loc) :
  x ∈ conseq (make_list n v) p → x ≥ p

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

lemma eval_sat :
  eval h t Q -> ∃ h v, Q h v

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

lemma evalExact_post :
  eval s t Q → evalExact s t Q' → Q' ===> Q

lemma evalExact_WellAlloc :
  evalExact s t Q →
  Q v s' →
  s'.keys = s.keys

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 evalExact_frame_val (v : val) (s h2 : state) :
  s.Disjoint h2 →
  evalExact (s ∪ h2) t (fun v' s' ↦ v' = v ∧ s' = s ∪ h2) →
  evalExact (s ∪ h2) t
    (qstar (fun v' s' ↦ v' = v ∧ s' = s) (tohProp (fun h ↦ h = h2)))

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

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 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 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 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 evalExact_frame_set :
  s.Disjoint h2 →
  p ∈ s →
  evalExact (s ∪ h2) t
    (fun v'' s' ↦ v'' = val_unit ∧ s' = Finmap.insert p v' (s ∪ h2)) →
  evalExact (s ∪ h2) t
    (qstar (fun v'' s' ↦ v'' = val_unit ∧ s' = Finmap.insert p v' s) (tohProp fun h ↦ h = h2))

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 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 triple_conseq t H' Q' H Q :
  triple t H' Q' →
  H ==> H'→
  Q' ===> Q →
  triple t H Q

lemma triple_frame t H (Q : val -> hProp) H' :
  triple t H Q →
  triple t (H ∗ H') (Q ∗ H')

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

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

lemma triple_hforall t A (x : A) (J : A → hProp) Q:
  triple t (J x) Q →
  triple t (hforall J) Q

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

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

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

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 triple_ramified_frame H1 Q1 t H Q :
  triple t H1 Q1 →
  H ==> H1 ∗ (Q1 -∗ Q) →
  triple t H Q

lemma triple_eval_like t1 t2 H Q :
  eval_like t1 t2 →
  triple t1 H Q →
  triple t2 H Q

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

lemma triple_val_minimal v :
  triple (trm_val v) emp (fun r ↦ ⌜r = v⌝)

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

lemma triple_fix f x t1 H Q :
  H ==> Q (val_fix f x t1) →
  triple (trm_fix f x t1) H Q

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_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 triple_let_val x v1 t2 H Q :
  triple (subst x v1 t2) H Q →
  triple (trm_let x v1 t2) H Q

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 triple_if (b : Bool) t1 t2 H Q :
  triple (if b then t1 else t2) H Q →
  triple (trm_if b t1 t2) H Q

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 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 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 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 read_state_single p v :
  read_state p (Finmap.singleton p v) = v

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

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 triple_unop op v1 (P : val → Prop) :
  evalunop op v1 P →
  triple (trm_app op v1) emp (fun r ↦ ⌜P r⌝)

lemma triple_binop op v1 v2 (P : val → Prop) :
  evalbinop op v1 v2 P →
  triple (trm_app op v1 v2) emp (fun r ↦ ⌜P r⌝)

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 triple_addr r1 r2 :
  triple (trm_app val_add (val_real r1) (val_real r2))
    emp
    (fun r ↦ ⌜r = val_real (r1 + r2)⌝)

lemma triple_div n1 n2 :
  n2 ≠ 0 →
  triple (trm_app val_div (val_int n1) (val_int n2))
    emp
    (fun r ↦ ⌜r = val_int (n1 / n2)⌝)

lemma triple_divr r1 r2 :
  r2 ≠ 0 →
  triple (trm_app val_div (val_real r1) (val_real r2))
    emp
    (fun r ↦ ⌜r = val_real (r1 / r2)⌝)

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

lemma triple_opp n1 :
  triple (trm_app val_opp (val_int n1))
    emp
    (fun r ↦ ⌜r = val_int (-n1)⌝)

lemma triple_oppr r1 :
  triple (trm_app val_opp (val_real r1))
    emp
    (fun r ↦ ⌜r = val_real (-r1)⌝)

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_neq v1 v2 :
  triple (trm_app val_neq (trm_val v1) (trm_val v2))
    emp
    (fun r ↦ ⌜r = is_true (v1 ≠ v2)⌝)

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 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_mul n1 n2 :
  triple (trm_app val_mul (val_int n1) (val_int n2))
    emp
    (fun r ↦ ⌜r = val_int (n1 * n2)⌝)

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 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 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_ler r1 r2 :
  triple (trm_app val_le (val_real r1) (val_real r2))
    emp
    (fun r ↦ ⌜r = val_bool (r1 <= r2)⌝)

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 triple_ltr r1 r2 :
  triple (trm_app val_lt (val_real r1) (val_real r2))
    emp
    (fun r ↦ ⌜r = val_bool (r1 < r2)⌝)

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

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 triple_gt n1 n2 :
  triple (trm_app val_gt (val_int n1) (val_int n2))
    emp
    (fun r ↦ ⌜r = val_bool (n1 > n2)⌝)

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

private lemma abs_nonneg' n :
  n ≥ 0 → Int.natAbs n = n

lemma triple_ptr_add (p : loc) (n : ℤ) :
  p + n >= 0 →
  triple (trm_app val_ptr_add p n)
    emp
    (fun r ↦ ⌜r = val_loc ((p + n).natAbs)⌝)

lemma triple_ptr_add_nat p (f : ℕ) :
  triple (trm_app val_ptr_add (val_loc p) (val_int (Int.ofNat f)))
    emp
    (fun r ↦ ⌜r = val_loc (p + f)⌝)

lemma hheader_eq p n :
  (hheader n p) = (p ~~> (val_int n))

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

lemma hcell_nonneg v p i :
  hcell v p i ==> hcell v p i ∗ ⌜i >= 0⌝

lemma harray_eq p L :
  harray L p = ∃ʰ n, ⌜n = L.length⌝ ∗ hheader n p ∗ hseg L p 0

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

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 hrange_intro L p :
  (hrange L p) (conseq L p)

lemma triple_alloc_arg :
  ¬trm_is_val t1 →
  triple t1 H Q1 →
  (∀ v, triple (trm_alloc x (trm_val v) t2) (Q1 v) Q ) →
  triple (trm_alloc x t1 t2) H Q

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

lemma list_inc_natabs {α : Type} (L : List α) :
  ((L.length : ℤ) + 1).natAbs = (L.length : ℤ).natAbs + 1

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 triple_alloc (n : Int) :
  n ≥ 0 →
  (∀ (p : loc), triple (subst x p t)
    (H ∗ ⌜p ≠ null⌝ ∗ hrange (make_list n.natAbs val_uninit) p)
    (Q ∗ ⌜p ≠ null⌝  ∗ ∃ʰ L, ⌜L.length = n⌝ ∗ hrange L p) ) →
  triple (trm_alloc x n t) H Q

lemma sP'_strongest :
  eval h t Q → sP' h t ===> Q

lemma evalExact_sP' :
  evalExact h t Q → evalExact h t (sP' h t)

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

lemma hforall_impl (J₁ J₂ : α -> hProp) :
  (forall x, J₁ x ==> J₂ x) ->
  hforall J₁ ==> hforall J₂

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

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

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

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

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

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

lemma wp_ramified_trans t H Q1 Q2 :
  H ==> (wp t Q1) ∗ (Q1 -∗ Q2) →
  H ==> (wp t Q2)

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

lemma wp_val v Q :
  Q v ==> wp (trm_val v) Q

lemma wp_fun x t Q :
  Q (val_fun x t) ==> wp (trm_fun x t) Q

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

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_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 wp_seq t1 t2 Q :
  wp t1 (fun _ ↦ wp t2 Q) ==> wp (trm_seq t1 t2) Q

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 wp_if (b : Bool) t1 t2 Q :
  wp (if b then t1 else t2) Q ==> wp (trm_if b t1 t2) Q

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

lemma wp_ref x v t Q :
  (h∀ p, (p ~~> v) -∗ wp (subst x p t) (Q ∗ ∃ʰ v', (p ~~> v'))) ==>
  wp (trm_ref x v t) Q

lemma wp_ref_trm x t1 t2 Q :
  wp t1 (fun v ↦ h∀ p, (p ~~> v) -∗ wp (subst x p t2) (Q ∗ ∃ʰ v', (p ~~> v'))) ==>
  wp (trm_ref x t1 t2) Q

lemma mem_conseq :
  x ∈ conseq L p → p ≤ x

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

lemma wp_alloc x (n : ℤ) t Q :
  n ≥ 0 →
  (h∀ p, (hrange (make_list n.natAbs val_uninit) p) -∗
    wp (subst x p t) (Q ∗ ⌜p ≠ null⌝ ∗ ∃ʰ L, ⌜L.length = n⌝ ∗ hrange L p)) ==>
  wp (trm_alloc x n t) Q

lemma mkstruct_ramified Q1 Q2 F :
  (mkstruct F Q1) ∗ (Q1 -∗ Q2) ==> (mkstruct F Q2)

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

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

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

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

lemma wp_sound t :
  formula_sound t (wp t)

lemma mkstruct_wp t :
  mkstruct (wp t) = wp t

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

lemma wpgen_fail_sound t :
  formula_sound t wpgen_fail

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

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 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 wpgen_seq_sound F1 F2 t1 t2 :
  formula_sound t1 F1 →
  formula_sound t2 F2 →
  formula_sound (trm_seq t1 t2) (wpgen_seq F1 F2)

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 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 wpgen_app_sound t :
  formula_sound t (wpgen_app t)

lemma qimpl_wp_of_triple t F :
  (forall Q, triple t (F Q) Q) →
  F ===> wp t

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_ref_sound x t1 t2 :
  formula_sound (trm_ref x t1 t2) (wpgen_ref x t1 t2)

lemma wpgen_alloc_sound x t1 t2 :
  formula_sound (trm_alloc x t1 t2) (wpgen_alloc x t1 t2)

lemma wpgen_sound t :
  formula_sound t (wpgen t)

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

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

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

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 xstruct_lemma F H Q :
  H ==> F Q →
  H ==> mkstruct F Q

lemma xval_lemma v H Q :
  H ==> Q v →
  H ==> wpgen_val v Q

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

lemma xseq_lemma H F1 F2 Q :
  H ==> F1 (fun _ => F2 Q) →
  H ==> wpgen_seq F1 F2 Q

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

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

lemma xfun_spec_lemma (S:val->Prop) H Q Fof :
  (forall (vf : val),
    (forall (vx : val) H' Q', (H' ==> Fof vx Q') → triple (trm_app vf vx) H' Q') →
    S vf) →
  (forall vf, S vf -> (H ==> Q vf)) →
  H ==> wpgen_fun Fof Q

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 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 xwp_lemma_fix : forall v1 v2 f x t H Q,
  v1 = val_fix f x t ->
  f != x ->
  H ==> wpgen (subst x v2 $ subst f v1 $ 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 xapp_simpl_lemma (F : formula) :
  H ==> F Q ->
  H ==> F Q ∗ (Q -∗ protect Q)

lemma trms_to_vals_some_equiv ts vs : trms_to_vals ts = some vs → ts = vs.map trm_val

lemma List.toAList_perm {α : Type u} {β : α → Type v} [DecidableEq α]
  (es es' : List (Sigma β)) (hnodup : es.NodupKeys) (hp : es.Perm es') :
  es.toAList.entries.Perm es'.toAList.entries

lemma List.mkAlist_snoc_to_cons [DecidableEq α] (xs : List α) (vs : List β)
    (x : α) (v : β) : x ∉ xs → xs.length = vs.length → xs.Nodup →
    ((xs ++ [x]).mkAlist (vs ++ [v])).entries.Perm (((x :: xs).mkAlist (v :: vs)).entries)

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

lemma AList.erase_insert_swap {α : Type u} {β : α → Type v} [DecidableEq α] (a a' : α) (b : β a) (l : AList β) :
  a ≠ a' → (AList.erase a' (AList.insert a b l)).entries.Perm (AList.insert a b (AList.erase a' l)).entries

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

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 AList.erase_empty {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) :
  AList.erase a (∅ : AList β) = ∅

lemma isubst_empty t : isubst ∅ t = t

lemma isubst_perm {al al'} t (hp : al.entries.Perm al'.entries) :
  isubst al t = isubst al' t

lemma isubst_insert (al : ctx) x v t :
  isubst (al.insert x v) t = subst x v (isubst (al.erase x) t)

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

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

lemma trm_apps2 :
  trm_apps (trm_app t1 t2) ts = trm_apps t1 (t2::ts)

lemma trm_apps_app :
  trm_apps t1 (ts ++ ts') = trm_apps (trm_apps t1 ts) ts'

lemma trm_funs_app :
  trm_funs (xs ++ xs') t1 = trm_funs xs (trm_funs xs' t1)

@[trans]
lemma eval_like_trans {t1 t2 t3 : trm} : eval_like t1 t2 → eval_like t2 t3 → eval_like t1 t3

lemma eval_like_trm_fun_val_fun x t : eval_like (trm_fun x t) (val_fun x t)

lemma eval_like_val_fun_trm_fun x t : eval_like (val_fun x t) (trm_fun x t)

lemma eval_like_val_funs_trm_funs xs t : xs ≠ [] → eval_like (val_funs xs t) (trm_funs xs t)

lemma eval_like_trm_funs_val_funs xs t : xs ≠ [] → eval_like (trm_funs xs t) (val_funs xs t)

lemma eval_like_trm_app_left t1 t1' t2 (hsat : ∃ s Q, eval s t1 Q) : eval_like t1 t1' → eval_like (trm_app t1 t2) (trm_app t1' t2)

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 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 val_funs_snoc (xs : List var) (x : var) (h : xs ≠ []) (t : trm) :
  val_funs (xs ++ [x]) t = val_funs xs (trm_fun x t)

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

lemma eval_like_trm_apps_funs_pre (heqv0 : v0 = trm_funs xs t1) :
  eval_like t (trm_apps (val_funs xs t1) ts) ∧  -- NOTE: this part do not require `xs.Nodup`, but anyway
  eval_like (isubst (xs.mkAlist vs) t1) t

lemma eval_like_trm_apps_funs (heqv0 : v0 = trm_funs xs t1) :
  eval_like (isubst (xs.mkAlist vs) t1) (trm_apps (val_funs xs t1) ts)

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

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

lemma xfor_inv_lemma (I : Int -> hProp) (a b : Int)
  (F : val -> formula)
  (Q : val -> hProp) :
  structural_pred F ->
  a <= b ->
    (∃ H',
      H ==> I a ∗ H' ∧
      (∀ i, a <= i ∧ i < b -> I i ==> F i fun _ => I (i + 1)) ∧
      (fun _ => I b ∗ H') ===> Q) ->
    H ==> wpgen_for a b F Q

lemma wp_structural : structural (wp t)

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 structural_imp : structural F ->
  Q ===> Q' -> F Q ==> F Q'

lemma xwhile_inv_basic_lemma (I : Bool -> α -> hProp) R
  -- (F1 F2 : formula)
  :
  WellFounded R ->
  -- structural F1 ->
  -- structural F2 ->
  (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')) ->
  H ==> wp (trm_while F1 F2) (fun _ => H' ∗ ∃ʰ a, I false a)

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 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 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 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 in_read_union_l (h1 h2 : state) (x : loc) :
  x ∈ h1 → read_state x (h1 ∪ h2) = read_state x h1

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 insert_disjoint_l (h1 h2 : state) (x : loc) (v : val) :
  h2.Disjoint (h1.insert x v) →
  x ∉ h2 ∧ h2.Disjoint h1

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 remove_not_in_l (h1 h2 : state) (p : loc) :
  p ∉ h1 →
  (h1 ∪ h2).erase p = h1 ∪ h2.erase p

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

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

lemma erase_disjoint (h1 h2 : state) (p : loc) :
  h1.Disjoint h2 →
  (h1.erase p).Disjoint h2

lemma disjoint_single (h : state) :
  p ∉ h →
  h.Disjoint (Finmap.singleton p v)

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

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

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

lemma insert_delete_id (h : state) (p : loc) :
  p ∉ h →
  h = (h.insert p v).erase p

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 insert_same_eq (h1 h2 : state) :
  p ∉ h1 → p ∉ h2 →
  h1.insert p v = h2.insert p v →
  h1 = h2

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 insert_eq_union_single (h : state) :
  p ∉ h →
  h.insert p v = h ∪ (Finmap.singleton p v)

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

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

lemma keys_eq_mem_r (h1 h2 : state) :
  h1.keys = h2.keys →
  p ∈ h2 →
  p ∈ h1

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

lemma erase_of_non_mem (h : state) :
  p ∉ h →
  h.erase p = h

lemma insert_neq_of_non_mem (h : state) :
  x ∉ h →
  x ≠ p →
  x ∉ h.insert p v

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 union_singleton_eq_erase (h h' : state) :
  h.Disjoint (Finmap.singleton p v) →
  h' = h ∪ Finmap.singleton p v →
  h = h'.erase p

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

lemma disjoint_keys (h₁ h₂ : state) :
  h₁.Disjoint h₂ →
  Disjoint h₁.keys h₂.keys

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 non_mem_diff_helper2 (h₁ : state) (l : @AList loc fun _ ↦ val) :
  p ∈ List.foldl (fun d s ↦ Finmap.erase s.fst d) (Finmap.erase a h₁) l.entries →
  p ∈ List.foldl (fun d s ↦ Finmap.erase s.fst d) h₁ l.entries

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

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

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

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₁

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

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

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

@[simp]
theorem mem_diff_iff (h₁ h₂ : state) :
  p ∈ h₁ \ h₂ ↔ p ∈ h₁ ∧ p ∉ h₂

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

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

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

lemma disjoint_disjoint_diff (h₁ h₂ h₃ : state) :
  h₁.Disjoint h₂ →
  (h₁ \ h₃).Disjoint h₂

lemma lookup_diff (h₁ h₂ : state) :
  p ∉ h₂ →
  (h₁ \ h₂).lookup p = h₁.lookup p

lemma lookup_diff_none (h₁ h₂ : state) :
  p ∈ h₂ →
  (h₁ \ h₂).lookup p = none

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

  lemma diff_disjoint_eq (s₁ s₂ s₃ : state) :
  s₁.Disjoint s₂ →
  s₂.keys = s₃.keys →
  (s₁ ∪ s₂) \ s₃  = s₁

  lemma intersect_comm (s2 d : state) (a₁ : loc) (b₁ : val) (a₂ : loc) (b₂ : val) :
  (fun s x _ ↦ if x ∈ s2 then s else Finmap.erase x s)
      ((fun s x _ ↦ if x ∈ s2 then s else Finmap.erase x s) d a₁ b₁) a₂ b₂ =
    (fun s x _ ↦ if x ∈ s2 then s else Finmap.erase x s)
      ((fun s x _ ↦ if x ∈ s2 then s else Finmap.erase x s) d a₂ b₂) a₁ b₁

lemma insert_eq_union_singleton (s : state) :
  p ∉ s →
  s.insert p v = Finmap.singleton p v ∪ s

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

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

lemma intersect_foldl_mem (s₂ : state) (l₁ l₂ : @AList loc fun _ ↦ val):
  p ∈ List.foldl (fun d s ↦ if s.fst ∈ s₂ then d else Finmap.erase s.fst d)
    l₁.toFinmap l₂.entries →
  p ∈ l₁

@[simp]
lemma intersect_mem_iff (s₁ s₂ : state) :
  p ∈ (intersect s₁ s₂) ↔ p ∈ s₁ ∧ p ∈ s₂

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

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

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

lemma non_mem_union' (s₁ s₂ : state) :
  x ∉ s₁ → x ∉ s₂ → x ∉ s₁ ∪ s₂

lemma union_same_eq_r (s₁ s₂ s₃ : state) :
  s₁.Disjoint s₃ →
  s₂.Disjoint s₃ →
  s₁ ∪ s₃ = s₂ ∪ s₃ →
  s₁ = s₂

lemma disjoint_intersect_r (s₁ s₂ s₃ : state) :
  s₂.Disjoint s₃ →
  (intersect s₁ s₂).Disjoint s₃

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

lemma xchange_lemma :
  H1 ==> H2 ->
  H3 ==> H1 ∗ (H2 -∗ protect H4) ->
  H3 ==> H4

lemma steps_of_step s1 s2 t1 t2 :
  step s1 t1 s2 t2 → steps s1 t1 s2 t2

lemma steps_trans s1 s2 s3 t1 t2 t3 :
  steps s1 t1 s2 t2 →
  steps s2 t2 s3 t3 →
  steps s1 t1 s3 t3

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

lemma evalbinop_unique :
  evalbinop op v1 v2 P → evalbinop op v1 v2 P' → P = P'

lemma conseq_nil B (l : Nat) :
  conseq ([] : List B) l = ∅

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

lemma disjoint_single_conseq B l l' L (v : B) :
  (l < l') ∨ (l ≥ l' + L.length) →
  Finmap.Disjoint (Finmap.singleton l v) (conseq L l')

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

lemma eval_add  s n1 n2 Q :
  Q (val_int (n1 + n2)) s →
  eval s (trm_app (trm_app val_add (val_int n1)) (val_int n2)) Q

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 eval_div s n1 n2 Q :
  n2 ≠ 0 ->
  Q (val_int (n1 / n2)) s ->
  eval s (trm_app (trm_app val_div (val_int n1)) (val_int n2)) 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 eval_app_arg1' s1 t1 t2 Q1 Q :
  eval s1 t1 Q1 ->
  (forall v1 s2, Q1 v1 s2 -> eval s2 (trm_app v1 t2) Q) ->
  eval s1 (trm_app t1 t2) 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 evalExact_post_eq :
  Q = Q' →
  evalExact s t Q →
  evalExact s t Q'

lemma exact_imp_eval :
  evalExact s t Q → eval s t Q
</all_available_lemmas>

<local_ctx>
import Lean

import Mathlib.Data.Finmap

import Mathlib.Algebra.Group.Basic

import Mathlib.Algebra.BigOperators.Group.Finset

import Mathlib.Algebra.BigOperators.Intervals

import Mathlib.Data.Int.Interval

import Mathlib.Order.Interval.Finset.Basic

import Batteries.Data.List.Perm

import Ssreflect.Lang

open Classical

abbrev loc := Nat

abbrev var := String

section Option.merge

variable {α : Type u} (f : α → α → α)

end Option.merge

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

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)

open PartialCommMonoid (valid)

section

variable {val : Type} [PartialCommMonoid val] -- [Inhabited val]

local notation "heap" => Heap.heap val

private def kmerge1 (l : loc) (v : val) (l₂ : List (Sigma (fun _ : loc => val))) : val :=
  match l₂.dlookup l with
  | .some v' => v + v'
  | _ => v

@[simp]
def kmerge : List (Sigma (fun _ : loc => val)) → List (Sigma (fun _ : loc => val)) → List (Sigma (fun _ : loc => val))
  | [], l₂ => l₂
  | s :: l₁, l₂ =>
    (if s.1 ∈ l₂.keys then
      ⟨s.1, kmerge1 s.1 s.2 l₂⟩ :: kmerge l₁ (l₂.kerase s.1)
    else s :: kmerge l₁ l₂)

noncomputable def AList.merge (h₁ h₂ : AList (fun _ : loc => val)) :  AList (fun _ : loc => val) :=
  ⟨kmerge h₁.entries h₂.entries, by admit /- proof elided -/
    ⟩

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

infixr:55 " +ʰ " => Heap.add

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

infixr:55 " ⊥ʰ " => validInter
</local_ctx>

<target_theorem>
lemma validInter_assoc_r (h₁ h₂ h₃ : heap) :
  h₂ ⊥ʰ h₃ -> h₁ ⊥ʰ (h₂ +ʰ h₃) -> (h₁ +ʰ h₂) ⊥ʰ h₃ :=
</target_theorem>

