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>
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 pureAbsorbing (φ : Prop) [BI PROP] : Absorbing (PROP := PROP) iprop(⌜φ⌝) where
  absorbing := absorbingly_pure.1

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

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

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

Nat.eq_or_lt_of_le in Init.Prelude

instance unit_total : IsTotal α where
  total _ :=
    have ⟨y, hy, _⟩ := pcore_mono' inc_unit pcore_unit
    ⟨y, hy⟩

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

instance Frac_CMRA [Fraction α] : CMRA (Frac α) where
  pcore _ := none
  op := Add.add
  ValidN _ x := Proper x.1
  Valid x := Proper x.1
  op_ne {x} := ⟨fun _ _ _ => congrArg <| Add.add x⟩
  pcore_ne _ := (exists_eq_right'.mpr ·)
  validN_ne H Hp := H ▸ Hp
  valid_iff_validN := forall_const _ |>.symm
  validN_succ := (·)
  validN_op_left := proper_add_mono_left
  assoc := Equiv.of_eq <| by simp only [Add.add]; rw [add_assoc]
  comm := Equiv.of_eq <| by simp only [Add.add]; rw [add_comm]
  pcore_op_left := by admit /- proof elided -/

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

Option in Init.Prelude

def LimitPreserving [COFE α] (P : α → Prop) : Prop :=
  ∀ (c : Chain α), (∀ n, P (c n)) → P (COFE.compl c)

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

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

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

Lean.MonadQuotation in Init.Prelude

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

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

let some { hyps, goal, .. } := parseIrisGoal? expr | failure

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 LeftId (R : Relation α) (i : α) (f : α → α → α) where
  left_id {x : α} : R (f i x) x

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

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

def headName (spats : List SpecPat) : Name :=
  match spats.head? with
    | some <| .ident _ => .anonymous
    | some <| .idents _ name => name
    | _ => .anonymous

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

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

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

instance {F} [COFE.OFunctor F] : RFunctor (ExclOF F) where
  cmra := inferInstance
  map f g := exclO_map (COFE.OFunctor.map f g)
  map_ne.ne := by admit /- proof elided -/

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

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

Fin in Init.Prelude

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)

abbrev DiscreteFunOF {C : Type _} (F : C → OFunctorPre) : OFunctorPre :=
  fun A B _ _ => (c : C) → F c A B

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

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

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

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

instance : COFE (iPrePropO FF) := inferInstanceAs (COFE (OFunctor.Fix _))

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

def up : ∀ k, A F k -n> A F (k+1)
  | 0 => ⟨fun _ => inh.default, ⟨fun _ _ _ _ => .rfl⟩⟩
  | k+1 => map (down k) (up k)

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

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

private def matchAlts' := leading_parser matchAlts

@[simp] protected def Excl.Dist [OFE α] (n : Nat) : Excl α → Excl α → Prop
  | excl a, excl b => a ≡{n}≡ b
  | invalid, invalid => True
  | _, _ => False

Lean.Expr.app in Lean.Expr

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

