phanerozoic/Coq-Iris huggingface dataset:
(* iris/si_logic/bi.v *)
Lemma siProp_or_unseal : bi_or = @siprop.siProp_or_def.
Proof. by rewrite -siprop.siProp_or_unseal. Qed.
(* iris/si_logic/bi.v *)
Lemma siProp_impl_unseal : bi_impl = @siprop.siProp_impl_def.
Proof. by rewrite -siprop.siProp_impl_unseal. Qed.
(* iris/si_logic/bi.v *)
Lemma siProp_forall_unseal : @bi_forall _ = @siprop.siProp_forall_def.
Proof. by rewrite -siprop.siProp_forall_unseal. Qed.
(* iris/si_logic/bi.v *)
Lemma siProp_exist_unseal : @bi_exist _ = @siprop.siProp_exist_def.
Proof. by rewrite -siprop.siProp_exist_unseal. Qed.
(* iris/si_logic/bi.v *)
Lemma siProp_sep_unseal : bi_sep = @siprop.siProp_and_def.
Proof. by rewrite -siprop.siProp_and_unseal. Qed.
(* iris/si_logic/bi.v *)
Lemma siProp_wand_unseal : bi_wand = @siprop.siProp_impl_def.
Proof. by rewrite -siprop.siProp_impl_unseal. Qed.
(* iris/si_logic/bi.v *)
Lemma siProp_persistently_unseal : bi_persistently = @id siProp.
Proof. done. Qed.
(* iris/si_logic/bi.v *)
Lemma siProp_later_unseal : bi_later = @siprop.siProp_later_def.
Proof. by rewrite -siprop.siProp_later_unseal. Qed.
(* iris/si_logic/bi.v *)
Lemma siProp_internal_eq_unseal :
    @siProp_internal_eq = @siprop.siProp_internal_eq_def.
Proof. apply siprop.siProp_internal_eq_unseal. Qed.
(* iris/si_logic/bi.v *)
Lemma siProp_cmra_valid_unseal :
    @siProp_cmra_valid = @siprop.siProp_cmra_valid_def.
Proof. apply siprop.siProp_cmra_valid_unseal. Qed.
(* iris/si_logic/bi.v *)
Definition siProp_unseal
:=
    (siProp_emp_unseal, siProp_pure_unseal, siProp_and_unseal, siProp_or_unseal,
    siProp_impl_unseal, siProp_forall_unseal, siProp_exist_unseal,
    siProp_sep_unseal, siProp_wand_unseal,
    siProp_persistently_unseal, siProp_later_unseal,
    siProp_internal_eq_unseal, siProp_cmra_valid_unseal).
(* iris/si_logic/bi.v *)
(* The final unseal tactic that also unfolds the BI layer. *)
Ltac unseal
:= rewrite !siProp_unseal /=.
(* iris/si_logic/siprop.v *)
(* The type [siProp] defines "plain" step-indexed propositions, on which we
define the usual connectives of higher-order logic, and prove that these satisfy
the usual laws of higher-order logic. *)
Record siProp
:= SiProp {
  siProp_holds : nat → Prop;
  siProp_closed n1 n2 : siProp_holds n1 → n2 ≤ n1 → siProp_holds n2
}.
(* iris/si_logic/siprop.v *)
Coercion siProp_holds : siProp >-> Funclass.
(* iris/si_logic/siprop.v *)
Inductive siProp_equiv' (P Q : siProp) : Prop
:=
    { siProp_in_equiv : ∀ n, P n ↔ Q n }.
(* iris/si_logic/siprop.v *)
Instance siProp_equiv : Equiv siProp
:= siProp_equiv'.
(* iris/si_logic/siprop.v *)
Inductive siProp_dist' (n : nat) (P Q : siProp) : Prop
:=
    { siProp_in_dist : ∀ n', n' ≤ n → P n' ↔ Q n' }.
(* iris/si_logic/siprop.v *)
Instance siProp_dist : Dist siProp
:= siProp_dist'.
(* iris/si_logic/siprop.v *)
Definition siProp_ofe_mixin : OfeMixin siProp.
Proof.
    apply ofe_mixin_finite.
    - intros P Q; split.
      + by intros HPQ n; split=> i ?; apply HPQ.
      + intros HPQ; split=> n; apply HPQ with n; auto.
    - intros n; split.
      + by intros P; split=> i.
      + by intros P Q HPQ; split=> i ?; symmetry; apply HPQ.
      + intros P Q Q' HP HQ; split=> i ?.
        by trans (Q i);[apply HP|apply HQ].
    - intros n P Q HPQ. split=> i ?; apply HPQ; lia.
  Qed.
