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

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

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₂

class Discrete (α : Type _) [OFE α] where
  discrete_0 {x y : α} : x ≡{0}≡ y → x ≡ y

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

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

class Fraction (α : Type _) extends Add α where
   
  Proper : α → Prop
  add_comm : ∀ a b : α, a + b = b + a
  add_assoc : ∀ a b c : α, a + (b + c) = (a + b) + c
  add_left_cancel : ∀ {a b c : α}, a + b = a + c → b = c
   
  add_ne : ∀ {a b : α}, a ≠ b + a
  proper_add_mono_left : ∀ {a b : α}, Proper (a + b) → Proper a

def Fractional [Fraction α] (a : α) : Prop := ∃ b, Proper (a + b)

class NumericFraction (α : Type _) extends One α, Add α, LE α, LT α where
  add_comm : ∀ a b : α, a + b = b + a
  add_assoc : ∀ a b c : α, a + (b + c) = (a + b) + c
  add_left_cancel : ∀ {a b c : α}, a + b = a + c → b = c
  le_def : ∀ {a b : α}, a ≤ b ↔ a = b ∨ a < b
  lt_def : ∀ {a b : α}, a < b ↔ ∃ c : α, a + c = b
  lt_irrefl : ∀ {a : α}, ¬a < a

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₂

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

class Discrete (α : Type _) [CMRA α] extends OFE.Discrete α where
  discrete_valid {x : α} : ✓{0} x → ✓ x

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)

instance exists_absorbing [BI PROP] (Φ : α → PROP) [∀ x, Absorbing (Φ x)] :
    Absorbing iprop(∃ x, Φ x) where
  absorbing := absorbingly_exists.1.trans (exists_mono fun _ => absorbing)

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 affinelyIf [BIBase PROP] (p : Bool) (P : PROP) : PROP := iprop(if p then <affine> P else P)

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)

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

class IntoPure [BI PROP] (P : PROP) (φ : outParam Prop) where
  into_pure : P ⊢ ⌜φ⌝

| .disjunction [] => throwUnsupportedSyntax

instance wand_absorbing_r [BI PROP] (P Q : PROP) [Absorbing Q] : Absorbing iprop(P -∗ Q) where
  absorbing := absorbingly_wand_1.trans (wand_mono absorbingly_intro absorbing)

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

def Hyps.split {prop : Q(Type u)} (bi : Q(BI $prop)) (toRight : Name → Name → Bool)
    {e} (hyps : Hyps bi e) :
    (elhs erhs : Q($prop)) × Hyps bi elhs × Hyps bi erhs × Q($e ⊣⊢ $elhs ∗ $erhs) :=
  match hyps.splitCore bi toRight with
  | .emp _ => ⟨_, _, hyps, hyps, q(sep_emp_rev)⟩
  | .left => ⟨_, _, hyps, .mkEmp bi, q(sep_emp_rev)⟩
  | .right => ⟨_, _, .mkEmp bi, hyps, q(emp_sep_rev)⟩
  | .split lhs rhs pf => ⟨_, _, lhs, rhs, pf⟩

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

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 [OFE α] : CMRA (Excl α) where
  pcore _ := none
  op _ _ := invalid
  ValidN _ := Valid
  Valid
  op_ne.ne _ _ _ _ := trivial
  pcore_ne := by admit /- proof elided -/

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

instance and_affine_l [BI PROP] (P Q : PROP) [Affine P] : Affine iprop(P ∧ Q) where
  affine := and_elim_l.trans affine

instance intoPure_pure (φ : Prop) [BI PROP] : IntoPure (PROP := PROP) iprop(⌜φ⌝) φ := ⟨.rfl⟩

Or in Init.Prelude

applyMonotonicity (goal : MVarId) : TacticM <| Option <| List MVarId := do
    for rule in (← getMonotonicityRules) do
      try
        if let some goals ← apply' goal rule then
          return ← goals.mapM normalizeGoal
      catch _ =>
        continue
    return none

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 _

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

class RightId (R : Relation α) (i : α) (f : α → α → α) where
  right_id {x : α} : R (f x i) x

instance : UCMRA (IResUR FF) :=
  ucmraDiscreteFunO (β := fun (i : GId FF) => GName → Option (FF[i] (iPrePropO FF) (iPrePropO FF)))

Lean.Name in Init.Prelude

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

def exclChain [OFE α] (c : Chain (Excl α)) (a : α) : Chain α :=

def GId (FF : GFunctors) : Type _ := Fin FF.size

