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 liftRel (R : α → β → Prop) (A : α → Prop) (B : β → Prop) : Prop :=
  (∀ a, A a → ∃ b, B b ∧ R a b) ∧ (∀ b, B b → ∃ a, A a ∧ R a b)

class BI (PROP : Type _) extends COFE PROP, BI.BIBase PROP where
  Equiv P Q := P ⊣⊢ Q

entails_preorder : Preorder Entails
  equiv_iff {P Q : PROP} : (P ≡ Q) ↔ P ⊣⊢ Q := by admit /- proof elided -/

abbrev Relation (α : Type _) := α → α → Prop

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 Preorder (R : Relation α) extends Reflexive R, Transitive R

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

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

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

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

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

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

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

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

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

class BIPositive (PROP : Type _) [BI PROP] where
  affinely_sep_l {P Q : PROP} : <affine> (P ∗ Q) ⊢ <affine> P ∗ Q

class Affine [BI PROP] (P : PROP) where
  affine : P ⊢ emp

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

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

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

macro "∃" xs:explicitBinders ", " b:term : term => do
  return ⟨← expandExplicitBinders ``BIBase.exists xs b⟩

def wandIff [BIBase PROP] (P Q : PROP) : PROP := iprop((P -∗ Q) ∧ (Q -∗ P))

def affinely    [BIBase PROP] (P : PROP) : PROP := iprop(emp ∧ P)

def absorbingly [BIBase PROP] (P : PROP) : PROP := iprop(True ∗ P)

structure BiEntails [BIBase PROP] (P Q : PROP) where
  mp : P ⊢ Q
  mpr : Q ⊢ P

macro:25 P:term:29 " ⊣⊢ " Q:term:29 : term => ``(BiEntails iprop($P) iprop($Q))

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

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

def intuitionistically [BIBase PROP] (P : PROP) : PROP := iprop(<affine> <pers> P)

def persistentlyIf [BIBase PROP] (p : Bool) (P : PROP) : PROP := iprop(if p then <pers> P else P)

def affinelyIf [BIBase PROP] (p : Bool) (P : PROP) : PROP := iprop(if p then <affine> P else P)

def absorbinglyIf [BIBase PROP] (p : Bool) (P : PROP) : PROP := iprop(if p then <absorb> P else P)

def intuitionisticallyIf [BIBase PROP] (p : Bool) (P : PROP) : PROP := iprop(if p then □ P else P)

def bigAnd [BIBase PROP] (Ps : List PROP) : PROP := bigOp and iprop(True) Ps

def bigOr [BIBase PROP] (Ps : List PROP) : PROP := bigOp or iprop(False) Ps

def bigSep [BIBase PROP] (Ps : List PROP) : PROP := bigOp sep iprop(emp) Ps

def bigOp (f : PROP → PROP → PROP) (unit : PROP) : List PROP → PROP
  | []      => unit
  | [P]     => P
  | P :: Ps => f P (bigOp f unit Ps)

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

instance COFE.OFunctor.constOF_RFunctor [CMRA B] : RFunctor (constOF B) where
  map f g := by admit /- proof elided -/

let m1 : Q($el ⊢ $Q1) ← mkFreshExprSyntheticOpaqueMVar <|
    IrisGoal.toExpr { u, prop, bi, hyps := lhs, goal := Q1, .. }
  let m2 : Q($er ⊢ $Q2) ← mkFreshExprSyntheticOpaqueMVar <|
    IrisGoal.toExpr { u, prop, bi, hyps := rhs, goal := Q2, .. }
  mvar.assign q(sep_split (Q := $goal) $pf $m1 $m2)
  replaceMainGoal [m1.mvarId!, m2.mvarId!]

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

let ⟨el, er, lhs, rhs, pf⟩ := hyps.split bi (fun _ uniq => uniqs.contains uniq == splitRight)

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

def addHypInfo (stx : Syntax) (name uniq : Name) (prop : Q(Type u)) (ty : Q($prop))
    (isBinder := false) : MetaM Unit := do
  let lctx ← getLCtx
  let ty := q(HypMarker $ty)
  addLocalVarInfo stx (lctx.mkLocalDecl ⟨uniq⟩ name ty) (.fvar ⟨uniq⟩) ty isBinder

