Merge branch 'robbert/sprop' into 'master'

Step-indexed propositions

See merge request iris/iris!304

CHANGELOG.md

@@ -42,6 +42,8 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 * Removed `Core` type class for defining the total core; it is now always
   defined in terms of the partial core. The only user of this type class was the
   STS RA.
+* Added the type `siProp` of "plain" step-indexed propositions, together with
+  basic proofmode support.
 
 ## Iris 3.2.0 (released 2019-08-29)
 

_CoqProject

@@ -41,6 +41,8 @@ theories/algebra/namespace_map.v
 theories/algebra/lib/excl_auth.v
 theories/algebra/lib/frac_auth.v
 theories/algebra/lib/ufrac_auth.v
+theories/si_logic/siprop.v
+theories/si_logic/bi.v
 theories/bi/notation.v
 theories/bi/interface.v
 theories/bi/derived_connectives.v

tests/proofmode_siprop.v

+From iris.proofmode Require Import tactics .
+From iris.si_logic Require Import bi.
+Set Ltac Backtrace.
+
+Section si_logic_tests.
+  Implicit Types P Q R : siProp.
+
+  Lemma test_everything_persistent P : P -∗ P.
+  Proof. by iIntros "#HP". Qed.
+
+  Lemma test_everything_affine P : P -∗ True.
+  Proof. by iIntros "_". Qed.
+
+  Lemma test_iIntro_impl P Q R : (P → Q ∧ R → P ∧ R)%I.
+  Proof. iIntros "#HP #[HQ HR]". auto. Qed.
+
+  Lemma test_iApply_impl_1 P Q R : (P → (P → Q) → Q)%I.
+  Proof. iIntros "HP HPQ". by iApply "HPQ". Qed.
+
+  Lemma test_iApply_impl_2 P Q R : (P → (P → Q) → Q)%I.
+  Proof. iIntros "#HP #HPQ". by iApply "HPQ". Qed.
+End si_logic_tests.

theories/si_logic/bi.v

