phanerozoic/Coq-Iris huggingface dataset:
(* iris/base_logic/upred.v *)
Instance uPredOF_contractive F :
  urFunctorContractive F → oFunctorContractive (uPredOF F).
Proof.
  intros ? A1 ? A2 ? B1 ? B2 ? n P Q HPQ.
  apply uPredO_map_ne, urFunctor_map_contractive.
  destruct HPQ as [HPQ]; split; intros ??; split; simpl; by eapply HPQ.
Qed.
(* iris/base_logic/upred.v *)
(* logical entailement *)
Inductive uPred_entails {M} (P Q : uPred M) : Prop
:=
  { uPred_in_entails : ∀ n x, ✓{n} x → P n x → Q n x }.
(* iris/base_logic/upred.v *)
(* logical connectives *)
Definition uPred_si_pure_def {M} (Pi : siProp) : uPred M
:=
  {| uPred_holds n x := siProp_holds Pi n |}.
(* iris/base_logic/upred.v *)
Definition uPred_si_pure_aux : seal (@uPred_si_pure_def).
Proof. by eexists. Qed.
(* iris/base_logic/upred.v *)
Definition uPred_si_pure
:= uPred_si_pure_aux.(unseal).
(* iris/base_logic/upred.v *)
Definition uPred_si_pure_unseal :
  @uPred_si_pure = @uPred_si_pure_def
:= uPred_si_pure_aux.(seal_eq).
(* iris/base_logic/upred.v *)
Definition uPred_si_emp_valid_def {M} (P : uPred M) : siProp
:=
  {| siProp_holds n := P n ε |}.
(* iris/base_logic/upred.v *)
Definition uPred_si_emp_valid_aux : seal (@uPred_si_emp_valid_def).
Proof. by eexists. Qed.
(* iris/base_logic/upred.v *)
Definition uPred_si_emp_valid
:= uPred_si_emp_valid_aux.(unseal).
(* iris/base_logic/upred.v *)
Definition uPred_si_emp_valid_unseal :
  @uPred_si_emp_valid = @uPred_si_emp_valid_def
:= uPred_si_emp_valid_aux.(seal_eq).
(* iris/base_logic/upred.v *)
Definition uPred_and_def {M} (P Q : uPred M) : uPred M
:=
  {| uPred_holds n x := P n x ∧ Q n x |}.
(* iris/base_logic/upred.v *)
Definition uPred_and_aux : seal (@uPred_and_def).
Proof. by eexists. Qed.
(* iris/base_logic/upred.v *)
Definition uPred_and
:= uPred_and_aux.(unseal).
(* iris/base_logic/upred.v *)
Definition uPred_and_unseal :
  @uPred_and = @uPred_and_def
:= uPred_and_aux.(seal_eq).
(* iris/base_logic/upred.v *)
Definition uPred_or_def {M} (P Q : uPred M) : uPred M
:=
  {| uPred_holds n x := P n x ∨ Q n x |}.
(* iris/base_logic/upred.v *)
Definition uPred_or_aux : seal (@uPred_or_def).
Proof. by eexists. Qed.
(* iris/base_logic/upred.v *)
Definition uPred_or
:= uPred_or_aux.(unseal).
(* iris/base_logic/upred.v *)
Definition uPred_or_unseal :
  @uPred_or = @uPred_or_def