Lean.Expr.fvar in Lean.Expr

instance persistently_persistent [BI PROP] (P : PROP) : Persistent iprop(<pers> P) where
  persistent := persistently_idem_2

instance emp_intuitionistic [BI PROP] : Intuitionistic iprop(emp : PROP) where
  intuitionistic := intuitionistically_emp.2

instance fromExists_affinely [BI PROP] (P : PROP) (Φ : α → PROP) [h : FromExists P Φ] :
    FromExists iprop(<affine> P) (fun a => iprop(<affine> (Φ a))) where
  from_exists := affinely_exists.2.trans <| affinely_mono h.1

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

@[simp] def Excl.Valid : Excl α → Prop
  | excl _ => True
  | invalid => False

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

macro "%" pat:icasesPat : icasesPat => `(icasesPat| ⌜$pat⌝)

instance and_persistent [BI PROP] (P Q : PROP) [Persistent P] [Persistent Q] :
    Persistent iprop(P ∧ Q) where
  persistent := (and_mono persistent persistent).trans persistently_and.2

protected def Hom.comp [OFE α] [OFE β] [OFE γ] (g : β -n> γ) (f : α -n> β) : α -n> γ where
  f := g.f ∘ f.f
  ne.1 _ _ _ h := g.ne.1 (f.ne.1 h)

instance asEmpValid1_equiv [BI PROP] (P Q : PROP) : AsEmpValid1 (P ⊣⊢ Q) iprop(P ∗-∗ Q) where
  as_emp_valid := ⟨equiv_wandIff, wandIff_equiv⟩

protected def sep (P Q : UPred M) : UPred M where
  holds n x := ∃ x1 x2, x ≡{n}≡ x1 • x2 ∧ P n x1 ∧ Q n x2
  mono {n₁ n₂ m₁ m₂} := fun ⟨x₁, x₂, Hx, HP, HQ⟩ ⟨m, Hm⟩ Hn => by admit /- proof elided -/

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

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

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

@[simp] def toMap [Store T K V] [OFE V] : T -n> (K → V) where
  f x := get x
  ne.1 {_ _ _} H k := H k

def Replaces [BI PROP] (K A B : PROP) := (B -∗ K) ⊢ (A -∗ K)

@[simp] def Heap.union [Heap T K V] : T → T → T := merge (fun v _ => v)

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

def Set.univ {α : Type _} : Set α := fun _ => True

instance intoPure_affinely [BI PROP] (P : PROP) (φ : Prop)
    [h : IntoPure P φ] : IntoPure iprop(<affine> P) φ where
  into_pure := affinely_elim.trans h.1

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

Lean.mkMData in Lean.Expr

instance : CMRA.Exclusive (own (1 : F)) :=
  own_whole_exclusive <| UFraction.one_whole

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

def Store.all [Store T K V] (P : K → V → Prop) : T → Prop :=
  fun t => ∀ k, P k (get t k)

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 fromOr_or [BI PROP] (P1 P2 : PROP) : FromOr iprop(P1 ∨ P2) P1 P2 := ⟨.rfl⟩

def const [OFE α] (a : α) : Chain α where
  chain := fun _ => a
  cauchy _ := OFE.Dist.rfl

instance fromPure_persistently [BI PROP] (P : PROP) (a : Bool) (φ : Prop)
    [h : FromPure true P φ] : FromPure a iprop(<pers> P) φ where
  from_pure := affinelyIf_elim.trans <| persistently_pure.2.trans <|
    persistently_affinely.2.trans <| persistently_mono h.1

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

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

instance fromAffinely_self [BI PROP] (P : PROP) : FromAffinely P P false := ⟨.rfl⟩

Qq.push in Qq.Match

instance urFunctorOptionOF [RFunctor F] : URFunctor (OptionOF F) where
  cmra {α β} := ucmraOption
  map f g := {
    toHom := COFE.OFunctor.map f g
    validN := by admit /- proof elided -/

instance [BI PROP] [BIAffine PROP] : BIPositive PROP where
  affinely_sep_l := (affine_affinely _).1.trans (sep_mono_l (affine_affinely _).2)

@[simp] def Excl.map (f : α → β) : Excl α → Excl β
  | excl a => excl (f a)
  | invalid => invalid

class IntoOr [BI PROP] (P : PROP) (Q1 Q2 : outParam PROP) where
  into_or : P ⊢ Q1 ∨ Q2

Lean.MonadRef in Init.Prelude

instance persistently_absorbing [BI PROP] (P : PROP) : Absorbing iprop(<pers> P) where
  absorbing := absorbingly_persistently.1

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

def appM? (e : Expr) (fName : Name) : Option <| Array Expr :=
  if e.isAppOf fName then
    e.getAppArgs
  else
    none

CoeFun in Init.Coe

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

instance : BIUpdate (UPred M) where
  intro {P} _ x _ HP _ _ Hn H := ⟨_, ⟨H, P.mono HP (CMRA.incN_refl x) Hn⟩⟩
  mono Himp n x Hx HP k yf Hn H := by admit /- proof elided -/

instance [BI PROP] : LeftId (α := PROP) BiEntails iprop(False) or := ⟨false_or⟩

abbrev pcore (x : α × β) : Option (α × β) :=
  (CMRA.pcore x.fst).bind fun a =>
  (CMRA.pcore x.snd).bind fun b =>
  return (a, b)

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

def valid : DFrac F → Prop
  | .own f        => Proper f
  | .discard      => True
  | .ownDiscard f => Fractional f

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 (priority := default - 10) intoSep_affinely_trim [BI PROP] (P Q1 Q2 : PROP)
    [h : IntoSep P Q1 Q2] : IntoSep iprop(<affine> P) Q1 Q2 where
  into_sep := affinely_elim.trans h.1

Option.elim in Init.Data.Option.Basic

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

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

Id in Init.Control.Id

def Agree.op (x y : Agree α) : Agree α :=
  ⟨x.car ++ y.car, by admit /- proof elided -/
  ⟩

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

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

instance urFunctorContractiveOptionOF
    [RFunctorContractive F] : URFunctorContractive (OptionOF F) where
  map_contractive.1 := COFE.OFunctorContractive.map_contractive.1

class FromAssumption (p : Bool) [BI PROP] (P : semiOutParam PROP) (Q : PROP) where
  from_assumption : □?p P ⊢ Q

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)

abbrev γ : GId FF1 := ⟨0, Nat.zero_lt_succ _⟩

class IntoExists [BI PROP] (P : PROP) {α : outParam (Sort _)} (Φ : outParam <| α → PROP) where
  into_exists : P ⊢ ∃ x, Φ x

Union.union in Init.Core

instance {ma : Option α} [∀ a : α, IdFree a] [∀ a : α, Cancelable a] : Cancelable ma :=

instance : Inhabited (Tower F) := ⟨Tower.embed 0 ⟨()⟩⟩

instance intoWand_intuitionistically (p q : Bool) [BI PROP] (R P Q : PROP)
    [h : IntoWand true q R P Q] : IntoWand p q iprop(□ R) P Q where
  into_wand := (intuitionisticallyIf_mono h.1).trans intuitionisticallyIf_elim

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

Add in Init.Prelude

instance : BIAffine (UPred M) := ⟨by admit /- proof elided -/
⟩

private def parseRewriteRule (rule : TSyntax ``rwRule) :
    TacticM <| RewriteDirection × TSyntax `term := do
  match rule with
  | `(rwRule| ← $rule)    => pure (.reverse, rule)
  | `(rwRule| $rule:term) => pure (.forward, rule)
  | _ => throwUnsupportedSyntax

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

