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.