phanerozoic/Coq-Iris huggingface dataset:
(* iris/proofmode/monpred.v *)
Instance elim_modal_at_fupd_goal `{!BiFUpd PROP} φ p p' E1 E2 E3 𝓟 𝓟' Q Q' i :
  ElimModal φ p p' 𝓟 𝓟' (|={E1,E3}=> Q i) (|={E2,E3}=> Q' i) →
  ElimModal φ p p' 𝓟 𝓟' ((|={E1,E3}=> Q) i) ((|={E2,E3}=> Q') i).
Proof. by rewrite /ElimModal !monPred_at_fupd. Qed.
(* iris/proofmode/monpred.v *)
Instance elim_modal_at_fupd_hyp `{!BiFUpd PROP} φ p p' E1 E2 P 𝓟 𝓟' 𝓠 𝓠' i :
  MakeMonPredAt i P 𝓟 →
  ElimModal φ p p' (|={E1,E2}=> 𝓟) 𝓟' 𝓠 𝓠' →
  ElimModal φ p p' ((|={E1,E2}=> P) i) 𝓟' 𝓠 𝓠'.
Proof. by rewrite /MakeMonPredAt /ElimModal monPred_at_fupd=><-. Qed.
(* iris/proofmode/monpred.v *)
Instance elim_acc_at_None `{!BiFUpd PROP} {X} φ E1 E2 E3 E4 α α' β β' P P'x i :
  (∀ x, MakeEmbed (α x) (α' x)) → (∀ x, MakeEmbed (β x) (β' x)) →
  ElimAcc (X:=X) φ (fupd E1 E2) (fupd E3 E4) α' β' (λ _, None) P P'x →
  ElimAcc (X:=X) φ (fupd E1 E2) (fupd E3 E4) α β (λ _, None) (P i) (λ x, P'x x i).
Proof.
  rewrite /ElimAcc /MakeEmbed. iIntros (Hα Hβ HEA ?) "Hinner Hacc".
  iApply (HEA with "[Hinner]"); first done.
  - iIntros (x).  iSpecialize ("Hinner" $! x). rewrite -Hα. by iIntros (? <-).
  - iMod "Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]". iModIntro. iExists x.
    rewrite -Hα -Hβ. iFrame. iIntros (? _) "Hβ". by iApply "Hclose".
Qed.
(* iris/proofmode/monpred.v *)
Instance elim_acc_at_Some `{!BiFUpd PROP} {X} φ E1 E2 E3 E4 α α' β β' γ γ' P P'x i :
  (∀ x, MakeEmbed (α x) (α' x)) →
  (∀ x, MakeEmbed (β x) (β' x)) →
  (∀ x, MakeEmbed (γ x) (γ' x)) →
  ElimAcc (X:=X) φ (fupd E1 E2) (fupd E3 E4) α' β' (λ x, Some (γ' x)) P P'x →
  ElimAcc (X:=X) φ (fupd E1 E2) (fupd E3 E4) α β (λ x, Some (γ x)) (P i) (λ x, P'x x i).
Proof.
  rewrite /ElimAcc /MakeEmbed. iIntros (Hα Hβ Hγ HEA ?) "Hinner Hacc".
  iApply (HEA with "[Hinner]"); first done.
  - iIntros (x).  iSpecialize ("Hinner" $! x). rewrite -Hα. by iIntros (? <-).
  - iMod "Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]". iModIntro. iExists x.
    rewrite -Hα -Hβ -Hγ. iFrame. iIntros (? _) "Hβ /=". by iApply "Hclose".
Qed.
(* iris/proofmode/monpred.v *)
Instance add_modal_at_fupd_goal `{!BiFUpd PROP} E1 E2 𝓟 𝓟' Q i :
  AddModal 𝓟 𝓟' (|={E1,E2}=> Q i) → AddModal 𝓟 𝓟' ((|={E1,E2}=> Q) i).
Proof. by rewrite /AddModal !monPred_at_fupd. Qed.
(* iris/proofmode/monpred.v *)
(* This hard-codes the fact that ElimInv with_close returns a
   [(λ _, ...)] as Q'. *)
Instance elim_inv_embed_with_close {X : Type} φ
    𝓟inv 𝓟in (𝓟out 𝓟close : X → PROP)
    Pin (Pout Pclose : X → monPred)
    Q Q' :
  (∀ i, ElimInv φ 𝓟inv 𝓟in 𝓟out (Some 𝓟close) (Q i) (λ _, Q' i)) →
  MakeEmbed 𝓟in Pin → (∀ x, MakeEmbed (𝓟out x) (Pout x)) →
  (∀ x, MakeEmbed (𝓟close x) (Pclose x)) →
  ElimInv (X:=X) φ ⎡𝓟inv⎤ Pin Pout (Some Pclose) Q (λ _, Q').
Proof.
  rewrite /MakeEmbed /ElimInv=>H <- Hout Hclose ?. iStartProof PROP.
  setoid_rewrite <-Hout. setoid_rewrite <-Hclose.
  iIntros (?) "(?&?&HQ')". iApply H; [done|]. iFrame. iIntros (x) "?".
  by iApply "HQ'".
Qed.
(* iris/proofmode/monpred.v *)
Instance elim_inv_embed_without_close  {X : Type}
    φ 𝓟inv 𝓟in (𝓟out : X → PROP) Pin (Pout : X → monPred) Q (Q' : X → monPred) :
  (∀ i, ElimInv φ 𝓟inv 𝓟in 𝓟out None (Q i) (λ x, Q' x i)) →
  MakeEmbed 𝓟in Pin → (∀ x, MakeEmbed (𝓟out x) (Pout x)) →
  ElimInv (X:=X) φ ⎡𝓟inv⎤ Pin Pout None Q Q'.
Proof.
  rewrite /MakeEmbed /ElimInv=>H <-Hout ?. iStartProof PROP.
  setoid_rewrite <-Hout.
  iIntros (?) "(?&?&HQ')". iApply H; [done|]. iFrame. iIntros (x) "?".
  by iApply "HQ'".
Qed.
(* iris/proofmode/notation.v *)
Notation ""
:= Enil (only printing) : proof_scope.
(* iris/proofmode/notation.v *)
Notation "Γ H : P"
:= (Esnoc Γ (INamed H) P%I)
  (at level 1, P at level 200,
   left associativity, format "Γ H  :  '[' P ']' '//'", only printing) : proof_scope.
(* iris/proofmode/notation.v *)
Notation "Γ '_' : P"
:= (Esnoc Γ (IAnon _) P%I)
  (at level 1, P at level 200,
   left associativity, format "Γ '_'  :  '[' P ']' '//'", only printing) : proof_scope.
(* iris/proofmode/notation.v *)
Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ∗ Q"
:=
  (envs_entails (Envs Γ Δ _) Q%I)
  (* The level of Δ is picked to silence warnings about incompatible prefixes. See https://github.com/coq/coq/issues/19631. *)
  (at level 1, Δ at level 200, Q at level 200, left associativity,
  format "'[' Γ '--------------------------------------' □ '//' Δ '--------------------------------------' ∗ '//' Q ']'", only printing) :
  stdpp_scope.
(* iris/proofmode/notation.v *)
Notation "Δ '--------------------------------------' ∗ Q"
:=
  (envs_entails (Envs Enil Δ _) Q%I)
  (at level 1, Q at level 200, left associativity,
  format "'[' Δ '--------------------------------------' ∗ '//' Q ']'", only printing) : stdpp_scope.
(* iris/proofmode/notation.v *)
Notation "Γ '--------------------------------------' □ Q"
:=
  (envs_entails (Envs Γ Enil _) Q%I)
  (at level 1, Q at level 200, left associativity,
  format "'[' Γ '--------------------------------------' □ '//' Q ']'", only printing) : stdpp_scope.
(* iris/proofmode/notation.v *)
Notation "'--------------------------------------' ∗ Q"
:= (envs_entails (Envs Enil Enil _) Q%I)
  (at level 1, Q at level 200, format "'[' '--------------------------------------' ∗ '//' Q ']'", only printing) : stdpp_scope.
(* iris/proofmode/reduction.v *)
Ltac pm_eval t
:=
  eval pm_eval in t.
(* iris/proofmode/reduction.v *)
Ltac pm_reduce
:=
  (* Use [change_no_check] instead of [change] to avoid performing the
  conversion check twice. *)
  match goal with |- ?u => let v := pm_eval u in change_no_check v end.
(* iris/proofmode/reduction.v *)
Ltac pm_reflexivity
:=
  pm_reduce; notypeclasses refine eq_refl.
(* iris/proofmode/reduction.v *)
Ltac pm_prettify
:=
  (* Use [change_no_check] instead of [change] to avoid performing the
  conversion check twice. *)
  match goal with |- ?u => let v := eval pm_prettify in u in change_no_check v end.
(* iris/proofmode/sel_patterns.v *)
Inductive sel_pat
:=
  | SelPure
  | SelIntuitionistic
  | SelSpatial
  | SelIdent : ident → sel_pat.
(* iris/proofmode/sel_patterns.v *)
Fixpoint sel_pat_pure (ps : list sel_pat) : bool
:=
  match ps with
  | [] => false
  | SelPure :: ps => true
  | _ :: ps => sel_pat_pure ps
  end.
(* iris/proofmode/sel_patterns.v *)
Fixpoint parse_go (ts : list token) (k : list sel_pat) : option (list sel_pat)
:=
  match ts with
  | [] => Some (reverse k)
  | TName s :: ts => parse_go ts (SelIdent s :: k)
  | TPure None :: ts => parse_go ts (SelPure :: k)
  | TIntuitionistic :: ts => parse_go ts (SelIntuitionistic :: k)
  | TSep :: ts => parse_go ts (SelSpatial :: k)
  | _ => None
  end.
(* iris/proofmode/sel_patterns.v *)
Definition parse (s : string) : option (list sel_pat)
:=
  parse_go (tokenize s) [].
(* iris/proofmode/sel_patterns.v *)
Ltac parse s
:=
  lazymatch type of s with
  | sel_pat => constr:([s])
  | list sel_pat => s
  | ident => constr:([SelIdent s])
  | list ident => eval vm_compute in (SelIdent <$> s)
  | list string => eval vm_compute in (SelIdent ∘ INamed <$> s)
  | string =>
     lazymatch eval vm_compute in (parse s) with
     | Some ?pats => pats
     | _ => fail "sel_pat.parse: cannot parse" s "as a selection pattern"
     end
  | ?X => fail "sel_pat.parse: the term" s
     "is expected to be a selection pattern"
     "(usually a string),"
     "but has unexpected type" X
  end.
(* iris/proofmode/spec_patterns.v *)
Inductive goal_kind
:= GSpatial | GModal | GIntuitionistic.
(* iris/proofmode/spec_patterns.v *)
Record spec_goal
:= SpecGoal {
  spec_goal_kind : goal_kind;
  spec_goal_negate : bool;
  spec_goal_frame : list ident;
  spec_goal_hyps : list ident;
  spec_goal_done : bool
}.
(* iris/proofmode/spec_patterns.v *)
Inductive spec_pat
:=
  | SIdent : ident → list spec_pat → spec_pat
  | SPureGoal (perform_done : bool) : spec_pat
  | SGoal : spec_goal → spec_pat
  | SAutoFrame : goal_kind → spec_pat.
(* iris/proofmode/spec_patterns.v *)
Definition goal_kind_modal (k : goal_kind) : bool
:=
  match k with GModal => true | _ => false end.
(* iris/proofmode/spec_patterns.v *)
Definition spec_pat_modal (p : spec_pat) : bool
:=
  match p with
  | SGoal g => goal_kind_modal (spec_goal_kind g)
  | SAutoFrame k => goal_kind_modal k
  | _ => false
  end.
(* iris/proofmode/spec_patterns.v *)
Inductive stack_item
:=
  | StPat : spec_pat → stack_item
  | StIdent : string → stack_item.
(* iris/proofmode/spec_patterns.v *)
Fixpoint close (k : stack) (ps : list spec_pat) : option (list spec_pat)
:=
  match k with
  | [] => Some ps
  | StPat p :: k => close k (p :: ps)
  | StIdent _ :: _ => None
  end.
(* iris/proofmode/spec_patterns.v *)
Fixpoint close_ident (k : stack) (ps : list spec_pat) : option stack
:=
  match k with
  | [] => None
  | StPat p :: k => close_ident k (p :: ps)
  | StIdent s :: k => Some (StPat (SIdent s ps) :: k)
  end.
(* iris/proofmode/spec_patterns.v *)
Fixpoint parse_go (ts : list token) (k : stack) : option (list spec_pat)
:=
  match ts with
  | [] => close k []
  | TParenL :: TName s :: ts => parse_go ts (StIdent s :: k)
  | TParenR :: ts => k ← close_ident k []; parse_go ts k
  | TName s :: ts => parse_go ts (StPat (SIdent s []) :: k)
  | TBracketL :: TIntuitionistic :: TFrame :: TBracketR :: ts =>
     parse_go ts (StPat (SAutoFrame GIntuitionistic) :: k)
  | TBracketL :: TFrame :: TBracketR :: ts =>
     parse_go ts (StPat (SAutoFrame GSpatial) :: k)
  | TBracketL :: TModal :: TFrame :: TBracketR :: ts =>
     parse_go ts (StPat (SAutoFrame GModal) :: k)
  | TBracketL :: TPure None :: TBracketR :: ts =>
     parse_go ts (StPat (SPureGoal false) :: k)
  | TBracketL :: TPure None :: TDone :: TBracketR :: ts =>
     parse_go ts (StPat (SPureGoal true) :: k)
  | TBracketL :: TIntuitionistic :: ts => parse_goal ts GIntuitionistic false [] [] k
  | TBracketL :: TModal :: ts => parse_goal ts GModal false [] [] k
  | TBracketL :: ts => parse_goal ts GSpatial false [] [] k
  | _ => None
  end
with parse_goal (ts : list token)
    (ki : goal_kind) (neg : bool) (frame hyps : list ident)
    (k : stack) : option (list spec_pat) :=
  match ts with
  | TMinus :: ts =>
     guard (¬neg ∧ frame = [] ∧ hyps = []);;
     parse_goal ts ki true frame hyps k
  | TName s :: ts => parse_goal ts ki neg frame (INamed s :: hyps) k
  | TFrame :: TName s :: ts => parse_goal ts ki neg (INamed s :: frame) hyps k
  | TDone :: TBracketR :: ts =>
     parse_go ts (StPat (SGoal (SpecGoal ki neg (reverse frame) (reverse hyps) true)) :: k)
  | TBracketR :: ts =>
     parse_go ts (StPat (SGoal (SpecGoal ki neg (reverse frame) (reverse hyps) false)) :: k)
  | _ => None
  end.
(* iris/proofmode/spec_patterns.v *)
Definition parse (s : string) : option (list spec_pat)
:=
  parse_go (tokenize s) [].
(* iris/proofmode/spec_patterns.v *)
Ltac parse s
:=
  lazymatch type of s with
  | list spec_pat => s
  | spec_pat => constr:([s])
  | string =>
     lazymatch eval vm_compute in (parse s) with
     | Some ?pats => pats
     | _ => fail "spec_pat.parse: cannot parse" s "as a specialization pattern"
     end
  | ident => constr:([SIdent s []])
  | ?X => fail "spec_pat.parse: the term" s
     "is expected to be a specialization pattern"
     "(usually a string),"
     "but has unexpected type" X
  end.
(* iris/proofmode/string_ident.v *)
Ltac2 Type exn :
:= [ NotStringLiteral(constr) | InvalidIdent(string) ].
(* iris/proofmode/string_ident.v *)
Ltac2 coq_byte_to_char (b : constr) : char
:=
    Char.of_int (coq_byte_to_int b).
(* iris/proofmode/string_ident.v *)
Fixpoint coq_string_to_list_byte (s : string) : list byte
:=
    match s with
    | EmptyString => []
    | String c s => Ascii.byte_of_ascii c :: coq_string_to_list_byte s
    end.
(* iris/proofmode/string_ident.v *)
(* copy a list of Coq byte constrs into a string (already of the right length) *)
Ltac2 rec coq_byte_list_blit_list (pos : int) (ls : constr) (str : string) : unit
:=
    match! ls with
    | nil => ()
    | ?c :: ?ls =>
      let b := coq_byte_to_char c in
      String.set str pos b; coq_byte_list_blit_list (Int.add pos 1) ls str
    end.
(* iris/proofmode/string_ident.v *)
Ltac2 rec coq_string_length (s : constr) : int
:=
    match! s with
    | EmptyString => 0
    | String _ ?s' => Int.add 1 (coq_string_length s')
    | _ => Control.throw (NotStringLiteral s)
    end.
(* iris/proofmode/string_ident.v *)
Ltac2 compute (c : constr) : constr
:=
    Std.eval_vm None c.
(* iris/proofmode/string_ident.v *)
(* [coq_string_to_string] converts a Gallina string in a constr to an Ltac2
  native string *)
Ltac2 coq_string_to_string (s : constr) : string
:=
    let l := coq_string_length s in
    let str := String.make l (Char.of_int 0) in
    let bytes := compute constr:(coq_string_to_list_byte $s) in
    let _ := coq_byte_list_blit_list 0 bytes str in
    str.
(* iris/proofmode/string_ident.v *)
Ltac2 string_to_ident (s : string) : ident
:=
    match Ident.of_string s with
    | Some id => id
    | None => Control.throw (InvalidIdent s)
    end.
(* iris/proofmode/string_ident.v *)
(* [coq_string_to_ident] implements the ident to string conversion in Ltac2 *)
Ltac2 coq_string_to_ident (s : constr) : ident
:=
    string_to_ident (coq_string_to_string s).
(* iris/proofmode/string_ident.v *)
(* We want to wrap [coq_string_to_ident] in an Ltac1 API, but Ltac1-2 FFI
  does not support returning values from Ltac2 to Ltac1. So we provide
  [string_to_ident_cps] in CPS instead. *)
Ltac string_to_ident_cps
:=
    ltac2:(s1 r |- let s := Option.get (Ltac1.to_constr s1) in
                   let ident := coq_string_to_ident s in
                   Ltac1.apply r [Ltac1.of_ident ident] Ltac1.run).
(* iris/proofmode/string_ident.v *)
Ltac2 get_bit (n : int) (i : int) : bool
:=
    Int.equal (Int.land (Int.lsr n i) 1) 1.
(* iris/proofmode/string_ident.v *)
Ltac2 get_bit_coq_bool (n : int) (i : int) : constr
:=
    if get_bit n i then constr:(true) else constr:(false).
(* iris/proofmode/string_ident.v *)
Ltac2 char_to_coq_ascii (c : char) : constr
:=
    let i := Char.to_int c in
    let bs := Array.init 8 (get_bit_coq_bool i) in
    Constr.Unsafe.make (Constr.Unsafe.App constr:(Ascii) bs).
(* iris/proofmode/string_ident.v *)
Ltac2 string_to_coq_string (s : string) : constr
:=
    let len := String.length s in
    let rec to_string i :=
      if Int.equal i len then constr:(EmptyString) else
        let tail := to_string (Int.add i 1) in
        let head := char_to_coq_ascii (String.get s i) in
        constr:(String $head $tail)
    in
    to_string 0.
(* iris/proofmode/string_ident.v *)
Ltac2 ident_to_string (id : ident) : constr
:=
    string_to_coq_string (Ident.to_string id).
(* iris/proofmode/string_ident.v *)
Ltac ident_to_string_cps
:=
    ltac2:(id r |- let id := Option.get (Ltac1.to_ident id) in
                   let s := ident_to_string id in
                   Ltac1.apply r [Ltac1.of_constr s] Ltac1.run).
(* iris/proofmode/string_ident.v *)
(* Finally we wrap everything up intro a tactic that renames a variable given
by ident [id] into the name given by string [s]. *)
Ltac rename_by_string id s
:=
  StringToIdent.string_to_ident_cps s ltac:(fun x => rename id into x).
(* iris/proofmode/string_ident.v *)
(* We also directly expose the CPS primitives. *)
Ltac string_to_ident_cps
:= StringToIdent.string_to_ident_cps.
(* iris/proofmode/string_ident.v *)
Ltac ident_to_string_cps
:= IdentToString.ident_to_string_cps.
(* iris/proofmode/tokens.v *)
Inductive token
:=
  | TName : string → token
  | TNat : nat → token
  | TAnon : token
  | TFrame : token
  | TBar : token
  | TBracketL : token
  | TBracketR : token
  | TAmp : token
  | TParenL : token
  | TParenR : token
  | TBraceL : token
  | TBraceR : token
  | TPure : option string → token
  | TIntuitionistic : token
  | TModal : token
  | TPureIntro : token
  | TIntuitionisticIntro : token
  | TModalIntro : token
  | TSimpl : token
  | TDone : token
  | TForall : token
  | TAll : token
  | TMinus : token
  | TSep : token
  | TArrow : direction → token.
(* iris/proofmode/tokens.v *)
Inductive state
:=
  | SName : string → state
  | SNat : nat → state
  | SPure : string -> state
  | SNone : state.
(* iris/proofmode/tokens.v *)
Definition cons_state (kn : state) (k : list token) : list token
:=
  match kn with
  | SNone => k
  | SName s => TName (String.rev s) :: k
  | SPure s => TPure (if String.eqb s "" then None else Some (String.rev s)) :: k
  | SNat n => TNat n :: k
  end.
(* iris/proofmode/tokens.v *)
Fixpoint tokenize_go (s : string) (k : list token) (kn : state) : list token
:=
  match s with
  | "" => reverse (cons_state kn k)
  | String "?" s => tokenize_go s (TAnon :: cons_state kn k) SNone
  | String "$" s => tokenize_go s (TFrame :: cons_state kn k) SNone
  | String "[" s => tokenize_go s (TBracketL :: cons_state kn k) SNone
  | String "]" s => tokenize_go s (TBracketR :: cons_state kn k) SNone
  | String "|" s => tokenize_go s (TBar :: cons_state kn k) SNone
  | String "(" s => tokenize_go s (TParenL :: cons_state kn k) SNone
  | String ")" s => tokenize_go s (TParenR :: cons_state kn k) SNone
  | String "&" s => tokenize_go s (TAmp :: cons_state kn k) SNone
  | String "{" s => tokenize_go s (TBraceL :: cons_state kn k) SNone
  | String "}" s => tokenize_go s (TBraceR :: cons_state kn k) SNone
  | String "%" s => tokenize_go s (cons_state kn k) (SPure "")
  | String "#" s => tokenize_go s (TIntuitionistic :: cons_state kn k) SNone
  | String ">" s => tokenize_go s (TModal :: cons_state kn k) SNone
  | String "!" (String "%" s) => tokenize_go s (TPureIntro :: cons_state kn k) SNone
  | String "!" (String "#" s) => tokenize_go s (TIntuitionisticIntro :: cons_state kn k) SNone
  | String "!" (String ">" s) => tokenize_go s (TModalIntro :: cons_state kn k) SNone
  | String "/" (String "/" (String "=" s)) =>
     tokenize_go s (TSimpl :: TDone :: cons_state kn k) SNone
  | String "/" (String "/" s) => tokenize_go s (TDone :: cons_state kn k) SNone
  | String "/" (String "=" s) => tokenize_go s (TSimpl :: cons_state kn k) SNone
  | String "*" (String "*" s) => tokenize_go s (TAll :: cons_state kn k) SNone
  | String "*" s => tokenize_go s (TForall :: cons_state kn k) SNone
  | String "-" (String ">" s) => tokenize_go s (TArrow Right :: cons_state kn k) SNone
  | String "<" (String "-" s) => tokenize_go s (TArrow Left :: cons_state kn k) SNone
  | String "-" s => tokenize_go s (TMinus :: cons_state kn k) SNone
  | String (Ascii.Ascii false true false false false true true true) (* unicode ∗ *)
      (String (Ascii.Ascii false false false true false false false true)
      (String (Ascii.Ascii true true true false true false false true) s)) =>
     tokenize_go s (TSep :: cons_state kn k) SNone
  | String a s =>
     (* TODO: Complain about invalid characters, to future-proof this
     against making more characters special. *)
     if Ascii.is_space a then tokenize_go s (cons_state kn k) SNone else
     match kn with
     | SNone =>
        match Ascii.is_nat a with
        | Some n => tokenize_go s k (SNat n)
        | None => tokenize_go s k (SName (String a ""))
        end
     | SName s' => tokenize_go s k (SName (String a s'))
     | SPure s' => tokenize_go s k (SPure (String a s'))
     | SNat n =>
        match Ascii.is_nat a with
        | Some n' => tokenize_go s k (SNat (n' + 10 * n))
        | None => tokenize_go s (TNat n :: k) (SName (String a ""))
        end
     end
  end.
(* iris/proofmode/tokens.v *)
Definition tokenize (s : string) : list token
:= tokenize_go s [] SNone.
(* iris/si_logic/bi.v *)
(* We pick [*] and [-*] to coincide with [∧] and [→], respectively. This seems
to be the most reasonable choice to fit a "pure" higher-order logic into the
proofmode's BI framework. *)
Definition siProp_emp : siProp
:= siProp_pure True.
(* iris/si_logic/bi.v *)
Definition siProp_sep : siProp → siProp → siProp
:= siProp_and.
(* iris/si_logic/bi.v *)
Definition siProp_wand : siProp → siProp → siProp
:= siProp_impl.
(* iris/si_logic/bi.v *)
Definition siProp_persistently (P : siProp) : siProp
:= P.
(* iris/si_logic/bi.v *)
Definition siProp_plainly (P : siProp) : siProp
:= P.
(* iris/si_logic/bi.v *)
Lemma siProp_bi_mixin :
  BiMixin
    siProp_entails siProp_emp siProp_pure siProp_and siProp_or siProp_impl
    (@siProp_forall) (@siProp_exist) siProp_sep siProp_wand.
Proof.
  split.
  - exact: entails_po.
  - exact: equiv_entails.
  - exact: pure_ne.
  - exact: and_ne.
  - exact: or_ne.
  - exact: impl_ne.
  - exact: forall_ne.
  - exact: exist_ne.
  - exact: and_ne.
  - exact: impl_ne.
  - exact: pure_intro.
  - exact: pure_elim'.
  - exact: and_elim_l.
  - exact: and_elim_r.
  - exact: and_intro.
  - exact: or_intro_l.
  - exact: or_intro_r.
  - exact: or_elim.
  - exact: impl_intro_r.
  - exact: impl_elim_l'.
  - exact: @forall_intro.
  - exact: @forall_elim.
  - exact: @exist_intro.
  - exact: @exist_elim.
  - (* (P ⊢ Q) → (P' ⊢ Q') → P ∗ P' ⊢ Q ∗ Q' *)
    intros P P' Q Q' H1 H2. apply and_intro.
    + by etrans; first apply and_elim_l.
    + by etrans; first apply and_elim_r.
  - (* P ⊢ emp ∗ P *)
    intros P. apply and_intro; last done. by apply pure_intro.
  - (* emp ∗ P ⊢ P *)
    intros P. apply and_elim_r.
  - (* P ∗ Q ⊢ Q ∗ P *)
    intros P Q. apply and_intro; [ apply and_elim_r | apply and_elim_l ].
  - (* (P ∗ Q) ∗ R ⊢ P ∗ (Q ∗ R) *)
    intros P Q R. repeat apply and_intro.
    + etrans; first apply and_elim_l. by apply and_elim_l.
    + etrans; first apply and_elim_l. by apply and_elim_r.
    + apply and_elim_r.
  - (* (P ∗ Q ⊢ R) → P ⊢ Q -∗ R *)
    apply impl_intro_r.
  - (* (P ⊢ Q -∗ R) → P ∗ Q ⊢ R *)
    apply impl_elim_l'.
Qed.
(* iris/si_logic/bi.v *)
Lemma siProp_bi_persistently_mixin :
  BiPersistentlyMixin
    siProp_entails siProp_emp siProp_and
    (@siProp_exist) siProp_sep siProp_persistently.
Proof.
  split.
  - solve_proper.
  - (* (P ⊢ Q) → <pers> P ⊢ <pers> Q *)
    done.
  - (* <pers> P ⊢ <pers> <pers> P *)
    done.
  - (* emp ⊢ <pers> emp *)
    done.
  - (* (∀ a, <pers> (Ψ a)) ⊢ <pers> (∀ a, Ψ a) *)
    done.
  - (* <pers> (∃ a, Ψ a) ⊢ ∃ a, <pers> (Ψ a) *)
    done.
  - (* <pers> P ∗ Q ⊢ <pers> P *)
    apply and_elim_l.
  - (* <pers> P ∧ Q ⊢ P ∗ Q *)
    done.
Qed.
(* iris/si_logic/bi.v *)
Lemma siProp_bi_later_mixin :
  BiLaterMixin
    siProp_entails siProp_pure siProp_or siProp_impl
    (@siProp_forall) (@siProp_exist) siProp_sep siProp_persistently siProp_later.
Proof.
  split.
  - apply contractive_ne, later_contractive.
  - exact: later_mono.
  - exact: later_intro.
  - exact: @later_forall_2.
  - exact: @later_exist_false.
  - (* ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q *)
    intros P Q.
    apply and_intro; apply later_mono.
    + apply and_elim_l.
    + apply and_elim_r.
  - (* ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q) *)
    intros P Q.
    trans (siProp_forall (λ b : bool, siProp_later (if b then P else Q))).
    { apply forall_intro=> -[].
      - apply and_elim_l.
      - apply and_elim_r. }
    etrans; [apply later_forall_2|apply later_mono].
    apply and_intro.
    + refine (forall_elim true).
    + refine (forall_elim false).
  - (* ▷ <pers> P ⊢ <pers> ▷ P *)
    done.
  - (* <pers> ▷ P ⊢ ▷ <pers> P *)
    done.
  - exact: later_false_em.
Qed.
(* iris/si_logic/bi.v *)
Canonical siPropI : bi
:=
  {| bi_ofe_mixin := ofe_mixin_of siProp;
     bi_bi_mixin := siProp_bi_mixin;
     bi_bi_persistently_mixin := siProp_bi_persistently_mixin;
     bi_bi_later_mixin := siProp_bi_later_mixin |}.
(* iris/si_logic/bi.v *)
Instance siProp_pure_forall : BiPureForall siPropI.
Proof. exact: @pure_forall_2. Qed.
(* iris/si_logic/bi.v *)
Instance siProp_later_contractive : BiLaterContractive siPropI.
Proof. exact: @later_contractive. Qed.
(* iris/si_logic/bi.v *)
(* extra BI instances *)
Instance siProp_affine : BiAffine siPropI | 0.
Proof. intros P. exact: pure_intro. Qed.
(* iris/si_logic/bi.v *)
Instance siProp_persistent (P : siProp) : Persistent P.
Proof. done. Qed.
(* iris/si_logic/bi.v *)
(* We restate the unsealing lemmas so that they also unfold the BI layer. The
  sealing lemmas are partially applied so that they also work under binders. *)
Lemma siProp_emp_unseal : bi_emp = @siprop.siProp_pure_def True.
Proof. by rewrite -siprop.siProp_pure_unseal. Qed.
(* iris/si_logic/bi.v *)
Lemma siProp_pure_unseal : bi_pure = @siprop.siProp_pure_def.
Proof. by rewrite -siprop.siProp_pure_unseal. Qed.
(* iris/si_logic/bi.v *)
Lemma siProp_and_unseal : bi_and = @siprop.siProp_and_def.
Proof. by rewrite -siprop.siProp_and_unseal. Qed.