instance : Trans Equiv (Included (α := α)) Included where
  trans := inc_of_eqv_of_inc

instance [OFE α] : DiscreteE (@invalid α) where
  discrete {x} h := by admit /- proof elided -/

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

def goalTracker {P} (goals : IO.Ref (Array MVarId)) (name : Name) (hyps : Hyps bi P)
    (goal : Q($prop)) : MetaM Q($P ⊢ $goal) := do
  let m : Q($P ⊢ $goal) ← mkFreshExprSyntheticOpaqueMVar <|
    IrisGoal.toExpr { prop, bi, hyps, goal, .. }
  m.mvarId!.setUserName name
  goals.modify (·.push m.mvarId!)
  pure m

instance intuitionistically_persistent [BI PROP] (P : PROP) : Persistent iprop(□ P) :=
  inferInstanceAs (Persistent iprop(<affine> _))

return rule?.isNone
    else
      
      applyReflexivity goal
      return false

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

MonadExcept in Init.Prelude

@[simp] instance [NumericFraction T] : One (Frac T) := ⟨⟨One.one⟩⟩

instance or_absorbing [BI PROP] (P Q : PROP) [Absorbing P] [Absorbing Q] :
    Absorbing iprop(P ∨ Q) where
  absorbing := absorbingly_or.1.trans (or_mono absorbing absorbing)

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

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

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

