(* iris/proofmode/modalities.v *)
From stdpp Require Import namespaces
From iris.bi Require Export bi
From iris.prelude Require Import options

Inductive modality_action(PROP1 : bi) : bi → Type :=
  | MIEnvIsEmpty {PROP2 : bi} : modality_action PROP1 PROP2
  | MIEnvForall (C : PROP1 → Prop) : modality_action PROP1 PROP1
  | MIEnvTransform {PROP2 : bi} (C : PROP2 → PROP1 → Prop) : modality_action PROP1 PROP2
  | MIEnvClear {PROP2} : modality_action PROP1 PROP2
  | MIEnvId : modality_action PROP1 PROP1.

Global ArgumentsMIEnvIsEmpty {_ _}.

Global ArgumentsMIEnvForall {_} _.

Global ArgumentsMIEnvTransform {_ _} _.

Global ArgumentsMIEnvClear {_ _}.

Global ArgumentsMIEnvId {_}.

Notation MIEnvFilterC := (MIEnvTransform (TCDiag C)).

Definition modality_intuitionistic_action_spec{PROP1 PROP2}
    (s : modality_action PROP1 PROP2) : (PROP1 → PROP2) → Prop :=
  match s with
  | MIEnvIsEmpty => λ M, True
  | MIEnvForall C => λ M,
     (∀ P, C P → □ P ⊢ M (□ P)) ∧
     (∀ P Q, M P ∧ M Q ⊢ M (P ∧ Q))
  | MIEnvTransform C => λ M,
     (∀ P Q, C P Q → □ P ⊢ M (□ Q)) ∧
     (∀ P Q, M P ∧ M Q ⊢ M (P ∧ Q))
  | MIEnvClear => λ M, True
  | MIEnvId => λ M, ∀ P, □ P ⊢ M (□ P)
  end.

Definition modality_spatial_action_spec{PROP1 PROP2}
    (s : modality_action PROP1 PROP2) : (PROP1 → PROP2) → Prop :=
  match s with
  | MIEnvIsEmpty => λ M, True
  | MIEnvForall C => λ M, ∀ P, C P → P ⊢ M P
  | MIEnvTransform C => λ M, ∀ P Q, C P Q → P ⊢ M Q
  | MIEnvClear => λ M, ∀ P, Absorbing (M P)
  | MIEnvId => λ M, ∀ P, P ⊢ M P
  end.

Record modality_mixin{PROP1 PROP2 : bi} (M : PROP1 → PROP2)
    (iaction saction : modality_action PROP1 PROP2) := {
  modality_mixin_intuitionistic : modality_intuitionistic_action_spec iaction M;
  modality_mixin_spatial : modality_spatial_action_spec saction M;
  modality_mixin_emp : emp ⊢ M emp;
  modality_mixin_mono P Q : (P ⊢ Q) → M P ⊢ M Q;
  modality_mixin_sep P Q : M P ∗ M Q ⊢ M (P ∗ Q)
}.

Record modality(PROP1 PROP2 : bi) := Modality {
  modality_car :> PROP1 → PROP2;
  modality_intuitionistic_action : modality_action PROP1 PROP2;
  modality_spatial_action : modality_action PROP1 PROP2;
  modality_mixin_of :
    modality_mixin modality_car modality_intuitionistic_action modality_spatial_action
}.

Global ArgumentsModality {_ _} _ {_ _} _.

Global Argumentsmodality_intuitionistic_action {_ _} _.

Global Argumentsmodality_spatial_action {_ _} _.

Lemma modality_intuitionistic_transformC P Q :
    modality_intuitionistic_action M = MIEnvTransform C → C P Q → □ P ⊢ M (□ Q).
  Proof. destruct M as [??? []]; naive_solver. Qed.

Lemma modality_and_transformC P Q :
    modality_intuitionistic_action M = MIEnvTransform C → M P ∧ M Q ⊢ M (P ∧ Q).
  Proof. destruct M as [??? []]; naive_solver. Qed.

Lemma modality_spatial_transformC P Q :
    modality_spatial_action M = MIEnvTransform C → C P Q → P ⊢ M Q.
  Proof. destruct M as [??? []]; naive_solver. Qed.

