From iris.base_logic Require Import lib.iprop. Module Type uses_spec. Parameter uses : Set. Parameter prop : ∀ {Σ}, uses -> iProp Σ -> iProp Σ. Parameter one : uses. Axiom one_spec : ∀ {Σ} {P : iProp Σ}, prop one P ⊣⊢ P. Parameter sep : uses -> uses -> uses. Axiom sep_spec : ∀ {Σ} {P : iProp Σ} u v, prop (sep u v) P ⊢ prop u P ∗ prop v P. Parameter and : uses -> uses -> uses. Axiom and_spec : ∀ {Σ} {P : iProp Σ} u v, prop (and u v) P ⊢ prop u P ∧ prop v P. End uses_spec. Module uses <: uses_spec. Inductive usesT := One | Many. Definition uses := usesT. Definition prop {Σ} (u : uses) (P : iProp Σ) : iProp Σ := match u with | One => P | Many => □P end. Definition one := One. Theorem one_spec {Σ} {P : iProp Σ} : prop one P ⊣⊢ P. Proof. done. Qed. Definition sep (u : uses) (v : uses) : uses := Many. Theorem sep_spec {Σ} {P : iProp Σ} u v : prop (sep u v) P ⊢ prop u P ∗ prop v P. Proof. have: ∀ x, □P ⊢ prop x P by case; [apply: bi.intuitionistically_elim | ]. move=> lemma. simpl. rewrite bi.intuitionistically_sep_dup. apply: bi.sep_mono; apply: lemma. Qed. Definition and (u : uses) (v : uses) : uses := match u, v with | One, One => One | _, _ => Many end. Theorem and_spec {Σ} {P : iProp Σ} u v : prop (and u v) P ⊢ prop u P ∧ prop v P. Proof. apply: bi.and_intro; case u; case v; try done; apply: bi.intuitionistically_elim. Qed. End uses.