instance intoAnd_and_affine_l [BI PROP] (P Q Q' : PROP) [Affine P]
    [h : FromAffinely Q' Q] : IntoAnd false iprop(P ∧ Q) P Q' where
  into_and := (and_mono_l (affine_affinely _).2).trans <|
    affinely_and_l.1.trans <| affinely_and.1.trans <| and_mono (affine_affinely _).1 h.1

instance sep_intuitionistic [BI PROP] (P Q : PROP) [Intuitionistic P] [Intuitionistic Q] :
    Intuitionistic iprop(P ∗ Q) where
  intuitionistic := (sep_mono intuitionistic intuitionistic).trans intuitionistically_sep_2

Qq.mkFreshExprMVarQ in Qq.MetaM

Or.inl in Init.Prelude

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

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

LT in Init.Prelude

protected def sForall (Ψ : UPred M → Prop) : UPred M where
  holds n x := ∀ p, Ψ p → p n x
  mono a a_1 a_2 p a_3 := p.mono (a p a_3) a_1 a_2

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

instance intuitionistically_intuitionistic [BI PROP] (P : PROP) : Intuitionistic iprop(□ P) where
  intuitionistic := intuitionistically_idem.2

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

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

instance fromPure_pure_or (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 := (affinelyIf_mono pure_or.2).trans <| affinelyIf_or.1.trans <| by
    refine or_mono ((affinelyIf_flag_mono ?_).trans h1.1) ((affinelyIf_flag_mono ?_).trans h2.1)
      <;> simp_all

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

Equiv in Mathlib.Logic.Equiv.Defs

Qq.elabTermEnsuringTypeQ in Qq.MetaM

Lean.Expr.fvar in Lean.Expr

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)

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

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

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

Lean.mkFreshId in Init.Meta.Defs

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)

Array in Init.Prelude

protected def Hom.id [CMRA α] : α -C> α where
  toHom := OFE.Hom.id
  validN := id
  pcore x := by admit /- proof elided -/

instance {α : Type _} : OFE.Discrete (LeibnizO α) := ⟨congrArg id⟩

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

class UFraction (α : Type _) extends Fraction α, One α where
  
  
  
  
  one_whole : Fraction.Whole (1 : α)

class Plainly (PROP : Type _) where
  plainly : PROP → PROP

instance emp_affine [BI PROP] : Affine (PROP := PROP) iprop(emp) where
  affine := .rfl

instance fromPure_pure_and (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 := (affinelyIf_mono pure_and.2).trans <| affinelyIf_and.1.trans <| by
    refine and_mono ((affinelyIf_flag_mono ?_).trans h1.1) ((affinelyIf_flag_mono ?_).trans h2.1)
      <;> simp_all

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

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

Lean.NameMap in Lean.Data.NameMap.Basic

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

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

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

def Hyps.mkEmp {prop : Q(Type u)} (bi : Q(BI $prop)) (e := q(BI.emp : $prop)) : Hyps bi e := .emp ⟨⟩

abbrev OFEFun {α : Type _} (β : α → Type _) := ∀ a, OFE (β a)

Union in Init.Core

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

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

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

Nat.succ in Init.Prelude

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

structure IrisGoal where
  u : Level
  prop : Q(Type u)
  bi : Q(BI $prop)
  e : Q($prop)
  hyps : Hyps bi e
  goal : Q($prop)

let goal ← match direction with
    | .forward => do
      goalR.setTag tag
      pure goalL
    | .reverse => do
      goalL.setTag tag
      pure goalR

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

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

protected def persistently (P : UPred M) : UPred M where
  holds n x := P n (CMRA.core x)
  mono H Hx Hn := P.mono H (CMRA.core_incN_core Hx) Hn

instance (priority := default - 10) intoAnd_and (p : Bool) [BI PROP] (P Q : PROP) :
    IntoAnd p iprop(P ∧ Q) P Q := ⟨.rfl⟩

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

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

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

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

op_ne := Agree.op_ne
  pcore_ne := by admit /- proof elided -/

def Tower.iso : OFE.Iso (F (Tower F) (Tower F)) (Tower F) where
  hom.f X := {
    val n := (down F n).comp (map (Tower.embed _) (Tower.proj _)) X
    down {n} := (down ..).ne.eqv <|
      (map_comp ..).symm.trans (map_ne.eqv Tower.embed_up (·.down) _)
  }
  hom.ne.1 _ _ _ h _ := by admit /- proof elided -/

class IntoWand [BI PROP] (p q : Bool) (R : PROP) (P Q : outParam PROP) where
  into_wand : □?p R ⊢ □?q P -∗ Q

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

instance cmraProd : CMRA (α × β) where
  pcore := pcore
  op := op
  ValidN := ValidN
  Valid := Valid
  op_ne {x} :=
    { ne n y z h := dist_prod_ext (Dist.op_r $ dist_fst h) (Dist.op_r $ dist_snd h) }
  pcore_ne {n x y cx} h ph := by admit /- proof elided -/

instance : BIBase (HeapProp Val) where
  Entails P Q      := ∀ σ, P σ → Q σ
  emp            σ := σ = ∅
  pure φ         _ := φ
  and P Q        σ := P σ ∧ Q σ
  or P Q         σ := P σ ∨ Q σ
  imp P Q        σ := P σ → Q σ
  sForall Ψ      σ := ∀ p, Ψ p → p σ
  sExists Ψ      σ := ∃ p, Ψ p ∧ p σ
  sep P Q        σ := ∃ σ1 σ2, σ = σ1 ∪ σ2 ∧ σ1 || σ2 ∧ P σ1 ∧ Q σ2
  wand P Q       σ := ∀ σ', σ || σ' → P σ' → Q (σ ∪ σ')
  persistently P _ := P ∅
  later P        σ := P σ

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

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

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 intoPure_intuitionistically [BI PROP] (P : PROP) (φ : Prop)
    [h : IntoPure P φ] : IntoPure iprop(□ P) φ where
  into_pure := intuitionistically_elim.trans h.1

Qq.instantiateMVarsQ in Qq.MetaM

Option.map in Init.Prelude

class IsoFunStore (T : Type _) (K V : outParam (Type _)) [Store T K V] extends RepFunStore T K V where
  of_fun_get {t : T} : of_fun ⟨get t, rep_get t⟩ = t

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

instance (priority := default + 20) fromAssumption_affinely_l (p : Bool) [BI PROP] (P Q : PROP)
    [h : FromAssumption p P Q] : FromAssumption p iprop(<affine> P) Q where
  from_assumption := (intuitionisticallyIf_mono affinely_elim).trans h.1

| .clear => do
    let pf ← clearCore bi q(iprop($P ∗ $A)) P A Q q(.rfl)
    pure q($pf $(← k hyps))

inductive SplitResult {prop : Q(Type u)} (bi : Q(BI $prop)) (e : Q($prop)) where
  | emp (_ : $e =Q BI.emp)
  | left
  | right
  | split {elhs erhs : Q($prop)} (lhs : Hyps bi elhs) (rhs : Hyps bi erhs)
          (pf : Q($e ⊣⊢ $elhs ∗ $erhs))

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 fromAssumption_later [BI PROP] (p : Bool) (P Q : PROP)
    [h : FromAssumption p P Q] : FromAssumption p P iprop(▷ Q) where
  from_assumption := h.1.trans later_intro

partial def PMTerm.parse (term : Syntax) : MacroM PMTerm := do
  match ← expandMacros term with
  | `(pmTerm| $trm:term) => return ⟨trm, [], []⟩
  | `(pmTerm| $trm:term with $spats,*) => return ⟨trm, [], ← parseSpats spats⟩
  | `(pmTerm| $trm:term $! $ts,*) => return ⟨trm, ts.getElems.toList, []⟩
  | `(pmTerm| $trm:term $! $ts,* with $spats,*) =>
    return ⟨trm, ts.getElems.toList, ← parseSpats spats⟩
  | _ => Macro.throwUnsupported
where
  parseSpats (spats : Syntax.TSepArray `specPat ",") : MacroM (List SpecPat) :=
      return (← spats.getElems.toList.mapM fun pat => SpecPat.parse pat.raw)

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

f₁ in QqTest.commandTest

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

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

def Plainly.plainlyIf [Iris.BI.BIBase PROP] [Plainly PROP] (p : Bool) (P : PROP) : PROP :=
  iprop(if p then ■ P else P)

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

instance intoAnd_persistently (p : Bool) [BI PROP] (P Q1 Q2 : PROP) [h : IntoAnd p P Q1 Q2] :
    IntoAnd p iprop(<pers> P) iprop(<pers> Q1) iprop(<pers> Q2) where
  into_and := by admit /- proof elided -/

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

class DiscreteE {α : Type _} [OFE α] (x : α) : Prop where
  discrete : x ≡{0}≡ y → x ≡ y

instance (priority := default + 30) fromAssumption_persistently_l_false [BI PROP] [BIAffine PROP]
    (P Q : PROP) [h : FromAssumption true P Q] : FromAssumption false iprop(<pers> P) Q where
  from_assumption := intuitionistically_iff_persistently.2.trans h.1

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

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

Lean.throwError in Lean.Exception

instance : OFE.NonExpansive (bupd : UPred M → UPred M) where
  ne {n} {x1 x2} H {n' x'} Hn' Hx' := by admit /- proof elided -/

instance : EmptyCollection (State Val) where
  emptyCollection := fun _ => unknown

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

@[delab app.Iris.ProofMode.Entails']
def delabIrisGoal : Delab := do
  let expr ← instantiateMVars <| ← getExpr

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

instance isCOFE_later [OFE A] [IsCOFE A] : IsCOFE (Later A) where
  compl c := Later.next (IsCOFE.compl (laterChain c))
  conv_compl {n} c := by admit /- proof elided -/

unif_hint (b : Bool) where
  |- false || b ≟ b
unif_hint (b : Bool) where
  |- true || b ≟ true
unif_hint (b : Bool) where
  |- false && b ≟ false
unif_hint (b : Bool) where
  |- true && b ≟ b

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

instance [BI PROP] : LeftId (α := PROP) BiEntails emp sep := ⟨emp_sep⟩

instance (priority := default + 30) intoAbsorbingly_true [BI PROP] :
    IntoAbsorbingly (PROP := PROP) iprop(True) emp where
  into_absorbingly := absorbingly_emp.2

instance : Union (State Val) where
  union a b := fun i =>
    match a i, b i with
    | unknown , unknown  => unknown
    | result x, unknown  => result x
    | unknown , result y => result y
    | _       , _        => conflict

instance : IsModal (PROP1 := PROP) intuitionistically (.id rfl) .isEmpty where
  spec_intuitionistic _ := intuitionistic
  spec_spatial := trivial
  emp := intuitionistic
  mono := (intuitionistically_mono ·)
  sep := intuitionistically_sep_2

def towerChain (c : Chain (Tower F)) (k : Nat) : Chain (A F k) where
  chain i := c.1 i k
  cauchy h := c.cauchy h k

instance intoExists_pure (φ : α → Prop) [BI PROP] :
    IntoExists (PROP := PROP) iprop(⌜∃ x, φ x⌝) (fun a => iprop(⌜φ a⌝)) where
  into_exists := pure_exists.2

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

instance instStoreCMRA : CMRA T where
  pcore := pcore
  op := op
  ValidN := validN
  Valid := valid
  op_ne.ne _ x1 x2 H i := by admit /- proof elided -/

inductive SpecPat
  | ident (name : TSyntax ``binderIdent)
  | idents (names : List (TSyntax ``binderIdent)) (goalName : Name)
  deriving Repr, Inhabited

instance (P : UPred M) : Affine P where
  affine _ := by admit /- proof elided -/

instance fromOr_affinely [BI PROP] (P Q1 Q2 : PROP) [h : FromOr P Q1 Q2] :
    FromOr iprop(<affine> P) iprop(<affine> Q1) iprop(<affine> Q2) where
  from_or := affinely_or.2.trans (affinely_mono h.1)

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

Qq.Quoted in Qq.Typ

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

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

Option.elim in Init.Data.Option.Basic

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

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

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

instance : Inhabited (DFrac F) := ⟨discard⟩
</all_available_defs>

<all_available_lemmas>
theorem validN_of_inc {n} {x y : α} : x ≼ y → ✓{n} y → ✓{n} x

theorem sep_split [BI PROP] {P P1 P2 Q Q1 Q2 : PROP} [inst : FromSep Q Q1 Q2]
    (h : P ⊣⊢ P1 ∗ P2) (h1 : P1 ⊢ Q1) (h2 : P2 ⊢ Q2) : P ⊢ Q

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

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

theorem Update.discrete [CMRA.Discrete α] {x y : α} :
    x ~~> y ↔ ∀ (mz : Option α), ✓ (x •? mz) → ✓ (y •? mz)

theorem intuitionistically_forall_1 [BI PROP] {Φ : α → PROP} : □ (∀ x, Φ x) ⊢ ∀ x, □ Φ x

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

theorem valid_own_op_discard {q : F} : ✓ own q • discard ↔ Fractional 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 as_emp_valid_2 [BI PROP] (φ : Prop) [AsEmpValid2 φ (P : PROP)] : (⊢ P) → φ

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

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

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

theorem LocalUpdate.delete_option_cancelable
    (mx : Option α) [CMRA.Cancelable mx] : (mx, mx) ~l~> (none, none)

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

theorem plainly_elim [Absorbing P] : ■ P ⊢ P

theorem plainly_cmra_cmraValid_1 [CMRA A] (a : A) :
    (cmraValid a : UPred M) ⊢ ■ cmraValid a

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

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

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

theorem Agree.idemp {x : Agree α} : x.op x ≡ x

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

theorem pure_or [BI PROP] {φ1 φ2 : Prop} : ⌜φ1⌝ ∨ (⌜φ2⌝ : PROP) ⊣⊢ ⌜φ1 ∨ φ2⌝

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

theorem persistentlyIf_persistently {p : Bool} [BI PROP] {P : PROP} :
    <pers>?p <pers> P ⊣⊢ <pers> P

theorem spatial_elim_spatial [BI PROP] {A A' Q : PROP} [FromAffinely A' A false]
    (h : P ∗ A' ⊢ Q) : P ∗ A ⊢ Q

theorem sep [BI PROP] [BIAffine PROP] (Q : PROP) : P1 ∗ P2 ∗ Q ⊢ Q

theorem affinely_intro [BI PROP] {P Q : PROP} [Affine P] (h : P ⊢ Q) : P ⊢ <affine> Q

theorem absorbinglyIf_wand_1 {p : Bool} [BI PROP] {P Q : PROP} :
    <absorb>?p (P -∗ Q) ⊢ (<absorb>?p P -∗ <absorb>?p Q)

theorem Update.prod (x : α × β) (uxy₁ : x.fst ~~> y.fst) (uxy₂ : x.snd ~~> y.snd) : x ~~> y

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

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

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

theorem or [BI PROP] : ⊢ True ∨ (False : PROP)

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

theorem valid_iff {x y : α} (e : x ≡ y) : ✓ x ↔ ✓ y

theorem inc_trans {x y z : α} : x ≼ y → y ≼ z → x ≼ z

theorem validN_get_validN {m : T} (Hv : ✓{n} m) (He : get m i ≡{n}≡ some x) : ✓{n} x

theorem intuitionisticallyIf_of_intuitionistically (p : Bool) [BI PROP] {P : PROP} : □ P ⊢ □?p P

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

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

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

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

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

protected theorem Tower.up (X : Tower F) : up F (k+1) (X (k+1)) ≡{k}≡ X (k+2)

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

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

theorem and_forall_bool [BI PROP] {P Q : PROP} :
    P ∧ Q ⊣⊢ «forall» (fun b : Bool => if b then P else Q)

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

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

theorem absorbinglyIf_flag_mono {p q : Bool} [BI PROP] {P : PROP} (h : p → q) :
    <absorb>?p P ⊢ <absorb>?q 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 wandIff_congr_l [BI PROP] {P P' Q : PROP} (h : P ⊣⊢ P') : (P ∗-∗ Q) ⊣⊢ (P' ∗-∗ Q)

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

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

theorem valid0_disjoint_dom {m1 m2 : T} (Hv : ✓{0} (m1 • m2)) (H : ∀ {k x}, get m1 k = some x → Exclusive x) :
    Set.Disjoint (dom m1) (dom m2)

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

theorem _root_.Iris.OFE.Dist.validN : (x : α) ≡{n}≡ y → (✓{n} x ↔ ✓{n} y)

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

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

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

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

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 LocalUpdate.exclusive [CMRA.Exclusive y] {x x' : α}
    (vx' : ✓ x') : (x, y) ~l~> (x', x')

theorem valid_of_eqv {x y : α} : x ≡ y → ✓ x → ✓ y

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

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

theorem Iso.hom_dist [OFE α] [OFE β] (iso : Iso α β) {n} ⦃x y⦄ :
    x ≡{n}≡ y ↔ iso.hom x ≡{n}≡ iso.hom y

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

theorem eqv_of_Equiv [OFE V] [Store T K V] {t1 t2 : T} (H : Store.Equiv t1 t2) : t1 ≡ t2

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

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

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

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

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

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

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

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

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

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

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

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

theorem Agree.agree_map_ext {g : α → β} [OFE.NonExpansive g] (heq : ∀ a, f a ≡ g a) :
    map f x ≡ map g x

theorem Update.op {x₁ x₂ y₁ y₂ : α} (xy₁ : x₁ ~~> y₁) (xy₂ : x₂ ~~> y₂) : x₁ • x₂ ~~> y₁ • y₂

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

theorem mem_of_agree (x : Agree α) : ∃ a, a ∈ x.car

theorem intuitionistically_and [BI 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)

theorem Proper.fractional_or_whole {a : α} (H : Proper a) : Fractional a ∨ Whole a

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

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

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

theorem impl_wand_affinely_plainly : (■ P → Q) ⊣⊢ (<affine> ■ P -∗ 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 absorbinglyIf_sep_l {p : Bool} [BI PROP] {P Q : PROP} :
    <absorb>?p P ∗ Q ⊣⊢ <absorb>?p (P ∗ Q)

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

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

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

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

theorem Dist.distLater [OFE α] {n} {x y : α} (h : x ≡{n}≡ y) : DistLater n x y

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

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

theorem exists_intro' [BI PROP] {Φ : α → PROP} {P Q : PROP} [inst : FromExists Q Φ]
    (a : α) (h : P ⊢ Φ a) : P ⊢ Q

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

theorem point_core_total_eq [IsTotal V] [IsoFunStore T K (Option V)] {i : K} {x : V} :
    core (point (T := T) i (some x)) = point i (some (core x))

theorem point_core_eqv {i : K} {x : V} {cx} (Hpcore : pcore x ≡ some cx) :
    core (point (T := T) i (some x)) ≡ point i (some cx)

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

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

theorem affinely_intro' [BI PROP] {P Q : PROP} (h : P ⊢ <affine> Q) :
    <affine> P ⊢ <affine> Q

theorem wand_intro_intuitionistic [BI PROP] {P Q A1 A2 B : PROP}
    [FromWand Q A1 A2] [inst : IntoPersistently false A1 B] [or : TCOr (Affine A1) (Absorbing A2)]
    (h : P ∗ □ B ⊢ A2) : P ⊢ Q

theorem intuitionistically_elim_emp [BI PROP] {P : PROP} : □ P ⊢ emp

theorem dom_op_union (m1 m2 : T) : dom (m1 • m2) = Set.Union (dom m1) (dom m2)

theorem op_eqv {x x' y y' : α} (ex : x ≡ x') (ey : y ≡ y') : x • y ≡ x' • y'

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

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

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

theorem valid_disjoint_dom {m1 m2 : T} (Hv : ✓ (m1 • m2)) (H : ∀ {k x}, get m1 k = some x → Exclusive x) :
    Set.Disjoint (dom m1) (dom m2)

theorem later_impl [BI PROP] {P Q : PROP} : ▷ (P → Q) ⊢ ▷ P → ▷ Q

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

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

theorem Agree.dist_def {x y : Agree α} : x ≡{n}≡ y ↔ Agree.dist n x y

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

theorem bigOp_and_nil [BI PROP] : iprop([∧] []) ⊣⊢ (True : PROP)

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

theorem _root_.Iris.OFE.Dist.op {x x' y y' : α}
    (ex : x ≡{n}≡ x') (ey : y ≡{n}≡ y') : x • y ≡{n}≡ x' • y'

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

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

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

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

theorem true_sep_2 [BI PROP] {P : PROP} : P ⊢ True ∗ P

theorem later_iff [BI PROP] {P Q : PROP} : ▷ (P ↔ Q) ⊢ (▷ P ↔ ▷ Q)

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

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

theorem plainly_emp_2 : (emp : PROP) ⊢ ■ emp

theorem Agree.dist_equiv : Equivalence (dist (α := α) n)

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

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

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

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

theorem UpdateP.discrete_total [CMRA.Discrete α] [CMRA.IsTotal α] :
    x ~~>: P ↔ ∀ (z : α), ✓ (x • z) → ∃ y, P y ∧ ✓ (y • z)

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

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

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

theorem as_intuitionistic_in_spatial [BI PROP] (Q : PROP) : ⊢ <pers> Q → Q

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem point_op_point {i : K} {x y : V} :
    Equiv ((point (T := T) i (some x)) • (point i (some y))) ((point i (some (x • y))))

theorem later_true [BI PROP] : (▷ True ⊣⊢ (True : PROP))

theorem LimitPreserving.impl [COFE α] (P1 P2 : α → Prop)
    (HP1 : ∀ {x y : α}, x ≡{0}≡ y → P1 x → P1 y)
    (Hcompl : LimitPreserving P2) :
    LimitPreserving (fun x => P1 x → P2 x)

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

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

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

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

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

theorem valid_get_valid {m : T} (Hv : ✓ m) (He : get m i ≡ some x) : ✓ x

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

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

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

theorem Update.op_r {x y : α} : x • y ~~> y

theorem union_assoc {a b c : State Val} : (a ∪ b) ∪ c = a ∪ (b ∪ c)

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

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

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

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

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

theorem affinelyIf_and_lr {p : Bool} [BI PROP] {P Q : PROP} :
    <affine>?p P ∧ Q ⊣⊢ P ∧ <affine>?p Q

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

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

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

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

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

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

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

theorem equiv_none [OFE α] {o : Option α} : o ≡ none ↔ o = none

@[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_intuitionistic [BI PROP] (Q : PROP) : ⊢ □ P -∗ □ Q -∗ Q

theorem DFrac.update_discard {dq : DFrac F} : dq ~~> .discard

theorem DFrac.update_acquire [IsSplitFraction F] :
    (.discard : DFrac F) ~~>: fun k => ∃ q, k = .own q

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

theorem cancel_local_update_unit (x y : α) [CMRA.Cancelable x] : (x • y, x) ~l~> (y, CMRA.unit)

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

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

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

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

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

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

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

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

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

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

@[simp] theorem Contractive.zero [OFE α] [OFE β] (f : α → β) [Contractive f] {x y} :
    f x ≡{0}≡ f y

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

theorem LocalUpdate.valid [CMRA.Discrete α] {x y x' y' : α}
    (h : ✓ x → ✓ y → some y ≼ some x → (x, y) ~l~> (x', y')) : (x, y) ~l~> (x', y')

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

theorem sExists_persistent [BI PROP] (Ψ : PROP → Prop)
    (H : ∀ p, Ψ p → Persistent p) : Persistent iprop(sExists Ψ)

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

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

theorem validN_of_incN_validN {a b : α} (Hv : ✓{n} a) (Hinc : some b ≼{n} some a) : ✓{n} b

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

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

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

theorem imp_trans [BI PROP] {P Q R : PROP} : (P → Q) ∧ (Q → R) ⊢ P → R

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

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

<local_ctx>
import Iris.Algebra.CMRA

import Iris.Algebra.OFE

namespace Iris

namespace Fraction

variable [Fraction α]

end Fraction

open Fraction OFE CMRA

section NumericFraction

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

variable {α} [NumericFraction α]

open NumericFraction
</local_ctx>

<target_theorem>
theorem not_add_le_self {a b : α} : ¬ a + b ≤ a :=
</target_theorem>