Lemma modality_spatial_clearP :
    modality_spatial_action M = MIEnvClear → Absorbing (M P).
  Proof. destruct M as [??? []]; naive_solver. Qed.

Lemma modality_emp: emp ⊢ M emp.
  Proof. eapply modality_mixin_emp, modality_mixin_of. Qed.

Lemma modality_monoP Q : (P ⊢ Q) → M P ⊢ M Q.
  Proof. eapply modality_mixin_mono, modality_mixin_of. Qed.

Lemma modality_sepP Q : M P ∗ M Q ⊢ M (P ∗ Q).
  Proof. eapply modality_mixin_sep, modality_mixin_of. Qed.

Global Instancemodality_mono' : Proper ((⊢) ==> (⊢)) M.
  Proof. intros P Q. apply modality_mono. Qed.

Global Instancemodality_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) M.
  Proof. intros P Q. apply modality_mono. Qed.

Global Instancemodality_proper : Proper ((≡) ==> (≡)) M.
  Proof. intros P Q. rewrite !equiv_entails=> -[??]; eauto using modality_mono. Qed.

Lemma modality_intuitionistic_forallC P :
    modality_intuitionistic_action M = MIEnvForall C → C P → □ P ⊢ M (□ P).
  Proof. destruct M as [??? []]; naive_solver. Qed.

Lemma modality_and_forallC P Q :
    modality_intuitionistic_action M = MIEnvForall C → M P ∧ M Q ⊢ M (P ∧ Q).
  Proof. destruct M as [??? []]; naive_solver. Qed.

Lemma modality_intuitionistic_idP :
    modality_intuitionistic_action M = MIEnvId → □ P ⊢ M (□ P).
  Proof. destruct M as [??? []]; naive_solver. Qed.

Lemma modality_spatial_forallC P :
    modality_spatial_action M = MIEnvForall C → C P → P ⊢ M P.
  Proof. destruct M as [??? []]; naive_solver. Qed.

Lemma modality_spatial_idP :
    modality_spatial_action M = MIEnvId → P ⊢ M P.
  Proof. destruct M as [??? []]; naive_solver. Qed.

Lemma modality_intuitionistic_forall_big_andC Ps :
    modality_intuitionistic_action M = MIEnvForall C →
    Forall C Ps →
    (<affine> [∧ list] P ∈ Ps, <pers> P) ⊢ M (<affine> [∧ list] P ∈ Ps, <pers> P).
  Proof.
    induction 2 as [|P Ps ? _ IH]; simpl.
    { rewrite affinely_True_emp. apply modality_emp. }
    rewrite affinely_and -modality_and_forall //. apply and_mono, IH.
    by eapply modality_intuitionistic_forall.
  Qed.

Lemma modality_intuitionistic_id_big_andPs :
    modality_intuitionistic_action M = MIEnvId →
    (<affine> [∧ list] P ∈ Ps, <pers> P) ⊢ M (<affine> [∧ list] P ∈ Ps, <pers> P).
  Proof.
    intros. induction Ps as [|P Ps IH]; simpl.
    { rewrite affinely_True_emp. apply modality_emp. }
    rewrite -affinely_and_r. rewrite {1}IH {IH}.
    rewrite !persistently_and_intuitionistically_sep_l.
    by rewrite {1}(modality_intuitionistic_id P) // modality_sep.
  Qed.

Lemma modality_spatial_forall_big_sepC Ps :
    modality_spatial_action M = MIEnvForall C →
    Forall C Ps → [∗] Ps ⊢ M ([∗] Ps).
  Proof.
    induction 2 as [|P Ps ? _ IH]; simpl.
    - by rewrite -modality_emp.
    - by rewrite -modality_sep -IH {1}(modality_spatial_forall _ P).
  Qed.

Lemma modality_id_mixin{PROP : bi} : modality_mixin (@id PROP) MIEnvId MIEnvId.
Proof. split; simpl; eauto. Qed.

Definition modality_id{PROP : bi} := Modality (@id PROP) modality_id_mixin.