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

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

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

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

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

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

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

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

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

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

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

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

open Set
open Mathlib
open SetRel

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

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

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

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

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

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

@[simp]
</local_ctx>

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

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

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

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

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

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

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

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

### Your task:
<all_available_defs>
def 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)

class Reflexive (R : Relation α) where
  refl {x : α} : R x x

class Transitive (R : Relation α) where
  trans {x y z : α} : R x y → R y z → R x z

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 IsModal [BI PROP1] [BI PROP2] (M : PROP1 → PROP2)
    (iaction saction : ModalityAction PROP1 PROP2) where
  spec_intuitionistic : iaction.intuitionistic_action_spec M
  spec_spatial : saction.spatial_action_spec M
  emp : iprop(emp) ⊢ M iprop(emp)
  mono : ∀ {P Q}, (P ⊢ Q) → M P ⊢ M Q
  sep : ∀ {P Q}, iprop(M P ∗ M Q) ⊢ M iprop(P ∗ Q)

@[ext]
structure UPred (M : Type _) [UCMRA M] where
  holds : Nat → M → Prop
  mono {n1 n2 x1 x2} : holds n1 x1 → x1 ≼{n2} x2 → n2 ≤ n1 → holds n2 x2

instance : OFE (Tower F) where
  Equiv f g := ∀ k, f k ≡ g k
  Dist n f g := ∀ k, f k ≡{n}≡ g k
  dist_eqv := {
    refl _ _ := dist_eqv.refl _
    symm h _ := dist_eqv.symm (h _)
    trans h1 h2 _ := dist_eqv.trans (h1 _) (h2 _)
  }
  equiv_dist {_ _} := by admit /- proof elided -/

instance (k : Nat) : NonExpansive (fun X : Tower F => X.val k) := ⟨fun _ _ _ => (· _)⟩

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

@[simp] def Store.Equiv [Store T K V] (t1 t2 : T) : Prop := get t1 = get t2

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

class HasStoreMap (T1 T2 : Type _) (K V1 V2 : outParam (Type _)) [Store T1 K V1] [Store T2 K V2] where
   
  dmap (f : K → V1 → V2) : T1 → T2
  get_dmap : get (dmap f t) k = f k (get t k)

instance [OFE α] : NonExpansive excl (α := α) where
  ne _ _ _ a := a

instance [OFE α] [IsCOFE α] : IsCOFE (Excl α) where
  compl c := (c 0).map fun x => IsCOFE.compl (exclChain c x)
  conv_compl {n} c := by admit /- proof elided -/

protected def later (P : UPred M) : UPred M where
  holds n x := match n with | 0 => True | Nat.succ n' => P n' x
  mono {n₁ n₂} := by admit /- proof elided -/

instance bupd_ne : OFE.NonExpansive (bupd : UPred M → UPred M) where
  ne n x1 x2 Hx m y Hm Hv := by admit /- proof elided -/

instance later_contractive : OFE.Contractive UPred.later (α := UPred M) where
  distLater_dist {n x y} Hl :=
    match n with
    | 0 => by admit /- proof elided -/
    | n + 1 => fun
      | 0 => by admit /- proof elided -/
      | n' + 1 => fun x' Hn' Hx' => Hl _ Hn' _ _ (Nat.le_refl _) (CMRA.validN_succ Hx')

instance : OFE.NonExpansive (BUpd.bupd (PROP := UPred M)) := bupd_ne

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)

instance instOFE [Store T K V] [OFE V] : OFE T where
  Equiv s0 s1  := get s0 ≡ get s1
  Dist n s0 s1 := get s0 ≡{n}≡ get s1
  dist_eqv     := ⟨fun _ => .of_eq rfl, (·.symm), (·.trans ·)⟩
  equiv_dist   := equiv_dist
  dist_lt      := dist_lt

instance get_ne [Store T K V] [OFE V] (k : K) : NonExpansive (get · k : T → V) where
  ne {_ _ _} Ht := Ht k

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

instance [Store T1 K V1] [Store T2 K V2] [OFE V1] [OFE V2] (f : K → V1 → V2)
  [∀ k, NonExpansive (f k)] [HasStoreMap T1 T2 K V1 V2] : NonExpansive (dmap f : T1 → T2) where
  ne _ {_ _} H k := by admit /- proof elided -/

instance Heap.instCOFE [Heap T K V] [COFE V] : COFE T where
  compl c := hmap (fun _ => COFE.compl <| c.map ⟨_, Store.get_ne ·⟩) (c 0)
  conv_compl {_ c} k := by admit /- proof elided -/

class BIUpdate (PROP : Type _) [BI PROP] extends BUpd PROP where
  [bupd_ne : OFE.NonExpansive (BUpd.bupd (PROP := PROP))]
  intro {P : PROP} : iprop(P ⊢ |==> P)
  mono {P Q : PROP} : iprop(P ⊢ Q) → iprop(|==> P ⊢ |==> Q)
  trans {P : PROP} : iprop(|==> |==> P ⊢ |==> P)
  frame_r {P R : PROP} : iprop((|==> P) ∗ R ⊢ |==> (P ∗ R))

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

