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>
class Reflexive (R : Relation α) where
  refl {x : α} : R x x

class Commutative (R : Relation α) (f : β → β → α) where
  comm {x y : β} : R (f x y) (f y x)

class Associative (R : Relation α) (f : α → α → α) where
  assoc {x y z : α} : R (f (f x y) z) (f x (f y z))

class NonExpansive [OFE α] [OFE β] (f : α → β) where
  ne : ∀ ⦃n x₁ x₂⦄, x₁ ≡{n}≡ x₂ → f x₁ ≡{n}≡ f x₂

class NonExpansive₂ [OFE α] [OFE β] [OFE γ] (f : α → β → γ) where
  ne : ∀ ⦃n x₁ x₂⦄, x₁ ≡{n}≡ x₂ → ∀ ⦃y₁ y₂⦄, y₁ ≡{n}≡ y₂ → f x₁ y₁ ≡{n}≡ f x₂ y₂

@[ext] structure Hom (α β : Type _) [OFE α] [OFE β] where
  f : α → β
  ne : NonExpansive f

@[ext] structure ContractiveHom (α β : Type _) [OFE α] [OFE β] extends Hom α β where
  [contractive : Contractive f]
  ne := ne_of_contractive f

instance OFE.Option.some.ne [OFE α] : OFE.NonExpansive (some : α → Option α) := ⟨fun _ _ _ => id⟩

instance Option.merge_ne [OFE α] {op : α → α → α} [NonExpansive₂ op] :
    NonExpansive₂ (Option.merge op) where
  ne n x1 x2 Hx y1 y2 Hy := by admit /- proof elided -/

structure Chain (α : Type _) [OFE α] where
  chain : Nat → α
  cauchy : n ≤ i → chain i ≡{n}≡ chain n

def map [OFE α] [OFE β] (f : α -n> β) (c : Chain α) : Chain β where
  chain n := f (c n)
  cauchy h := f.ne.1 (c.cauchy h)

instance OFE.ContractiveHom.fixpoint_ne [COFE α] [Inhabited α] :
    NonExpansive (ContractiveHom.fixpoint (α := α)) where
  ne n f1 f2 H := by admit /- proof elided -/

inductive DFrac (F : Type _) where
 
| own (f : F) : DFrac F
 
| discard : DFrac F
 
| ownDiscard (f : F) : DFrac F

def pcore : DFrac F → Option (DFrac F)
  | own _        => none
  | .discard     => some discard
  | ownDiscard _ => some discard

def op : DFrac F → DFrac F → DFrac F
  | .discard, .discard => discard
  | own f, .discard
  | ownDiscard f, .discard
  | .discard, own f
  | .discard, ownDiscard f => ownDiscard f
  | own f, own f' => own (f + f')
  | own f, ownDiscard f'
  | ownDiscard f, own f'
  | ownDiscard f, ownDiscard f' => ownDiscard (f + f')

class CMRA (α : Type _) extends OFE α where
  pcore : α → Option α
  op : α → α → α
  ValidN : Nat → α → Prop
  Valid : α → Prop

op_ne : NonExpansive (op x)
  pcore_ne : x ≡{n}≡ y → pcore x = some cx →
    ∃ cy, pcore y = some cy ∧ cx ≡{n}≡ cy
  validN_ne : x ≡{n}≡ y → ValidN n x → ValidN n y

valid_iff_validN : Valid x ↔ ∀ n, ValidN n x
  validN_succ : ValidN n.succ x → ValidN n x
  validN_op_left : ValidN n (op x y) → ValidN n x

assoc : op x (op y z) ≡ op (op x y) z
  comm : op x y ≡ op y x

pcore_op_left : pcore x = some cx → op cx x ≡ x
  pcore_idem : pcore x = some cx → pcore cx ≡ some cx
  pcore_op_mono : pcore x = some cx → ∀ y, ∃ cy, pcore (op x y) ≡ some (op cx cy)

extend : ValidN n x → x ≡{n}≡ op y₁ y₂ →
    Σ' z₁ z₂, x ≡ op z₁ z₂ ∧ z₁ ≡{n}≡ y₁ ∧ z₂ ≡{n}≡ y₂

CoeFun in Init.Coe

def op? [CMRA α] (x : α) : Option α → α
  | some y => x • y
  | none => x

abbrev IProp := UPred (IResUR FF)

instance [Fraction α] [CMRA α] {a : Frac α} (Hw : Whole a.1) : Exclusive a where
  exclusive0_l _ Hk := (not_exists.mp Hw.2) _ Hk

@[delab app.Iris.ProofMode.HypMarker]
def delabHypMarker : Delab := do unpackIprop (← withAppArg delab)

instance : CoeFun (Tower F) (fun _ => ∀ k, A F k) := ⟨Tower.val⟩

def cmraValid [CMRA A] (a : A) : UPred M where
  holds n _ := ✓{n} a
  mono hv _ le := CMRA.validN_of_le le hv

Add.add in Init.Prelude

@[simp] def unit : T := empty

instance [URFunctorContractive F] : COFE.OFunctorContractive (UPredOF F) where
  map_contractive.1 {_ x y} HKL _ _ _ Hn _ := by admit /- proof elided -/

class OFE (α : Type _) where
  Equiv : α → α → Prop
  Dist : Nat → α → α → Prop
  dist_eqv : Equivalence (Dist n)
  equiv_dist : Equiv x y ↔ ∀ n, Dist n x y
  dist_lt : Dist n x y → m < n → Dist m x y

let state ← saveState
    if let some goals ← applyMonotonicity goal then
      let mut rule? := some rule

EmptyCollection in Init.Core

Lean.Expr in Lean.Expr

instance [OFE α] {x : Excl α} : CMRA.Exclusive x where exclusive0_l := fun _ a => a

inductive splitSide where
| splitLeft | splitRight

def Frac (α : Type _) := LeibnizO α

instance (priority := default + 20) fromSep_pure (φ ψ : Prop) [BI PROP] :
    FromSep (PROP := PROP) iprop(⌜φ ∧ ψ⌝) iprop(⌜φ⌝) iprop(⌜ψ⌝) where
  from_sep := pure_sep.1

def chain [Store T K V] [OFE V] (k : K) (c : Chain T) : Chain V where
  chain i := get (c i) k
  cauchy Hni := c.cauchy Hni k

instance fromPure_exists (a : Bool) [BI PROP] (Φ : α → PROP) (φ : α → Prop)
    [h : ∀ x, FromPure a iprop(Φ x) (φ x)] : FromPure a iprop(∃ x, Φ x) (∃ x, φ x) where
  from_pure := (affinelyIf_mono pure_exists.2).trans <|
    affinelyIf_exists.1.trans (exists_mono fun x => (h x).1)

Lean.NameSet in Lean.Data.NameMap.Basic

instance {P : PROP} [Plain P] : Plain iprop(|==> P) :=
  ⟨(mono Plain.plain).trans <| (bupd_elim).trans <| BIPlainly.mono intro⟩

instance (priority := default + 10) fromSep_absorbingly [BI PROP] (P Q1 Q2 : PROP)
    [h : FromSep P Q1 Q2] : FromSep iprop(<absorb> P) iprop(<absorb> Q1) iprop(<absorb> Q2) where
  from_sep := absorbingly_sep.2.trans (absorbingly_mono h.1)

instance fromOr_persistently [BI PROP] (P Q1 Q2 : PROP) [h : FromOr P Q1 Q2] :
    FromOr iprop(<pers> P) iprop(<pers> Q1) iprop(<pers> Q2) where
  from_or := persistently_or.2.trans (persistently_mono h.1)

class Heap (T : Type _) (K V : outParam (Type _)) extends Store T K (Option V) where
  empty : T
  hmap (f : K → V → Option V) : T → T
  merge (op : V → V → V) : T → T → T
  get_empty : get empty k = none
  get_hmap : get (hmap f t) k = (get t k).bind (f k)
  get_merge : get (merge op t1 t2) k = Option.merge op (get t1 k) (get t2 k)