class Preorder (R : Relation α) extends Reflexive R, Transitive R

instance : IsModal (PROP1 := PROP) affinely (.id rfl) (.forall rfl Affine) where
  spec_intuitionistic _ := affinely_intro .rfl
  spec_spatial _ _ := affinely_intro .rfl
  emp := affinely_intro .rfl
  mono := (affinely_mono ·)
  sep := affinely_sep_2

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

delab_rule BIBase.Entails
  | `($_ $P $Q) => do ``($(← unpackIprop P) ⊢ $(← unpackIprop Q))

@[ext] structure Tower : Type u where
  val k : A F k
  protected down {k} : down F k (val (k+1)) ≡ val k

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)

partial def instantiateForalls {prop : Q(Type u)} (bi : Q(BI $prop)) (hyp : Q($prop))
    (pf : Q(⊢ $hyp)) (terms : List Term) : TacticM (Expr × Expr) := do
  if let some t := terms.head? then
    let texpr ← mkAppM' (← elabTerm t none) #[]
    let ⟨_, ttype, texpr⟩ ← inferTypeQ texpr
    let Φ ← mkFreshExprMVarQ q($ttype → $prop)
    let _ ← synthInstanceQ q(IntoForall $hyp $Φ)
    let res ← mkAppM' Φ #[texpr]
    let pf' ← mkAppM ``pose_forall #[texpr, Φ, pf]
    return ← instantiateForalls bi res pf' terms.tail
  else
    let pf ← mkAppM ``as_emp_valid_1 #[hyp, pf]
    return ⟨hyp, pf⟩

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

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)

class FromSep [BI PROP] (P : PROP) (Q1 Q2 : outParam PROP) where
  from_sep : Q1 ∗ Q2 ⊢ P

instance {x : Agree α} : CMRA.Cancelable x where
  cancelableN {n y z} hval heq := by admit /- proof elided -/

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

Qq.synthInstanceQ in Qq.MetaM

Lean.NameMap in Lean.Data.NameMap.Basic

structure SpecializeState {prop : Q(Type u)} (bi : Q(BI $prop)) (orig : Q($prop)) where
  (e : Q($prop)) (hyps : Hyps bi e) (b : Q(Bool)) (out : Q($prop))
  pf : Q($orig ⊢ $e ∗ □?$b $out)

instance [Heap T K V] [OFE V] (op : V → V → V) [NonExpansive₂ op] :
    NonExpansive₂ (merge (T := T) op) where
  ne _ {_ _} Ht {_ _} Hs k := by admit /- proof elided -/

absurd in Init.Prelude

instance cmraUnit : CMRA Unit where
  pcore _ := some ()
  op _ _ := ()
  ValidN _ _ := True
  Valid _ := True
  op_ne.ne _ _ _ := id
  pcore_ne _ _ := ⟨(), rfl, .rfl⟩
  validN_ne _ := id
  valid_iff_validN := ⟨fun _ _ => ⟨⟩, fun _ => ⟨⟩⟩
  validN_succ := id
  validN_op_left := id
  assoc := .rfl
  comm := .rfl
  pcore_op_left _ := .rfl
  pcore_idem _ := .rfl
  pcore_op_mono _ _ := ⟨.unit, .rfl⟩
  extend _ _ := ⟨(), (), .rfl, .rfl, .rfl⟩

EmptyCollection.emptyCollection in Init.Core

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

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

def LocalUpdate [CMRA α] (x y : α × α) : Prop :=
  ∀n mz, ✓{n} x.1 → x.1 ≡{n}≡ x.2 •? mz → ✓{n} y.1 ∧ y.1 ≡{n}≡ y.2 •? mz

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

class BILaterContractive (PROP : Type _) [BI PROP] extends OFE.Contractive later (α := PROP)

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

abbrev IResF (FF : GFunctors) : COFE.OFunctorPre :=
  DiscreteFunOF (fun i : GId FF => GenMapOF GName FF[i])

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

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

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

Lean.KVMap in Lean.Data.KVMap

class FUpd (PROP : Type _) (MASK : Type _) where
  fupd : Set MASK → Set MASK → PROP → PROP

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

class IntoPersistently (p : Bool) [BI PROP] (P : PROP) (Q : outParam PROP) where
  into_persistently : <pers>?p P ⊢ <pers> Q

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)

Lean.throwError in Lean.Exception

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 _

protected def Entails (P Q : UPred M) : Prop := ∀ n x, ✓{n} x → P n x → Q n x

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

Exists in Init.Core

instance [COFE α] : COFE (ULift α) where
  compl c := ⟨compl (c.map uliftDownHom)⟩
  conv_compl := conv_compl

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

instance intoOr_or [BI PROP] (P Q : PROP) : IntoOr iprop(P ∨ Q) P Q := ⟨.rfl⟩

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

Inhabited.default in Init.Prelude

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

def «forall» [BIBase PROP] {α : Sort _} (P : α → PROP) : PROP := sForall fun p => ∃ a, P a = p

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

class FromWand [BI PROP] (P : PROP) (Q1 Q2 : outParam PROP) where
  from_wand : (Q1 -∗ Q2) ⊢ P

def parseIrisGoal? (expr : Expr) : Option IrisGoal := do
  let some #[prop, bi, P, goal] := expr.appM? ``Entails' | none
  let u := expr.getAppFn.constLevels![0]!
  let ⟨e, hyps⟩ ← parseHyps? bi P
  some { u, prop, bi, e, hyps, goal }

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

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)

instance Store.Equiv_trans [Store T K V] : Trans Equiv (Equiv (T := T)) Equiv := ⟨by admit /- proof elided -/
⟩

def ownM (m : M) : UPred M where
  holds n x := m ≼{n} x
  mono {n₁ n₂ x₁ x₂} := fun ⟨m₁, Hm₁⟩ ⟨m₂, Hm₂⟩ Hn => by admit /- proof elided -/

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

Lean.Expr.fvar in Lean.Expr

Lean.Expr in Lean.Expr

@[ext]
structure Agree where
  car : List α
  not_nil : car ≠ []

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

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

instance [BI PROP] [BIAffine PROP] (P : PROP) : Absorbing P where
  absorbing := (sep_mono_l affine).trans emp_sep.1

instance : BIPlainlyExists (UPred M) where
  plainly_sExists_1 _ _ _ := fun ⟨_, hp⟩ => ⟨_, ⟨_, rfl⟩, hp⟩

go (goal : MVarId) (rule : TSyntax `term) : TacticM Bool := do
    
    try
      withFocus goal <| withoutRecover <| evalTactic (← `(tactic|
        exact $rule
      ))
      return true
    catch _ => pure ()

def getMDataName? : Expr → Option Name
  | Expr.mdata md _ => md.get? `name
  | _ => none

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

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 affinelyIf_persistent (p : Bool) [BI PROP] (P : PROP) [Persistent P] :
    Persistent iprop(<affine>?p P) :=

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

instance [OFunctorContractive F] : OFunctorContractive (OptionOF F) where
  map_contractive.1 H z := by admit /- proof elided -/

def HasStoreMap.map (f : V1 → V2) [Store T1 K V1] [Store T2 K V2] [HasStoreMap T1 T2 K V1 V2] : T1 → T2 :=
  HasStoreMap.dmap (fun _ => f)

class BIPlainly (PROP : Type _) [Iris.BI PROP] extends Plainly PROP where
  [ne : Iris.OFE.NonExpansive (Plainly.plainly (PROP := PROP))]
  mono {P Q : PROP} : (P ⊢ Q) → ■ P ⊢ ■ Q
  elim_persistently {P : PROP} : ■ P ⊢ <pers> P
  idem {P : PROP} : ■ P ⊢ ■ ■ P
  plainly_sForall_2 {Φ : PROP → Prop} : (∀ p, ⌜Φ p⌝ → ■ p) ⊢ ■ sForall Φ
  plainly_impl_plainly {P Q : PROP} : (■ P → ■ Q) ⊢ ■ (■ P → Q)
  emp_intro {P : PROP} : P ⊢ ■ emp
  plainly_absorb {P Q : PROP} : ■ P ∗ Q ⊢ ■ P
  later_plainly {P : PROP} : ▷ ■ P ⊣⊢ ■ ▷ P

instance [CMRA α] : Trans Update UpdateP UpdateP (α := α) where
  trans := Update.transP

class CoreId (x : α) where
  core_id : pcore x ≡ some x

def SpecializeState.process1 :
    @SpecializeState u prop bi orig → Term → TermElabM (SpecializeState bi orig)
  | { e, hyps, b, out, pf }, arg => do
    let uniq ← match arg with
      | `($x:ident) => try? (hyps.findWithInfo x)
      | _ => pure none
    if let some uniq := uniq then
      
      let ⟨e', hyps', out₁, out₁', b1, _, pf'⟩ := hyps.remove false uniq
      let b2 := if b1.constName! == ``true then b else q(false)
      have : $out₁ =Q iprop(□?$b1 $out₁') := ⟨⟩
      have : $b2 =Q ($b1 && $b) := ⟨⟩

def isTrue (p : Q(Bool)) : Bool := p.constName! == ``true

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

nonrec abbrev OFE.ContractiveHom.fixpoint [COFE α] [Inhabited α] (f : α -c> α) : α := fixpoint f.f

instance [OFE.Discrete α] : CMRA.Discrete (Agree α) where
  discrete_0 := by admit /- proof elided -/

instance [URFunctor F] : COFE.OFunctor (UPredOF F) where
  cofe := inferInstance
  map f g := uPred_map (URFunctor.map (F := F) g f)
  map_ne.ne _ _ _ Hx _ _ Hy _ _ z2 Hn _ :=
    uPred_ne <| URFunctor.map_ne.ne (Hy.le Hn) (Hx.le Hn) z2
  map_id _ _ z _ := uPred_proper <| URFunctor.map_id z
  map_comp f g f' g' _ _ H _ := uPred_proper <| URFunctor.map_comp g' f' g f H

instance later_persistent [BI PROP] {P : PROP} [Persistent P] : Persistent iprop(▷ P) where
  persistent := (later_mono persistently_intro).trans later_persistently.mp

protected def or (P Q : UPred M) : UPred M where
  holds n x := P n x ∨ Q n x
  mono
  | .inl H, Hle, Hn => .inl (P.mono H Hle Hn)
  | .inr H, Hle, Hn => .inr (Q.mono H Hle Hn)

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

class Persistent [BI PROP] (P : PROP) where
  persistent : P ⊢ <pers> P

class BIPersistentlyImplPlainly (PROP : Type _) [Iris.BI PROP] [BIPlainly PROP] where
  pers_impl_plainly (P Q : PROP) : (■ P → <pers> Q) ⊢ <pers> (■ P → Q)

instance pureAbsorbing (φ : Prop) [BI PROP] : Absorbing (PROP := PROP) iprop(⌜φ⌝) where
  absorbing := absorbingly_pure.1

local instance : OFE.NonExpansive (Agree.map' f) where
  ne := by admit /- proof elided -/

instance : UFraction α where
  Proper x := x ≤ 1
  add_comm := add_comm
  add_assoc := add_assoc
  add_left_cancel := add_left_cancel
  add_ne H := add_ne_self ((add_comm ..).trans H.symm)
  proper_add_mono_left := add_le_mono
  
  
  
  
  
  
  
  one_whole := by admit /- proof elided -/

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

instance : BI (UPred M) where
  entails_preorder := inferInstance
  equiv_iff {P Q} := by admit /- proof elided -/

Lean.TSyntax in Init.Prelude

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

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 HypMarker {PROP : Type _} (_A : PROP) : Prop := True

class BIFUpdatePlainly (PROP MASK : Type _) [BI PROP] [BIFUpdate PROP MASK] [BIPlainly PROP] where
  fupd_plainly_keep_l (E E' : Set MASK) (P R : PROP) : (R ={E,E'}=∗ ■ P) ∗ R ⊢ |={E}=> P ∗ R
  fupd_plainly_later (E : Set MASK) (P : PROP) : (▷ |={E}=> ■ P) ⊢ |={E}=> ▷ ◇ P
  fupd_plainly_sForall_2 (E : Set MASK) (Φ : PROP → Prop) :
    (∀ p, ⌜Φ p⌝ → |={E}=> ■ p) ⊢ |={E}=> sForall Φ

Fix in Mathlib.Control.Fix

propext in Init.Core

instance [Fraction α] {a : Frac α} : CMRA.IdFree a where
  id_free0_r b _ H := 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 ucmraOption : UCMRA (Option α) where
  unit := none
  unit_valid := by admit /- proof elided -/

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

def SubG (FF₁ FF₂ : GFunctors) : Prop :=
  ∀ i : GId FF₁, ∃ j : GId FF₂, FF₁[i] = FF₂[j]

instance [u : U] : TCOr T U := @TCOr.r T U u

instance : Inhabited (QuotedDefEq a b) := ⟨⟨⟩⟩

GetElem in Init.GetElem

instance RFunctorContractive.toOFunctorContractive
    [RFunctorContractive F] : COFE.OFunctorContractive F where
  map_contractive.1 := map_contractive.1

structure Later (A : Type u) : Type (u+1) where
  next :: car : A

instance [CMRA.Discrete α] [CMRA.Discrete β]: CMRA.Discrete (α × β) where
  discrete_valid := by admit /- proof elided -/

| .disjunction (arg :: args) =>
    iCasesOr bi P Q A' p
      (iCasesCore hyps Q p · · · arg @k)
      (iCasesCore hyps Q p · · · (.disjunction args) @k)

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

instance : Plainly (UPred M) := ⟨UPred.plainly⟩

Lean.mkAppN in Lean.Expr
</all_available_defs>

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

theorem Valid.validN : ✓ (x : α) → ✓{n} x

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

theorem valid_iff_validN' [Discrete α] (n) {x : α} : ✓ x ↔ ✓{n} x

theorem sep_or_r [BI PROP] {P Q R : PROP} : (P ∨ Q) ∗ R ⊣⊢ (P ∗ R) ∨ (Q ∗ R)

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

theorem apply_forall [BI PROP] (P Q : α → PROP) (a b : α) (H : ⊢ ∀ x, ∀ y, P x -∗ Q y) : P a ⊢ Q b

theorem false_elim [BI PROP] {P : PROP} : False ⊢ P

@[simp] theorem some_eqv_some [OFE α] {x y : α} : (some x ≡ some y) ↔ x ≡ y

theorem inc_iff_right (e : (b : α) ≡ c) : a ≼ b ↔ a ≼ c

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

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

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

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

theorem from_forall_intro [BI PROP] {P Q : PROP} {Φ : α → PROP} [inst : FromForall Q Φ]
    (h : ∀ a, P ⊢ Φ a) : P ⊢ Q

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

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

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

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

theorem rename_twice [BI PROP] (Q : PROP) : Q ⊢ Q

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

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

theorem split_ls [BI PROP] {P Q Q1 Q2 : PROP} (h : Q ⊣⊢ Q1 ∗ Q2) : P ∗ Q ⊣⊢ (P ∗ Q1) ∗ Q2

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

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

theorem delete_valid {m : T} (Hv : ✓ m) : ✓ (delete m i)

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

theorem core_op_core {x : α} : core x • core x ≡ core x

theorem incN_op_right (n) (x y : α) : y ≼{n} x • y

theorem _root_.Iris.OFE.Dist.idFree {x₁ x₂ : α} (e : x₁ ≡{n}≡ x₂) : IdFree x₁ ↔ IdFree x₂

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

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

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

theorem plainly_and_sep_l : ■ P ∧ Q ⊣⊢ ■ P ∗ Q

theorem IsoFunStore.ext [Store T K V] [IsoFunStore T K V] {t1 t2 : T}
    (H : ∀ k, get t1 k = get t2 k) : t1 = t2

theorem op_assocN {x y z : α} : x • (y • z) ≡{n}≡ (x • y) • z

theorem exact_lean'' [BI PROP] (Q : PROP) (H : 0 = 0 → ⊢ Q) : ⊢ Q

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

theorem plainly_or_2 : ■ P ∨ ■ Q ⊢ ■ (P ∨ Q)

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

theorem Equiv.of_eq [OFE α] {x y : α} : x = y → x ≡ y

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

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

theorem Hom.comp_assoc [OFE α] [OFE β] [OFE γ] [OFE δ]
    (h : γ -n> δ) (g : β -n> γ) (f : α -n> β) : (h.comp g).comp f = h.comp (g.comp f)

theorem intuitionistic_elim_spatial [BI PROP] {A A' Q : PROP}
    [IntoPersistently false A A'] [TCOr (Affine A) (Absorbing Q)]
    (h : P ∗ □ A' ⊢ Q) : P ∗ A ⊢ Q

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

theorem affinelyIf_intro' {p : Bool} [BI PROP] {P Q : PROP} :
    (P ⊢ <affine>?p Q) → <affine>?p P ⊢ <affine>?p Q

theorem as_emp_valid_1 [BI PROP] (P : PROP) [AsEmpValid1 φ P] : φ → ⊢ P

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

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

theorem to_persistent_spatial [BI PROP] {P P' Q : PROP}
    [hP : IntoPersistently false P P'] [or : TCOr (Affine P) (Absorbing Q)] :
    Replaces Q P iprop(□ P')

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

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

theorem bigOp_nil {f : PROP → PROP → PROP} {unit : PROP} : bigOp f unit [] = unit

theorem absorbinglyIf_ne {p : Bool} [BI PROP] : OFE.NonExpansive (absorbinglyIf (PROP := PROP) p)

theorem coreId_iff {x₁ x₂ : α} (e : x₁ ≡ x₂) : CoreId x₁ ↔ CoreId x₂

theorem point_valid_iff : ✓ (point i x : T) ↔ ✓ x

theorem imp_intro_drop [BI PROP] {P Q A1 A2 : PROP} [inst : FromImp Q A1 A2] (h : P ⊢ A2) : P ⊢ Q

theorem set_op_eq [IsoFunStore T K (Option V)] {m1 m2 : T} :
    (set (V := Option V) (m1 • m2) i (x • y)) = (set m1 i x • set m2 i y)

theorem Store.get_set [Store T K V] {t : T} {k k' : K} {v : V} :
    get (set t k v) k' = if k = k' then v else get t k'

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

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

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

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

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

theorem sep_assoc [BI PROP] {P Q R : PROP} : (P ∗ Q) ∗ R ⊣⊢ P ∗ Q ∗ R

theorem intuitionistically_false [BI PROP] : □ False ⊣⊢ (False : PROP)

theorem imp_self [BI PROP] {P Q : PROP} : Q ⊢ P → P

theorem pure_congr [BI PROP] {φ1 φ2 : Prop} (h : φ1 ↔ φ2) : ⌜φ1⌝ ⊣⊢ (⌜φ2⌝ : PROP)

@[simp] theorem BIBase.Entails.rfl [BI PROP] {P : PROP} : P ⊢ P

theorem exact_lean' [BI PROP] (Q : PROP) : Q ⊢ (emp ∗ Q) ∗ emp

theorem pcore_proper' {x y : α} (e : x ≡ y) : pcore x ≡ pcore y

theorem down_eqToHom {k k'} {x : A F (k+1)} (e : k = k') :
    down F k' (eqToHom (congrArg Nat.succ e) x) = eqToHom e (down F k x)

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

theorem later_soundness : iprop(True ⊢ ▷ P) → iprop((True : UPred M) ⊢ P)

theorem incN_iff {ma mb : Option α} :
    ma ≼{n} mb ↔ ma = none ∨ ∃ a b, ma = some a ∧ mb = some b ∧ (a ≡{n}≡ b ∨ a ≼{n} b)

theorem excl_map_ne [OFE α] [OFE β] (f : α -n> β) : NonExpansive (map f)

theorem wand_spatial_multiple [BI PROP] (Q : PROP) : ⊢ P1 -∗ P2 -∗ (P1 -∗ P2 -∗ Q) -∗ Q

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

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

theorem affinely_absorbingly [BI PROP] [BIPositive PROP] {P : PROP} :
    <affine> <absorb> P ⊣⊢ <affine> P

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

theorem intuitionisticallyIf_def' {p : Bool} [BI PROP] {P : PROP} :
    iprop(□?p P) = iprop(<affine>?p <pers>?p P)

theorem and_sep_plainly : ■ P ∧ ■ Q ⊣⊢ ■ P ∗ ■ Q

theorem pcore_op_self' {x : α} {cx} (e : pcore x ≡ some cx) : cx • cx ≡ cx

theorem Contractive.eqv [OFE α] [OFE β] (f : α → β) [Contractive f] ⦃x y : α⦄ (h : x ≡ y) :
    f x ≡ f y

theorem sep_emp_intro_intuitionistic [BI PROP] {P Q : PROP}
    (h : P ⊢ Q) : P ∗ □ emp ⊢ Q

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

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

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

@[symm] theorem DistLater.symm [OFE α] {n} {x : α} (h : DistLater n x y) : DistLater n y x

theorem not_valid_some_exclN_op_left {n} {x : α} [Exclusive x] {y : α} : ¬✓{n} (some x • some y)

theorem affinelyIf_emp {p : Bool} [BI PROP] : (<affine>?p emp : PROP) ⊣⊢ emp

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

theorem add_right_cancel {a b c : α} (H : b + a = c + a) : b = c

theorem bupd_elim {P : PROP} [Plain P] : |==> P ⊢ P

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

theorem and_true [BI PROP] {P : PROP} : P ∧ True ⊣⊢ P

theorem sep_sep_sep_comm [BI PROP] {P Q R S : PROP} : (P ∗ Q) ∗ (R ∗ S) ⊣⊢ (P ∗ R) ∗ (Q ∗ S)

theorem intuitionisticallyIf_ne {p : Bool} [BI PROP] :
    OFE.NonExpansive (intuitionisticallyIf (PROP := PROP) p)

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

theorem Fractional.proper {a : α} : Fractional a → Proper a

theorem valid_op_right (x y : α) : ✓ (x • y) → ✓ y

theorem proof_example_1 [BI PROP] (P Q R : PROP) (Φ : α → PROP) :
  P ∗ Q ∗ □ R ⊢ □ (R -∗ ∃ x, Φ x) -∗ ∃ x, Φ x ∗ P ∗ Q

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

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

theorem Agree.toAgree_uninj {x : Agree α} : ✓ x → ∃ a, toAgree a ≡ x

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

theorem disjunction_clear [BI PROP] [BIAffine PROP] (Q : PROP) : Q ⊢ P1 ∨ P2 -∗ Q

theorem from_affine [BI PROP] {p : Bool} {P P' Q : PROP} [hP : FromAffinely P' P p] :
    Replaces Q iprop(□?p P) P'

theorem persistently_ite {p : Bool} [BI PROP] {P Q : PROP} :
    iprop(<pers> if p then P else Q) = iprop(if p then <pers> P else <pers> Q)

theorem persistentlyIf_ne {p : Bool} [BI PROP] :
    OFE.NonExpansive (persistentlyIf (PROP := PROP) p)

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

theorem multiple_lean' [BI PROP] (P Q R : PROP) (H : P ∗ Q ⊢ R) (HP : ⊢ P) : ⊢ Q -∗ R

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

@[simp] theorem compl_const [COFE α] (a : α) : compl (Chain.const a) ≡ a

theorem LocalUpdate.replace (x y : α) [CMRA.IdFree x] (h : ✓ y) : (x, x) ~l~> (y, y)

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

theorem Fix.unfold_fold (X : F (Fix F) (Fix F)) : Fix.unfold (Fix.fold X) ≡ X

theorem Update.lift_updateP (x y : β)
    (H : ∀ P, x ~~>: P → g x ~~>: λ a' ↦ ∃ b', a' = g b' ∧ P b')
    (uxy : x ~~> y) : g x ~~> g y

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

@[rw_mono_rule]
theorem forall_congr [BI PROP] {Φ Ψ : α → PROP} (h : ∀ a, Φ a ⊣⊢ Ψ a) : (∀ a, Φ a) ⊣⊢ ∀ a, Ψ a

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

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

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

theorem cmra_valid_intro P [CMRA A] (a : A) : ✓ a → P ⊢ (cmraValid a : UPred M)

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

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

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

theorem plainly_into_absorbingly : ■ P ⊢ <absorb> P

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

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

theorem absorbinglyIf_forall_1 {p : Bool} [BI PROP] {Φ : α → PROP} :
    <absorb>?p (∀ a, Φ a) ⊢ ∀ a, <absorb>?p (Φ a)

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

theorem wand_intro_spatial [BI PROP] {P Q A1 A2 : PROP}
    [FromWand Q A1 A2] (h : P ∗ A1 ⊢ A2) : P ⊢ Q

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

theorem point_incN_iff {m : T} :
    (point (T := T) i (some x)) ≼{n} m ↔ ∃ y, (get m i ≡{n}≡ some y) ∧ some x ≼{n} some y

theorem with_proof [BI PROP] (H : A → B) (P Q : PROP) : <affine> P ⊢ <pers> Q → ⌜A⌝ → ⌜B⌝

theorem persistently_and_emp_elim {P : PROP} [BI PROP] : emp ∧ <pers> P ⊢ P

theorem persistentlyIf_forall_1 {p : Bool} [BI PROP] {Φ : α → PROP} :
    <pers>?p (∀ a, Φ a) ⊢ ∀ a, <pers>?p (Φ a)

theorem dist_prod_ext {n} [OFE α] [OFE β] {x₁ x₂ : α} {y₁ y₂ : β}
    (ex : x₁ ≡{n}≡ x₂) (ey : y₁ ≡{n}≡ y₂) : (x₁, y₁) ≡{n}≡ (x₂, y₂)

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

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

theorem down_up : ∀ {k} x, down F k (up F k x) ≡ x

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

theorem absorbinglyIf_intro {p : Bool} [BI PROP] {P : PROP} : P ⊢ <absorb>?p P

theorem later_or [BI PROP] {P Q : PROP} : ▷ (P ∨ Q) ⊣⊢ ▷ P ∨ ▷ Q

theorem pcore_op_self {x : α} {cx} (e : pcore x = some cx) : cx • cx ≡ cx

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

theorem core_incN_core {n} {x y : α} (inc : x ≼{n} y) : core x ≼{n} core y

theorem sep_true [BI PROP] {P : PROP} [Absorbing P] : P ∗ True ⊣⊢ P

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

theorem pure_true [BI PROP] {φ : Prop} (h : φ) : ⌜φ⌝ ⊣⊢ (True : PROP)

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

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

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

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

theorem and_left_comm [BI PROP] {P Q R : PROP} : P ∧ Q ∧ R ⊣⊢ Q ∧ P ∧ R

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

theorem plainly_wand : ■ (P -∗ Q) ⊢ ■ P -∗ ■ Q

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

theorem unit_right_id {x : α} : x • unit ≡ x

theorem core_ne : NonExpansive (core : α → α)

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

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

theorem coreId_iff_core_eqv_self : CoreId (x : α) ↔ core x ≡ x

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

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

theorem clear_spatial [BI PROP] {P P' A Q : PROP} [TCOr (Affine A) (Absorbing Q)]
    (h_rem : P ⊣⊢ P' ∗ A) (h : P' ⊢ Q) : P ⊢ Q

theorem inc_of_eqv_of_inc (e : (a : α) ≡ b) : b ≼ c → a ≼ c

theorem affinely_emp [BI PROP] : <affine> emp ⊣⊢ (emp : PROP)

theorem Discrete.discrete [OFE α] [Discrete α] {n} {x y : α} (h : x ≡{n}≡ y) : x ≡ y

theorem apply_forall' [BI PROP] (P Q : α → PROP) (a b : α) : (∀ x, ∀ y, P x -∗ Q y) ⊢ P a -∗ Q b

theorem opM_opM_assoc {x : α} {y z : Option α} : (x •? y) •? z ≡ x •? (y • z)

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

@[simp] theorem Leibniz.leibniz [OFE α] [Leibniz α] {x y : α} : x ≡ y ↔ x = y

@[simp] theorem intuitionisticallyIf_false' [BI PROP] (P : PROP) : iprop(□?false P) = P

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

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

theorem later_affinely [BI PROP] [BIAffine PROP] {P : PROP} : <affine> ▷ P ⊣⊢ ▷ <affine> P

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

@[rw_mono_rule]
theorem absorbingly_congr [BI PROP] {P P' : PROP} (h : P ⊣⊢ P') :
    <absorb> P ⊣⊢ <absorb> P'

theorem equiv_some [OFE α] {o : Option α} {y : α} (e : o ≡ some y) :
    ∃ z, o = some z ∧ z ≡ y

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

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

theorem point_inc_point_iff : (point i (T := T) (some x)) ≼ (point i (some y)) ↔ some x ≼ some y

@[simp] theorem map_id [OFE α] {c : Chain α} : map (Hom.id : α -n> α) c = c

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

theorem Heap.get_point [Heap T K V] {k k' : K} {v : Option V} :
    get (point k v : T) k' = if k = k' then v else .none

theorem set_equiv_point_op_point {m : T} (Hemp : get m i = none) : Equiv (set m i x) (point i x • m)

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

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

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

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

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

@[rw_mono_rule]
theorem intuitionistically_congr [BI PROP] {P Q : PROP} (h : P ⊣⊢ Q) : □ P ⊣⊢ □ Q

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

theorem le_rfl {a : α} : a ≤ a

theorem intuitionistic [BI PROP] (Q : PROP) : □ Q ⊢ Q

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

theorem imp_intro_intuitionistic [BI PROP] {P Q A1 A2 B : PROP}
    [FromImp Q A1 A2] [inst : IntoPersistently false A1 B] (h : P ∗ □ B ⊢ A2) : P ⊢ Q

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

theorem discrete_cancelable {x : α} [Discrete α]
    (H : ∀ {y z : α}, ✓(x • y) → x • y ≡ x • z → y ≡ z) : Cancelable x

theorem op_monoN_right {n x y} (z : α) : x ≼{n} y → z • x ≼{n} z • y

theorem core_eqv_self (x : α) [CoreId x] : core (x : α) ≡ x

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

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

<local_ctx>
import Iris.Algebra.CMRA

import Iris.Algebra.OFE

import Iris.Algebra.Frac

import Iris.Algebra.Updates

import Iris.Algebra.LocalUpdates

namespace Iris

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

section dfrac

open DFrac Fraction OFE.Discrete

variable [UFraction F]

def valid : DFrac F → Prop
  | .own f        => Proper f
  | .discard      => True
  | .ownDiscard f => Fractional 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')
</local_ctx>

<target_theorem>
theorem DFrac.update_discard {dq : DFrac F} : dq ~~> .discard :=
</target_theorem>