(* iris/si_logic/siprop.v *)
Canonical siPropO : ofe
:= Ofe siProp siProp_ofe_mixin.
(* iris/si_logic/siprop.v *)
Definition siProp_compl : Compl siPropO := λ c,
    {| siProp_holds n := c n n |}.
Next Obligation.
    intros c n1 n2 ??; simpl in *.
    apply (chain_cauchy c n2 n1); eauto using siProp_closed.
  Qed.
(* iris/si_logic/siprop.v *)
Instance siProp_cofe : Cofe siPropO := cofe_finite siProp_compl _.
Next Obligation.
    intros n c; split=>i ?; symmetry; apply (chain_cauchy c i n); auto.
  Qed.
(* iris/si_logic/siprop.v *)
(* [SiProp_downclose] takes a nat-based predicate and turns it into an [siProp]
by closing it off. It is used for [siProp_impl] and [SbiUnfold]. *)
Definition SiProp_downclose (Pi : nat → Prop) : siProp
:=
  SiProp (λ n, ∀ n', n' ≤ n → Pi n') ltac:(simpl; eauto using Nat.le_trans).
(* iris/si_logic/siprop.v *)
(* logical entailement *)
Inductive siProp_entails (P Q : siProp) : Prop
:=
  { siProp_in_entails : ∀ n, P n → Q n }.
(* iris/si_logic/siprop.v *)
(* logical connectives *)
Definition siProp_pure_def (φ : Prop) : siProp
:=
  {| siProp_holds n := φ |}.
(* iris/si_logic/siprop.v *)
Definition siProp_pure_aux : seal (@siProp_pure_def).
Proof. by eexists. Qed.
(* iris/si_logic/siprop.v *)
Definition siProp_pure
:= unseal siProp_pure_aux.
(* iris/si_logic/siprop.v *)
Definition siProp_pure_unseal :
  @siProp_pure = @siProp_pure_def
:= seal_eq siProp_pure_aux.
(* iris/si_logic/siprop.v *)
Definition siProp_and_def (P Q : siProp) : siProp
:=
  {| siProp_holds n := P n ∧ Q n |}.
(* iris/si_logic/siprop.v *)
Definition siProp_and_aux : seal (@siProp_and_def).
Proof. by eexists. Qed.
(* iris/si_logic/siprop.v *)
Definition siProp_and
:= unseal siProp_and_aux.
(* iris/si_logic/siprop.v *)
Definition siProp_and_unseal :
  @siProp_and = @siProp_and_def
:= seal_eq siProp_and_aux.
(* iris/si_logic/siprop.v *)
Definition siProp_or_def (P Q : siProp) : siProp
:=
  {| siProp_holds n := P n ∨ Q n |}.
(* iris/si_logic/siprop.v *)
Definition siProp_or_aux : seal (@siProp_or_def).
Proof. by eexists. Qed.
(* iris/si_logic/siprop.v *)
Definition siProp_or
:= unseal siProp_or_aux.
(* iris/si_logic/siprop.v *)
Definition siProp_or_unseal :
  @siProp_or = @siProp_or_def
:= seal_eq siProp_or_aux.
(* iris/si_logic/siprop.v *)
Definition siProp_impl_def (P Q : siProp) : siProp
:=
  SiProp_downclose (λ n, P n → Q n).
(* iris/si_logic/siprop.v *)
Definition siProp_impl_aux : seal (@siProp_impl_def).
Proof. by eexists. Qed.
(* iris/si_logic/siprop.v *)
Definition siProp_impl
:= unseal siProp_impl_aux.
(* iris/si_logic/siprop.v *)
Definition siProp_impl_unseal :
  @siProp_impl = @siProp_impl_def
:= seal_eq siProp_impl_aux.
(* iris/si_logic/siprop.v *)
Definition siProp_forall_def {A} (Ψ : A → siProp) : siProp
:=
  {| siProp_holds n := ∀ a, Ψ a n |}.
(* iris/si_logic/siprop.v *)
Definition siProp_forall_aux : seal (@siProp_forall_def).
Proof. by eexists. Qed.
(* iris/si_logic/siprop.v *)
Definition siProp_forall {A}
:= unseal siProp_forall_aux A.
(* iris/si_logic/siprop.v *)
Definition siProp_forall_unseal :
  @siProp_forall = @siProp_forall_def
:= seal_eq siProp_forall_aux.
(* iris/si_logic/siprop.v *)
Definition siProp_exist_def {A} (Ψ : A → siProp) : siProp
:=
  {| siProp_holds n := ∃ a, Ψ a n |}.
(* iris/si_logic/siprop.v *)
Definition siProp_exist_aux : seal (@siProp_exist_def).
Proof. by eexists. Qed.
(* iris/si_logic/siprop.v *)
Definition siProp_exist {A}
:= unseal siProp_exist_aux A.
(* iris/si_logic/siprop.v *)
Definition siProp_exist_unseal :
  @siProp_exist = @siProp_exist_def
:= seal_eq siProp_exist_aux.
(* iris/si_logic/siprop.v *)
Definition siProp_later_def (P : siProp) : siProp :=
  {| siProp_holds n := match n return _ with 0 => True | S n' => P n' end |}.
Next Obligation. intros P [|n1] [|n2]; eauto using siProp_closed with lia. Qed.
(* iris/si_logic/siprop.v *)
Definition siProp_later_aux : seal (@siProp_later_def).
Proof. by eexists. Qed.
(* iris/si_logic/siprop.v *)
Definition siProp_later
:= unseal siProp_later_aux.
(* iris/si_logic/siprop.v *)
Definition siProp_later_unseal :
  @siProp_later = @siProp_later_def
:= seal_eq siProp_later_aux.
(* iris/si_logic/siprop.v *)
Definition siProp_internal_eq_def {A : ofe} (a1 a2 : A) : siProp
:=
  {| siProp_holds n := a1 ≡{n}≡ a2 |}.
(* iris/si_logic/siprop.v *)
Definition siProp_internal_eq_aux : seal (@siProp_internal_eq_def).
Proof. by eexists. Qed.
(* iris/si_logic/siprop.v *)
Definition siProp_internal_eq {A}
:= unseal siProp_internal_eq_aux A.
(* iris/si_logic/siprop.v *)
Definition siProp_internal_eq_unseal :
  @siProp_internal_eq = @siProp_internal_eq_def
:= seal_eq siProp_internal_eq_aux.
(* iris/si_logic/siprop.v *)
Definition siProp_cmra_valid_def {A : cmra} (a : A) : siProp
:=
  {| siProp_holds n := ✓{n} a |}.
(* iris/si_logic/siprop.v *)
Definition siProp_cmra_valid_aux : seal (@siProp_cmra_valid_def).
Proof. by eexists. Qed.
(* iris/si_logic/siprop.v *)
Definition siProp_cmra_valid
:= siProp_cmra_valid_aux.(unseal).
(* iris/si_logic/siprop.v *)
Definition siProp_cmra_valid_unseal :
  @siProp_cmra_valid = @siProp_cmra_valid_def
:= siProp_cmra_valid_aux.(seal_eq).
(* iris/si_logic/siprop.v *)
Definition siProp_unseal
:=
  (siProp_pure_unseal, siProp_and_unseal, siProp_or_unseal,
  siProp_impl_unseal, siProp_forall_unseal, siProp_exist_unseal,
  siProp_later_unseal, siProp_internal_eq_unseal, siProp_cmra_valid_unseal).
(* iris/si_logic/siprop.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"
:= (siProp_entails P Q).
(* iris/si_logic/siprop.v *)
Notation "'True'"
:= (siProp_pure True) : bi_scope.
(* iris/si_logic/siprop.v *)
Notation "'False'"
:= (siProp_pure False) : bi_scope.
(* iris/si_logic/siprop.v *)
Notation "'⌜' φ '⌝'"
:= (siProp_pure φ%type%stdpp) : bi_scope.
(* iris/si_logic/siprop.v *)
Notation "∀ x .. y , P"
:=
    (siProp_forall (λ x, .. (siProp_forall (λ y, P%I)) ..)) : bi_scope.
(* iris/si_logic/siprop.v *)
Notation "∃ x .. y , P"
:=
    (siProp_exist (λ x, .. (siProp_exist (λ y, P%I)) ..)) : bi_scope.
(* iris/si_logic/siprop.v *)
Notation "▷ P"
:= (siProp_later P) : bi_scope.
(* iris/si_logic/siprop.v *)
Notation "x ≡ y"
:= (siProp_internal_eq x y) : bi_scope.
(* iris/si_logic/siprop.v *)
Notation "✓ x"
:= (siProp_cmra_valid x) : bi_scope.
(* iris/si_logic/siprop.v *)
(* Entailment *)
Lemma entails_po : PreOrder siProp_entails.
Proof.
    split.
    - intros P; by split=> i.
    - intros P Q Q' HP HQ; split=> i ?; by apply HQ, HP.
  Qed.
(* iris/si_logic/siprop.v *)
Lemma entails_anti_symm : AntiSymm (≡) siProp_entails.
Proof. intros P Q HPQ HQP; split=> n; by split; [apply HPQ|apply HQP]. Qed.
(* iris/si_logic/siprop.v *)
Lemma equiv_entails P Q : (P ≡ Q) ↔ (P ⊢ Q) ∧ (Q ⊢ P).
Proof.
    split.
    - intros HPQ; split; split=> i; apply HPQ.
    - intros [??]. by apply entails_anti_symm.
  Qed.
(* iris/si_logic/siprop.v *)
(* Non-expansiveness and setoid morphisms *)
Lemma pure_ne n : Proper (iff ==> dist n) siProp_pure.
Proof. intros φ1 φ2 Hφ. by unseal. Qed.
(* iris/si_logic/siprop.v *)
Lemma and_ne : NonExpansive2 siProp_and.
Proof.
    intros n P P' HP Q Q' HQ; unseal; split=> n' ?.
    split; (intros [??]; split; [by apply HP|by apply HQ]).
  Qed.
(* iris/si_logic/siprop.v *)
Lemma or_ne : NonExpansive2 siProp_or.
Proof.
    intros n P P' HP Q Q' HQ; split=> n' ?.
    unseal; split; (intros [?|?]; [left; by apply HP|right; by apply HQ]).
  Qed.
(* iris/si_logic/siprop.v *)
Lemma impl_ne : NonExpansive2 siProp_impl.
Proof.
    intros n P P' HP Q Q' HQ; split=> n' ?.
    unseal; split; intros HPQ n'' ??; apply HQ, HPQ, HP; auto with lia.
  Qed.
(* iris/si_logic/siprop.v *)
Lemma forall_ne A n :
    Proper (pointwise_relation _ (dist n) ==> dist n) (@siProp_forall A).
Proof.
     by intros Ψ1 Ψ2 HΨ; unseal; split=> n' x; split; intros HP a; apply HΨ.
  Qed.
(* iris/si_logic/siprop.v *)
Lemma exist_ne A n :
    Proper (pointwise_relation _ (dist n) ==> dist n) (@siProp_exist A).
Proof.
    intros Ψ1 Ψ2 HΨ.
    unseal; split=> n' ?; split; intros [a ?]; exists a; by apply HΨ.
  Qed.
(* iris/si_logic/siprop.v *)
Lemma later_contractive : Contractive siProp_later.
Proof.
    unseal; intros [|n] P Q HPQ; split=> -[|n'] ? //=; try lia.
    eapply HPQ; eauto using cmra_validN_S.
  Qed.
(* iris/si_logic/siprop.v *)
Lemma internal_eq_ne (A : ofe) : NonExpansive2 (@siProp_internal_eq A).
Proof.
    intros n x x' Hx y y' Hy; split=> n' z; unseal; split; intros; simpl in *.
    - by rewrite -(dist_le _ _ _ _ Hx) -?(dist_le _ _ _ _ Hy); auto.
    - by rewrite (dist_le _ _ _ _ Hx) ?(dist_le _ _ _ _ Hy); auto.
  Qed.
(* iris/si_logic/siprop.v *)
Lemma cmra_valid_ne (A : cmra) : NonExpansive (@siProp_cmra_valid A).
Proof.
    intros n x x' Hx. unseal; split=> /= n' z.
    by rewrite (dist_le _ _ _ _ Hx).
  Qed.
(* iris/si_logic/siprop.v *)
(* Introduction and elimination rules *)
Lemma pure_intro (φ : Prop) P : φ → P ⊢ ⌜ φ ⌝.
Proof. intros ?. unseal; by split. Qed.
(* iris/si_logic/siprop.v *)
Lemma pure_elim' (φ : Prop) P : (φ → True ⊢ P) → ⌜ φ ⌝ ⊢ P.
Proof. unseal=> HP; split=> n ?. by apply HP. Qed.
(* iris/si_logic/siprop.v *)
Lemma pure_forall_2 {A} (φ : A → Prop) : (∀ a, ⌜ φ a ⌝) ⊢ ⌜ ∀ a, φ a ⌝.
Proof. by unseal. Qed.
(* iris/si_logic/siprop.v *)
Lemma and_elim_l P Q : P ∧ Q ⊢ P.
Proof. unseal; by split=> n [??]. Qed.
(* iris/si_logic/siprop.v *)
Lemma and_elim_r P Q : P ∧ Q ⊢ Q.
Proof. unseal; by split=> n [??]. Qed.
(* iris/si_logic/siprop.v *)
Lemma and_intro P Q R : (P ⊢ Q) → (P ⊢ R) → P ⊢ Q ∧ R.
Proof.
    intros HQ HR; unseal; split=> n ?.
    split.
    - by apply HQ.
    - by apply HR.
  Qed.
(* iris/si_logic/siprop.v *)
Lemma or_intro_l P Q : P ⊢ P ∨ Q.
Proof. unseal; split=> n ?; left; auto. Qed.
(* iris/si_logic/siprop.v *)
Lemma or_intro_r P Q : Q ⊢ P ∨ Q.
Proof. unseal; split=> n ?; right; auto. Qed.
(* iris/si_logic/siprop.v *)
Lemma or_elim P Q R : (P ⊢ R) → (Q ⊢ R) → P ∨ Q ⊢ R.
Proof.
    intros HP HQ. unseal; split=> n [?|?].
    - by apply HP.
    - by apply HQ.
  Qed.
(* iris/si_logic/siprop.v *)
Lemma impl_intro_r P Q R : (P ∧ Q ⊢ R) → P ⊢ Q → R.
Proof.
    unseal=> HQ; split=> n ? n' ??.
    apply HQ; naive_solver eauto using siProp_closed.
  Qed.
(* iris/si_logic/siprop.v *)
Lemma impl_elim_l' P Q R : (P ⊢ Q → R) → P ∧ Q ⊢ R.
Proof. unseal=> HP; split=> n [??]. apply HP with n; auto. Qed.
(* iris/si_logic/siprop.v *)
Lemma forall_intro {A} P (Ψ : A → siProp) : (∀ a, P ⊢ Ψ a) → P ⊢ ∀ a, Ψ a.
Proof. unseal; intros HPΨ; split=> n ? a; by apply HPΨ. Qed.
(* iris/si_logic/siprop.v *)
Lemma forall_elim {A} {Ψ : A → siProp} a : (∀ a, Ψ a) ⊢ Ψ a.
Proof. unseal; split=> n HP; apply HP. Qed.
(* iris/si_logic/siprop.v *)
Lemma exist_intro {A} {Ψ : A → siProp} a : Ψ a ⊢ ∃ a, Ψ a.
Proof. unseal; split=> n ?; by exists a. Qed.
(* iris/si_logic/siprop.v *)
Lemma exist_elim {A} (Φ : A → siProp) Q : (∀ a, Φ a ⊢ Q) → (∃ a, Φ a) ⊢ Q.
Proof. unseal; intros HΨ; split=> n [a ?]; by apply HΨ with a. Qed.
(* iris/si_logic/siprop.v *)
(* Later *)
Lemma later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q.
Proof. unseal=> HP; split=>-[|n]; [done|apply HP; eauto using cmra_validN_S]. Qed.
(* iris/si_logic/siprop.v *)
Lemma later_intro P : P ⊢ ▷ P.
Proof. unseal; split=> -[|n] /= HP; eauto using siProp_closed. Qed.
(* iris/si_logic/siprop.v *)
Lemma later_forall_2 {A} (Φ : A → siProp) : (∀ a, ▷ Φ a) ⊢ ▷ ∀ a, Φ a.
Proof. unseal; by split=> -[|n]. Qed.
(* iris/si_logic/siprop.v *)
Lemma later_exist_false {A} (Φ : A → siProp) :
    (▷ ∃ a, Φ a) ⊢ ▷ False ∨ (∃ a, ▷ Φ a).
Proof. unseal; split=> -[|[|n]] /=; eauto. Qed.
(* iris/si_logic/siprop.v *)
Lemma later_false_em P : ▷ P ⊢ ▷ False ∨ (▷ False → P).
Proof.
    unseal; split=> -[|n] /= HP; [by left|right].
    intros [|n'] ?; eauto using siProp_closed with lia.
  Qed.
(* iris/si_logic/siprop.v *)
(* Equality *)
Lemma internal_eq_refl {A : ofe} P (a : A) : P ⊢ (a ≡ a).
Proof. unseal; by split=> n ? /=. Qed.
(* iris/si_logic/siprop.v *)
Lemma internal_eq_rewrite {A : ofe} a b (Ψ : A → siProp) :
    NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b.
Proof.
    intros Hnonexp. unseal; split=> n Hab n' ? HΨ. eapply Hnonexp with n a; auto.
  Qed.
(* iris/si_logic/siprop.v *)
Lemma prop_ext_2 P Q : ((P → Q) ∧ (Q → P)) ⊢ P ≡ Q.
Proof.
    unseal; split=> n /= HPQ. split=> n' ?.
    move: HPQ=> [] /(_ n') ? /(_ n'). naive_solver.
  Qed.
(* iris/si_logic/siprop.v *)
Lemma fun_extI {A} {B : A → ofe} (g1 g2 : discrete_fun B) :
    (∀ i, g1 i ≡ g2 i) ⊢ g1 ≡ g2.
Proof. by unseal. Qed.
(* iris/si_logic/siprop.v *)
Lemma sig_equivI_1 {A : ofe} (P : A → Prop) (x y : sigO P) :
    proj1_sig x ≡ proj1_sig y ⊢ x ≡ y.
Proof. by unseal. Qed.
(* iris/si_logic/siprop.v *)
Lemma later_equivI_1 {A : ofe} (x y : A) : Next x ≡ Next y ⊢ ▷ (x ≡ y).
Proof.
    unseal. split. intros [|n]; simpl; [done|].
    intros Heq; apply Heq; auto using SIdx.lt_succ_diag_r.
  Qed.
(* iris/si_logic/siprop.v *)
Lemma later_equivI_2 {A : ofe} (x y : A) : ▷ (x ≡ y) ⊢ Next x ≡ Next y.
Proof.
    unseal. split. intros n ?; split; intros m Hlt; simpl in *.
    destruct n as [|n]; first lia.
    by eapply dist_le, SIdx.lt_succ_r.
  Qed.
(* iris/si_logic/siprop.v *)
Lemma discrete_eq_1 {A : ofe} (a b : A) :
    TCOr (Discrete a) (Discrete b) →
    a ≡ b ⊢ ⌜a ≡ b⌝.
Proof. unseal=> ?. split=> n. by apply (discrete_iff n). Qed.
(* iris/si_logic/siprop.v *)
Lemma internal_eq_entails {A B : ofe} (a1 a2 : A) (b1 b2 : B) :
    (a1 ≡ a2 ⊢ b1 ≡ b2) ↔ (∀ n, a1 ≡{n}≡ a2 → b1 ≡{n}≡ b2).
Proof. unseal. split; [by intros []|done]. Qed.
(* iris/si_logic/siprop.v *)
(* Validity *)
Lemma cmra_valid_intro {A : cmra} P (a : A) : ✓ a → P ⊢ (✓ a).
Proof. unseal=> ?; split=> n ? /=; by apply cmra_valid_validN. Qed.
(* iris/si_logic/siprop.v *)
Lemma cmra_valid_elim {A : cmra} (a : A) : ✓ a ⊢ ⌜ ✓{0} a ⌝.
Proof. unseal; split=> n ?; by apply cmra_validN_le with n, SIdx.le_0_l. Qed.
(* iris/si_logic/siprop.v *)
Lemma cmra_valid_weaken {A : cmra} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
Proof. unseal; split=> n; apply cmra_validN_op_l. Qed.
(* iris/si_logic/siprop.v *)
Lemma valid_entails {A B : cmra} (a : A) (b : B) :
    (✓ a ⊢ ✓ b) ↔ ∀ n, ✓{n} a → ✓{n} b.
Proof. unseal. split; [by intros []|done]. Qed.
(* iris/si_logic/siprop.v *)
(* Consistency/soundness statements *)
Lemma pure_soundness φ : (True ⊢ ⌜ φ ⌝) → φ.
Proof. unseal=> -[H]. by apply (H 0). Qed.
(* iris/si_logic/siprop.v *)
Lemma internal_eq_soundness {A : ofe} (x y : A) : (True ⊢ x ≡ y) → x ≡ y.
Proof. unseal=> -[H]. apply equiv_dist=> n. by apply (H n). Qed.
(* iris/si_logic/siprop.v *)
Lemma later_soundness P : (True ⊢ ▷ P) → (True ⊢ P).
Proof.
    unseal=> -[HP]; split=> n _. apply siProp_closed with n; last done.
    by apply (HP (S n)).
  Qed.
(* iris_deprecated/base_logic/auth.v *)
(* The CMRA we need. *)
Class authG Σ (A : ucmra)
:= AuthG {
  #[local] auth_inG :: inG Σ (authR A);
  #[global] auth_cmra_discrete :: CmraDiscrete A;
}.
(* iris_deprecated/base_logic/auth.v *)
Definition authΣ (A : ucmra) : gFunctors
:= #[ GFunctor (authR A) ].
(* iris_deprecated/base_logic/auth.v *)
Instance subG_authΣ Σ A : subG (authΣ A) Σ → CmraDiscrete A → authG Σ A.
Proof. solve_inG. Qed.
(* iris_deprecated/base_logic/auth.v *)
Definition auth_own (a : A) : iProp Σ
:=
    own γ (◯ a).
(* iris_deprecated/base_logic/auth.v *)
Definition auth_inv (f : T → A) (φ : T → iProp Σ) : iProp Σ
:=
    ∃ t, own γ (● f t) ∗ φ t.
(* iris_deprecated/base_logic/auth.v *)
Definition auth_ctx (N : namespace) (f : T → A) (φ : T → iProp Σ) : iProp Σ
:=
    inv N (auth_inv f φ).
(* iris_deprecated/base_logic/auth.v *)
Instance auth_own_ne : NonExpansive auth_own.
Proof. solve_proper. Qed.
(* iris_deprecated/base_logic/auth.v *)
Instance auth_own_proper : Proper ((≡) ==> (⊣⊢)) auth_own.
Proof. solve_proper. Qed.
(* iris_deprecated/base_logic/auth.v *)
Instance auth_own_timeless a : Timeless (auth_own a).
Proof. apply _. Qed.
(* iris_deprecated/base_logic/auth.v *)
Instance auth_own_core_id a : CoreId a → Persistent (auth_own a).
Proof. apply _. Qed.
(* iris_deprecated/base_logic/auth.v *)
Instance auth_inv_ne n :
    Proper (pointwise_relation T (dist n) ==>
            pointwise_relation T (dist n) ==> dist n) auth_inv.
Proof. solve_proper. Qed.
(* iris_deprecated/base_logic/auth.v *)
Instance auth_inv_proper :
    Proper (pointwise_relation T (≡) ==>
            pointwise_relation T (⊣⊢) ==> (⊣⊢)) auth_inv.
Proof. solve_proper. Qed.
(* iris_deprecated/base_logic/auth.v *)
Instance auth_ctx_ne N n :
    Proper (pointwise_relation T (dist n) ==>
            pointwise_relation T (dist n) ==> dist n) (auth_ctx N).
Proof. solve_proper. Qed.
(* iris_deprecated/base_logic/auth.v *)
Instance auth_ctx_proper N :
    Proper (pointwise_relation T (≡) ==>
            pointwise_relation T (⊣⊢) ==> (⊣⊢)) (auth_ctx N).
Proof. solve_proper. Qed.
(* iris_deprecated/base_logic/auth.v *)
Instance auth_ctx_persistent N f φ : Persistent (auth_ctx N f φ).
Proof. apply _. Qed.
(* iris_deprecated/base_logic/auth.v *)
Instance : Params (@auth_own) 4
:= {}.
(* iris_deprecated/base_logic/auth.v *)
Instance : Params (@auth_inv) 5
:= {}.
(* iris_deprecated/base_logic/auth.v *)
Instance : Params (@auth_ctx) 7
:= {}.
(* iris_deprecated/base_logic/auth.v *)
Lemma auth_own_op γ a b : auth_own γ (a ⋅ b) ⊣⊢ auth_own γ a ∗ auth_own γ b.
Proof. by rewrite /auth_own -own_op auth_frag_op. Qed.
(* iris_deprecated/base_logic/auth.v *)
(* Global Instance from_and_auth_own γ a b1 b2 :
    IsOp a b1 b2 →
    FromAnd false (auth_own γ a) (auth_own γ b1) (auth_own γ b2) | 90.
  Proof. rewrite /IsOp /FromAnd=> ->. by rewrite auth_own_op. Qed.
  Global Instance from_and_auth_own_persistent γ a b1 b2 :
    IsOp a b1 b2 → Or (CoreId b1) (CoreId b2) →
    FromAnd true (auth_own γ a) (auth_own γ b1) (auth_own γ b2) | 91.
  Proof.
    intros ? Hper; apply mk_from_and_persistent; [destruct Hper; apply _|].
    by rewrite -auth_own_op -is_op.
  Qed.

  Global Instance into_and_auth_own p γ a b1 b2 :
    IsOp a b1 b2 →
    IntoAnd p (auth_own γ a) (auth_own γ b1) (auth_own γ b2) | 90.
  Proof. intros. apply mk_into_and_sep. by rewrite (is_op a) auth_own_op. Qed. *)
Lemma auth_own_mono γ a b : a ≼ b → auth_own γ b ⊢ auth_own γ a.
Proof. intros [? ->]. by rewrite auth_own_op sep_elim_l. Qed.
(* iris_deprecated/base_logic/auth.v *)
Lemma auth_own_valid γ a : auth_own γ a ⊢ ✓ a.
Proof. by rewrite /auth_own own_valid auth_frag_validI. Qed.
(* iris_deprecated/base_logic/auth.v *)
Instance auth_own_sep_homomorphism γ :
    WeakMonoidHomomorphism op uPred_sep (≡) (auth_own γ).
Proof. split; try apply _. apply auth_own_op. Qed.
(* iris_deprecated/base_logic/auth.v *)
Lemma big_opL_auth_own {B} γ (g : nat → B → A) (l : list B) :
    l ≠ [] →
    auth_own γ ([^op list] k↦x ∈ l, g k x) ⊣⊢
             [∗ list] k↦x ∈ l, auth_own γ (g k x).
Proof. apply (big_opL_commute1 _). Qed.
(* iris_deprecated/base_logic/auth.v *)
Lemma big_opM_auth_own `{Countable K} {B} γ (g : K → B → A) (m : gmap K B) :
    m ≠ ∅ →
    auth_own γ ([^op map] k↦x ∈ m, g k x) ⊣⊢
             [∗ map] k↦x ∈ m, auth_own γ (g k x).
Proof. apply (big_opM_commute1 _). Qed.
(* iris_deprecated/base_logic/auth.v *)
Lemma big_opS_auth_own `{Countable B} γ (g : B → A) (X : gset B) :
    X ≠ ∅ →
    auth_own γ ([^op set] x ∈ X, g x) ⊣⊢ [∗ set] x ∈ X, auth_own γ (g x).
Proof. apply (big_opS_commute1 _). Qed.
(* iris_deprecated/base_logic/auth.v *)
Lemma big_opMS_auth_own `{Countable B} γ (g : B → A) (X : gmultiset B) :
    X ≠ ∅ →
    auth_own γ ([^op mset] x ∈ X, g x) ⊣⊢ [∗ mset] x ∈ X, auth_own γ (g x).
Proof. apply (big_opMS_commute1 _). Qed.
(* iris_deprecated/base_logic/auth.v *)
Instance auth_own_cmra_sep_entails_homomorphism γ :
    MonoidHomomorphism op uPred_sep (⊢) (auth_own γ).
Proof.
    split; [split|]; try apply _.
    - intros. by rewrite auth_own_op.
    - apply (affine _).
  Qed.
(* iris_deprecated/base_logic/auth.v *)
Lemma big_opL_auth_own_1 {B} γ (g : nat → B → A) (l : list B) :
    auth_own γ ([^op list] k↦x ∈ l, g k x) ⊢
             [∗ list] k↦x ∈ l, auth_own γ (g k x).
Proof. apply (big_opL_commute _). Qed.
(* iris_deprecated/base_logic/auth.v *)
Lemma big_opM_auth_own_1 `{Countable K} {B} γ (g : K → B → A)
        (m : gmap K B) :
    auth_own γ ([^op map] k↦x ∈ m, g k x) ⊢ [∗ map] k↦x ∈ m, auth_own γ (g k x).
Proof. apply (big_opM_commute _). Qed.
(* iris_deprecated/base_logic/auth.v *)
Lemma big_opS_auth_own_1 `{Countable B} γ (g : B → A) (X : gset B) :
    auth_own γ ([^op set] x ∈ X, g x) ⊢ [∗ set] x ∈ X, auth_own γ (g x).
Proof. apply (big_opS_commute _). Qed.
(* iris_deprecated/base_logic/auth.v *)
Lemma big_opMS_auth_own_1 `{Countable B} γ (g : B → A)
        (X : gmultiset B) :
    auth_own γ ([^op mset] x ∈ X, g x) ⊢ [∗ mset] x ∈ X, auth_own γ (g x).
Proof. apply (big_opMS_commute _). Qed.
(* iris_deprecated/base_logic/auth.v *)
Instance own_mono' γ : Proper (flip (≼) ==> (⊢)) (auth_own γ).
Proof. intros a1 a2. apply auth_own_mono. Qed.