class Antisymmetric (R : Relation α) (S : outParam <| Relation α) where
  antisymm {x y : α} : (left : S x y) → (right : S y x) → R x y

protected def pure (p : Prop) : UPred M where
  holds _ _ := p
  mono h _ _ := h

macro:25 P:term:29 " ⊢ " Q:term:25 : term => ``(BIBase.Entails iprop($P) iprop($Q))

Nat.le in Init.Prelude

let out₂ ← mkFreshExprMVarQ prop
      let _ ← synthInstanceQ q(IntoWand $b $b1 $out $out₁' $out₂)
      let pf := q(specialize_wand $pf $pf')
      return { e := e', hyps := hyps', b := b2, out := out₂, pf }
    else
      
      let v ← mkFreshLevelMVar
      let α : Q(Sort v) ← mkFreshExprMVarQ q(Sort v)
      let Φ : Q($α → $prop) ← mkFreshExprMVarQ q($α → $prop)
      let _ ← synthInstanceQ q(IntoForall $out $Φ)
      let x ← elabTermEnsuringTypeQ (u := .succ .zero) arg α
      have out' : Q($prop) := Expr.headBeta q($Φ $x)
      have : $out' =Q $Φ $x := ⟨⟩
      return { e, hyps, b, out := out', pf := q(specialize_forall $pf $x) }

def binderIdentHasName (name : Name) (id : TSyntax ``binderIdent) : Bool :=
  match id with
  | `(binderIdent| $name':ident) => name'.getId == name
  | _ => false

class Idempotent (R : Relation α) (f : α → α → α) where
  idem {x : α} : R (f x x) x

instance fromOr_pure (φ ψ : Prop) [BI PROP] :
    FromOr (PROP := PROP) iprop(⌜φ ∨ ψ⌝) iprop(⌜φ⌝) iprop(⌜ψ⌝) where
  from_or := pure_or.1

instance [OFE α] [OFE β] : CoeFun (α -c> β) (fun _ => α → β) := ⟨fun x => x.toHom.f⟩

instance DiscreteFunOF_URFC {C} (F : C → COFE.OFunctorPre) [HURF : ∀ c, URFunctorContractive (F c)] :
    URFunctorContractive (DiscreteFunOF F) where
  map_contractive.1 h _ _ := URFunctorContractive.map_contractive.distLater_dist h _

instance : COFE (HeapProp Val) := COFE.ofDiscrete Eq equivalence_eq

instance intoPure_pure_or (φ1 φ2 : Prop) [BI PROP] (P1 P2 : PROP)
    [h1 : IntoPure P1 φ1] [h2 : IntoPure P2 φ2] : IntoPure iprop(P1 ∨ P2) (φ1 ∨ φ2) where
  into_pure := (or_mono h1.1 h2.1).trans pure_or.1

instance fromWand_wand [BI PROP] (P1 P2 : PROP) : FromWand iprop(P1 -∗ P2) P1 P2 := ⟨.rfl⟩

class FromOr [BI PROP] (P : PROP) (Q1 Q2 : outParam PROP) where
  from_or : Q1 ∨ Q2 ⊢ P

String in Init.Prelude

class Leibniz (α : Type _) [OFE α] where
  eq_of_eqv {x y : α} : x ≡ y → x = y

absurd in Init.Prelude

inductive StateResult (α : Type _)
  | unknown
  | result (x : α)
  | conflict

| .conjunction [] => iCasesEmptyConj bi hyps Q A' p @k

instance : IsModal (PROP1 := PROP) persistently (.id rfl) .clear where
  spec_intuitionistic _ := persistent
  spec_spatial P := persistently_absorbing P
  emp := persistently_emp_2
  mono := (persistently_mono ·)
  sep := persistently_sep_2

instance : Trans (IncludedN (α := α) n) (IncludedN n) (IncludedN n) where
  trans := incN_trans

def Agree.dist (n : Nat) (x y : Agree α) : Prop :=
  (∀ a ∈ x.car, ∃ b ∈ y.car, a ≡{n}≡ b) ∧
  (∀ b ∈ y.car, ∃ a ∈ x.car, a ≡{n}≡ b)

def getFreshName : TSyntax ``binderIdent → CoreM (Name × Syntax)
  | `(binderIdent| $name:ident) => pure (name.getId, name)
  | stx => return (← mkFreshUserName `x, stx)

def laterMap [OFE A] [OFE B] (f : A -n> B)  : Later A -n> Later B :=

instance (priority := default - 10) intoAbsorbingly_default [BI PROP] (P : PROP) :
    IntoAbsorbingly iprop(<absorb> P) P := ⟨.rfl⟩

Lean.Elab.Tactic.getMainGoal in Lean.Elab.Tactic.Basic

instance fromPure_forall (a : Bool) [BI PROP] (Φ : α → PROP) (φ : α → Prop)
    [h : ∀ x, FromPure a iprop(Φ x) (φ x)] : FromPure a iprop(∀ x, Φ x) (∀ x, φ x) where
  from_pure := (affinelyIf_mono pure_forall_2).trans <|
    affinelyIf_forall_1.trans (forall_mono fun x => (h x).1)

def Disjoint {X : Type _} (S1 S2 : X → Prop) : Prop :=
  ∀ x : X, ¬(S1 x ∧ S2 x)

def Agree.map : CMRA.Hom (Agree α) (Agree β) where
  f := map' f
  ne := inferInstance
  validN {n x} hval := by admit /- proof elided -/

return ⟨← `(irisGoalStx| $hyps.reverse* ⊢ $goal:term)⟩
where
  delabHypotheses {u prop bi s} (hyps : @Hyps u prop bi s)
      (acc : NameMap Nat × Array (TSyntax ``irisHyp)) :
      DelabM (NameMap Nat × Array (TSyntax ``irisHyp)) := do
    match hyps with
    | .emp _ => pure acc
    | .hyp _ name _ p ty _ =>
      let mut (map, acc) := acc
      let (idx, name') ← if let some idx := map.find? name then
        pure (idx + 1, name.appendAfter <| if idx == 0 then "✝" else "✝" ++ idx.toSuperscriptString)
      else
        pure (0, name)
      let stx ← if isTrue p then
        `(irisHyp| □$(mkIdent name') : $(← unpackIprop (← delab ty)))
      else
        `(irisHyp| ∗$(mkIdent name') : $(← unpackIprop (← delab ty)))
      pure (map.insert name idx, acc.push stx)
    | .sep _ _ _ _ lhs rhs => delabHypotheses lhs (← delabHypotheses rhs acc)

instance intoPure_pure_and (φ1 φ2 : Prop) [BI PROP] (P1 P2 : PROP)
    [h1 : IntoPure P1 φ1] [h2 : IntoPure P2 φ2] : IntoPure iprop(P1 ∧ P2) (φ1 ∧ φ2) where
  into_pure := (and_mono h1.1 h2.1).trans pure_and.1

def Agree.map' {α β} (f : α → β) (a : Agree α) : Agree β := ⟨a.car.map f, by admit /- proof elided -/
⟩

def iPrePropO : Type _ := OFunctor.Fix (UPredOF (IResF FF))

def iff     [BIBase PROP] (P Q : PROP) : PROP := iprop((P → Q) ∧ (Q → P))

instance : OFE.NonExpansive (@toAgree α) where
  ne n x₁ x₂ heq := by admit /- proof elided -/

Lean.PrettyPrinter.Unexpander in Init.Prelude

@[simp] instance [NumericFraction T] : LE (Frac T) := ⟨(·.1 ≤ ·.1)⟩

propext in Init.Core

instance : CMRA.Discrete (DFrac F) where
  discrete_valid {x} := by admit /- proof elided -/

instance intoSep_persistently_affine [BI PROP] (P Q1 Q2 : PROP) [h : IntoSep P Q1 Q2]
    [TCOr (Affine Q1) (Absorbing Q2)] [TCOr (Affine Q2) (Absorbing Q1)] :
    IntoSep iprop(<pers> P) iprop(<pers> Q1) iprop(<pers> Q2) where
  into_sep := (persistently_mono <| h.1.trans sep_and).trans <|
    persistently_and.1.trans persistently_and_imp_sep

instance : OFE (Agree α) where
  Equiv x y := ∀ n, Agree.dist n x y
  Dist := Agree.dist
  dist_eqv := Agree.dist_equiv
  equiv_dist := by admit /- proof elided -/

protected def Hom.id [OFE α] : α -n> α where
  f := id
  ne.ne _ _ _ := id

instance (priority := default - 20) fromSep_and [BI PROP] (P1 P2 : PROP)
    [TCOr (Affine P1) (Absorbing P2)] [TCOr (Affine P2) (Absorbing P1)] :
    FromSep iprop(P1 ∧ P2) P1 P2 where
  from_sep := sep_and

instance [OFE α] [OFE.Discrete α] : CMRA.Discrete (Excl α) where
  discrete_valid a := a

partial def iCasesPat.parse (pat : TSyntax `icasesPat) : MacroM iCasesPat := do
  match go ⟨← expandMacros pat⟩ with
  | none => Macro.throwUnsupported
  | some pat => return pat
where
  go : TSyntax `icasesPat → Option iCasesPat
  | `(icasesPat| $name:binderIdent) => some <| .one name
  | `(icasesPat| -) => some <| .clear
  | `(icasesPat| ⟨$[$args],*⟩) => args.mapM goAlts |>.map (.conjunction ·.toList)
  | `(icasesPat| ⌜$pat⌝) => go pat |>.map .pure
  | `(icasesPat| □$pat) => go pat |>.map .intuitionistic
  | `(icasesPat| ∗$pat) => go pat |>.map .spatial
  | `(icasesPat| ($pat)) => goAlts pat
  | _ => none
  goAlts : TSyntax ``icasesPatAlts → Option iCasesPat
  | `(icasesPatAlts| $args|*) =>
    match args.getElems with
    | #[arg] => go arg
    | args   => args.mapM go |>.map (.disjunction ·.toList)
  | _ => none

instance intoExists_absorbingly [BI PROP] (P : PROP) (Φ : α → PROP) [h : IntoExists P Φ] :
    IntoExists iprop(<absorb> P) (fun a => iprop(<absorb> (Φ a))) where
  into_exists := (absorbingly_mono h.1).trans absorbingly_exists.1

class IntoAbsorbingly [BI PROP] (P : outParam PROP) (Q : PROP) where
  into_absorbingly : P ⊢ <absorb> Q

abbrev IsCOFEFun {α : Type _} (β : α → Type _) [OFEFun β] := ∀ x : α, IsCOFE (β x)

class BIBUpdatePlainly (PROP : Type _) [BI PROP] [BIUpdate PROP] [BIPlainly PROP] where
  bupd_plainly {P : PROP} : iprop((|==> ■ P)) ⊢ P

def toAgree (a : α) : Agree α := ⟨[a], by admit /- proof elided -/
⟩

Fin in Init.Prelude

Lean.Expr.headBeta in Lean.Expr

def IrisGoal.toExpr : IrisGoal → Expr
  | { hyps, goal, .. } => q(Entails' $(hyps.tm) $goal)

instance (FF : GFunctors) : GetElem GFunctors (GId FF) COFE.OFunctorPre (fun _ _ => True) where
  getElem _ x _ := (show Array _ from FF)[x.1]

class RepFunStore (T : Type _) (K V : outParam (Type _)) [Store T K V] where
  rep : (K → V) → Prop
  rep_get (t : T) : rep (get t)
  of_fun : { f : K → V // rep f } → T
  get_of_fun : get (of_fun f) = f

instance : OFE.NonExpansive (ownM : M → UPred M) where
  ne _ _ _ H _ _ Hn _ := OFE.Dist.incN (OFE.Dist.le H Hn) .rfl

instance (priority := default + 10) asEmpValidEmpValid2
    [BI PROP] (P : PROP) : AsEmpValid2 (⊢ P) P := AsEmpValid1.to2

instance affinelyIf_persistent (p : Bool) [BI PROP] (P : PROP) [Persistent P] :
    Persistent iprop(<affine>?p P) :=

instance (priority := default + 10) fromSep_affinely [BI PROP] (P Q1 Q2 : PROP)
    [h : FromSep P Q1 Q2] : FromSep iprop(<affine> P) iprop(<affine> Q1) iprop(<affine> Q2) where
  from_sep := affinely_sep_2.trans (affinely_mono h.1)

def findGoalFromTag? (tag : Name) : TacticM <| Option MVarId := do
  (← getUnsolvedGoals).findM? fun goal => do return (← goal.getTag) == tag

instance [Fraction α] : Coe α (Frac α) := ⟨(⟨·⟩)⟩

@[simp] def optionValid : Option α → Prop
  | some x => ✓ x
  | none => True

applyReflexivity (goal : MVarId) : TacticM Unit := do
    try
      discard <| apply' goal ``refl
    catch _ => pure ()

instance : COFE (Fix F) := inferInstanceAs (COFE (Tower F))

instance ucmraDiscreteFunO {α : Type _} (β : α → Type _) [∀ x, UCMRA (β x)] : UCMRA (∀ x, β x) where
  unit _ := unit
  unit_valid _ := unit_valid
  unit_left_id _ := unit_left_id
  pcore_unit _ := core_eqv_self _

@[simp] def pcore (s : T) : Option T := some <| hmap (fun _ => CMRA.pcore) s

instance : BUpd (UPred M) := ⟨bupd⟩

def Set (α : Type _) := α → Prop

class BIFUpdate (PROP MASK : Type _) [BI PROP] extends FUpd PROP MASK where
  [ne {E1 E2 : Set MASK} : OFE.NonExpansive (FUpd.fupd E1 E2 (PROP := PROP))]
  subset {E1 E2 : Set MASK} : Subset E2 E1 → ⊢ |={E1, E2}=> |={E2, E1}=> (emp : PROP)
  except0 {E1 E2 : Set MASK} (P : PROP) : (◇ |={E1, E2}=> P) ⊢ |={E1, E2}=> P
  trans {E1 E2 E3 : Set MASK} (P : PROP) : (|={E1, E2}=> |={E2, E3}=> P) ⊢ |={E1, E3}=> P
  mask_frame_r' {E1 E2 Ef : Set MASK} (P : PROP) :
    Disjoint E1 Ef → (|={E1,E2}=> ⌜Disjoint E2 Ef⌝ → P) ⊢ |={union E1 Ef, union E2 Ef}=> P
  frame_r {E1 E2 : Set MASK} (P R : PROP) :
    iprop((|={E1, E2}=> P) ∗ R ⊢ |={E1, E2}=> P ∗ R)

def setMDataName? (e : Expr) (name : Name) : Expr := match e with
  | Expr.mdata md e =>
    mkMData (md.insert `name name) e
  | e =>
    mkMData (KVMap.empty.insert `name name) e

instance fromPure_absorbingly (a : Bool) [BI PROP] (P : PROP) (φ : Prop)
    [h : FromPure a P φ] : FromPure false iprop(<absorb> P) φ where
  from_pure := absorbingly_affinely_intro_of_persistent.trans <|
    absorbingly_mono <| affinely_affinelyIf.trans h.1

class HasHeapMap (T1 T2 : Type _) (K V1 V2 : outParam (Type _))
   [Store T1 K (Option V1)] [Store T2 K (Option V2)] where
  hhmap (f : K → V1 → Option V2) : T1 → T2
  hhmap_get (f : K → V1 → Option V2) : get (hhmap f t) k = (get t k).bind (f k)

instance fromExists_persistently [BI PROP] (P : PROP) (Φ : α → PROP) [h : FromExists P Φ] :
    FromExists iprop(<pers> P) (fun a => iprop(<pers> (Φ a))) where
  from_exists := persistently_exists.2.trans <| persistently_mono h.1

instance absorbingly_absorbing [BI PROP] (P : PROP) : Absorbing iprop(<absorb> P) where
  absorbing := absorbingly_idem.1

def matchBool (p : Q(Bool)) : ($p =Q true) ⊕' ($p =Q false) :=
  if isTrue p then .inl ⟨⟩ else .inr ⟨⟩

instance asEmpValid1_entails [BI PROP] (P Q : PROP) : AsEmpValid1 (P ⊢ Q) iprop(P -∗ Q) where
  as_emp_valid := ⟨entails_wand, wand_entails⟩

def Fixpoint.chain [OFE α] [Inhabited α] (f : α → α) [Contractive f] : Chain α where
  chain n := Nat.repeat f (n + 1) default
  cauchy {n} := by admit /- proof elided -/

instance pure_persistent (φ : Prop) [BI PROP] : Persistent (PROP := PROP) iprop(⌜φ⌝) where
  persistent := persistently_pure.2

Exists in Init.Core

@[simp] def optionCore (x : Option α) : Option α := x.bind pcore

def Iso.id [OFE α] : Iso α α where
  hom := Hom.id
  inv := Hom.id
  hom_inv := by admit /- proof elided -/

instance {f : F} : CMRA.Cancelable (own f) where
  cancelableN {_} := by admit /- proof elided -/

instance intuitionisticallyIf_affine (p : Bool) [BI PROP] (P : PROP) [Affine P] :
    Affine iprop(□?p P) :=

protected def imp (P Q : UPred M) : UPred M where
  holds n x := ∀ n' x', x ≼ x' → n' ≤ n → ✓{n'} x' → P n' x' → Q n' x'
  mono {n₁ n₂ x₁ x₂} H := fun ⟨m₁, Hle⟩ Hn n x ⟨m₂, Hxle⟩ Hnle Hv HP => by admit /- proof elided -/

instance or_affine [BI PROP] (P Q : PROP) [Affine P] [Affine Q] : Affine iprop(P ∨ Q) where
  affine := or_elim affine affine

class BIPlainlyExists (PROP : Type _) [Iris.BI PROP] [BIPlainly PROP] where
  plainly_sExists_1 {Φ : PROP → Prop} : ■ sExists Φ ⊢ ∃ p, ⌜Φ p⌝ ∧ ■ p

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

partial def handleDependentArrows {prop : Q(Type u)} (bi : Q(BI $prop)) (val : Expr) (goals : IO.Ref (Array MVarId)) : TacticM (Expr × Q(Prop)) := do
  let p : Q(Prop) ← inferType val
  if let .forallE _ binderType _ _ := p then
    let m ← mkFreshExprMVar binderType
    let val' := mkApp val m
    goals.modify (·.push m.mvarId!)
    return ← handleDependentArrows bi val' goals
  else
    return (val, p)

@[simp] def optionOp (x y : Option α) : Option α :=
  match x, y with
  | some x', some y' => some (CMRA.op x' y')
  | none, _ => y
  | _, none => x

partial def SpecPat.parse (pat : Syntax) : MacroM SpecPat := do
  match go ⟨← expandMacros pat⟩ with
  | none => Macro.throwUnsupported
  | some pat => return pat
where
  go : TSyntax `specPat → Option SpecPat
  | `(specPat| $name:binderIdent) => some <| .ident name
  | `(specPat| [$[$names:binderIdent],*]) => some <| .idents names.toList .anonymous
  | `(specPat| [$[$names:binderIdent],*] as $goal:ident) => match goal.raw with
    | .ident _ _ val _ => some <| .idents names.toList val
    | _ => none
  | _ => none

instance : BILaterContractive (UPred M) where
  toContractive := later_contractive

instance intoAnd_sep_affine (p : Bool) [BI PROP] (P Q : PROP)
    [TCOr (Affine P) (Absorbing Q)] [TCOr (Affine Q) (Absorbing P)] :
    IntoAnd p iprop(P ∗ Q) P Q where
  into_and := intuitionisticallyIf_mono sep_and

def addLocalVarInfo (stx : Syntax) (lctx : LocalContext)
    (expr : Expr) (expectedType? : Option Expr) (isBinder := false) : MetaM Unit := do
  Elab.withInfoContext' (pure ())
    (fun _ =>
      return .inl <| .ofTermInfo
        { elaborator := .anonymous, lctx, expr, stx, expectedType?, isBinder })
    (return .ofPartialTermInfo { elaborator := .anonymous, lctx, stx, expectedType? })

abbrev GenMap := α → Option β

instance persistentlyIf_absorbing [BI PROP] (P : PROP) (p : Bool) [Absorbing P] :
    Absorbing iprop(<pers>?p P) :=

instance [OFE α] [OFE β] : OFE (α -c> β) where
  Equiv f g := Equiv f.toHom g.toHom
  Dist n f g := Dist n f.toHom g.toHom
  dist_eqv := {
    refl _ := dist_eqv.refl _
    symm h := dist_eqv.symm h
    trans h1 h2 := dist_eqv.trans h1 h2
  }
  equiv_dist := equiv_dist
  dist_lt := dist_lt

instance : BIPlainly (UPred M) where
  mono H _ _ _ := H _ _ CMRA.unit_validN
  elim_persistently {P} n x Hx := by admit /- proof elided -/

def Included (x y : α) : Prop := ∃ z, y ≡ x • z

def GName := LeibnizO Nat

instance {n : Nat} : Trans (Dist (α := α) n) (IncludedN n) (IncludedN n) where
  trans := incN_of_dist_of_incN

instance : OFE.Leibniz (DFrac F) := ⟨(·)⟩

class LawfulBigOp (f : PROP → PROP → PROP) (unit : outParam PROP)
    (eq : outParam (PROP → PROP → Prop)) where
  refl : eq a a
  symm : eq a b → eq b a
  trans : eq a b → eq b c → eq a c
  comm : eq (f a b) (f b a)
  assoc : eq (f (f a b) c) (f a (f b c))
  left_id : eq (f unit a) a
  congr_l : eq a a' → eq (f a b) (f a' b)

instance OFunctor.constOF_contractive [OFE B] : OFunctorContractive (constOF B) where
  map_contractive.1 := by admit /- proof elided -/

instance fromAssumption_later [BI PROP] (p : Bool) (P Q : PROP)
    [h : FromAssumption p P Q] : FromAssumption p P iprop(▷ Q) where
  from_assumption := h.1.trans later_intro

instance [BI PROP] : Associative (α := PROP) BiEntails and := ⟨and_assoc⟩

instance intoSep_and_persistent_l [BI PROP] (P Q P' Q' : PROP) [Persistent P]
    [inst : AndIntoSep P P' Q Q'] : IntoSep iprop(P ∧ Q) P' Q' where
  into_sep :=
    match P', inst with
    | _, AndIntoSep.affine (h := h) .. =>
      (and_mono_l (affine_affinely _).2).trans <| affinely_and_lr.1.trans <|
        persistent_and_affinely_sep_l_1.trans (sep_mono (affine_affinely _).1 h.1)
    | _, AndIntoSep.affinely .. => persistent_and_affinely_sep_l_1

| .pure arg => do
    let .one n := arg
      | throwError "cannot further destruct a hypothesis after moving it to the Lean context"
    (·.2) <$> ipureCore bi q(iprop($P ∗ $A)) P A Q n q(.rfl) fun _ _ =>
      ((), ·) <$> k hyps

Qq.QuotedDefEq in Qq.Typ

instance unit_CoreId : CoreId (unit : α) where
  core_id := pcore_unit

instance (priority := default - 10) asEmpValidEmpValid1
    [BI PROP] (P : PROP) : AsEmpValid1 (⊢ P) P := ⟨by admit /- proof elided -/
    ⟩

instance : OFE.NonExpansive (plainly : UPred M → UPred M) where
  ne n P1 P2 HP n' y Hn' Hy := by admit /- proof elided -/

instance [t : T] : TCIte (no_index true) T U := TCIte.t (t := t)

instance intoEmpValid_entails [BI PROP] (P Q : PROP) : IntoEmpValid (P ⊢ Q) iprop(P -∗ Q) where
  into_emp_valid := entails_wand

instance intoWand_affinely (p q : Bool) [BI  PROP] (R P Q : PROP) [h : IntoWand p q R P Q] :
    IntoWand p q iprop(<affine> R) iprop(<affine> P) iprop(<affine> Q) where
  into_wand := wand_intro <|
    (sep_congr intuitionisticallyIf_affinely intuitionisticallyIf_affinely).1.trans <|
    affinely_sep_2.trans <| affinely_mono <| wand_elim h.1

instance NextContractive {A : Type} [OFE A] : Contractive (@Later.next A) where
  distLater_dist := id

instance : BIBase (UPred M) where
  Entails      := UPred.Entails
  emp          := UPred.emp
  pure         := UPred.pure
  and          := UPred.and
  or           := UPred.or
  imp          := UPred.imp
  sForall      := UPred.sForall
  sExists      := UPred.sExists
  sep          := UPred.sep
  wand         := UPred.wand
  persistently := UPred.persistently
  later        := UPred.later

class Disjoint (α : Type u) where
  disjoint : α → α → Prop

instance [BI PROP] : Idempotent (α := PROP) BiEntails and := ⟨and_self⟩

instance : TCTrue := TCTrue.t
</all_available_defs>

<all_available_lemmas>
@[simp, refl] theorem Dist.rfl [OFE α] {n} {x : α} : x ≡{n}≡ x

@[symm] theorem Dist.symm [OFE α] {n} {x : α} : x ≡{n}≡ y → y ≡{n}≡ x

theorem Dist.trans [OFE α] {n} {x : α} : x ≡{n}≡ y → y ≡{n}≡ z → x ≡{n}≡ z

theorem equiv_eqv [ofe : OFE α] : Equivalence ofe.Equiv

@[simp, refl] theorem Equiv.rfl [OFE α] {x : α} : x ≡ x

theorem op_right_eqv (x : α) {y z : α} (e : y ≡ z) : x • y ≡ x • z

theorem clear_intuitionistic [BI PROP] {P P' A Q : PROP}
    (h_rem : P ⊣⊢ P' ∗ □ A) (h : P' ⊢ Q) : P ⊢ Q

theorem or_mono_r [BI PROP] {P Q Q' : PROP} (h : Q ⊢ Q') : P ∨ Q ⊢ P ∨ Q'

theorem uPred_ne {P : UPred M} {n} {m₁ m₂} (H : m₁ ≡{n}≡ m₂) : P n m₁ ↔ P n m₂

theorem _root_.Iris.OFE.Dist.incN_r : (b : α) ≡{n}≡ c → (a ≼{n} b ↔ a ≼{n} c)

theorem affinely_and_l [BI PROP] {P Q : PROP} : <affine> P ∧ Q ⊣⊢ <affine> (P ∧ Q)

theorem core_op_dist (x : α) : core x • x ≡{n}≡ x

theorem absorbingly_ne [BI PROP] : OFE.NonExpansive (@absorbingly PROP _)

theorem BIBase.BiEntails.of_eq [BI PROP] {P Q : PROP} (h : P = Q) : P ⊣⊢ Q

theorem wand_multiple [BI PROP] (Q : PROP) :
    ⊢ P1 -∗ □ P2 -∗ P3 -∗ □ (P1 -∗ P2 -∗ P3 -∗ Q) -∗ Q

theorem Agree.op_def {x y : Agree α} : x • y = x.op y

theorem persistently_sep [BI PROP] [BIPositive PROP] {P Q : PROP} :
    <pers> (P ∗ Q) ⊣⊢ <pers> P ∗ <pers> Q

theorem idFree_iff {x₁ x₂ : α} (e : x₁ ≡ x₂) : IdFree x₁ ↔ IdFree x₂

theorem op_commN {x y : α} : x • y ≡{n}≡ y • x

theorem and_clear_spatial_multiple [BI PROP] (Q : PROP) : P1 ∧ P2 ∧ Q ∧ P3 ⊢ Q

theorem total_point_inc_point_iff [IsTotal V] : (point i (T := T) (some x)) ≼ (point i (some y)) ↔ x ≼ y

theorem wand_iff_exists_persistently [BI PROP] [BIAffine PROP] {P Q : PROP} :
    (P -∗ Q) ⊣⊢ ∃ R, R ∗ <pers> (P ∗ R → Q)

theorem wand_congr_l [BI PROP] {P P' Q : PROP} (h : P ⊣⊢ P') : (P -∗ Q) ⊣⊢ (P' -∗ Q)

theorem apply_lean [BI PROP] (P Q : PROP) (H : P ⊢ Q) (HP : ⊢ P) : ⊢ Q

theorem or_congr_r [BI PROP] {P Q Q' : PROP} (h : Q ⊣⊢ Q') : P ∨ Q ⊣⊢ P ∨ Q'

theorem core_idem (x : α) : core (core x) ≡ core x

theorem wand_rfl [BI PROP] {P : PROP} : ⊢ P -∗ P

theorem absorbingly_intro [BI PROP] {P : PROP} : P ⊢ <absorb> P

@[rw_mono_rule]
theorem absorbinglyIf_mono {p : Bool} [BI PROP] {P Q : PROP} (h : P ⊢ Q) :
    <absorb>?p P ⊢ <absorb>?p Q

theorem persistently_absorb_r [BI PROP] {P Q : PROP} : P ∗ <pers> Q ⊢ <pers> Q

theorem specialize_forall [BI PROP] {p : Bool} {A1 A2 P : PROP} {α : Sort _} {Φ : α → PROP}
    [inst : IntoForall P Φ] (h : A1 ⊢ A2 ∗ □?p P) (a : α) : A1 ⊢ A2 ∗ □?p (Φ a)

theorem affinelyIf_exists {p : Bool} [BI PROP] {Ψ : α → PROP} :
    <affine>?p (∃ a, Ψ a) ⊣⊢ ∃ a, <affine>?p (Ψ a)

theorem id_freeN_r {n n'} {x : α} [IdFree x] {y} (v : ✓{n} x) : ¬(x • y ≡{n'}≡ x)

theorem Included.trans : (x : α) ≼ y → y ≼ z → x ≼ z

theorem pure_soundness : iprop(True ⊢ (⌜P⌝ : UPred M)) → P

theorem move_to_pure_disjunction [BI PROP] (Q : PROP) :
    ⊢ <affine> ⌜φ1⌝ ∨ <affine> ⌜φ2⌝ -∗ Q -∗ Q

theorem later_and [BI PROP] {P Q : PROP} : ▷ (P ∧ Q) ⊣⊢ ▷ P ∧ ▷ Q

theorem later_intuitionistically_2 [BI PROP] {P : PROP} : □ ▷ P ⊢ ▷ □ P

theorem Agree.op_commN {x y : Agree α} :  x.op y ≡{n}≡ y.op x

theorem cmraValid_entails [CMRA A] [CMRA B] {a : A} {b : B} (Hv : ∀ n, ✓{n} a → ✓{n} b) :
    (cmraValid a : UPred M) ⊢ cmraValid b

theorem sep_left_all [BI PROP] [BIAffine PROP] (Q : PROP) : ⊢ P -∗ □ Q -∗ R -∗ P ∗ Q

theorem incN_iff (ea : (a : α) ≡{n}≡ a') (eb : (b : α) ≡{n}≡ b') : a ≼{n} b ↔ a' ≼{n} b'

theorem loeb_wand [BI PROP] [BILoeb PROP] {P : PROP} : □ (▷ P -∗ P) ⊢ P

theorem intuitionisticallyIf_affinely {p : Bool} [BI PROP] {P : PROP} :
    □?p <affine> P ⊣⊢ <affine> □?p P

theorem mp [BI PROP] {P Q R : PROP} (h1 : P ⊢ Q → R) (h2 : P ⊢ Q) : P ⊢ R

theorem affinely_and [BI PROP] {P Q : PROP} : <affine> (P ∧ Q) ⊣⊢ <affine> P ∧ <affine> Q

theorem wand_spatial [BI PROP] (Q : PROP) : P ⊢ (P -∗ Q) -∗ Q

theorem affinely_forall_1 [BI PROP] {Φ : α → PROP} : <affine> (∀ a, Φ a) ⊢ ∀ a, <affine> (Φ a)

theorem some_incN_some_iff {a b : α} : some a ≼{n} some b ↔ a ≡{n}≡ b ∨ a ≼{n} b

theorem LimitPreserving.and [COFE α] {P Q : α → Prop}  (HP : LimitPreserving P)
    (HQ : LimitPreserving Q) : LimitPreserving fun a => P a ∧ Q a

theorem LocalUpdate.discrete_fun {β : α → Type _} [∀ x, UCMRA (β x)]
    {f g f' g' : ∀ x, β x} (h : ∀ x : α, (f x, g x) ~l~> (f' x, g' x)) :
    (f, g) ~l~> (f', g')

@[simp] theorem Iso.inv_hom_dist [OFE α] [OFE β] (iso : Iso α β) {n} {x} :
    iso.inv (iso.hom x) ≡{n}≡ x

theorem id_free_r {x : α} [IdFree x] {y} (v : ✓x) : ¬(x • y ≡ x)

theorem later_wand [BI PROP] {P Q : PROP} : ▷ (P -∗ Q) ⊢ ▷ P -∗ ▷ Q

theorem or_elim_spatial [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoOr A A1 A2]
    (h1 : P ∗ A1 ⊢ Q) (h2 : P ∗ A2 ⊢ Q) : P ∗ A ⊢ Q

theorem valid_own_op {dq : DFrac F} {q : F} : ✓ own q • dq → Fractional q

theorem core_op_L {x : α} [IsTotal α] : core x • x = x

@[rw_mono_rule]
theorem wandIff_congr [BI PROP] {P P' Q Q' : PROP} (h1 : P ⊣⊢ Q) (h2 : P' ⊣⊢ Q') :
    (P ∗-∗ P') ⊣⊢ (Q ∗-∗ Q')

theorem _root_.Iris.OFE.Dist.op_l {x y z : α} : x ≡{n}≡ y → x • z ≡{n}≡ y • z

theorem pcore_idem_L {x cx : α} (h : pcore x = some cx) : pcore cx = some cx

theorem validN_fst {n} {x : α × β} (h : ✓{n} x) : ✓{n} x.fst

theorem core_inc_self {x : α} [CoreId x] : core x ≼ x

theorem plainly_and_sep_r_1 : P ∧ ■ Q ⊢ P ∗ ■ Q

theorem rename [BI PROP] (P : PROP) : P ⊢ P

theorem LocalUpdate.option {x y x' y' : α}
    (h : (x, y) ~l~> (x', y')) : (some x, some y) ~l~> (some x', some y')

theorem persistentlyIf_and {p : Bool} [BI PROP] {P Q : PROP} :
    <pers>?p (P ∧ Q) ⊣⊢ <pers>?p P ∧ <pers>?p Q

theorem persistently_and_emp {P : PROP} [BI PROP] : <pers> P ⊣⊢ <pers> (emp ∧ P)

theorem and_assoc [BI PROP] {P Q R : PROP} : (P ∧ Q) ∧ R ⊣⊢ P ∧ Q ∧ R

theorem inc_0_iff_incN [OFE.Discrete α] (n) {x y : α} : x ≼{0} y ↔ x ≼{n} y

theorem intuitionistically_sep_2 [BI PROP] {P Q : PROP} : □ P ∗ □ Q ⊢ □ (P ∗ Q)

theorem entails_impl_true [BI PROP] {P Q : PROP} :
    (P ⊢ Q) ↔ iprop((True : PROP) ⊢ (P → Q))

theorem intuitionisticallyIf_comm {p q : Bool} [BI PROP] {P : PROP} :
    iprop(□?p □?q P) = iprop(□?q □?p P)

@[simp] theorem absorbinglyIf_false [BI PROP] (P : PROP) : iprop(<absorb>?false P) = P

theorem plainly_and_sep_l_1 : ■ P ∧ Q ⊢ ■ P ∗ Q

theorem persistent_and_affinely_sep_l_1 [BI PROP] {P Q : PROP} [Persistent P] :
    P ∧ Q ⊢ <affine> P ∗ Q

theorem simple [BI PROP] : ⊢ (⌜True⌝ : PROP)

theorem LocalUpdate.equiv_right (x : α × α) {y z : α × α} (h : y ≡ z) : x ~l~> y → x ~l~> z

theorem Update.exclusive {x y : α} [CMRA.Exclusive x] (vy : ✓ y) : x ~~> y

theorem validN_op_right {n} {x y : α} : ✓{n} (x • y) → ✓{n} y

theorem affinelyIf_forall_1 {p : Bool} [BI PROP] {Ψ : α → PROP} :
    <affine>?p (∀ a, Ψ a) ⊢ ∀ a, <affine>?p (Ψ a)

@[simp] theorem Hom.comp_apply [OFE α] [OFE β] [OFE γ] {g : β -n> γ} {f : α -n> β} {x} :
    (g.comp f) x = g (f x)

theorem op_core (x : α) : x • core x ≡ x

theorem absorbingly_affinely_intro_of_persistent [BI PROP] {P : PROP} [Persistent P] :
    P ⊢ <absorb> <affine> P

theorem sep_mono_r [BI PROP] {P Q Q' : PROP} (h : Q ⊢ Q') : P ∗ Q ⊢ P ∗ Q'

@[simp] theorem distLater_zero [OFE α] {x y : α} : DistLater 0 x y

theorem Agree.op_assoc {x y z : Agree α} :  x.op (y.op z) ≡ (x.op y).op z

theorem not_valid_of_exclN_inc {n} {x : α} [Exclusive x] {y} : x ≼{n} y → ¬✓{n} y

theorem affinely_or [BI PROP] {P Q : PROP} : <affine> (P ∨ Q) ⊣⊢ <affine> P ∨ <affine> Q

theorem move_twice [BI PROP] (P : PROP) : □ P ⊢ □ Q -∗ Q

theorem pure_imp_2 [BI PROP] {φ1 φ2 : Prop} : ⌜φ1 → φ2⌝ ⊢ (⌜φ1⌝ → ⌜φ2⌝ : PROP)

theorem or_self [BI PROP] {P : PROP} : P ∨ P ⊣⊢ P

theorem and_destruct_spatial_right [BI PROP] (Q : PROP) : P ∧ Q ⊢ Q

theorem bigOp_sep_cons [BI PROP] {P : PROP} {Ps : List PROP} :
    [∗] (P :: Ps) ⊣⊢ P ∗ [∗] Ps

theorem plainly_impl_wand : ■ (P → Q) ⊣⊢ ■ (P -∗ Q)

theorem validN_of_le {n n'} {x : α} : n' ≤ n → ✓{n} x → ✓{n'} x

theorem Included.incN {n} {x y : α} : x ≼ y → x ≼{n} y

theorem _root_.Iris.OFE.Equiv.op_l {x y z : α} : x ≡ y → x • z ≡ y • z

@[rw_mono_rule]
theorem and_congr [BI PROP] {P P' Q Q' : PROP} (h1 : P ⊣⊢ Q) (h2 : P' ⊣⊢ Q') : P ∧ P' ⊣⊢ Q ∧ Q'

theorem persistently_elim [BI PROP] {P : PROP} [Absorbing P] : <pers> P ⊢ P

theorem from_and_intro [BI PROP] {P Q A1 A2 : PROP} [inst : FromAnd Q A1 A2]
    (h1 : P ⊢ A1) (h2 : P ⊢ A2) : P ⊢ Q

theorem persistently_emp [BI PROP] : <pers> (emp : PROP) ⊣⊢ True

theorem UpdateP.discrete [CMRA.Discrete α] :
    x ~~>: P ↔ ∀ (mz : Option α), ✓ (x •? mz) → ∃ y, P y ∧ ✓ (y •? mz)

theorem persistently_and_iff_sep [BI PROP] [BIAffine PROP] {P Q : PROP} :
    <pers> P ∧ Q ⊣⊢ <pers> P ∗ Q

theorem compl_map [COFE α] [COFE β] (f : α -n> β) (c : Chain α) :
    compl (Chain.map f c) ≡ f (compl c)

theorem none_of_excl_valid_op {n} {x : α} [Exclusive x] {my} : ✓{n} (x •? my) → my = none

theorem pcore_op_left_L {x cx : α} (h : pcore x = some cx) : cx • x = x

theorem Exclusive.of_eqv {x₁ x₂ : α} (e : x₁ ≡ x₂) (h : Exclusive x₁) : Exclusive x₂

theorem persistently_forall [BI PROP] [h : BIPersistentlyForall PROP] {Ψ : α → PROP} :
    <pers> (∀ a, Ψ a) ⊣⊢ ∀ a, <pers> (Ψ a)

theorem core_point_equiv {i : K} {x : V} {cx} (Hpcore : pcore x = some cx) :
    Equiv (T := T) (core <| point i (some x)) (point i (some cx))

theorem affine_affinely [BI PROP] (P : PROP) [Affine P] : <affine> P ⊣⊢ P

theorem move_multiple [BI PROP] (P : PROP) : □ P ⊢ □ Q -∗ Q

theorem Equiv.dist [OFE α] {x : α} : x ≡ y → x ≡{n}≡ y

theorem ownM_unit P : P ⊢ □ ownM (CMRA.unit : M)

theorem and_elim_r_intuitionistic [BI PROP] {P A Q A1 A2 : PROP} [IntoAnd true A A1 A2]
    (h : P ∗ □ A2 ⊢ Q) : P ∗ □ A ⊢ Q

theorem affinely_sep_persistently [BI PROP] {P : PROP} : <affine> P ∗ <pers> P ⊣⊢ <pers> P

theorem intuitionistically_emp [BI PROP] : □ emp ⊣⊢ (emp : PROP)

@[refl] theorem Included.rfl {x : α} : x ≼ x

theorem absorbingly_of_persistently [BI PROP] {P : PROP} : <pers> P ⊢ <absorb> P

theorem intuitionistically_and [BI PROP] {P Q : PROP} : □ (P ∧ Q) ⊣⊢ □ P ∧ □ Q

theorem persistently_exists [BI PROP] {Ψ : α → PROP} : <pers> (∃ a, Ψ a) ⊣⊢ ∃ a, <pers> (Ψ a)

theorem intuitionistically_or [BI PROP] {P Q : PROP} : □ (P ∨ Q) ⊣⊢ □ P ∨ □ Q

theorem false [BI PROP] (P : PROP) : □ P ⊢ False -∗ Q

theorem core_op_mono (x y : α) : core x ≼ core (x • y)

@[rw_mono_rule]
theorem affinely_mono [BI PROP] {P Q : PROP} : (P ⊢ Q) → <affine> P ⊢ <affine> Q

theorem entails_wand [BI PROP] {P Q : PROP} (h : P ⊢ Q) : ⊢ P -∗ Q

theorem multiple_patterns [BI PROP] (Q : PROP) : ⊢ □ (P1 ∧ P2) -∗ Q ∨ Q -∗ Q

@[simp] theorem absorbinglyIf_true [BI PROP] (P : PROP) :
    iprop(<absorb>?true P) = iprop(<absorb> P)

theorem affinely_sep [BI PROP] [BIPositive PROP] {P Q : PROP} :
    <affine> (P ∗ Q) ⊣⊢ <affine> P ∗ <affine> Q

theorem false_elim_intuitionistic [BI PROP] {P Q : PROP} : P ∗ □ False ⊢ Q

theorem absorbingly_intuitionistically [BI PROP] {P : PROP} : <absorb> □ P ⊣⊢ <pers> P

theorem imp_mono_l [BI PROP] {P P' Q : PROP} (h : P' ⊢ P) : (P → Q) ⊢ (P' → Q)

theorem lean_pure [BI PROP] (Q : PROP) : <affine> ⌜⊢ Q⌝ ⊢ Q

theorem unit_left_id_dist {n} (x : α) : unit • x ≡{n}≡ x

theorem persistentlyIf_or {p : Bool} [BI PROP] {P Q : PROP} :
    <pers>?p (P ∨ Q) ⊣⊢ <pers>?p P ∨ <pers>?p Q

theorem plainly_pure {φ} : ■ ⌜φ⌝ ⊣⊢ (⌜φ⌝ : PROP)

theorem Agree.op_commN {x y : Agree α} :  x.op y ≡{n}≡ y.op x

theorem false_intro [BI PROP] (Q : PROP) : False ⊢ Q

theorem cancelable_iff {x₁ x₂ : α} (e : x₁ ≡ x₂) : Cancelable x₁ ↔ Cancelable x₂

theorem later_intuitionistically [BI PROP] [BIAffine PROP] {P : PROP} : □ ▷ P ⊣⊢ ▷ □ P

theorem f [BI PROP] : ⊢ (∃ (_x : Nat), True ∨ False : PROP)

theorem Update.equiv_right {x y z : α} (e : y ≡ z) (u : x ~~> y) : x ~~> z

theorem absorbingly_sep [BI PROP] {P Q : PROP} : <absorb> (P ∗ Q) ⊣⊢ <absorb> P ∗ <absorb> Q

theorem intuitionistically_plainly_elim : □ ■ P ⊢ □ P

theorem plainly_intro' (H : ■ P ⊢ Q) : ■ P ⊢ ■ Q

theorem persistently_sep_2 [BI PROP] {P Q : PROP} : <pers> P ∗ <pers> Q ⊢ <pers> (P ∗ Q)

theorem split_sr [BI PROP] {P Q P1 P2 : PROP} (h : P ⊣⊢ P1 ∗ P2) : P ∗ Q ⊣⊢ P1 ∗ (P2 ∗ Q)

@[simp] theorem const_apply [OFE α] {a : α} {n} : const a n = a

theorem split_sl [BI PROP] {P Q P1 P2 : PROP} (h : P ⊣⊢ P1 ∗ P2) : P ∗ Q ⊣⊢ (P1 ∗ Q) ∗ P2

theorem fixpoint_unique [COFE α] [Inhabited α] {f : α -c> α} {x : α} (H : x ≡ f x) :
    x ≡ fixpoint f

@[simp] theorem discrete_cofe_compl [COFE α] [OFE.Discrete α] (c : Chain α) : compl c ≡ c 0

theorem chain_get [Store T K V] [OFE V] (k : K) (c : Chain T) :
    (chain k c) i = get (c i) k

theorem move_to_intuitionistic_and_back_conjunction [BI PROP] (Q : PROP) : ⊢ □ (P ∧ Q) -∗ Q

theorem intuitionisticallyIf_elim {p : Bool} [BI PROP] {P : PROP} : □?p P ⊢ P

theorem replaces_r [BI PROP] {K P Q Q' : PROP} (h : Replaces K Q Q') :
    Replaces K iprop(P ∗ Q) iprop(P ∗ Q')

theorem Fractional.of_add_right {a a' : α} (H : Fractional (a + a')) : Fractional a'

theorem false_or [BI PROP] {P : PROP} : False ∨ P ⊣⊢ P

theorem conv_compl' [COFE α] {c : Chain α} {n i} (h : n ≤ i) : compl c ≡{n}≡ c i

@[rw_mono_rule]
theorem affinelyIf_congr {p : Bool} [BI PROP] {P Q : PROP} (h : P ⊣⊢ Q) :
    <affine>?p P ⊣⊢ <affine>?p Q

@[simp]
theorem Agree.toAgree_included_L [OFE.Leibniz α] {a b : α} :
    toAgree a ≼ toAgree b ↔ a = b

@[simp] theorem Iso.hom_inv_dist [OFE α] [OFE β] (iso : Iso α β) {n} {x} :
    iso.hom (iso.inv x) ≡{n}≡ x

theorem persistently_intro [BI PROP] {P : PROP} [Persistent P] : P ⊢ <pers> P

theorem later_congr [BI PROP] {P Q : PROP} (h : P ⊣⊢ Q) : ▷ P ⊣⊢ ▷ Q

theorem persistently_imp_1 [BI PROP] {P Q : PROP} : <pers> (P → Q) ⊢ (<pers> P → <pers> Q)

theorem forall_multiple [BI PROP] (Q : Nat → Nat → PROP) : ⊢ (∀ x, □ (∀ y, Q x y)) -∗ □ Q x y

theorem _root_.Iris.OFE.Equiv.core : ∀ {x₁ x₂ : α}, x₁ ≡ x₂ → core x₁ ≡ core x₂

theorem affinelyIf_idem {p : Bool} [BI PROP] [BIPositive PROP] {P : PROP} :
    <affine>?p <affine>?p P ⊣⊢ <affine>?p P

theorem plainly_and : ■ (P ∧ Q) ⊣⊢ ■ P ∧ ■ Q

theorem left [BI PROP] (P : PROP) : P ⊢ P ∨ Q

theorem _root_.Iris.OFE.Equiv.inc : (a : α) ≡ a' → b ≡ b' → (a ≼ b ↔ a' ≼ b')

theorem or_mono_l [BI PROP] {P P' Q : PROP} (h : P ⊢ P') : P ∨ Q ⊢ P' ∨ Q

theorem op_core_L {x : α} [IsTotal α] : x • core x = x

theorem wand_intuitionistic [BI PROP] (Q : PROP) : □ P ⊢ □ (P -∗ Q) -∗ □ Q

theorem or_symm [BI PROP] {P Q : PROP} : P ∨ Q ⊢ Q ∨ P

theorem later_intuitionisticallyIf_2 [BI PROP] {P : PROP} : □?p ▷ P ⊢ ▷ □?p P

theorem assumption_l [BI PROP] {P Q R : PROP} [Affine Q] (h : P ⊢ R) : P ∗ Q ⊢ R

protected theorem Hom.valid [CMRA β] (f : α -C> β) {x : α} (H : ✓ x) : ✓ f x

@[simp] theorem map_apply [OFE α] [OFE β] {f : α -n> β} {c : Chain α} {n} :
    map f c n = f (c n)

theorem persistently_entails_l [BI PROP] {P Q : PROP} (h : P ⊢ <pers> Q) : P ⊢ <pers> Q ∗ P

theorem absorbingly_true [BI PROP] : <absorb> True ⊣⊢ (True : PROP)

theorem persistently_emp' [BI PROP] [BIAffine PROP] : <pers> (emp : PROP) ⊣⊢ emp

theorem and_destruct_intuitionistic_right [BI PROP] (Q : PROP) : □ (P ∧ Q) ⊢ Q

theorem equiv_fst [OFE α] [OFE β] {x y : α × β} (h : x ≡ y) : x.fst ≡ y.fst

theorem and_congr_l [BI PROP] {P P' Q : PROP} (h : P ⊣⊢ P') : P ∧ Q ⊣⊢ P' ∧ Q

theorem set_op_equiv {m1 m2 : T} :
    Equiv ((set (V := Option V) (m1 • m2) i (x • y))) (set m1 i x • set m2 i y)

theorem Tower.embed_self (X : Tower F) :
    Tower.embed (k+1) (X (k+1)) ≡{k}≡ X

theorem plainly_wand_affinely_plainly : (<affine> ■ P -∗ ■ Q) ⊢ ■ (<affine> ■ P -∗ Q)

theorem move_multiple [BI PROP] (Q : PROP) : <affine> ⌜φ1⌝ ⊢ <affine> ⌜φ2⌝ -∗ Q -∗ Q

theorem persistently_imp_wand_2 [BI PROP] {P Q : PROP} : <pers> (P -∗ Q) ⊢ <pers> (P → Q)

theorem CoreId.of_pcore_eq_some {x y : α} (e : pcore x = some y) : CoreId y

@[rw_mono_rule]
theorem intuitionisticallyIf_mono {p : Bool} [BI PROP] {P Q : PROP} (h : P ⊢ Q) : □?p P ⊢ □?p Q

theorem wandIff_congr_r [BI PROP] {P Q Q' : PROP} (h : Q ⊣⊢ Q') : (P ∗-∗ Q) ⊣⊢ (P ∗-∗ Q')

theorem pure [BI PROP] [BIAffine PROP] (Q : PROP) : ⊢ ⌜φ⌝ -∗ Q -∗ Q

theorem Agree.toAgree_inj {a b : α} : toAgree a ≡ toAgree b → a ≡ b

theorem drop [BI PROP] (Q : PROP) : ⊢ P → Q -∗ Q

theorem _root_.Iris.OFE.Equiv.cancelable {x₁ x₂ : α} : x₁ ≡ x₂ → (Cancelable x₁ ↔ Cancelable x₂)

theorem intuitionistically_elim [BI PROP] {P : PROP} : □ P ⊢ P

theorem wand_entails [BI PROP] {P Q : PROP} (h : ⊢ P -∗ Q) : P ⊢ Q

theorem impl_wand_affinely_plainly : (■ P → Q) ⊣⊢ (<affine> ■ P -∗ Q)

theorem hmap_unalloc [Heap T K V] {t : T} (H : get t k = none) : get (hmap f t) k = none

theorem pcore_mono' {x y : α} {cx} (le : x ≼ y) (e : pcore x ≡ some cx) :
    ∃ cy, pcore y = some cy ∧ cx ≼ cy

theorem valid_core {x : α} (v : ✓ x) : ✓ core x

theorem forall_intuitionistic_overwrite [BI PROP] (Q : Nat → PROP) : ⊢ □ (∀ x, Q x) -∗ □ Q y

theorem affinely_elim_emp [BI PROP] {P : PROP} : <affine> P ⊢ emp

theorem plainly_exists_1 [BIPlainlyExists PROP] {Ψ : α → PROP} :
    ■ (∃ a, Ψ a) ⊢ ∃ a, ■ (Ψ a)

theorem UpdateP.weaken {x : α} (uxp : x ~~>: P) (pq : ∀ y, P y → Q y) : x ~~>: Q

theorem persistently_sep_persistently [BI PROP] {P : PROP} : <pers> P ∗ <pers> P ⊣⊢ <pers> P
</all_available_lemmas>

<local_ctx>
import Iris.Algebra.CMRA

namespace Iris

def UpdateP [CMRA α] (x : α) (P : α → Prop) := ∀ n mz,
  ✓{n} (x •? mz) → ∃ y, P y ∧ ✓{n} (y •? mz)

infixr:50 " ~~>: " => UpdateP

def Update [CMRA α] (x y : α) := ∀ n mz,
  ✓{n} (x •? mz) → ✓{n} (y •? mz)

infixr:50 " ~~> " => Update

section updates

variable [CMRA α] [CMRA β] (f : α → β) (g : β → α)
</local_ctx>

<target_theorem>
theorem UpdateP.iso
    (gf : ∀ x, g (f x) ≡ x)
    (g_op : ∀ y1 y2, g (y1 • y2) ≡ g y1 • g y2)
    (g_validN : ∀ n y, ✓{n} (g y) ↔ ✓{n} y)
    (uyp : y ~~>: P)
    (pq : ∀ y', P y' → Q (g y')) :
    g y ~~>: Q :=
</target_theorem>