instance : OFE.Discrete (DFrac F) := ⟨congrArg id⟩

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₂

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

class UCMRA (α : Type _) extends CMRA α where
  unit : α
  unit_valid : ✓ unit
  unit_left_id : unit • x ≡ x
  pcore_unit : pcore unit ≡ some unit

instance : NonExpansive (pcore (α := α)) where
  ne n x {y} e := by admit /- proof elided -/

instance [CMRA β] : OFE (α -C> β) where
  Equiv f g := f.toHom ≡ g.toHom
  Dist n f g := f.toHom ≡{n}≡ 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

def bupd (Q : UPred M) : UPred M where
  holds n x := ∀ k yf, k ≤ n → ✓{k} (x • yf) → ∃ x', ✓{k} (x' • yf) ∧ Q k x'
  mono {n1 n2} {x1 x2} HQ := by admit /- proof elided -/

inductive Excl α where
  | excl : α → Excl α
  | invalid : Excl α

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

class BIBase (PROP : Type u) where
  Entails : PROP → PROP → Prop
  emp : PROP
  pure : Prop → PROP
  and : PROP → PROP → PROP
  or : PROP → PROP → PROP
  imp : PROP → PROP → PROP
  sForall : (PROP → Prop) → PROP
  sExists : (PROP → Prop) → PROP
  sep : PROP → PROP → PROP
  wand : PROP → PROP → PROP
  persistently : PROP → PROP
  later : PROP → PROP

