(* iris/bi/lib/counterexamples.v *)
From iris.bi Require Export bi
From iris.proofmode Require Import proofmode
From iris.prelude Require Import options
FromExist P Φ → FromExist (fupd E P) (λ a, fupd E (Φ a))

Lemma sep_dupP : P -∗ P ∗ P.
  Proof.
    iIntros "HP". iDestruct (em P) as "[HP'|HnotP]".
    - iFrame "HP HP'".
    - iExFalso. by iApply "HnotP".
  Qed.

Lemma and_sepP Q : P ∧ Q -∗ P ∗ Q.
  Proof.
    iIntros "HPQ". iDestruct (sep_dup with "HPQ") as "[HPQ HPQ']".
    iSplitL "HPQ".
    - by iDestruct "HPQ" as "[HP _]".
    - by iDestruct "HPQ'" as "[_ HQ]".
  Qed.

Lemma later_anythingP : ⊢@{PROP} ▷ P.
  Proof.
    iDestruct (em (▷ False)) as "#[HP|HnotP]".
    - iNext. done.
    - iExFalso. iLöb as "IH". iSpecialize ("HnotP" with "IH"). done.
  Qed.

Global Instancebupd_mono' : Proper ((⊢) ==> (⊢)) bupd.
  Proof. intros P Q ?. by apply bupd_mono. Qed.

Global Instanceelim_modal_bupd p P Q : ElimModal True p false (|==> P) P (|==> Q) (|==> Q).
  Proof.
    by rewrite /ElimModal bi.intuitionistically_if_elim
      bupd_frame_r bi.wand_elim_r bupd_trans.
  Qed.

Definition A(i : ident) : PROP := ∃ P, □ ¬ P ∗ saved i P.

Lemma A_alloc: ⊢ |==> ∃ i, saved i (A i).
  Proof. by apply sprop_alloc_dep. Qed.

Lemma saved_NAi : saved i (A i) ⊢ ¬ A i.
  Proof.
    iIntros "#Hs #HA". iPoseProof "HA" as "HA'".
    iDestruct "HA'" as (P) "[HNP HsP]". iApply "HNP".
    iDestruct (sprop_agree i P (A i) with "[]") as "#[_ HP]".
    { eauto. }
    iApply "HP". done.
  Qed.

Lemma saved_Ai : saved i (A i) ⊢ A i.
  Proof.
    iIntros "#Hs". iExists (A i). iFrame "Hs".
    iIntros "!>". by iApply saved_NA.
  Qed.

Lemma contradiction: False.
  Proof using All.
    apply consistency.
    iMod A_alloc as (i) "#H".
    iPoseProof (saved_NA with "H") as "HN".
    iApply bupd_intro. iApply "HN". iApply saved_A. done.
  Qed.

Inductive mask:= M0 | M1.
  Context (fupd : mask → PROP → PROP).
  Hypothesis fupd_intro : ∀ E P, P ⊢ fupd E P.
  Hypothesis fupd_mono : ∀ E P Q, (P ⊢ Q) → fupd E P ⊢ fupd E Q.
  Hypothesis fupd_fupd : ∀ E P, fupd E (fupd E P) ⊢ fupd E P.
  Hypothesis fupd_frame_l : ∀ E P Q, P ∗ fupd E Q ⊢ fupd E (P ∗ Q).
  Hypothesis fupd_mask_mono : ∀ P, fupd M0 P ⊢ fupd M1 P.

Global Argumentsinv _ _%_I.
  Hypothesis inv_persistent : ∀ i P, Persistent (inv i P).
  Hypothesis inv_alloc : ∀ P, P ⊢ fupd M1 (∃ i, inv i P).
  Hypothesis inv_fupd :
    ∀ i P Q R, (P ∗ Q ⊢ fupd M0 (P ∗ R)) → (inv i P ∗ Q ⊢ fupd M1 R).

