(* tests/proofmode_iris.v *)
From iris.algebra Require Import frac
From iris.proofmode Require Import proofmode monpred
From iris.base_logic Require Import base_logic
From iris.base_logic.lib Require Import invariants cancelable_invariants na_invariants ghost_var
From iris.program_logic Require Import total_weakestpre
From iris.prelude Require Import options

Lemma test_random_stuff(P1 P2 P3 : nat → uPred M) :
    ⊢ ∀ (x y : nat) a b,
      x ≡ y →
      □ (uPred_ownM (a ⋅ b) -∗
      (∃ y1 y2 c, P1 ((x + y1) + y2) ∧ True ∧ □ uPred_ownM c) -∗
      □ ▷ (∀ z, P2 z ∨ True → P2 z) -∗
      ▷ (∀ n m : nat, P1 n → □ ((True ∧ P2 n) → □ (⌜n = n⌝ ↔ P3 n))) -∗
      ▷ ⌜x = 0⌝ ∨ ∃ x z, ▷ P3 (x + z) ∗ uPred_ownM b ∗ uPred_ownM (core b)).
  Proof.
    iIntros (i [|j] a b ?) "!> [Ha Hb] H1 #H2 H3"; setoid_subst.
    { iLeft. by iNext. }
    iRight.
    iDestruct "H1" as (z1 z2 c) "(H1&_&#Hc)".
    iPoseProof "Hc" as "foo".
    iRevert (a b) "Ha Hb". iIntros (b a) "Hb {foo} Ha".
    iAssert (uPred_ownM (a ⋅ core a)) with "[Ha]" as "[Ha #Hac]".
    { by rewrite cmra_core_r. }
    iIntros "{$Hac $Ha}".
    iExists (S j + z1), z2.
    iNext.
    iApply ("H3" $! _ 0 with "[$]").
    - iSplit; first done. iApply "H2". iLeft. iApply "H2". by iRight.
    - done.
  Qed.

Lemma test_iFrame_pure(x y z : M) :
    ✓ x → ⌜y ≡ z⌝ -∗ (✓ x ∧ ✓ x ∧ y ≡ z : uPred M).
  Proof. iIntros (Hv) "Hxy". by iFrame (Hv) "Hxy". Qed.

Lemma test_iAssert_modalityP : (|==> False) -∗ |==> P.
  Proof. iIntros. iAssert False%I with "[> - //]" as %[]. Qed.

Lemma test_iStartProof_1P : P -∗ P.
  Proof. iStartProof. iStartProof. iIntros "$". Qed.

Lemma test_iStartProof_2P : P -∗ P.
  Proof. iStartProof (uPred _). iStartProof (uPredI _). iIntros "$". Qed.

Lemma test_iStartProof_3P : P -∗ P.
  Proof. iStartProof (uPredI _). iStartProof (uPredI _). iIntros "$". Qed.

Lemma test_iStartProof_4P : P -∗ P.
  Proof. iStartProof (uPredI _). iStartProof (uPred _). iIntros "$". Qed.

Lemma test_except_0_invN P : ▷ False -∗ inv N P.
  Proof.
    iIntros "H". by iMod "H".
  Qed.

Lemma test_masksN E P Q R :
    ↑N ⊆ E →
    (True -∗ P -∗ inv N Q -∗ True -∗ R) -∗ P -∗ ▷ Q ={E}=∗ R.
  Proof.
    iIntros (?) "H HP HQ".
    iApply ("H" with "[% //] [$] [> HQ] [> //]").
    by iApply inv_alloc.
  Qed.

Lemma test_iInv_0N P: inv N (<pers> P) ={⊤}=∗ ▷ P.
  Proof.
    iIntros "#H".
    iInv N as "#H2". Show.
    iModIntro. iSplit; auto.
  Qed.

Lemma test_iInv_0_with_closeN P: inv N (<pers> P) ={⊤}=∗ ▷ P.
  Proof.
    iIntros "#H".
    iInv N as "#H2" "Hclose". Show.
    iMod ("Hclose" with "H2").
    iModIntro. by iNext.
  Qed.