class Store (T : Type _) (K V : outParam (Type _)) where
  get : T → K → V
  set : T → K → V → T
  get_set_eq {t k k' v} : k = k' → get (set t k v) k' = v
  get_set_ne {t k k' v} : k ≠ k' → get (set t k v) k' = get t k'

instance intoWand_intuitionistically_wand (p : Bool) [BI PROP] (P Q : PROP) :
    IntoWand p true iprop(□ P -∗ Q) P Q where
  into_wand := intuitionisticallyIf_elim

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

instance [OFE α] [OFE.Discrete α] : OFE.Discrete (Option α) where
  discrete_0 {mx my} e :=
    match mx, my with
    | none,   none   => e
    | none,   some _ => e
    | some _, none   => e
    | some x, some y => show x ≡ y from discrete_0 e

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

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

partial def unpackIprop [Monad m] [MonadRef m] [MonadQuotation m] : Term → m Term
  | `(iprop($P))             => do `($P)
  | `($P:ident)              => do `($P)
  | `(?$P:ident)             => do `(?$P)
  | `(($P))                  => do `(($(← unpackIprop P)))
  | `($P $[ $Q]*)            => do ``($P $[ $Q]*)
  | `(if $c then $t else $e) => do
    let t ← unpackIprop t
    let e ← unpackIprop e
    `(if $c then $t else $e)
  | `(($P : $t))             => do ``(($(← unpackIprop P) : $t))
  | `($t)                    => `($t:term)

@[simp] instance : COFE (DFrac F) := COFE.ofDiscrete _ Eq_Equivalence

private def matchAlts' := leading_parser matchAlts

structure RemoveHyp {prop : Q(Type u)} (bi : Q(BI $prop)) (e : Q($prop)) where
  (e' : Q($prop)) (hyps' : Hyps bi e') (out out' : Q($prop)) (p : Q(Bool))
  (eq : $out =Q iprop(□?$p $out'))
  (pf : Q($e ⊣⊢ $e' ∗ $out))
  deriving Inhabited

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

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

inductive ReplaceHyp {prop : Q(Type u)} (bi : Q(BI $prop)) (Q : Q($prop)) where
  | none
  | unchanged (ehyps') (hyps' : Hyps bi ehyps')
  | main (e e' : Q($prop)) (hyps' : Hyps bi e') (pf : Q(Replaces $Q $e $e'))

class FromAffinely [BI PROP] (P : outParam PROP) (Q : PROP) (p : Bool := true) where
  from_affinely : <affine>?p Q ⊢ P

instance [BI PROP] : Idempotent (α := PROP) BiEntails or := ⟨or_self⟩

instance : CMRA (Agree α) where
  pcore := some
  op := Agree.op
  ValidN := Agree.validN
  Valid := Agree.valid

Lean.MonadRef in Init.Prelude

instance intoWand_and_r (p q : Bool) [BI PROP] (R1 R2 P' Q' : PROP)
    [h : IntoWand p q R2 Q' P'] : IntoWand p q iprop(R1 ∧ R2) Q' P' where
  into_wand := (intuitionisticallyIf_mono and_elim_r).trans h.1

private def getMonotonicityRules : TacticM <| Array Name := do
  return monoRulesExt.getState (← getEnv) |>.toArray

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

abbrev FF1 : GFunctors := #[COFE.constOF (Agree (LeibnizO String))]

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

instance instA (n) : COFE (A F n) := (A' F n).2

instance (priority := default - 50) fromAffinely_affinely [BI PROP] (P : PROP) :
    FromAffinely iprop(<affine> P) P true := ⟨.rfl⟩

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 _

macro:max "iprop(" P:term " : " t:term ")" : term => `((iprop($P) : $t))

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

inductive iCasesPat
  | one (name : TSyntax ``binderIdent)
  | clear
  | conjunction (args : List iCasesPat)
  | disjunction (args : List iCasesPat)
  | pure           (pat : iCasesPat)
  | intuitionistic (pat : iCasesPat)
  | spatial        (pat : iCasesPat)
  deriving Repr, Inhabited

def Agree.valid (x : Agree α) : Prop := ∀ n, x.validN n

instance exclusive_cancelable {x : α} [Exclusive x] : Cancelable x where
  cancelableN v _ := absurd v not_valid_exclN_op_left

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

Lean.Expr.fvar in Lean.Expr

Qq.elabTermEnsuringTypeQ in Qq.MetaM

instance or_persistent [BI PROP] (P Q : PROP) [Persistent P] [Persistent Q] :
    Persistent iprop(P ∨ Q) where
  persistent := (or_mono persistent persistent).trans persistently_or.2

| .intuitionistic arg =>
    iCasesIntuitionistic bi P Q A' p fun B' =>
      iCasesCore hyps Q q(true) q(iprop(□ $B')) B' ⟨⟩ arg @k

def Hyps.remove {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
    (rp : Bool) (hyps : Hyps bi e) (uniq : Name) : RemoveHyp bi e :=
  match Id.run (hyps.removeG rp fun _ uniq' _ _ => if uniq == uniq' then some () else none) with
  | some (_, r) => r
  | none => panic! "variable not found"

def Disjoint (x y : Set α) : Prop := ∀ a, ¬(x a ∧ y a)

Option.elim in Init.Data.Option.Basic

def selectHyp (ty : Expr) : ∀ {s}, @Hyps u prop bi s → MetaM (Name × Q(Bool) × Q($prop))
  | _, .emp _ => failure
  | _, .hyp _ _ uniq p ty' _ => do
    let .true ← isDefEq ty ty' | failure
    pure (uniq, p, ty')
  | _, .sep _ _ _ _ lhs rhs => try selectHyp ty rhs catch _ => selectHyp ty lhs

def downN {k} : ∀ n, A F (k + n) -n> A F k
  | 0 => .id
  | n+1 => (downN n).comp (down F (k + n))

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

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

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

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

instance intoAnd_pure (p : Bool) (φ ψ : Prop) [BI PROP] :
    IntoAnd (PROP := PROP) p iprop(⌜φ ∧ ψ⌝) iprop(⌜φ⌝) iprop(⌜ψ⌝) where
  into_and := intuitionisticallyIf_mono pure_and.2

semiOutParam in Init.Prelude

-- A proof with no resources
example (P Q : IProp FF0) : P ∗ Q ⊢ ⌜True⌝ :=

class AsEmpValid1 (φ : semiOutParam Prop) {PROP : Type _} (P : PROP) [BI PROP] where
  as_emp_valid : φ ↔ ⊢ P

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 emp_persistent [BI PROP] : Persistent (PROP := PROP) iprop(emp) where
  persistent := persistently_emp_intro

instance (priority := default + 20) intoAbsorbingly_absorbing [BI PROP] (P : PROP) [Absorbing P] :
    IntoAbsorbingly P P where
  into_absorbingly := absorbing_absorbingly.2

Lean.KVMap in Lean.Data.KVMap

abbrev IProp := UPred (IResUR FF)

instance intoOr_affinely [BI PROP] (P Q1 Q2 : PROP) [h : IntoOr P Q1 Q2] :
    IntoOr iprop(<affine> P) iprop(<affine> Q1) iprop(<affine> Q2) where
  into_or := (affinely_mono h.1).trans affinely_or.1

instance sep_absorbing_r [BI PROP] (P Q : PROP) [Absorbing Q] : Absorbing iprop(P ∗ Q) where
  absorbing := absorbingly_sep_r.2.trans (sep_mono_r absorbing)

instance : Disjoint (State Val) where
  disjoint a b := ∀ i, a i = unknown ∨ b i = unknown

protected def eq [OFE O] (o1 o2 : O) : UPred M where
  holds n _ := o1 ≡{n}≡ o2
  mono H1 _ H2 := H1.le H2

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

Array in Init.Prelude

instance OFunctor.constOF_RFunctorContractive [CMRA B] :
    RFunctorContractive (COFE.constOF B) where
  map_contractive.1 := by admit /- proof elided -/

LE in Init.Prelude

instance [OFE α] {P : α → Prop} : OFE { x : α // P x } where
  Equiv := (·.val ≡ ·.val)
  Dist n := (·.val ≡{n}≡ ·.val)
  dist_eqv := {
    refl x := dist_eqv.refl x.val
    symm H := H.symm
    trans H1 H2 := H1.trans H2
  }
  equiv_dist := equiv_dist
  dist_lt := dist_lt

Qq.push in Qq.Match

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

instance (priority := default + 20) intoPersistently_affinely (p : Bool) [BI PROP] (P Q : PROP)
    [h : IntoPersistently p P Q] : IntoPersistently p iprop(<affine> P) Q where
  into_persistently := (persistentlyIf_mono affinely_elim).trans h.1

def isplitCore (side : splitSide) (names : Array (TSyntax `ident)) : TacticM Unit := do
  let splitRight := match side with
    | .splitLeft => false
    | .splitRight => true

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

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

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)

class AllocHeap (T : Type _) (K V : outParam (Type _)) extends Heap T K V where
  notFull : T → Prop
  fresh {t : T} : notFull t → K
  get_fresh {H : notFull t} : get t (fresh H) = none

instance forall_persistent [BI PROP] [BIPersistentlyForall PROP] (Ψ : α → PROP)
    [h : ∀ x, Persistent (Ψ x)] : Persistent iprop(∀ x, Ψ x) :=
  sForall_persistent _ fun _ ⟨_, eq⟩ => eq ▸ h _

def withFocus (goal : MVarId) (f : TacticM α) : TacticM α := do
  let goals ← getUnsolvedGoals
  setGoals [goal]
  let result ← f
  setGoals <| goals ++ (← getUnsolvedGoals)
  return result

instance : Inhabited (DFrac F) := ⟨discard⟩

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

instance and_absorbing [BI PROP] (P Q : PROP) [Absorbing P] [Absorbing Q] :
    Absorbing iprop(P ∧ Q) where
  absorbing := absorbingly_and_1.trans (and_mono absorbing absorbing)

local instance : IsGFunctors FF0 := nofun

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 [BI PROP] : LeftId (α := PROP) BiEntails iprop(True) and := ⟨true_and⟩

if A.isAppOfArity ``intuitionistically 3 then
      have A' : Q($prop) := A.appArg!
      have : $A =Q iprop(□ $A') := ⟨⟩
      have : Q(IntoPure $A' $φ) := inst
      pure (a, q(pure_elim_intuitionistic $pf $f))
    else
      let _ ← synthInstanceQ q(TCOr (Affine $A) (Absorbing $Q))
      have : Q(IntoPure $A $φ) := inst
      pure (a, q(pure_elim_spatial $pf $f))

partial def parseHyps? {prop : Q(Type u)} (bi : Q(BI $prop)) (expr : Expr) :
    Option ((s : Q($prop)) × Hyps bi s) := do
  if let some #[_, _, P, Q] := appM? expr ``sep then
    let ⟨elhs, lhs⟩ ← parseHyps? bi P
    let ⟨erhs, rhs⟩ ← parseHyps? bi Q
    some ⟨q(BI.sep $elhs $erhs), .sep expr elhs erhs ⟨⟩ lhs rhs⟩
  else if expr.isAppOfArity ``emp 2 then
    some ⟨expr, .emp ⟨⟩⟩
  else if let some #[_, _, P] := appM? expr ``intuitionistically then
    let (name, uniq, (ty : Q($prop))) ← parseName? P
    some ⟨q(iprop(□ $ty)), .hyp expr name uniq q(true) ty ⟨⟩⟩
  else
    let (name, uniq, ty) ← parseName? expr
    some ⟨ty, .hyp expr name uniq q(false) ty ⟨⟩⟩

False.elim in Init.Prelude

instance fromOr_intuitionistically [BI PROP] (P Q1 Q2 : PROP) [h : FromOr P Q1 Q2] :
    FromOr iprop(□ P) iprop(□ Q1) iprop(□ Q2) where
  from_or := intuitionistically_or.2.trans (intuitionistically_mono h.1)

def unexpand : Lean.PrettyPrinter.Unexpander
          $[| $p => $s]*)
    else
      `(@[app_unexpander $(mkIdent f)]

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

instance : COFE Unit where
  compl _ := ()
  conv_compl := ⟨⟩

instance fromPure_pure_sep_true (a1 a2 : Bool) (φ1 φ2 : Prop) [BI PROP] (P1 P2 : PROP)
    [h1 : FromPure a1 P1 φ1] [h2 : FromPure a2 P2 φ2] :
    FromPure (a1 && a2) iprop(P1 ∗ P2) (φ1 ∧ φ2) where
  from_pure := by admit /- proof elided -/

partial def iIntroCore
    {P} (hyps : Hyps bi P) (Q : Q($prop)) (pats : List iCasesPat)
    (k : ∀ {P}, Hyps bi P → (Q : Q($prop)) → MetaM Q($P ⊢ $Q)) :
    MetaM (Q($P ⊢ $Q)) := do
  match pats with
  | [] => k hyps Q
  | pat :: pats =>
    let A1 ← mkFreshExprMVarQ q($prop)
    let A2 ← mkFreshExprMVarQ q($prop)
    let fromImp ← try? (α := Q(FromImp $Q $A1 $A2)) do
      synthInstanceQ q(FromImp $Q $A1 $A2)
    if let (.clear, some _) := (pat, fromImp) then
      let pf ← iIntroCore hyps A2 pats k
      return q(imp_intro_drop (Q := $Q) $pf)
    else
    let alres ← try? (α := _ × (v : Level) × (α : Q(Sort v)) × (Φ : Q($α → $prop)) ×
        Q(FromForall $Q $Φ)) do
      let .one n := pat | failure
      let v ← mkFreshLevelMVar
      let α ← mkFreshExprMVarQ q(Sort v)
      let Φ ← mkFreshExprMVarQ q($α → $prop)
      Pure.pure ⟨n, v, α, Φ, ← synthInstanceQ q(FromForall $Q $Φ)⟩
    if let some ⟨n, _, α, Φ, _⟩ := alres then
      let (n, ref) ← getFreshName n
      withLocalDeclDQ n α fun x => do
        addLocalVarInfo ref (← getLCtx) x α
        have B : Q($prop) := Expr.headBeta q($Φ $x)
        have : $B =Q $Φ $x := ⟨⟩
        let pf : Q(∀ x, $P ⊢ $Φ x) ← mkLambdaFVars #[x] <|← iIntroCore hyps B pats k
        return q(from_forall_intro (Q := $Q) $pf)
    else
    let B ← mkFreshExprMVarQ q($prop)
    match pat, fromImp with
    | .intuitionistic pat, some _ =>
      let _ ← synthInstanceQ q(IntoPersistently false $A1 $B)
      let pf ← iCasesCore bi hyps A2 q(true) q(iprop(□ $B)) B ⟨⟩ pat (iIntroCore · A2 pats k)
      return q(imp_intro_intuitionistic (Q := $Q) $pf)
    | .intuitionistic pat, none =>
      let _ ← synthInstanceQ q(FromWand $Q $A1 $A2)
      let _ ← synthInstanceQ q(IntoPersistently false $A1 $B)
      let _ ← synthInstanceQ q(TCOr (Affine $A1) (Absorbing $A2))
      let pf ← iCasesCore bi hyps A2 q(true) q(iprop(□ $B)) B ⟨⟩ pat (iIntroCore · A2 pats k)
      return q(wand_intro_intuitionistic (Q := $Q) $pf)
    | _, some _ =>
      let _ ← synthInstanceQ q(FromAffinely $B $A1)
      let _ ← synthInstanceQ q(TCOr (Persistent $A1) (Intuitionistic $P))
      let pf ← iCasesCore bi hyps A2 q(false) B B ⟨⟩ pat (iIntroCore · A2 pats k)
      return q(imp_intro_spatial (Q := $Q) $pf)
    | _, none =>
      let _ ← synthInstanceQ q(FromWand $Q $A1 $A2)
      let pf ← iCasesCore bi hyps A2 q(false) A1 A1 ⟨⟩ pat (iIntroCore · A2 pats k)
      return q(wand_intro_spatial (Q := $Q) $pf)

structure PMTerm where
  term : Term
  terms : List Term
  spats : List SpecPat
  deriving Repr, Inhabited

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

instance fromPure_pure_wand_false (φ1 φ2 : Prop) [BI PROP] (P1 P2 : PROP)
    [h1 : IntoPure P1 φ1] [h2 : FromPure false P2 φ2] :
    FromPure false iprop(P1 -∗ P2) (φ1 → φ2) where
  from_pure := by admit /- proof elided -/

Lean.Parser.Term.matchAlts in Lean.Parser.Term

k in QqTest.matching
</all_available_defs>

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

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

theorem some_op_opM {a : α} {ma : Option α} : some a • ma = some (a •? ma)

theorem «exists» [BI PROP] (Q : Nat → PROP) : (∃ x, Q x) ⊢ ∃ x, Q x ∨ False

theorem Agree.toAgree_op_valid_iff_equiv {a : α} : ✓ (toAgree a • toAgree b) ↔ a ≡ b

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

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

theorem excl_includedN [OFE α] {x y : Excl α} (n) : x ≼{n} y ↔ y = invalid

theorem exists_intro' [BI PROP] {P : PROP} {Ψ : α → PROP} (a : α) (h : P ⊢ Ψ a) : P ⊢ ∃ a, Ψ a

theorem LocalUpdate.prod {x y x' y' : α × β}
    (hl : (x.1, y.1) ~l~> (x'.1, y'.1)) (hr : (x.2, y.2) ~l~> (x'.2, y'.2)) :
    (x, y) ~l~> (x', y')

theorem later_exists [BI PROP] [Inhabited α] {Φ : α → PROP} :
    (∃ a, ▷ Φ a) ⊣⊢ ▷ (∃ a, Φ a)

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

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 persistently_affinely [BI PROP] {P : PROP} : <pers> <affine> P ⊣⊢ <pers> P

protected theorem Tower.upN (X : Tower F) : ∀ i, upN F i (X (k+1)) ≡{k}≡ X (k+1+i)

theorem DFrac.is_discrete {q : DFrac F} : OFE.DiscreteE q

theorem plainly_entails_r (H : P ⊢ ■ Q) : P ⊢ P ∗ ■ Q

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

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

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

theorem intuitionisticallyIf_comm' {p q : Bool} [BI PROP] {P : PROP} :
    □?p □?q P ⊣⊢ □?q □?p P

theorem impl_wand_plainly_2 : (■ P -∗ Q) ⊢ (■ P → Q)

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

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

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

theorem DistLater.dist_lt [OFE α] {m n} {x y : α} (h : DistLater n x y) (hm : m < n) : x ≡{m}≡ y

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

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

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

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

theorem UpdateP.total [CMRA.IsTotal α] :
    x ~~>: P ↔ ∀ (n : Nat) (z : α), ✓{n} (x • z) → ∃ y, P y ∧ ✓{n} (y • z)

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

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

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

theorem Heap.point_get_ne [Heap T K V] (H : k ≠ k') : get (point k v : T) k' = none

theorem true_intro [BI PROP] {P : PROP} : P ⊢ True

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

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

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

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

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

theorem plainly_sep_2 : ■ P ∗ ■ Q ⊢ ■ (P ∗ Q)

theorem simple [BI PROP] : ⊢ (emp : PROP)

@[simp] theorem not_none_eqv_some [OFE α] {x : α} : ¬none ≡ some x

theorem cmra_cmraValid_weaken [CMRA A] (a b : A) :
    (cmraValid (a • b) : UPred M) ⊢ cmraValid a

theorem op_core_left_of_inc {x y : α} [CoreId x] (le : x ≼ y) : y • x ≡ y

theorem exclusive_iff {x₁ x₂ : α} (e : x₁ ≡ x₂) : Exclusive x₁ ↔ Exclusive x₂

theorem set_validN {m : T} (Hx : ✓{n} x) (Hm : ✓{n} m) : ✓{n} (set m i x)

theorem UpdateP.trans {x : α} (ux : x ~~>: P) (upq : ∀ y, P y → y ~~>: Q) : x ~~>: Q

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

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

theorem disjoint_union {a b c : State Val} : a |

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

theorem op_some_opM_assoc_dist {x y : α} {mz : Option α} : (x • y) •? mz ≡{n}≡ x •? (some y • mz)

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

theorem intuitionisticallyIf_emp {p : Bool} [BI PROP] : (□?p emp : PROP) ⊣⊢ emp

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

theorem intuitionisticallyIf_or (p : Bool) [BI PROP] {P Q : PROP} : □?p (P ∨ Q) ⊣⊢ □?p P ∨ □?p Q

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

theorem bigOp_and_cons [BI PROP] {P : PROP} {Ps : List PROP} :
    [∧] (P :: Ps) ⊣⊢ P ∧ [∧] Ps

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

theorem core_eq_self {x : α} [IsTotal α] [c : CoreId x] : core x = x

theorem UpdateP.option' (P : α → Prop) (x : α) (uxp : x ~~>: P) : some x ~~>: Option.rec False P

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

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

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

theorem local_update_unital {x y x' y' : α} :
    (x, y) ~l~> (x', y') ↔ ∀ n z, ✓{n} x → x ≡{n}≡ y • z → (✓{n} x' ∧ x' ≡{n}≡ y' • z)

theorem from_or_l [BI PROP] {P Q A1 A2 : PROP} [inst : FromOr Q A1 A2]
    (h1 : P ⊢ A1) : P ⊢ Q

theorem op_opM_assoc_dist (x y : α) (mz : Option α) : (x • y) •? mz ≡{n}≡ x • (y •? mz)

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

theorem and_elim_r_spatial [BI PROP] {P A Q A1 A2 : PROP} [IntoAnd false A A1 A2]
    (h : P ∗ A2 ⊢ Q) : P ∗ A ⊢ Q

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

theorem persistently_elim_plainly : <pers> ■ P ⊣⊢ ■ P

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

theorem empty_union {s : State Val} : s = ∅ ∪ s

theorem pure_elim_intuitionistic [BI PROP] {P P' A Q : PROP} {φ : Prop}
    [IntoPure A φ] (h : P ⊣⊢ P' ∗ □ A) (h' : φ → P' ⊢ Q) : P ⊢ Q

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

theorem persistently_iff [BI PROP] {P : PROP} [Persistent P] [Absorbing P] :
    <pers> P ⊣⊢ P

theorem _root_.Iris.OFE.Dist.opM {x₁ x₂ : α} {y₁ y₂ : Option α}
    (H1 : x₁ ≡{n}≡ x₂) (H2 : y₁ ≡{n}≡ y₂) : x₁ •? y₁ ≡{n}≡ x₂ •? y₂

theorem disjoint_assoc {a b c : State Val} : a ∪ b |

theorem incN_unit {n} {x : α} : unit ≼{n} x

theorem absorbingly_elim_plainly : <absorb> ■ P ⊣⊢ ■ P

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

theorem pure_intro_affine [BI PROP] {Q : PROP} {φ : Prop}
    [h : FromPure true Q φ] [Affine P] (hφ : φ) : P ⊢ Q

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

theorem inc_of_inc_of_eqv : (a : α) ≼ b → b ≡ c → a ≼ c

theorem bigOp_cons {f : PROP → PROP → PROP} {unit : PROP} [LawfulBigOp f unit eq] :
    eq (bigOp f unit (P :: Ps)) (f P (bigOp f unit Ps))

theorem comm_L {x y : α} : x • y = y • x

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

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

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

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

theorem and_sep_intuitionistically [BI PROP] {P Q : PROP} : □ P ∧ □ Q ⊣⊢ □ P ∗ □ Q

theorem pcore_monoN' {n} {x y : α} {cx} :
    x ≼{n} y → pcore x ≡{n}≡ some cx → ∃ cy, pcore y = some cy ∧ cx ≼{n} cy

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

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

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

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

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

theorem excl_map_compose (f : α → β) (g : β → γ) :
    map (g ∘ f) x = map g (map f x)

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

theorem later_affine [BI PROP] [BIAffine PROP] (P Q : PROP) : ⊢ (▷ P → Q) -∗ P -∗ Q

theorem eqToHom_up {k k'} {x : A F k} (e : k = k') :
    eqToHom (congrArg Nat.succ e) (up F k x) = up F k' (eqToHom e x)

@[simp] theorem Hom.id_comp [OFE α] [OFE β] {f : α -n> β} : Hom.id.comp f = f

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

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

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

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

theorem valid_own_op_discard {q : F} : ✓ own q • discard ↔ Fractional q

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

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

theorem or_mono_r [BI PROP] {P Q Q' : PROP} (h : Q ⊢ Q') : 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 affinelyIf_idem {p : Bool} [BI PROP] [BIPositive PROP] {P : PROP} :
    <affine>?p <affine>?p P ⊣⊢ <affine>?p P

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

theorem lookup_inc {m1 m2 : T} :
    (∃ (z : T), m2 ≡ op m1 z) ↔
    ∀ i, (∃ z, (get m2 i) ≡ (get m1 i) • z)

theorem inc_refl (x : α) : x ≼ x

theorem LocalUpdate.prod_2 (x1 y1 : α) {x2 y2 x2' y2' : β}
    (h : (x2, y2) ~l~> (x2', y2')) : ((x1, x2), (y1, y2)) ~l~> ((x1, x2'), (y1, y2'))

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

theorem pure_wand [BI PROP] {φ1 φ2 : Prop} : (⌜φ1⌝ -∗ (⌜φ2⌝ : PROP)) ⊣⊢ ⌜φ1 → φ2⌝

theorem plainly_forall_2 {Ψ : α → PROP} : (∀ a, ■ (Ψ a)) ⊢ ■ (∀ a, Ψ a)

theorem UpdateP.id {P : α → Prop} {x} (h : P x) : x ~~>: P

theorem persistent_and_sep_1 [BI PROP] {P Q : PROP} :
    [TCOr (Persistent P) (Persistent Q)] → P ∧ Q ⊢ P ∗ Q

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

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

theorem or_emp [BI PROP] {P : PROP} [Affine P] : P ∨ emp ⊣⊢ emp

theorem validN_op_opM_left {mz : Option α} : ✓{n} (x • y : α) •? mz → ✓{n} x •? mz

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

theorem ownM_valid (m : M) : ownM m ⊢ cmraValid m

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

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

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

theorem def_eq [BI PROP] (Q : PROP) : <affine> <pers> Q ⊢ □ Q

theorem op_core_right_of_inc {x y : α} [CoreId x] : x ≼ y → x • y ≡ y

theorem later_absorbingly [BI PROP] {P : PROP} : ▷ <absorb> P ⊣⊢ <absorb> ▷ P

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

theorem spatial [BI PROP] (Q : PROP) : <affine> P ⊢ Q -∗ Q

theorem Iso.hom_eqv [OFE α] [OFE β] (iso : Iso α β) ⦃x y⦄ :
    x ≡ y ↔ iso.hom x ≡ iso.hom y

theorem and_false [BI PROP] {P : PROP} : P ∧ False ⊣⊢ False

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

theorem included_dist_l {n} {x1 x2 x1' : α} :
    x1 ≼ x2 → x1' ≡{n}≡ x1 → ∃ x2', x1' ≼ x2' ∧ x2' ≡{n}≡ x2

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

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

theorem op_monoN {n} {x x' y y' : α} (hx : x ≼{n} x') (hy : y ≼{n} y') : x • y ≼{n} x' • y'

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

theorem id [BI PROP] : ⊢ (∃ x, x : PROP)

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

theorem lt_trans {a b c : α} : a < b → b < c → a < c

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

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

theorem Agree.validN_def {x : Agree α} : ✓{n} x ↔ x.validN n

theorem intuitionistically_sep_idem [BI PROP] {P : PROP} : □ P ∗ □ P ⊣⊢ □ P

theorem multiple_intuitionistic [BI PROP] (P Q R : PROP) : ⊢ □ P -∗ Q -∗ □ (P -∗ Q -∗ □ R) -∗ R
</all_available_lemmas>

<local_ctx>
namespace Iris

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

open OFE

scoped infix:40 " ≡ " => OFE.Equiv

scoped notation:40 x " ≡{" n "}≡ " y:41 => OFE.Dist n x y

namespace OFE

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

instance id_ne [OFE α] : NonExpansive (@id α) := ⟨fun _ _ _ h => h⟩

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₂

def DistLater [OFE α] (n : Nat) (x y : α) : Prop := ∀ m, m < n → x ≡{m}≡ y

class Contractive [OFE α] [OFE β] (f : α → β) where
  distLater_dist : DistLater n x y → f x ≡{n}≡ f y

instance ne_of_contractive [OFE α] [OFE β] (f : α → β) [Contractive f] : NonExpansive f where
  ne := fun _ _ _ h => Contractive.distLater_dist (Dist.distLater h)

instance [OFE α] [OFE β] {x : β} : Contractive (fun _ : α => x) where
  distLater_dist := fun _ => Dist.rfl

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

@[inherit_doc]
infixr:25 " -n> " => Hom

instance [OFE α] [OFE β] (f : α -n> β) : NonExpansive f := f.ne

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

infixr:25 " -c> " => ContractiveHom

instance [OFE α] [OFE β] (f : α -c> β) : Contractive f := f.contractive

instance : OFE Unit where
  Equiv _ _ := True
  Dist _ _ _ := True
  dist_eqv := ⟨fun _ => ⟨⟩, id, fun _ => id⟩
  equiv_dist := by admit /- proof elided -/

instance [OFE α] : OFE (ULift α) where
  Equiv x y := x.down ≡ y.down
  Dist n x y := x.down ≡{n}≡ y.down
  dist_eqv := InvImage.equivalence dist_eqv
  equiv_dist := equiv_dist
  dist_lt := dist_lt

instance [OFE α] : OFE (Option α) where
  Equiv := Option.Forall₂ Equiv
  Dist n := Option.Forall₂ (Dist n)
  dist_eqv := Option.Forall₂.equivalence dist_eqv
  equiv_dist {x y} := by admit /- proof elided -/

instance [OFE α] [OFE.Discrete α] : OFE.Discrete (Option α) where
  discrete_0 {mx my} e :=
    match mx, my with
    | none,   none   => e
    | none,   some _ => e
    | some _, none   => e
    | some x, some y => show x ≡ y from discrete_0 e

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 [OFEFun (β : α → _)] : OFE ((x : α) → β x) where
  Equiv f g := ∀ x, f x ≡ g x
  Dist n f g := ∀ x, f x ≡{n}≡ g x
  dist_eqv := {
    refl _ _ := dist_eqv.refl _
    symm h _ := dist_eqv.symm (h _)
    trans h1 h2 _ := dist_eqv.trans (h1 _) (h2 _)
  }
  equiv_dist {_ _} := by admit /- proof elided -/

instance [OFE α] [OFE β] : OFE (α -n> β) where
  Equiv f g := f.f ≡ g.f
  Dist n f g := f.f ≡{n}≡ g.f
  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 [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 [OFE α] [OFE β] : OFE (α × β) where
  Equiv a b := a.1 ≡ b.1 ∧ a.2 ≡ b.2
  Dist n a b := a.1 ≡{n}≡ b.1 ∧ a.2 ≡{n}≡ b.2
  dist_eqv := {
    refl _ := ⟨dist_eqv.refl _, dist_eqv.refl _⟩
    symm h := ⟨dist_eqv.symm h.1, dist_eqv.symm h.2⟩
    trans h1 h2 := ⟨dist_eqv.trans h1.1 h2.1, dist_eqv.trans h1.2 h2.2⟩
  }
  equiv_dist {_ _} := by admit /- proof elided -/

@[ext] structure Iso (α β : Type _) [OFE α] [OFE β] where
  hom : α -n> β
  inv : β -n> α
  hom_inv : hom (inv x) ≡ x
  inv_hom : inv (hom x) ≡ x

instance [OFE α] [OFE β] (iso : Iso α β) : NonExpansive iso.hom := iso.hom.ne

instance [OFE α] [OFE β] (iso : Iso α β) : NonExpansive iso.inv := iso.inv.ne

def Iso.symm [OFE α] [OFE β] (iso : Iso α β) : Iso β α where
  hom := iso.inv
  inv := iso.hom
  hom_inv := by admit /- proof elided -/

end OFE

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

namespace Chain

end Chain

class IsCOFE (α : Type _) [OFE α] where
  compl : Chain α → α
  conv_compl {c : Chain α} : compl c ≡{n}≡ c n

namespace COFE

end COFE

@[ext] structure LeibnizO (α : Type _) where
  car : α

section DiscreteFunOF

open COFE

end DiscreteFunOF

section Option

variable [OFE α]

def optionChain (c : Chain (Option α)) (x : α) : Chain α :=

instance isCOFE_option [IsCOFE α] : IsCOFE (Option α) where
  compl c := (c 0).map fun x => IsCOFE.compl (optionChain c x)
  conv_compl {n} c := by admit /- proof elided -/

end Option

section OptionOF

open COFE

variable (F : OFunctorPre)

end OptionOF

section Fixpoint

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

def fixpoint [COFE α] [Inhabited α] (f : α → α) [Contractive f] : α :=
  COFE.compl <| Fixpoint.chain f

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

<target_theorem>
theorem fixpoint_unfold [COFE α] [Inhabited α] (f : α -c> α) :
    fixpoint f ≡ f (fixpoint f) :=
</target_theorem>