Lemma inv_fupd'i P R : inv i P ∗ (P -∗ fupd M0 (P ∗ fupd M1 R)) ⊢ fupd M1 R.
  Proof.
    iIntros "(#HiP & HP)". iApply fupd_fupd. iApply inv_fupd; last first.
    { iSplit; first done. iExact "HP". }
    iIntros "(HP & HPw)". by iApply "HPw".
  Qed.

Global Instancefupd_mono' E : Proper ((⊢) ==> (⊢)) (fupd E).
  Proof. intros P Q ?. by apply fupd_mono. Qed.

Global Instancefupd_proper E : Proper ((⊣⊢) ==> (⊣⊢)) (fupd E).
  Proof.
    intros P Q; rewrite !bi.equiv_entails=> -[??]; split; by apply fupd_mono.
  Qed.

Lemma fupd_frame_rE P Q : fupd E P ∗ Q ⊢ fupd E (P ∗ Q).
  Proof. by rewrite comm fupd_frame_l comm. Qed.

Global Instanceelim_fupd_fupd p E P Q :
    ElimModal True p false (fupd E P) P (fupd E Q) (fupd E Q).
  Proof.
    by rewrite /ElimModal bi.intuitionistically_if_elim
      fupd_frame_r bi.wand_elim_r fupd_fupd.
  Qed.

Global Instanceelim_fupd0_fupd1 p P Q :
    ElimModal True p false (fupd M0 P) P (fupd M1 Q) (fupd M1 Q).
  Proof.
    by rewrite /ElimModal bi.intuitionistically_if_elim
      fupd_frame_r bi.wand_elim_r fupd_mask_mono fupd_fupd.
  Qed.

Global Instanceexists_split_fupd0 {A} E P (Φ : A → PROP) :
    FromExist P Φ → FromExist (fupd E P) (λ a, fupd E (Φ a)).
  Proof.
    rewrite /FromExist=>HP. apply bi.exist_elim=> a.
    apply fupd_mono. by rewrite -HP -(bi.exist_intro a).
  Qed.

Definition saved(γ : gname) (P : PROP) : PROP :=
      ∃ i, inv i (start γ ∨ (finished γ ∗ □ P)).

Global Instancesaved_persistent γ P : Persistent (saved γ P) := _.

Lemma saved_alloc(P : gname → PROP) : ⊢ fupd M1 (∃ γ, saved γ (P γ)).
    Proof.
      iIntros "". iMod (sts_alloc) as (γ) "Hs".
      iMod (inv_alloc (start γ ∨ (finished γ ∗ □ (P γ))) with "[Hs]") as (i) "#Hi".
      { auto. }
      iApply fupd_intro. by iExists γ, i.
    Qed.