Lemma test_iInv_1N E P:
    ↑N ⊆ E →
    inv N (<pers> P) ={E}=∗ ▷ P.
  Proof.
    iIntros (?) "#H".
    iInv N as "#H2".
    iModIntro. iSplit; auto.
  Qed.

Lemma test_iInv_2γ p N P:
    cinv N γ (<pers> P) ∗ cinv_own γ p ={⊤}=∗ cinv_own γ p ∗ ▷ P.
  Proof.
    Show.
    iIntros "(#?&?)".
    iInv N as "(#HP&Hown)". Show.
    iModIntro. iSplit; auto with iFrame.
  Qed.
  Check "test_iInv_2_with_close".

Lemma test_iInv_2_with_closeγ p N P:
    cinv N γ (<pers> P) ∗ cinv_own γ p ={⊤}=∗ cinv_own γ p ∗ ▷ P.
  Proof.
    iIntros "(#?&?)".
    iInv N as "(#HP&Hown)" "Hclose". Show.
    iMod ("Hclose" with "HP").
    iModIntro. iFrame. by iNext.
  Qed.

Lemma test_iInv_3γ p1 p2 N P:
    cinv N γ (<pers> P) ∗ cinv_own γ p1 ∗ cinv_own γ p2
      ={⊤}=∗ cinv_own γ p1 ∗ cinv_own γ p2  ∗ ▷ P.
  Proof.
    iIntros "(#?&Hown1&Hown2)".
    iInv N with "[Hown2 //]" as "(#HP&Hown2)".
    iModIntro. iSplit; auto with iFrame.
  Qed.
  Check "test_iInv_4".

Lemma test_iInv_4t N E1 E2 P:
    ↑N ⊆ E2 →
    na_inv t N (<pers> P) ∗ na_own t E1 ∗ na_own t E2
       ={⊤}=∗ na_own t E1 ∗ na_own t E2  ∗ ▷ P.
  Proof.
    iIntros (?) "(#?&Hown1&Hown2)".
    iInv N as "(#HP&Hown2)". Show.
    iModIntro. iSplitL "Hown2"; auto with iFrame.
  Qed.
  Check "test_iInv_4_with_close".

Lemma test_iInv_4_with_closet N E1 E2 P:
    ↑N ⊆ E2 →
    na_inv t N (<pers> P) ∗ na_own t E1 ∗ na_own t E2
         ={⊤}=∗ na_own t E1 ∗ na_own t E2  ∗ ▷ P.
  Proof.
    iIntros (?) "(#?&Hown1&Hown2)".
    iInv N as "(#HP&Hown2)" "Hclose". Show.
    iMod ("Hclose" with "[HP Hown2]").
    { iFrame. done. }
    iModIntro. iFrame. by iNext.
  Qed.

Lemma test_iInv_5t N E1 E2 P:
    ↑N ⊆ E2 →
    na_inv t N (<pers> P) ∗ na_own t E1 ∗ na_own t E2
      ={⊤}=∗ na_own t E1 ∗ na_own t E2  ∗ ▷ P.
  Proof.
    iIntros (?) "(#?&Hown1&Hown2)".
    iInv N with "Hown2" as "(#HP&Hown2)".
    iModIntro. iSplitL "Hown2"; auto with iFrame.
  Qed.

Lemma test_iInv_6t N E1 E2 P:
    ↑N ⊆ E1 →
    na_inv t N (<pers> P) ∗ na_own t E1 ∗ na_own t E2
      ={⊤}=∗ na_own t E1 ∗ na_own t E2  ∗ ▷ P.
  Proof.
    iIntros (?) "(#?&Hown1&Hown2)".
    iInv N with "Hown1" as "(#HP&Hown1)".
    iModIntro. iSplitL "Hown1"; auto with iFrame.
  Qed.

Lemma test_iInv_7t N1 N2 N3 E1 E2 P:
    ↑N3 ⊆ E1 →
    inv N1 P ∗ na_inv t N3 (<pers> P) ∗ inv N2 P  ∗ na_own t E1 ∗ na_own t E2
      ={⊤}=∗ na_own t E1 ∗ na_own t E2  ∗ ▷ P.
  Proof.
    iIntros (?) "(#?&#?&#?&Hown1&Hown2)".
    iInv N3 with "Hown1" as "(#HP&Hown1)".
    iModIntro. iSplitL "Hown1"; auto with iFrame.
  Qed.