:= uPred_or_aux.(seal_eq).
(* iris/base_logic/upred.v *)
Definition uPred_impl_def {M} (P Q : uPred M) : uPred M :=
  {| uPred_holds n x := ∀ n' x',
       x ≼ x' → n' ≤ n → ✓{n'} x' → P n' x' → Q n' x' |}.
Next Obligation.
  intros M P Q n1 n1' x1 x1' HPQ [x2 Hx1'] Hn1 n2 x3 [x4 Hx3] ?; simpl in *.
  rewrite Hx3 (dist_le _ _ _ _ Hx1'); auto. intros ??.
  eapply HPQ; auto. exists (x2 ⋅ x4); by rewrite assoc.
Qed.
(* iris/base_logic/upred.v *)
Definition uPred_impl_aux : seal (@uPred_impl_def).
Proof. by eexists. Qed.
(* iris/base_logic/upred.v *)
Definition uPred_impl
:= uPred_impl_aux.(unseal).
(* iris/base_logic/upred.v *)
Definition uPred_impl_unseal :
  @uPred_impl = @uPred_impl_def
:= uPred_impl_aux.(seal_eq).
(* iris/base_logic/upred.v *)
Definition uPred_forall_def {M A} (Ψ : A → uPred M) : uPred M
:=
  {| uPred_holds n x := ∀ a, Ψ a n x |}.
(* iris/base_logic/upred.v *)
Definition uPred_forall_aux : seal (@uPred_forall_def).
Proof. by eexists. Qed.
(* iris/base_logic/upred.v *)
Definition uPred_forall
:= uPred_forall_aux.(unseal).
(* iris/base_logic/upred.v *)
Definition uPred_forall_unseal :
  @uPred_forall = @uPred_forall_def
:= uPred_forall_aux.(seal_eq).
(* iris/base_logic/upred.v *)
Definition uPred_exist_def {M A} (Ψ : A → uPred M) : uPred M
:=
  {| uPred_holds n x := ∃ a, Ψ a n x |}.
(* iris/base_logic/upred.v *)
Definition uPred_exist_aux : seal (@uPred_exist_def).
Proof. by eexists. Qed.
(* iris/base_logic/upred.v *)
Definition uPred_exist
:= uPred_exist_aux.(unseal).
(* iris/base_logic/upred.v *)
Definition uPred_exist_unseal :
  @uPred_exist = @uPred_exist_def
:= uPred_exist_aux.(seal_eq).
(* iris/base_logic/upred.v *)
Definition uPred_sep_def {M} (P Q : uPred M) : uPred M :=
  {| uPred_holds n x := ∃ x1 x2, x ≡{n}≡ x1 ⋅ x2 ∧ P n x1 ∧ Q n x2 |}.
Next Obligation.
  intros M P Q n1 n2 x y (x1&x2&Hx&?&?) [z Hy] Hn.
  exists x1, (x2 ⋅ z); split_and?; eauto using uPred_mono, cmra_includedN_l.
  rewrite Hy. eapply dist_le, Hn. by rewrite Hx assoc.
Qed.
(* iris/base_logic/upred.v *)
Definition uPred_sep_aux : seal (@uPred_sep_def).
Proof. by eexists. Qed.
(* iris/base_logic/upred.v *)
Definition uPred_sep
:= uPred_sep_aux.(unseal).
(* iris/base_logic/upred.v *)
Definition uPred_sep_unseal :
  @uPred_sep = @uPred_sep_def
:= uPred_sep_aux.(seal_eq).
(* iris/base_logic/upred.v *)
Definition uPred_wand_def {M} (P Q : uPred M) : uPred M :=
  {| uPred_holds n x := ∀ n' x',
       n' ≤ n → ✓{n'} (x ⋅ x') → P n' x' → Q n' (x ⋅ x') |}.
Next Obligation.
  intros M P Q n1 n1' x1 x1' HPQ ? Hn n3 x3 ???; simpl in *.
  eapply uPred_mono with n3 (x1 ⋅ x3);
    eauto using cmra_validN_includedN, cmra_monoN_r, cmra_includedN_le.
Qed.
(* iris/base_logic/upred.v *)
Definition uPred_wand_aux : seal (@uPred_wand_def).
Proof. by eexists. Qed.
(* iris/base_logic/upred.v *)
Definition uPred_wand
:= uPred_wand_aux.(unseal).
(* iris/base_logic/upred.v *)
Definition uPred_wand_unseal :
  @uPred_wand = @uPred_wand_def
:= uPred_wand_aux.(seal_eq).
(* iris/base_logic/upred.v *)
Definition uPred_persistently_def {M} (P : uPred M) : uPred M
:=
  {| uPred_holds n x := P n (core x) |}.
(* iris/base_logic/upred.v *)
Definition uPred_persistently_aux : seal (@uPred_persistently_def).
Proof. by eexists. Qed.
(* iris/base_logic/upred.v *)
Definition uPred_persistently
:= uPred_persistently_aux.(unseal).
(* iris/base_logic/upred.v *)
Definition uPred_persistently_unseal :
  @uPred_persistently = @uPred_persistently_def
:= uPred_persistently_aux.(seal_eq).
(* iris/base_logic/upred.v *)
Definition uPred_later_def {M} (P : uPred M) : uPred M :=
  {| uPred_holds n x := match n return _ with 0 => True | S n' => P n' x end |}.
Next Obligation.
  intros M P [|n1] [|n2] x1 x2; eauto using uPred_mono, cmra_includedN_S with lia.
Qed.
(* iris/base_logic/upred.v *)
Definition uPred_later_aux : seal (@uPred_later_def).
Proof. by eexists. Qed.
(* iris/base_logic/upred.v *)
Definition uPred_later
:= uPred_later_aux.(unseal).
(* iris/base_logic/upred.v *)
Definition uPred_later_unseal :
  @uPred_later = @uPred_later_def
:= uPred_later_aux.(seal_eq).
(* iris/base_logic/upred.v *)
Definition uPred_ownM_def {M : ucmra} (a : M) : uPred M :=
  {| uPred_holds n x := a ≼{n} x |}.
Next Obligation.
  intros M a n1 n2 x1 x [a' Hx1] [x2 Hx] Hn.
  exists (a' ⋅ x2). rewrite Hx. eapply dist_le, Hn. rewrite (assoc op) -Hx1 //.
Qed.
(* iris/base_logic/upred.v *)
Definition uPred_ownM_aux : seal (@uPred_ownM_def).
Proof. by eexists. Qed.
(* iris/base_logic/upred.v *)
Definition uPred_ownM
:= uPred_ownM_aux.(unseal).
(* iris/base_logic/upred.v *)
Definition uPred_ownM_unseal :
  @uPred_ownM = @uPred_ownM_def
:= uPred_ownM_aux.(seal_eq).
(* iris/base_logic/upred.v *)
Definition uPred_bupd_def {M} (Q : uPred M) : uPred M :=
  {| uPred_holds n x := ∀ k yf,
      k ≤ n → ✓{k} (x ⋅ yf) → ∃ x', ✓{k} (x' ⋅ yf) ∧ Q k x' |}.
Next Obligation.
  intros M Q n1 n2 x1 x2 HQ [x3 Hx] Hn k yf Hk.
  rewrite (dist_le _ _ _ _ Hx Hk). intros Hxy.
  destruct (HQ k (x3 ⋅ yf)) as (x'&?&?); [auto|by rewrite assoc|].
  exists (x' ⋅ x3); split; first by rewrite -assoc.
  eauto using uPred_mono, cmra_includedN_l.
Qed.
(* iris/base_logic/upred.v *)
Definition uPred_bupd_aux : seal (@uPred_bupd_def).
Proof. by eexists. Qed.
(* iris/base_logic/upred.v *)
Definition uPred_bupd
:= uPred_bupd_aux.(unseal).
(* iris/base_logic/upred.v *)
Definition uPred_bupd_unseal :
  @uPred_bupd = @uPred_bupd_def
:= uPred_bupd_aux.(seal_eq).
(* iris/base_logic/upred.v *)
Definition uPred_unseal
:=
  (uPred_si_pure_unseal, uPred_si_emp_valid_unseal,
  uPred_and_unseal, uPred_or_unseal, uPred_impl_unseal,
  uPred_forall_unseal, uPred_exist_unseal,
  uPred_sep_unseal, uPred_wand_unseal,
  uPred_persistently_unseal, uPred_later_unseal, uPred_ownM_unseal,
  @uPred_bupd_unseal).
(* iris/base_logic/upred.v *)
Ltac unseal
:=
  rewrite !uPred_unseal /=.
(* iris/base_logic/upred.v *)
(* The notations below are implicitly local due to the section, so we do not
  mind the overlap with the general BI notations. *)
Notation "P ⊢ Q"
:= (@uPred_entails M P%I Q%I) : stdpp_scope.
(* iris/base_logic/upred.v *)
Notation "(⊢)"
:= (@uPred_entails M) (only parsing) : stdpp_scope.
(* iris/base_logic/upred.v *)
Notation "P ⊣⊢ Q"
:= (@uPred_equiv M P%I Q%I) : stdpp_scope.
(* iris/base_logic/upred.v *)
Notation "(⊣⊢)"
:= (@uPred_equiv M) (only parsing) : stdpp_scope.
(* iris/base_logic/upred.v *)
Notation "<si_pure> Pi"
:= (uPred_si_pure Pi) : bi_scope.
(* iris/base_logic/upred.v *)
Notation "<si_emp_valid> P"
:= (uPred_si_emp_valid P).
(* iris/base_logic/upred.v *)
Notation "'⌜' φ '⌝'"
:= (<si_pure> siProp_pure φ%type%stdpp)%I : bi_scope.
(* iris/base_logic/upred.v *)
Notation "'True'"
:= ⌜ True ⌝%I : bi_scope.
(* iris/base_logic/upred.v *)
Notation "'False'"
:= ⌜ False ⌝%I : bi_scope.
(* iris/base_logic/upred.v *)
Notation "∀ x .. y , P"
:=
    (uPred_forall (λ x, .. (uPred_forall (λ y, P)) ..)) : bi_scope.
(* iris/base_logic/upred.v *)
Notation "∃ x .. y , P"
:=
    (uPred_exist (λ x, .. (uPred_exist (λ y, P)) ..)) : bi_scope.
(* iris/base_logic/upred.v *)
Notation "□ P"
:= (uPred_persistently P) : bi_scope.
(* iris/base_logic/upred.v *)
Notation "▷ P"
:= (uPred_later P) : bi_scope.
(* iris/base_logic/upred.v *)
Notation "|==> P"
:= (uPred_bupd P) : bi_scope.
(* iris/base_logic/upred.v *)
(* Entailment *)
Lemma entails_po : PreOrder (⊢).
Proof.
    split.
    - by intros P; split=> x i.
    - by intros P Q Q' HP HQ; split=> x i ??; apply HQ, HP.
  Qed.
(* iris/base_logic/upred.v *)
Lemma entails_anti_sym : AntiSymm (⊣⊢) (⊢).
Proof. intros P Q HPQ HQP; split=> x n; by split; [apply HPQ|apply HQP]. Qed.
(* iris/base_logic/upred.v *)
Lemma equiv_entails P Q : (P ⊣⊢ Q) ↔ (P ⊢ Q) ∧ (Q ⊢ P).
Proof.
    split.
    - intros HPQ; split; split=> x i; apply HPQ.
    - intros [??]. exact: entails_anti_sym.
  Qed.
(* iris/base_logic/upred.v *)
Lemma entails_lim (cP cQ : chain (uPredO M)) :
    (∀ n, cP n ⊢ cQ n) → compl cP ⊢ compl cQ.
Proof.
    intros Hlim; split=> n m ? HP.
    eapply uPred_holds_ne, Hlim; [..|apply: HP]; rewrite ?conv_compl; eauto.
  Qed.
(* iris/base_logic/upred.v *)
(* Non-expansiveness and setoid morphisms *)
Lemma si_pure_ne : NonExpansive (@uPred_si_pure M).
Proof. intros n Pi Pi' HPi. unseal; split; intros; by apply HPi. Qed.
(* iris/base_logic/upred.v *)
Lemma si_emp_valid_ne : NonExpansive (@uPred_si_emp_valid M).
Proof.
    intros n P P' HP.
    unseal; split; intros; apply HP; auto using ucmra_unit_validN.
  Qed.
(* iris/base_logic/upred.v *)
Lemma and_ne : NonExpansive2 (@uPred_and M).
Proof.
    intros n P P' HP Q Q' HQ; unseal; split=> x n' ??.
    split; (intros [??]; split; [by apply HP|by apply HQ]).
  Qed.
(* iris/base_logic/upred.v *)
Lemma or_ne : NonExpansive2 (@uPred_or M).
Proof.
    intros n P P' HP Q Q' HQ; split=> x n' ??.
    unseal; split; (intros [?|?]; [left; by apply HP|right; by apply HQ]).
  Qed.
(* iris/base_logic/upred.v *)
Lemma impl_ne :
    NonExpansive2 (@uPred_impl M).
Proof.
    intros n P P' HP Q Q' HQ; split=> x n' ??.
    unseal; split; intros HPQ x' n'' ????; apply HQ, HPQ, HP; auto.
  Qed.
(* iris/base_logic/upred.v *)
Lemma sep_ne : NonExpansive2 (@uPred_sep M).
Proof.
    intros n P P' HP Q Q' HQ; split=> n' x ??.
    unseal; split; intros (x1&x2&?&?&?); ofe_subst x;
      exists x1, x2; split_and!; try (apply HP || apply HQ);
      eauto using cmra_validN_op_l, cmra_validN_op_r.
  Qed.
(* iris/base_logic/upred.v *)
Lemma wand_ne :
    NonExpansive2 (@uPred_wand M).
Proof.
    intros n P P' HP Q Q' HQ; split=> n' x ??; unseal; split; intros HPQ x' n'' ???;
      apply HQ, HPQ, HP; eauto using cmra_validN_op_r.
  Qed.
(* iris/base_logic/upred.v *)
Lemma forall_ne A n :
    Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_forall M A).
Proof.
    by intros Ψ1 Ψ2 HΨ; unseal; split=> n' x; split; intros HP a; apply HΨ.
  Qed.
(* iris/base_logic/upred.v *)
Lemma exist_ne A n :
    Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_exist M A).
Proof.
    intros Ψ1 Ψ2 HΨ.
    unseal; split=> n' x ??; split; intros [a ?]; exists a; by apply HΨ.
  Qed.
(* iris/base_logic/upred.v *)
Lemma later_contractive : Contractive (@uPred_later M).
Proof.
    unseal; intros [|n] P Q HPQ; split=> -[|n'] x ?? //=; try lia.
    eapply HPQ; eauto using cmra_validN_S.
  Qed.
(* iris/base_logic/upred.v *)
Lemma persistently_ne : NonExpansive (@uPred_persistently M).
Proof.
    intros n P1 P2 HP.
    unseal; split=> n' x; split; apply HP; eauto using cmra_core_validN.
  Qed.
(* iris/base_logic/upred.v *)
Lemma ownM_ne : NonExpansive (@uPred_ownM M).
Proof.
    intros n a b Ha.
    unseal; split=> n' x ? /=. by rewrite (dist_le _ _ _ _ Ha).
  Qed.
(* iris/base_logic/upred.v *)
Lemma bupd_ne : NonExpansive (@uPred_bupd M).
Proof.
    intros n P Q HPQ.
    unseal; split=> n' x; split; intros HP k yf ??;
      destruct (HP k yf) as (x'&?&?); auto;
      exists x'; split; auto; apply HPQ; eauto using cmra_validN_op_l.
  Qed.
(* iris/base_logic/upred.v *)
(* Rules for the [siProp] embedding *)
Lemma si_pure_mono Pi Qi : siProp_entails Pi Qi → <si_pure> Pi ⊢ <si_pure> Qi.
Proof. intros HPQi. unseal; split=> n ??. apply HPQi. Qed.
(* iris/base_logic/upred.v *)
Lemma si_emp_valid_mono P Q :
    (P ⊢ Q) → siProp_entails (<si_emp_valid> P) (<si_emp_valid> Q).
Proof. intros HPQ. unseal; split=> n. apply HPQ, ucmra_unit_validN. Qed.
(* iris/base_logic/upred.v *)
Lemma si_pure_impl_2 Pi Qi :
    (<si_pure> Pi → <si_pure> Qi) ⊢ <si_pure> siProp_impl Pi Qi.
Proof.
    unseal; siProp_primitive.unseal. split; simpl; eauto using cmra_validN_le.
  Qed.
(* iris/base_logic/upred.v *)
Lemma si_pure_forall_2 {A} (Φi : A → siProp) :
   (∀ x, <si_pure> Φi x) ⊢ <si_pure> siProp_forall Φi.
Proof. by unseal; siProp_primitive.unseal. Qed.
(* iris/base_logic/upred.v *)
Lemma si_pure_later Pi : <si_pure> siProp_later Pi ⊣⊢ ▷ <si_pure> Pi.
Proof. by unseal; siProp_primitive.unseal. Qed.
(* iris/base_logic/upred.v *)
Lemma si_emp_valid_later_1 P :
    siProp_entails (<si_emp_valid> ▷ P) (siProp_later (<si_emp_valid> P)).
Proof. by unseal; siProp_primitive.unseal. Qed.
(* iris/base_logic/upred.v *)
Lemma si_emp_valid_exist_1 {A} (Φ : A → uPred M) :
    siProp_entails (<si_emp_valid> ∃ x, Φ x)
                   (siProp_exist (λ x, <si_emp_valid> Φ x)).
Proof. by unseal; siProp_primitive.unseal. Qed.
(* iris/base_logic/upred.v *)
Lemma si_emp_valid_si_pure Pi :
    <si_emp_valid> (<si_pure> Pi : uPred M)%I ≡ Pi.
Proof. by unseal. Qed.
(* iris/base_logic/upred.v *)
Lemma si_pure_si_emp_valid P :
    <si_pure> <si_emp_valid> P ⊢ □ P.
Proof.
    unseal. split=> /= n x _ ?.
    eapply uPred_mono with n ε; eauto using ucmra_unit_leastN.
  Qed.
(* iris/base_logic/upred.v *)
Lemma persistently_impl_si_pure Pi Q :
    (<si_pure> Pi → □ Q) ⊢ □ (<si_pure> Pi → Q).
Proof.
    unseal; split=> /= n x ? HPQ n' x' ????.
    eapply uPred_mono with n' (core x)=>//; [|by apply cmra_included_includedN].
    apply (HPQ n' x); eauto using cmra_validN_le.
  Qed.
(* iris/base_logic/upred.v *)
Lemma prop_ext_2 P Q :
    siProp_entails (<si_emp_valid> ((P -∗ Q) ∧ (Q -∗ P)))
                   (siProp_internal_eq P Q).
Proof.
    unseal; siProp_primitive.unseal.
    split=> n /=. setoid_rewrite (left_id ε op). split; naive_solver.
  Qed.
(* iris/base_logic/upred.v *)
(* Introduction and elimination rules *)
Lemma and_elim_l P Q : P ∧ Q ⊢ P.
Proof. by unseal; split=> n x ? [??]. Qed.
(* iris/base_logic/upred.v *)
Lemma and_elim_r P Q : P ∧ Q ⊢ Q.
Proof. by unseal; split=> n x ? [??]. Qed.
(* iris/base_logic/upred.v *)
Lemma and_intro P Q R : (P ⊢ Q) → (P ⊢ R) → P ⊢ Q ∧ R.
Proof. intros HQ HR; unseal; split=> n x ??; by split; [apply HQ|apply HR]. Qed.
(* iris/base_logic/upred.v *)
Lemma or_intro_l P Q : P ⊢ P ∨ Q.
Proof. unseal; split=> n x ??; left; auto. Qed.
(* iris/base_logic/upred.v *)
Lemma or_intro_r P Q : Q ⊢ P ∨ Q.
Proof. unseal; split=> n x ??; right; auto. Qed.
(* iris/base_logic/upred.v *)
Lemma or_elim P Q R : (P ⊢ R) → (Q ⊢ R) → P ∨ Q ⊢ R.
Proof.
    intros HP HQ; unseal; split=> n x ? [?|?].
    - by apply HP.
    - by apply HQ.
  Qed.
(* iris/base_logic/upred.v *)
Lemma impl_intro_r P Q R : (P ∧ Q ⊢ R) → P ⊢ Q → R.
Proof.
    unseal; intros HQ; split=> n x ?? n' x' ????. apply HQ;
      naive_solver eauto using uPred_mono, cmra_included_includedN.
  Qed.
(* iris/base_logic/upred.v *)
Lemma impl_elim_l' P Q R : (P ⊢ Q → R) → P ∧ Q ⊢ R.
Proof. unseal; intros HP ; split=> n x ? [??]; apply HP with n x; auto. Qed.
(* iris/base_logic/upred.v *)
Lemma forall_intro {A} P (Ψ : A → uPred M): (∀ a, P ⊢ Ψ a) → P ⊢ ∀ a, Ψ a.
Proof. unseal; intros HPΨ; split=> n x ?? a; by apply HPΨ. Qed.
(* iris/base_logic/upred.v *)
Lemma forall_elim {A} {Ψ : A → uPred M} a : (∀ a, Ψ a) ⊢ Ψ a.
Proof. unseal; split=> n x ? HP; apply HP. Qed.
(* iris/base_logic/upred.v *)
Lemma exist_intro {A} {Ψ : A → uPred M} a : Ψ a ⊢ ∃ a, Ψ a.
Proof. unseal; split=> n x ??; by exists a. Qed.
(* iris/base_logic/upred.v *)
Lemma exist_elim {A} (Φ : A → uPred M) Q : (∀ a, Φ a ⊢ Q) → (∃ a, Φ a) ⊢ Q.
Proof. unseal; intros HΦΨ; split=> n x ? [a ?]; by apply HΦΨ with a. Qed.
(* iris/base_logic/upred.v *)
(* BI connectives *)
Lemma sep_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∗ P' ⊢ Q ∗ Q'.
Proof.
    intros HQ HQ'; unseal.
    split; intros n' x ? (x1&x2&?&?&?); exists x1,x2; ofe_subst x;
      eauto 7 using cmra_validN_op_l, cmra_validN_op_r, uPred_in_entails.
  Qed.
(* iris/base_logic/upred.v *)
Lemma True_sep_1 P : P ⊢ True ∗ P.
Proof.
    unseal; siProp_primitive.unseal; split; intros n x ??.
    exists (core x), x. by rewrite cmra_core_l.
  Qed.
(* iris/base_logic/upred.v *)
Lemma True_sep_2 P : True ∗ P ⊢ P.
Proof.
    unseal; split; intros n x ? (x1&x2&?&_&?); ofe_subst;
      eauto using uPred_mono, cmra_includedN_r.
  Qed.
(* iris/base_logic/upred.v *)
Lemma sep_comm' P Q : P ∗ Q ⊢ Q ∗ P.
Proof.
    unseal; split; intros n x ? (x1&x2&?&?&?); exists x2, x1; by rewrite (comm op).
  Qed.
(* iris/base_logic/upred.v *)
Lemma sep_assoc' P Q R : (P ∗ Q) ∗ R ⊢ P ∗ (Q ∗ R).
Proof.
    unseal; split; intros n x ? (x1&x2&Hx&(y1&y2&Hy&?&?)&?).
    exists y1, (y2 ⋅ x2); split_and?; auto.
    + by rewrite (assoc op) -Hy -Hx.
    + by exists y2, x2.
  Qed.
(* iris/base_logic/upred.v *)
Lemma wand_intro_r P Q R : (P ∗ Q ⊢ R) → P ⊢ Q -∗ R.
Proof.
    unseal=> HPQR; split=> n x ?? n' x' ???; apply HPQR; auto.
    exists x, x'; split_and?; auto.
    eapply uPred_mono with n x; eauto using cmra_validN_op_l.
  Qed.
(* iris/base_logic/upred.v *)
Lemma wand_elim_l' P Q R : (P ⊢ Q -∗ R) → P ∗ Q ⊢ R.
Proof.
    unseal =>HPQR. split; intros n x ? (?&?&?&?&?). ofe_subst.
    eapply HPQR; eauto using cmra_validN_op_l.
  Qed.
(* iris/base_logic/upred.v *)
(* Persistently *)
Lemma persistently_mono P Q : (P ⊢ Q) → □ P ⊢ □ Q.
Proof. intros HP; unseal; split=> n x ? /=. by apply HP, cmra_core_validN. Qed.
(* iris/base_logic/upred.v *)
Lemma persistently_elim P : □ P ⊢ P.
Proof.
    unseal; split=> n x ? /=.
    eauto using uPred_mono, cmra_included_core, cmra_included_includedN.
  Qed.
(* iris/base_logic/upred.v *)
Lemma persistently_idemp_2 P : □ P ⊢ □ □ P.
Proof. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp. Qed.
(* iris/base_logic/upred.v *)
Lemma persistently_forall_2 {A} (Ψ : A → uPred M) : (∀ a, □ Ψ a) ⊢ (□ ∀ a, Ψ a).
Proof. by unseal. Qed.
(* iris/base_logic/upred.v *)
Lemma persistently_exist_1 {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a) ⊢ (∃ a, □ Ψ a).
Proof. by unseal. Qed.
(* iris/base_logic/upred.v *)
Lemma persistently_and_sep_l_1 P Q : □ P ∧ Q ⊢ P ∗ Q.
Proof.
    unseal; split=> n x ? [??]; exists (core x), x; simpl in *.
    by rewrite cmra_core_l.
  Qed.
(* iris/base_logic/upred.v *)
(* Later *)
Lemma later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q.
Proof.
    unseal=> HP; split=>-[|n] x ??; [done|apply HP; eauto using cmra_validN_S].
  Qed.
(* iris/base_logic/upred.v *)
Lemma later_intro P : P ⊢ ▷ P.
Proof.
    unseal; split=> -[|n] /= x ? HP; first done.
    apply uPred_mono with (S n) x; eauto using cmra_validN_S.
  Qed.
(* iris/base_logic/upred.v *)
Lemma later_forall_2 {A} (Φ : A → uPred M) : (∀ a, ▷ Φ a) ⊢ ▷ ∀ a, Φ a.
Proof. unseal; by split=> -[|n] x. Qed.
(* iris/base_logic/upred.v *)
Lemma later_exist_false {A} (Φ : A → uPred M) :
    (▷ ∃ a, Φ a) ⊢ ▷ False ∨ (∃ a, ▷ Φ a).
Proof. unseal; split=> -[|[|n]] x /=; eauto. Qed.
(* iris/base_logic/upred.v *)
Lemma later_sep_1 P Q : ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q.
Proof.
    unseal; split=> n x ?.
    destruct n as [|n]; simpl.
    { by exists x, (core x); rewrite cmra_core_r. }
    intros (x1&x2&Hx&?&?); destruct (cmra_extend n x x1 x2)
      as (y1&y2&Hx'&Hy1&Hy2); eauto using cmra_validN_S; simpl in *.
    exists y1, y2; split; [by rewrite Hx'|by rewrite Hy1 Hy2].
  Qed.
(* iris/base_logic/upred.v *)
Lemma later_sep_2 P Q : ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q).
Proof.
    unseal; split=> n x ?.
    destruct n as [|n]; simpl; [done|intros (x1&x2&Hx&?&?)].
    exists x1, x2; eauto using dist_S.
  Qed.
(* iris/base_logic/upred.v *)
Lemma later_false_em P : ▷ P ⊢ ▷ False ∨ (▷ False → P).
Proof.
    unseal; siProp_primitive.unseal; split=> -[|n] x ? /= HP; [by left|right].
    intros [|n'] x' ????; eauto using uPred_mono, cmra_included_includedN.
  Qed.
(* iris/base_logic/upred.v *)
Lemma later_persistently_1 P : ▷ □ P ⊢ □ ▷ P.
Proof. by unseal. Qed.
(* iris/base_logic/upred.v *)
Lemma later_persistently_2 P : □ ▷ P ⊢ ▷ □ P.
Proof. by unseal. Qed.
(* iris/base_logic/upred.v *)
(* Basic update modality *)
Lemma bupd_intro P : P ⊢ |==> P.
Proof.
    unseal. split=> n x ? HP k yf ?; exists x; split; first done.
    apply uPred_mono with n x; eauto using cmra_validN_op_l.
  Qed.
(* iris/base_logic/upred.v *)
Lemma bupd_mono P Q : (P ⊢ Q) → (|==> P) ⊢ |==> Q.
Proof.
    unseal. intros HPQ; split=> n x ? HP k yf ??.
    destruct (HP k yf) as (x'&?&?); eauto.
    exists x'; split; eauto using uPred_in_entails, cmra_validN_op_l.
  Qed.
(* iris/base_logic/upred.v *)
Lemma bupd_trans P : (|==> |==> P) ⊢ |==> P.
Proof. unseal; split; naive_solver. Qed.
(* iris/base_logic/upred.v *)
Lemma bupd_frame_r P R : (|==> P) ∗ R ⊢ |==> P ∗ R.
Proof.
    unseal; split; intros n x ? (x1&x2&Hx&HP&?) k yf ??.
    destruct (HP k (x2 ⋅ yf)) as (x'&?&?); eauto.
    { by rewrite assoc -(dist_le _ _ _ _ Hx). }
    exists (x' ⋅ x2); split; first by rewrite -assoc.
    exists x', x2. eauto using uPred_mono, cmra_validN_op_l, cmra_validN_op_r.
  Qed.
(* iris/base_logic/upred.v *)
Lemma bupd_si_pure Pi : (|==> <si_pure> Pi) ⊢ <si_pure> Pi.
Proof.
    unseal; split => n x Hnx /= Hng.
    destruct (Hng n ε) as [? [_ Hng']]; try rewrite right_id; auto.
  Qed.
(* iris/base_logic/upred.v *)
(* Own *)
Lemma ownM_op (a1 a2 : M) :
    uPred_ownM (a1 ⋅ a2) ⊣⊢ uPred_ownM a1 ∗ uPred_ownM a2.
Proof.
    unseal; split=> n x ?; split.
    - intros [z ?]; exists a1, (a2 ⋅ z); split; [by rewrite (assoc op)|].
      split.
      + by exists (core a1); rewrite cmra_core_r.
      + by exists z.
    - intros (y1&y2&Hx&[z1 Hy1]&[z2 Hy2]); exists (z1 ⋅ z2).
      by rewrite (assoc op _ z1) -(comm op z1) (assoc op z1)
        -(assoc op _ a2) (comm op z1) -Hy1 -Hy2.
  Qed.
(* iris/base_logic/upred.v *)
Lemma persistently_ownM_core (a : M) : uPred_ownM a ⊢ □ uPred_ownM (core a).
Proof.
    split=> n x /=; unseal; intros Hx. simpl. by apply cmra_core_monoN.
  Qed.
(* iris/base_logic/upred.v *)
Lemma ownM_unit P : P ⊢ (uPred_ownM ε).
Proof. unseal; split=> n x ??; by  exists x; rewrite left_id. Qed.
(* iris/base_logic/upred.v *)
Lemma later_ownM a :
    ▷ uPred_ownM a ⊢ ∃ b, uPred_ownM b ∧ ▷ <si_pure> siProp_internal_eq a b.
Proof.
    unseal; siProp_primitive.unseal.
    split=> -[|n] x /= ? Hax; first by eauto using ucmra_unit_leastN.
    destruct Hax as [y ?].
    destruct (cmra_extend n x a y) as (a'&y'&Hx&?&?); auto using cmra_validN_S.
    exists a'. rewrite Hx. eauto using cmra_includedN_l.
  Qed.