Lemma saved_castγ P Q : saved γ P ∗ saved γ Q ∗ □ P ⊢ fupd M1 (□ Q).
    Proof.
      iIntros "(#HsP & #HsQ & #HP)". iDestruct "HsP" as (i) "HiP".
      iApply (inv_fupd' i). iSplit; first done.
      iIntros "HaP". iAssert (fupd M0 (finished γ)) with "[HaP]" as "> Hf".
      { iDestruct "HaP" as "[Hs | [Hf _]]".
        - by iApply start_finish.
        - by iApply fupd_intro. }
      iDestruct (finished_dup with "Hf") as "[Hf Hf']".
      iApply fupd_intro. iSplitL "Hf'"; first by eauto.

Notation not_fupdP := (□ (P -∗ fupd M1 False))%I.

Definition Ai : PROP := ∃ P, not_fupd P ∗ saved i P.

Global InstanceA_persistent i : Persistent (A i) := _.

Lemma A_alloc: ⊢ fupd M1 (∃ i, saved i (A i)).
    Proof. by apply saved_alloc. Qed.

Lemma saved_NAi : saved i (A i) ⊢ not_fupd (A i).
    Proof.
      iIntros "#Hi !> #HA". iPoseProof "HA" as "HA'".
      iDestruct "HA'" as (P) "#[HNP Hi']".
      iMod (saved_cast i (A i) P with "[]") as "HP".
      { eauto. }
      by iApply "HNP".
    Qed.

Lemma saved_Ai : saved i (A i) ⊢ A i.
    Proof.
      iIntros "#Hi". iExists (A i). iFrame "#".
      by iApply saved_NA.
    Qed.

Lemma contradiction: False.
    Proof using All.
      apply consistency. iIntros "".
      iMod A_alloc as (i) "#H".
      iPoseProof (saved_NA with "H") as "HN".
      iApply "HN". iApply saved_A. done.
    Qed.

Definition B: PROP := □ fupd M1 False.

Definition P(γ : gname) : PROP := start γ ∨ B.

Definition I(i : name) (γ : gname) : PROP := inv i (P γ).

Lemma finished_contradictionγ i :
      finished γ ∗ I i γ -∗ B.
    Proof.
      iIntros "[#Hfin #HI] !>".
      iApply (inv_fupd' i). iSplit; first done.
      iIntros "[Hstart|#Hfalse]".
      { iDestruct (finished_not_start with "[$Hfin $Hstart]") as %[]. }
      iApply fupd_intro. iSplitR; last done.
      by iRight.
    Qed.

Lemma invariant_contradictionγ i :
      I i γ -∗ B.
    Proof.
      iIntros "#HI !>".
      iApply (inv_fupd' i). iSplit; first done.
      iIntros "HP".
      iAssert (fupd M0 B) with "[HP]" as ">#Hfalse".
      { iDestruct "HP" as "[Hstart|#Hfalse]"; last by iApply fupd_intro.
        iMod (start_finish with "Hstart"). iApply fupd_intro.

Lemma contradiction': False.
    Proof using All.
      apply consistency.
      iMod sts_alloc as (γ) "Hstart".
      iMod (inv_alloc (P γ) with "[Hstart]") as (i) "HI".
      { by iLeft. }
      iDestruct (invariant_contradiction with "HI") as "#>[]".
    Qed.

Inductive mask:= M0 | M1.
  Context (fupd : mask → mask → PROP → PROP).
  Hypothesis fupd_intro : ∀ E P, P ⊢ fupd E E P.
  Hypothesis fupd_mono : ∀ E1 E2 P Q, (P ⊢ Q) → fupd E1 E2 P ⊢ fupd E1 E2 Q.
  Hypothesis fupd_fupd : ∀ E1 E2 E3 P, fupd E1 E2 (fupd E2 E3 P) ⊢ fupd E1 E3 P.
  Hypothesis fupd_frame_l : ∀ E1 E2 P Q, P ∗ fupd E1 E2 Q ⊢ fupd E1 E2 (P ∗ Q).

Global Instancefupd_mono' E1 E2 : Proper ((⊢) ==> (⊢)) (fupd E1 E2).
  Proof. intros P Q ?. by apply fupd_mono. Qed.

Global Instancefupd_proper E1 E2 : Proper ((⊣⊢) ==> (⊣⊢)) (fupd E1 E2).
  Proof.
    intros P Q; rewrite !bi.equiv_entails=> -[??]; split; by apply fupd_mono.
  Qed.

Lemma fupd_frame_rE1 E2 P Q : fupd E1 E2 P ∗ Q ⊢ fupd E1 E2 (P ∗ Q).
  Proof. by rewrite comm fupd_frame_l comm. Qed.

Global Instanceelim_fupd_fupd p E1 E2 E3 P Q :
    ElimModal True p false (fupd E1 E2 P) P (fupd E1 E3 Q) (fupd E2 E3 Q).
  Proof.
    by rewrite /ElimModal bi.intuitionistically_if_elim
      fupd_frame_r bi.wand_elim_r fupd_fupd.
  Qed.

Lemma leakP : P -∗ fupd M1 M1 emp.
  Proof.
    iIntros "HP".
    iMod (cinv_alloc _ True with "[//]") as (γ) "[Hinv Htok]".
    iMod (cinv_acc with "Hinv Htok") as "(Htrue & Htok & Hclose)".
    iApply "Hclose". done.
  Qed.