Lemma test_iInv_8N : ∃ P, inv N P ={⊤}=∗ P ≡ True ∧ inv N P.
  Proof.
    eexists. iIntros "#H".
    iInv N as "HP". iFrame "HP". auto.
  Qed.

Lemma test_iInv_9t N1 N2 N3 E1 E2 P:
    ↑N3 ⊆ E1 →
    inv N1 P ∗ na_inv t N3 (<pers> P) ∗ inv N2 P  ∗ na_own t E1 ∗ na_own t E2
      ={⊤}=∗ na_own t E1 ∗ na_own t E2  ∗ ▷ P.
  Proof.
    iIntros (?) "(#?&#HInv&#?&Hown1&Hown2)".
    iInv "HInv" with "Hown1" as "(#HP&Hown1)".
    iModIntro. iSplitL "Hown1"; auto with iFrame.
  Qed.

Lemma test_iInv_10t N1 N2 N3 E1 E2 P:
    ↑N3 ⊆ E1 →
    inv N1 P ∗ na_inv t N3 (<pers> P) ∗ inv N2 P  ∗ na_own t E1 ∗ na_own t E2
      ={⊤}=∗ na_own t E1 ∗ na_own t E2  ∗ ▷ P.
  Proof.
    iIntros (?) "(#?&#HInv&#?&Hown1&Hown2)".
    iInv "HInv" as "(#HP&Hown1)".
    iModIntro. iSplitL "Hown1"; auto with iFrame.
  Qed.

Lemma test_iInv_11N P: inv N (<pers> P) ={⊤}=∗ ▷ P.
  Proof.
    let H := iFresh in
    (iIntros H; iInv H as "#H2"). auto.
  Qed.

Lemma test_iInv_12N P: inv N (<pers> P) ={⊤}=∗ True.
  Proof.
    iIntros "H".
    Fail iInv 34 as "#H2".
    Fail iInv nroot as "#H2".
    Fail iInv "H2" as "#H2".
    done.
  Qed.
  Check "test_iInv_error_no_update".

Lemma test_iInv_error_no_updateN P : inv N P -∗ True.
  Proof.
    iIntros "H".
    Fail iInv N as "H".
  Abort.

Lemma test_iInv_13N:
    inv N (∃ (v1 v2 v3 : nat), emp ∗ emp ∗ emp) ={⊤}=∗ ▷ emp.
  Proof.
    iIntros "H"; iInv "H" as (v1 v2 v3) "(?&?&_)".
    eauto.
  Qed.

Lemma test_iInv_accessor_variableΦ : INV Φ ={⊤}=∗ INV Φ.
    Proof.
      iIntros "HINV".

Theorem test_iApply_inG`{!inG Σ A} γ (x x' : A) :
    x' ≼ x →
    own γ x -∗ own γ x'.
  Proof. intros. by iApply own_mono. Qed.
  Check "test_frac_split_combine".

Lemma test_frac_split_combine`{!inG Σ fracR} γ :
    own γ 1%Qp -∗ own γ 1%Qp.
  Proof.
    iIntros "[H1 H2]". Show.
    iCombine "H1 H2" as "H". Show.
    iExact "H".
  Qed.
  Check "test_iDestruct_mod_not_fresh".

Lemma test_iDestruct_mod_not_freshP Q :
    P -∗ (|={⊤}=> Q) -∗ (|={⊤}=> False).
  Proof.
    iIntros "H H'". Fail iDestruct "H'" as ">H".
  Abort.

Lemma test_iIntros_lcn m : £ (S n + m) -∗ £ (S n).
  Proof. iIntros "[Hlc1 Hlc2]". Show. iExact "Hlc1". Qed.
  Check "lc_iSplit_lc".

Lemma lc_iSplit_lcn m : £ (S n) -∗ £ m -∗ £ (S n + m).
  Proof. iIntros "Hlc1 Hlc2". iSplitL "Hlc1". Show. all: done. Qed.