instance {m : T} [∀ x : V, CoreId x] : CoreId m where
  core_id i := by admit /- proof elided -/

class IntoSep [BI PROP] (P : PROP) (Q1 Q2 : outParam PROP) where
  into_sep : P ⊢ Q1 ∗ Q2

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

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)

partial def Hyps.find? {u prop bi} (name : Name) :
    ∀ {s}, @Hyps u prop bi s → Option (Name × Q(Bool) × Q($prop))
  | _, .emp _ => none
  | _, .hyp _ name' uniq p ty _ => if name == name' then (uniq, p, ty) else none
  | _, .sep _ _ _ _ lhs rhs => rhs.find? name <|> lhs.find? name

Lean.expandMacros in Init.Meta.Defs

instance intoSep_intuitionistically_affine [BI PROP] (P Q1 Q2 : PROP) [h : IntoSep P Q1 Q2]
    [TCOr (Affine Q1) (Absorbing Q2)] [TCOr (Affine Q2) (Absorbing Q1)] :
    IntoSep iprop(□ P) iprop(□ Q1) iprop(□ Q2) where
  into_sep := (intuitionistically_mono <| h.1.trans sep_and).trans <|
    intuitionistically_and.1.trans and_sep_intuitionistically.1

instance asEmpValid2_equiv [BI PROP] (P Q : PROP) : AsEmpValid2 (P ⊣⊢ Q) iprop(P ∗-∗ Q) :=
  AsEmpValid1.to2

f₂ in QqTest.commandTest

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

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)

def RFunctor.ap [RFunctor F] [OFE T] := F T T

instance : Leibniz (Frac α) := inferInstanceAs (Leibniz (LeibnizO α))

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

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

instance fromExists_intuitionistically [BI PROP] (P : PROP) (Φ : α → PROP) [h : FromExists P Φ] :
    FromExists iprop(□ P) (fun a => iprop(□ (Φ a))) where
  from_exists := intuitionistically_exists.2.trans <| intuitionistically_mono h.1

Lean.MonadQuotation in Init.Prelude

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