+From iris.bi Require Export bi.
+From iris.si_logic Require Export siprop.
+Import siProp_primitive.
+
+(** BI instances for [siProp], and re-stating the remaining primitive laws in
+terms of the BI interface.  This file does *not* unseal. *)
+
+(** 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.
+Definition siProp_sep : siProp → siProp → siProp := siProp_and.
+Definition siProp_wand : siProp → siProp → siProp := siProp_impl.
+Definition siProp_persistently (P : siProp) : siProp := P.
+Definition siProp_plainly (P : siProp) : siProp := P.
+
+Local Existing Instance entails_po.
+
+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
+    siProp_persistently.
+Proof.
+  split.
+  - exact: entails_po.
+  - exact: equiv_spec.
+  - exact: pure_ne.
+  - exact: and_ne.
+  - exact: or_ne.
+  - exact: impl_ne.
+  - exact: forall_ne.
+  - exact: exist_ne.
+  - exact: and_ne.
+  - exact: impl_ne.
+  - solve_proper.
+  - exact: pure_intro.
+  - exact: pure_elim'.
+  - exact: @pure_forall_2.
+  - 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'.
+  - (* (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.
+
+Lemma siProp_sbi_mixin : SbiMixin
+  siProp_entails siProp_pure siProp_or siProp_impl
+  (@siProp_forall) (@siProp_exist) siProp_sep
+  siProp_persistently (@siProp_internal_eq) siProp_later.
+Proof.
+  split.
+  - exact: later_contractive.
+  - exact: internal_eq_ne.
+  - exact: @internal_eq_refl.
+  - exact: @internal_eq_rewrite.
+  - exact: @fun_ext.
+  - exact: @sig_eq.
+  - exact: @discrete_eq_1.
+  - exact: @later_eq_1.
+  - exact: @later_eq_2.
+  - 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.
+
+Canonical Structure siPropI : bi :=
+  {| bi_ofe_mixin := ofe_mixin_of siProp; bi_bi_mixin := siProp_bi_mixin |}.
+Canonical Structure siPropSI : sbi :=
+  {| sbi_ofe_mixin := ofe_mixin_of siProp;
+     sbi_bi_mixin := siProp_bi_mixin; sbi_sbi_mixin := siProp_sbi_mixin |}.
+
+Coercion siProp_valid (P : siProp) : Prop := bi_emp_valid P.
+
+Lemma siProp_plainly_mixin : BiPlainlyMixin siPropSI siProp_plainly.
+Proof.
+  split; try done.
+  - solve_proper.
+  - (* P ⊢ ■ emp *)
+    intros P. by apply pure_intro.
+  - (* ■ P ∗ Q ⊢ ■ P *)
+    intros P Q. apply and_elim_l.
+  - (* ■ ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q *)
+    intros P Q. apply prop_ext_2.
+Qed.
+Global Instance siProp_plainlyC : BiPlainly siPropSI :=
+  {| bi_plainly_mixin := siProp_plainly_mixin |}.
+
+(** extra BI instances *)
+
+Global Instance siProp_affine : BiAffine siPropI | 0.
+Proof. intros P. exact: pure_intro. Qed.
+(* Also add this to the global hint database, otherwise [eauto] won't work for
+many lemmas that have [BiAffine] as a premise. *)
+Hint Immediate siProp_affine : core.
+
+Global Instance siProp_plain (P : siProp) : Plain P | 0.
+Proof. done. Qed.
+Global Instance siProp_persistent (P : siProp) : Persistent P.
+Proof. done. Qed.
+
+Global Instance siProp_plainly_exist_1 : BiPlainlyExist siPropSI.
+Proof. done. Qed.
+
+(** Re-state/export soundness lemmas *)
+
+Module siProp.
+Section restate.
+Lemma pure_soundness φ : bi_emp_valid (PROP:=siPropI) ⌜ φ ⌝ → φ.
+Proof. apply pure_soundness. Qed.
+
+Lemma internal_eq_soundness {A : ofeT} (x y : A) : (True ⊢@{siPropI} x ≡ y) → x ≡ y.
+Proof. apply internal_eq_soundness. Qed.
+
+Lemma later_soundness P : bi_emp_valid (PROP:=siPropI) (▷ P) → bi_emp_valid P.
+Proof. apply later_soundness. Qed.
+End restate.
+End siProp.

theories/si_logic/siprop.v

+From iris.algebra Require Export ofe.
+From iris.bi Require Import notation.
+
+(** 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
+}.
+Arguments siProp_holds : simpl never.
+Add Printing Constructor siProp.
+Delimit Scope siProp_scope with SI.
+Bind Scope siProp_scope with siProp.
+
+Section cofe.
+  Inductive siProp_equiv' (P Q : siProp) : Prop :=
+    { siProp_in_equiv : ∀ n, P n ↔ Q n }.
+  Instance siProp_equiv : Equiv siProp := siProp_equiv'.
+  Inductive siProp_dist' (n : nat) (P Q : siProp) : Prop :=
+    { siProp_in_dist : ∀ n', n' ≤ n → P n' ↔ Q n' }.
+  Instance siProp_dist : Dist siProp := siProp_dist'.
+  Definition siProp_ofe_mixin : OfeMixin siProp.
+  Proof.
+    split.
+    - 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; auto.
+  Qed.
+  Canonical Structure siPropC : ofeT := OfeT siProp siProp_ofe_mixin.
+
+  Program Definition siProp_compl : Compl siPropC := λ 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.
+  Global Program Instance siProp_cofe : Cofe siPropC := {| compl := siProp_compl |}.
+  Next Obligation.
+    intros n c; split=>i ?; symmetry; apply (chain_cauchy c i n); auto.
+  Qed.
+End cofe.
+
+(** logical entailement *)
+Inductive siProp_entails (P Q : siProp) : Prop :=
+  { siProp_in_entails : ∀ n, P n → Q n }.
+Hint Resolve siProp_closed : siProp_def.
+
+(** logical connectives *)
+Program Definition siProp_pure_def (φ : Prop) : siProp :=
+  {| siProp_holds n := φ |}.
+Solve Obligations with done.
+Definition siProp_pure_aux : seal (@siProp_pure_def). by eexists. Qed.
+Definition siProp_pure := unseal siProp_pure_aux.
+Definition siProp_pure_eq :
+  @siProp_pure = @siProp_pure_def := seal_eq siProp_pure_aux.
+
+Program Definition siProp_and_def (P Q : siProp) : siProp :=
+  {| siProp_holds n := P n ∧ Q n |}.
+Solve Obligations with naive_solver eauto 2 with siProp_def.
+Definition siProp_and_aux : seal (@siProp_and_def). by eexists. Qed.
+Definition siProp_and := unseal siProp_and_aux.
+Definition siProp_and_eq: @siProp_and = @siProp_and_def := seal_eq siProp_and_aux.
+
+Program Definition siProp_or_def (P Q : siProp) : siProp :=
+  {| siProp_holds n := P n ∨ Q n |}.
+Solve Obligations with naive_solver eauto 2 with siProp_def.
+Definition siProp_or_aux : seal (@siProp_or_def). by eexists. Qed.
+Definition siProp_or := unseal siProp_or_aux.
+Definition siProp_or_eq: @siProp_or = @siProp_or_def := seal_eq siProp_or_aux.
+
+Program Definition siProp_impl_def (P Q : siProp) : siProp :=
+  {| siProp_holds n := ∀ n', n' ≤ n → P n' → Q n' |}.
+Next Obligation. intros P Q [|n1] [|n2]; auto with lia. Qed.
+Definition siProp_impl_aux : seal (@siProp_impl_def). by eexists. Qed.
+Definition siProp_impl := unseal siProp_impl_aux.
+Definition siProp_impl_eq :
+  @siProp_impl = @siProp_impl_def := seal_eq siProp_impl_aux.
+
+Program Definition siProp_forall_def {A} (Ψ : A → siProp) : siProp :=
+  {| siProp_holds n := ∀ a, Ψ a n |}.
+Solve Obligations with naive_solver eauto 2 with siProp_def.
+Definition siProp_forall_aux : seal (@siProp_forall_def). by eexists. Qed.
+Definition siProp_forall {A} := unseal siProp_forall_aux A.
+Definition siProp_forall_eq :
+  @siProp_forall = @siProp_forall_def := seal_eq siProp_forall_aux.
+
+Program Definition siProp_exist_def {A} (Ψ : A → siProp) : siProp :=
+  {| siProp_holds n := ∃ a, Ψ a n |}.
+Solve Obligations with naive_solver eauto 2 with siProp_def.
+Definition siProp_exist_aux : seal (@siProp_exist_def). by eexists. Qed.
+Definition siProp_exist {A} := unseal siProp_exist_aux A.
+Definition siProp_exist_eq: @siProp_exist = @siProp_exist_def := seal_eq siProp_exist_aux.
+
+Program Definition siProp_internal_eq_def {A : ofeT} (a1 a2 : A) : siProp :=
+  {| siProp_holds n := a1 ≡{n}≡ a2 |}.
+Solve Obligations with naive_solver eauto 2 using (dist_le (A:=A)).
+Definition siProp_internal_eq_aux : seal (@siProp_internal_eq_def). by eexists. Qed.
+Definition siProp_internal_eq {A} := unseal siProp_internal_eq_aux A.
+Definition siProp_internal_eq_eq:
+  @siProp_internal_eq = @siProp_internal_eq_def := seal_eq siProp_internal_eq_aux.
+
+Program 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.
+Definition siProp_later_aux : seal (@siProp_later_def). by eexists. Qed.
+Definition siProp_later := unseal siProp_later_aux.
+Definition siProp_later_eq :
+  @siProp_later = @siProp_later_def := seal_eq siProp_later_aux.
+
+(** Primitive logical rules.
+    These are not directly usable later because they do not refer to the BI
+    connectives. *)
+Module siProp_primitive.
+Definition unseal_eqs :=
+  (siProp_pure_eq, siProp_and_eq, siProp_or_eq, siProp_impl_eq, siProp_forall_eq,
+  siProp_exist_eq, siProp_internal_eq_eq, siProp_later_eq).
+Ltac unseal := rewrite !unseal_eqs /=.
+
+Section primitive.
+Arguments siProp_holds !_ _ /.
+
+Notation "P ⊢ Q" := (siProp_entails P Q)
+  (at level 99, Q at level 200, right associativity).
+Notation "'True'" := (siProp_pure True) : siProp_scope.
+Notation "'False'" := (siProp_pure False) : siProp_scope.
+Notation "'⌜' φ '⌝'" := (siProp_pure φ%type%stdpp) : siProp_scope.
+Infix "∧" := siProp_and : siProp_scope.
+Infix "∨" := siProp_or : siProp_scope.
+Infix "→" := siProp_impl : siProp_scope.
+Notation "∀ x .. y , P" := (siProp_forall (λ x, .. (siProp_forall (λ y, P%SI)) ..)) : siProp_scope.
+Notation "∃ x .. y , P" := (siProp_exist (λ x, .. (siProp_exist (λ y, P%SI)) ..)) : siProp_scope.
+Notation "x ≡ y" := (siProp_internal_eq x y) : siProp_scope.
+Notation "▷ P" := (siProp_later P) (at level 20, right associativity) : siProp_scope.
+
+(** Below there follow the primitive laws for [siProp]. There are no derived laws
+in this file. *)
+
+(** 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.
+Lemma entails_anti_symm : AntiSymm (≡) siProp_entails.
+Proof. intros P Q HPQ HQP; split=> n; by split; [apply HPQ|apply HQP]. Qed.
+Lemma equiv_spec P Q : (P ≡ Q) ↔ (P ⊢ Q) ∧ (Q ⊢ P).
+Proof.
+  split.
+  - intros HPQ; split; split=> i; apply HPQ.
+  - intros [??]. by apply entails_anti_symm.
+Qed.
+
+(** Non-expansiveness and setoid morphisms *)
+Lemma pure_ne n : Proper (iff ==> dist n) siProp_pure.
+Proof. intros φ1 φ2 Hφ. by unseal. Qed.
+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.
+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.
+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.
+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.
+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.
+Lemma later_contractive : Contractive siProp_later.
+Proof.
+  unseal; intros [|n] P Q HPQ; split=> -[|n'] ? //=; try lia.
+  apply HPQ; lia.
+Qed.
+Lemma internal_eq_ne (A : ofeT) : 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.
+
+(** Introduction and elimination rules *)
+Lemma pure_intro (φ : Prop) P : φ → P ⊢ ⌜ φ ⌝.
+Proof. intros ?. unseal; by split. Qed.
+Lemma pure_elim' (φ : Prop) P : (φ → True ⊢ P) → ⌜ φ ⌝ ⊢ P.
+Proof. unseal=> HP; split=> n ?. by apply HP. Qed.
+Lemma pure_forall_2 {A} (φ : A → Prop) : (∀ a, ⌜ φ a ⌝) ⊢ ⌜ ∀ a, φ a ⌝.
+Proof. by unseal. Qed.
+
+Lemma and_elim_l P Q : P ∧ Q ⊢ P.
+Proof. unseal; by split=> n [??]. Qed.
+Lemma and_elim_r P Q : P ∧ Q ⊢ Q.
+Proof. unseal; by split=> n [??]. Qed.
+Lemma and_intro P Q R : (P ⊢ Q) → (P ⊢ R) → P ⊢ Q ∧ R.
+Proof. intros HQ HR; unseal; split=> n ?; by split; [apply HQ|apply HR]. Qed.
+
+Lemma or_intro_l P Q : P ⊢ P ∨ Q.
+Proof. unseal; split=> n ?; left; auto. Qed.
+Lemma or_intro_r P Q : Q ⊢ P ∨ Q.
+Proof. unseal; split=> n ?; right; auto. Qed.
+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.
+
+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.
+Lemma impl_elim_l' P Q R : (P ⊢ Q → R) → P ∧ Q ⊢ R.
+Proof. unseal=> HP; split=> n [??]. apply HP with n; auto. Qed.
+
+Lemma forall_intro {A} P (Ψ : A → siProp) : (∀ a, P ⊢ Ψ a) → P ⊢ ∀ a, Ψ a.
+Proof. unseal; intros HPΨ; split=> n ? a; by apply HPΨ. Qed.
+Lemma forall_elim {A} {Ψ : A → siProp} a : (∀ a, Ψ a) ⊢ Ψ a.
+Proof. unseal; split=> n HP; apply HP. Qed.
+
+Lemma exist_intro {A} {Ψ : A → siProp} a : Ψ a ⊢ ∃ a, Ψ a.
+Proof. unseal; split=> n ?; by exists a. Qed.
+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.
+
+(** Equality *)
+Lemma internal_eq_refl {A : ofeT} P (a : A) : P ⊢ (a ≡ a).
+Proof. unseal; by split=> n ? /=. Qed.
+Lemma internal_eq_rewrite {A : ofeT} 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.
+
+Lemma fun_ext {A} {B : A → ofeT} (f g : discrete_fun B) : (∀ x, f x ≡ g x) ⊢ f ≡ g.
+Proof. by unseal. Qed.
+Lemma sig_eq {A : ofeT} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊢ x ≡ y.
+Proof. by unseal. Qed.
+Lemma discrete_eq_1 {A : ofeT} (a b : A) : Discrete a → a ≡ b ⊢ ⌜a ≡ b⌝.
+Proof. unseal=> ?. split=> n. by apply (discrete_iff n). Qed.
+
+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.
+
+(** Later *)
+Lemma later_eq_1 {A : ofeT} (x y : A) : Next x ≡ Next y ⊢ ▷ (x ≡ y).
+Proof. by unseal. Qed.
+Lemma later_eq_2 {A : ofeT} (x y : A) : ▷ (x ≡ y) ⊢ Next x ≡ Next y.
+Proof. by unseal. Qed.
+
+Lemma later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q.
+Proof. unseal=> HP; split=>-[|n]; [done|apply HP; eauto using cmra_validN_S]. Qed.
+Lemma later_intro P : P ⊢ ▷ P.
+Proof. unseal; split=> -[|n] /= HP; eauto using siProp_closed. Qed.
+
+Lemma later_forall_2 {A} (Φ : A → siProp) : (∀ a, ▷ Φ a) ⊢ ▷ ∀ a, Φ a.
+Proof. unseal; by split=> -[|n]. Qed.
+Lemma later_exist_false {A} (Φ : A → siProp) :
+  (▷ ∃ a, Φ a) ⊢ ▷ False ∨ (∃ a, ▷ Φ a).
+Proof. unseal; split=> -[|[|n]] /=; eauto. Qed.
+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.
+
+(** Consistency/soundness statement *)
+Lemma pure_soundness φ : (True ⊢ ⌜ φ ⌝) → φ.
+Proof. unseal=> -[H]. by apply (H 0). Qed.
+
+Lemma internal_eq_soundness {A : ofeT} (x y : A) : (True ⊢ x ≡ y) → x ≡ y.
+Proof. unseal=> -[H]. apply equiv_dist=> n. by apply (H n). Qed.
+
+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.
+End primitive.
+End siProp_primitive.