Lemma test_iCombine_ghost_var_no_beta`{!ghost_varG Σ nat} l (v : nat) q1 q2 :
    ghost_var l q1 v -∗ ghost_var l q2 v -∗ ghost_var l (q1+q2) v.
  Proof.
    iIntros "H1 H2". iCombine "H1 H2" as "H". Show. done.
  Qed.

Lemma iMod_WP_mask_mismatchE1 E2 P (e : expr Λ) :
    (|={E2}=> P) ⊢ WP e @ E1 {{ _, True }}.
  Proof.
    Fail iIntros ">HP".
    iIntros "HP". Fail iMod "HP".
    iApply fupd_wp; iMod (fupd_mask_subseteq E2).
  Abort.
  Check "iMod_WP_atomic_mask_mismatch".

Lemma iMod_WP_atomic_mask_mismatchE1 E2 E2' P (e : expr Λ) :
    (|={E2,E2'}=> P) ⊢ WP e @ E1 {{ _, True }}.
  Proof.
    Fail iIntros ">HP".
    iIntros "HP". Fail iMod "HP".
    iMod (fupd_mask_subseteq E2).
  Abort.
  Check "iFrame_WP_no_instantiate".

Lemma iFrame_WP_no_instantiate(e : expr Λ) (Φ : nat → iProp Σ) :
    □ Φ 0 ⊢ WP e {{ _, Φ 0 ∗ ∃ n, Φ n }}.
  Proof.
    iIntros "#$".

Lemma iInv_WP(e : expr Λ) N E P :
    ↑N ⊆ E →
    inv N P ⊢ WP e @ E {{ _, True }}.
  Proof.
    iIntros (?) "Hinv".
    iInv N as "HP". Show.
  Abort.

Lemma iMod_TWP_mask_mismatchE1 E2 P (e : expr Λ) :
    (|={E2}=> P) ⊢ WP e @ E1 [{ _, True }].
  Proof.
    Fail iIntros ">HP".
    iIntros "HP". Fail iMod "HP".
    iApply fupd_twp; iMod (fupd_mask_subseteq E2).
  Abort.
  Check "iMod_TWP_atomic_mask_mismatch".

Lemma iMod_TWP_atomic_mask_mismatchE1 E2 E2' P (e : expr Λ) :
    (|={E2,E2'}=> P) ⊢ WP e @ E1 [{ _, True }].
  Proof.
    Fail iIntros ">HP".
    iIntros "HP". Fail iMod "HP".
    iMod (fupd_mask_subseteq E2).
  Abort.
  Check "iFrame_TWP_no_instantiate".

Lemma iFrame_TWP_no_instantiate(e : expr Λ) (Φ : nat → iProp Σ) :
    □ Φ 0 ⊢ WP e [{ _, Φ 0 ∗ ∃ n, Φ n }].
  Proof.
    iIntros "#$".

Lemma iInv_TWP(e : expr Λ) N E P :
    ↑N ⊆ E →
    inv N P ⊢ WP e @ E [{ _, True }].
  Proof.
    iIntros (?) "Hinv".
    iInv N as "HP". Show.
  Abort.

Local NotationmonPred := (monPred I (iPropI Σ)).

Local NotationmonPredI := (monPredI I (iPropI Σ)).
  Implicit Types P Q R : monPred.
  Implicit Types 𝓟 𝓠 𝓡 : iProp Σ.
  Check "test_iInv".

Lemma test_iInvN E 𝓟 :
    ↑N ⊆ E →
    ⎡inv N 𝓟⎤ ⊢@{monPredI} |={E}=> emp.
  Proof.
    iIntros (?) "Hinv".
    iInv N as "HP". Show.
    iFrame "HP". auto.
  Qed.
  Check "test_iInv_with_close".

Lemma test_iInv_with_closeN E 𝓟 :
    ↑N ⊆ E →
    ⎡inv N 𝓟⎤ ⊢@{monPredI} |={E}=> emp.
  Proof.
    iIntros (?) "Hinv".
    iInv N as "HP" "Hclose". Show.
    iMod ("Hclose" with "HP"). auto.
  Qed.