let _ ← isDefEq er goal
  if let (some _, some _) := (← try? <| synthInstanceQ q(FromAssumption false $er $goal),
                              ← try? <| synthInstanceQ q(TCOr (Affine $el) (Absorbing $goal))) then
    
    return q(assumption (p := false) .rfl)
  else if let some _ ← try? <| synthInstanceQ q(IntoWand false false $er $A1 $goal) then
    
    let m ← specPatGoal A1 hypsl spats addGoal
    return q(apply $m)
  else if let some _ ← try? <| synthInstanceQ q(IntoWand false false $er $A1 $A2) then
    
    let ⟨el', _, m, hypsl', h'⟩ ← processSpecPats A1 hypsl spats addGoal
    let res : Q($el' ∗ $A2 ⊢ $goal) ← iApplyCore goal el' A2 hypsl' spats.tail addGoal
    return q(rec_apply $h' $m $res)
  else
    throwError "iapply: cannot apply {er} to {goal}"

instance (priority := default - 10) fromSep_sep [BI PROP] (P1 P2 : PROP) :
    FromSep iprop(P1 ∗ P2) P1 P2 := ⟨.rfl⟩

class Cancelable (x : α) where
  cancelableN : ✓{n} x • y → x • y ≡{n}≡ x • z → y ≡{n}≡ z

Bool in Init.Prelude

instance later_absorbing [BI PROP] {P : PROP} [Absorbing P] : Absorbing iprop(▷ P) where
  absorbing := later_absorbingly.mpr.trans <| later_mono absorbing

instance [OFE α] [OFE β] [Discrete α] [Discrete β] : Discrete (α × β) where
  discrete_0 H := by admit /- proof elided -/

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

ULift in Init.Prelude

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 {P : PROP} [Absorbing P] : Absorbing iprop(|==> P) :=
  ⟨bupd_frame_l.trans <| mono sep_elim_r⟩

Lean.Elab.withInfoContext' in Lean.Elab.InfoTree.Main

instance [OFunctorContractive F] : OFunctorContractive (LaterOF F) where
  map_contractive.1 H z m := Dist.lt <| by
    have := (OFunctorContractive.map_contractive (F := F)).distLater_dist H
    simp_all only [Dist, DistLater, Function.uncurry, OFunctor.map, laterMap]

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

LT in Init.Prelude

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

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

def iCasesExists {prop : Q(Type u)} (_bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool))
    (name : TSyntax ``binderIdent) (α : Q(Sort v)) (Φ : Q(«$α» → «$prop»))
    (_inst : Q(IntoExists «$A'» «$Φ»))
    (k : (B B' : Q($prop)) → (_ : $B =Q iprop(□?$p $B')) → MetaM Q($P ∗ $B ⊢ $Q)) :
    MetaM (Q($P ∗ □?$p $A' ⊢ $Q)) := do
  let (name, ref) ← getFreshName name
  withLocalDeclDQ name α fun x => do
    addLocalVarInfo ref (← getLCtx) x α
    have B' : Q($prop) := Expr.headBeta q($Φ $x)
    have : $B' =Q $Φ $x := ⟨⟩
    if p.constName! == ``true then
      have : $p =Q true := ⟨⟩
      let pf : Q(∀ x, $P ∗ □ $Φ x ⊢ $Q) ← mkLambdaFVars #[x] <|← k q(iprop(□ $B')) B' ⟨⟩
      return q(exists_elim_intuitionistic (A := $A') $pf)
    else
      have : $p =Q false := ⟨⟩
      let pf : Q(∀ x, $P ∗ $Φ x ⊢ $Q) ← mkLambdaFVars #[x] <|← k B' B' ⟨⟩
      return q(exists_elim_spatial (A := $A') $pf)

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

def Agree.map : CMRA.Hom (Agree α) (Agree β) where
  f := map' f
  ne := inferInstance
  validN {n x} hval := 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 intoForall_forall [BI PROP] (Φ : α → PROP) : IntoForall iprop(∀ a, Φ a) Φ := ⟨.rfl⟩

protected def Tower.embed (k) : A F k -n> Tower F :=

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

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

f₁ in QqTest.commandTest

instance {m : T} [Hid : ∀ x : V, IdFree x] [Hc : ∀ x : V, Cancelable x] : Cancelable m where
  cancelableN {n m1 m2} Hv He i := by admit /- proof elided -/

Coe in Init.Coe

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

EmptyCollection in Init.Core

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

class Plain [BI PROP] [Plainly PROP] [BIPlainly PROP] (P : PROP) where
  plain : P ⊢ ■ P

def uliftUpHom [OFE α] : α -n> ULift α where
  f := .up
  ne.1 _ _ _ := id

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 : 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 + 30) fromAssumption_persistently_r [BI PROP] (P Q : PROP)
    [h : FromAssumption true P Q] : FromAssumption true P iprop(<pers> Q) where
  from_assumption := (persistent (P := iprop(□ P))).trans (persistently_mono h.1)

instance forall_absorbing [BI PROP] (Φ : α → PROP) [∀ x, Absorbing (Φ x)] :
    Absorbing iprop(∀ x, Φ x) where
  absorbing := absorbingly_forall_1.trans (forall_mono fun _ => absorbing)

@[simp] def optionValidN (n : Nat) : Option α → Prop
  | some x => ✓{n} x
  | none => True

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

instance (priority := default + 30) fromAssumption_affinely_r [BI PROP] (P Q : PROP)
    [h : FromAssumption true P Q] : FromAssumption true P iprop(<affine> Q) where
  from_assumption := affinely_idem.2.trans <| affinely_mono h.1

instance intoAnd_intuitionistically (p : Bool) [BI PROP] (P Q1 Q2 : PROP) [h : IntoAnd p P Q1 Q2] :
    IntoAnd p iprop(□ P) iprop(□ Q1) iprop(□ Q2) where
  into_and := (intuitionisticallyIf_comm' (q := true)).1.trans <|
      (intuitionistically_mono h.1).trans <| (intuitionisticallyIf_comm' (q := true)).2.trans <|
      intuitionisticallyIf_mono intuitionistically_and.1

Eq in Init.Prelude

semiOutParam in Init.Prelude

def iCasesAndLR {prop : Q(Type u)} (_bi : Q(BI $prop)) (P Q A' A1 A2 : Q($prop)) (p : Q(Bool))
    (_inst : Q(IntoAnd $p $A' $A1 $A2)) (right : Bool)
    (k : (B B' : Q($prop)) → (_ : $B =Q iprop(□?$p $B')) → MetaM Q($P ∗ $B ⊢ $Q)) :
    MetaM (Q($P ∗ □?$p $A' ⊢ $Q)) := do
  if p.constName! == ``true then
    have : $p =Q true := ⟨⟩
    if right then
      return q(and_elim_r_intuitionistic (A := $A') $(← k q(iprop(□ $A2)) A2 ⟨⟩))
    else
      return q(and_elim_l_intuitionistic (A := $A') $(← k q(iprop(□ $A1)) A1 ⟨⟩))
  else
    have : $p =Q false := ⟨⟩
    if right then
      return q(and_elim_r_spatial (A := $A') $(← k A2 A2 ⟨⟩))
    else
      return q(and_elim_l_spatial (A := $A') $(← k A1 A1 ⟨⟩))

abbrev GenMapOF (C : Type _) (F : COFE.OFunctorPre) :=
  DiscreteFunOF fun (_ : C) => OptionOF F

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

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)

Lean.Macro.throwUnsupported in Init.Prelude

instance [BI PROP] : RightId (α := PROP) BiEntails emp sep := ⟨sep_emp⟩
</all_available_defs>

<all_available_lemmas>
theorem BIBase.Entails.trans [BI PROP] {P Q R : PROP} (h1 : P ⊢ Q) (h2 : Q ⊢ R) : P ⊢ R

theorem BIBase.BiEntails.trans [BI PROP] {P Q R : PROP} (h1 : P ⊣⊢ Q) (h2 : Q ⊣⊢ R) : P ⊣⊢ R

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

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

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

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

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

theorem DistLater.trans [OFE α] {n} {x : α} (h1 : DistLater n x y) (h2 : DistLater n y z) :
    DistLater n x z

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

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

theorem bupd_wand_l {P Q : PROP} : iprop((P -∗ Q) ∗ (|==> P) ⊢ |==> Q)

theorem LocalUpdate.discrete [CMRA.Discrete α] (x y x' y' : α) :
    (x, y) ~l~> (x', y') ↔ ∀ mz, ✓ x → x ≡ y •? mz → (✓ x' ∧ x' ≡ y' •? mz)

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

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

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

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

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

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

theorem LocalUpdate.option_none {α} [UCMRA α] {x x' y' : α}
    (h : (x, CMRA.unit) ~l~> (x', y')) : (some x, none) ~l~> (some x', some y')

theorem IncludedN.succ {n} {x y : α} : x ≼{n.succ} y → x ≼{n} y

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

theorem Dist.le [OFE α] {m n} {x y : α} (h : x ≡{n}≡ y) (h' : m ≤ n) : x ≡{m}≡ y

theorem valid_mapN {x y : α} (f : ∀ n, ✓{n} x → ✓{n} y) (v : ✓ x) : ✓ y

theorem LeibnizO.dist_inj {x y : α} {n} (H : LeibnizO.mk x ≡{n}≡ LeibnizO.mk y) : x = y

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

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

theorem LocalUpdate.exclusive [CMRA.Exclusive y] {x x' : α}
    (vx' : ✓ x') : (x, y) ~l~> (x', x')

theorem distLater_eqv [OFE α] {n} : Equivalence (α := α) (DistLater n)

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

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

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

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

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

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

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

theorem discrete_id_free {x : α} [Discrete α] (H : ∀ y, ✓ x → ¬(x • y ≡ x)) : IdFree x

theorem equiv_of_some_equiv_some {x y : α} (H : some x ≡ some y) : x ≡ y

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 Replaces.apply [BI PROP] {P P' Q : PROP}
    (h : Replaces Q P P') (h_entails : P' ⊢ Q) : P ⊢ Q

theorem valid_discard : ✓ (discard : DFrac F)

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 multiple_lean [BI PROP] (P Q R : PROP) (H : P ⊢ Q -∗ R) (HP : ⊢ P) : ⊢ Q -∗ R

theorem plainly_exists_2 {α : Sort _} {Ψ : α → PROP} : (∃ a, ■ (Ψ a)) ⊢ ■ (∃ a, Ψ a)

theorem MyR_always_invalid (S₁ S₂ : String) (Hne : S₁ ≠ S₂) (n : Nat) : ¬✓{n} MyR S₁ • MyR S₂

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

theorem forall_elim [BI PROP] {Ψ : α → PROP} (a : α) : (∀ a, Ψ a) ⊢ Ψ a

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

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

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

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

theorem toAgree_op_valid_iff_eq [OFE.Leibniz α] {a : α} :
    ✓ (toAgree a • toAgree b) ↔ a = b

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

theorem Frac.inc_iff_lt {p q : Frac α} : p ≼ q ↔ p < q

theorem downN_upN {k} (x : A F k) : ∀ {i}, downN F i (upN F i x) ≡ x

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

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

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

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

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

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

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

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

theorem Agree.validN_ne {x y : Agree α} : x ≡{n}≡ y → x.validN n → y.validN n

protected theorem Hom.monoN [CMRA β] (f : α -C> β) n {x₁ x₂ : α} : x₁ ≼{n} x₂ → f x₁ ≼{n} f x₂

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

theorem inc_dom_inc {m1 m2 : T} (Hinc : m1 ≼ m2) : Set.Included (dom m1) (dom m2)

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

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

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

theorem affine_mono [BI PROP] {P Q : PROP} (h : P ⊢ Q) [Affine Q] : Affine P

theorem core_mono {x y : α} (Hinc : x ≼ y) : core x ≼ core y

theorem pure [BI PROP] : ⊢ (⌜∃ x, x ∨ False⌝ : PROP)

theorem bupd_sep {P Q : PROP} : iprop((|==> P) ∗ (|==> Q) ⊢ |==> (P ∗ Q))

theorem prod.is_discrete [OFE α] [OFE β] {a : α} {b : β} (Ha : DiscreteE a) (Hb : DiscreteE b) :
    DiscreteE (a, b)

theorem plainly_or [BIPlainlyExists PROP] : ■ (P ∨ Q) ⊣⊢ ■ P ∨ ■ Q

theorem LimitPreserving.discrete [COFE α] {P : α → Prop} :
    (∀ {x y : α}, x ≡{0}≡ y → (P x → P y)) → LimitPreserving P

theorem pure [BI PROP] (P : PROP) (HF : False) : ⊢ P

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

theorem Agree.op_ne {x : Agree α} : OFE.NonExpansive x.op

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

theorem ownM_always_invalid_elim (m : M) (H : ∀ n, ¬✓{n} m) : (cmraValid m : UPred M) ⊢ False

theorem discrete_inc_r {x y : α} [HD : DiscreteE y] : x ≼{0} y → x ≼ y

theorem and_congr_r [BI PROP] {P Q Q' : PROP} (h : Q ⊣⊢ Q') : 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)

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

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

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

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

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

theorem IncludedN.trans : (x : α) ≼{n} y → y ≼{n} z → x ≼{n} z

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

theorem plainly_into_absorbingly : ■ P ⊢ <absorb> P

theorem dist_some [OFE α] {n mx y} (h : mx ≡{n}≡ some y) :
    ∃ z : α, mx = some z ∧ y ≡{n}≡ z :=
  suffices hh : ∀ mx my y, mx ≡{n}≡ my → my = some y → ∃ t, mx = some t ∧ t ≡{n}≡ y from
    (hh mx (some y) _ h rfl).elim (fun t h => ⟨t, h.left, h.right.symm⟩)
  fun mx _ y e1 e2 =>
    match mx with

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

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

theorem bupd_except0 {P : PROP} : iprop(◇ (|==> P) ⊢ (|==> ◇ P))

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

theorem not_excl_op_right {x : α} [Exclusive x] {y} : ¬✓ (y • x)

theorem bupd_and {P Q : PROP} : iprop((|==> (P ∧ Q)) ⊢ (|==> P) ∧ (|==> Q))

theorem _root_.Iris.OFE.Equiv.valid : (x : α) ≡ y → (✓ x ↔ ✓ y)

congrArg in Init.Prelude

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

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

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

theorem plainly_true_emp : ■ True ⊣⊢ ■ (emp : PROP)

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 op_left_dist {x y : α} (z : α) (e : x ≡{n}≡ y) : x • z ≡{n}≡ y • z

theorem exact_lean [BI PROP] (Q : PROP) (H : ⊢ Q) : ⊢ Q

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

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

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

theorem inc_op_right (x y : α) : y ≼ x • y

theorem IncludedN.le {n n'} {x y : α} : n' ≤ n → x ≼{n} y → x ≼{n'} y

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

theorem and_emp [BI PROP] {P : PROP} [Affine P] : P ∧ emp ⊣⊢ P

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 bupd_idem {P : PROP} : iprop((|==> |==> P) ⊣⊢ |==> P)

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

theorem IsoFunStore.store_eq_of_Equiv [Store T K V] [IsoFunStore T K V] {t1 t2 : T}
    (H : Store.Equiv t1 t2) : t1 = t2

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

theorem persistently_wand_affinely_plainly [BIPersistentlyImplPlainly PROP] :
    (<affine> ■ P -∗ <pers> Q) ⊢ <pers> (<affine> ■ P -∗ Q)

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

theorem exact_forall' [BI PROP] (P : α → PROP) (a : α) (H : ∀ x, ⊢ P x) : ⊢ P a

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

theorem core_idem_L {x : α} [IsTotal α] : core (core x) = core x

theorem validN_core {n} {x : α} (v : ✓{n} x) : ✓{n} core x

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

theorem affinely_exists [BI PROP] {Φ : α → PROP} : <affine> (∃ a, Φ a) ⊣⊢ ∃ a, <affine> (Φ a)

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

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

theorem up_down {k} (x) : up F (k+1) (down F (k+1) x) ≡{k}≡ 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 or_intro_l' [BI PROP] {P Q R : PROP} (h : P ⊢ Q) : P ⊢ Q ∨ R

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

theorem lean [BI PROP] (Q : PROP) (H : ⊢ Q) : <affine> P ⊢ Q

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

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

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

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

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

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

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

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

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

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

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

theorem Excl.dist_eqv [OFE α] {n} : Equivalence (Excl.Dist (α := α) n)

theorem true_emp [BI PROP] [h : BIAffine PROP] : (True : PROP) ⊣⊢ emp

theorem intuitionistically_plainly : □ ■ P ⊢ ■ □ P

protected theorem Hom.mono [CMRA β] (f : α -C> β) {x₁ x₂ : α} : x₁ ≼ x₂ → f x₁ ≼ f x₂

@[elab_as_elim]
theorem OFE.ContractiveHom.fixpoint_ind [COFE α] [Inhabited α] (f : α -c> α)
    (P : α → Prop) (HProper : ∀ A B : α, A ≡ B → P A → P B) (x : α) (Hbase : P x)
    (Hind : ∀ x, P x → P (f x)) (Hlim : LimitPreserving P) :
    P f.fixpoint

theorem Agree.includedN {x y : Agree α} : x ≼{n} y ↔ y ≡{n}≡ y • x

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

theorem Option.some_is_discrete [OFE α] {a : α} (Ha : DiscreteE a) : DiscreteE (some a)

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

theorem as_emp_valid_2 [BI PROP] (φ : Prop) [AsEmpValid2 φ (P : PROP)] : (⊢ P) → φ

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

<local_ctx>
import Iris.BI.Classes

import Iris.BI.Extensions

import Iris.BI.BI

import Iris.Std.Classes

import Iris.Std.Rewrite

import Iris.Std.TC

namespace Iris.BI

open Iris.Std BI
</local_ctx>

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

