From iris.program_logic Require Export weakestpre.
From iris.base_logic.lib Require Export viewshifts.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".

Definition ht `{irisG Λ Σ} (s : stuckness) (E : coPset) (P : iProp Σ)
    (e : expr Λ) (Φ : val Λ → iProp Σ) : iProp Σ :=
  (□ (P -∗ WP e @ s; E {{ Φ }}))%I.
Instance: Params (@ht) 5.

Notation "{{ P } } e @ s ; E {{ Φ } }" := (ht s E P%I e%E Φ%I)
  (at level 20, P, e, Φ at level 200,
   format "{{  P  } }  e  @  s ;  E  {{  Φ  } }") : C_scope.
Notation "{{ P } } e @ E {{ Φ } }" := (ht not_stuck E P%I e%E Φ%I)
  (at level 20, P, e, Φ at level 200,
   format "{{  P  } }  e  @  E  {{  Φ  } }") : C_scope.
Notation "{{ P } } e @ E ? {{ Φ } }" := (ht maybe_stuck E P%I e%E Φ%I)
  (at level 20, P, e, Φ at level 200,
   format "{{  P  } }  e  @  E  ? {{  Φ  } }") : C_scope.
Notation "{{ P } } e {{ Φ } }" := (ht not_stuck ⊤ P%I e%E Φ%I)
  (at level 20, P, e, Φ at level 200,
   format "{{  P  } }  e  {{  Φ  } }") : C_scope.
Notation "{{ P } } e ? {{ Φ } }" := (ht maybe_stuck ⊤ P%I e%E Φ%I)
  (at level 20, P, e, Φ at level 200,
   format "{{  P  } }  e  ? {{  Φ  } }") : C_scope.

Notation "{{ P } } e @ s ; E {{ v , Q } }" := (ht s E P%I e%E (λ v, Q)%I)
  (at level 20, P, e, Q at level 200,
   format "{{  P  } }  e  @  s ;  E  {{  v ,  Q  } }") : C_scope.
Notation "{{ P } } e @ E {{ v , Q } }" := (ht not_stuck E P%I e%E (λ v, Q)%I)
  (at level 20, P, e, Q at level 200,
   format "{{  P  } }  e  @  E  {{  v ,  Q  } }") : C_scope.
Notation "{{ P } } e @ E ? {{ v , Q } }" := (ht maybe_stuck E P%I e%E (λ v, Q)%I)
  (at level 20, P, e, Q at level 200,
   format "{{  P  } }  e  @  E  ? {{  v ,  Q  } }") : C_scope.
Notation "{{ P } } e {{ v , Q } }" := (ht not_stuck ⊤ P%I e%E (λ v, Q)%I)
  (at level 20, P, e, Q at level 200,
   format "{{  P  } }  e  {{  v ,  Q  } }") : C_scope.
Notation "{{ P } } e ? {{ v , Q } }" := (ht maybe_stuck ⊤ P%I e%E (λ v, Q)%I)
  (at level 20, P, e, Q at level 200,
   format "{{  P  } }  e  ? {{  v ,  Q  } }") : C_scope.

Section hoare.
Context `{irisG Λ Σ}.
Implicit Types s : stuckness.
Implicit Types P Q : iProp Σ.
Implicit Types Φ Ψ : val Λ → iProp Σ.
Implicit Types v : val Λ.
Import uPred.

Global Instance ht_ne s E n :
  Proper (dist n ==> eq ==> pointwise_relation _ (dist n) ==> dist n) (ht s E).
Proof. solve_proper. Qed.
Global Instance ht_proper s E :
  Proper ((≡) ==> eq ==> pointwise_relation _ (≡) ==> (≡)) (ht s E).
Proof. solve_proper. Qed.
Lemma ht_mono s E P P' Φ Φ' e :
  (P ⊢ P') → (∀ v, Φ' v ⊢ Φ v) → {{ P' }} e @ s; E {{ Φ' }} ⊢ {{ P }} e @ s; E {{ Φ }}.
Proof. by intros; apply persistently_mono, wand_mono, wp_mono. Qed.
Lemma ht_stuckness_mono s1 s2 E P Φ e :
  (s1 ≤ s2)%stuckness → {{ P }} e @ s1; E {{ Φ }} ⊢ {{ P }} e @ s2; E {{ Φ }}.
Proof. by intros; apply persistently_mono, wand_mono, wp_stuckness_mono. Qed.
Global Instance ht_mono' s E :
  Proper (flip (⊢) ==> eq ==> pointwise_relation _ (⊢) ==> (⊢)) (ht s E).
Proof. solve_proper. Qed.

Lemma ht_alt s E P Φ e : (P ⊢ WP e @ s; E {{ Φ }}) → {{ P }} e @ s; E {{ Φ }}.
Proof. iIntros (Hwp) "!# HP". by iApply Hwp. Qed.

Lemma ht_val s E v : {{ True }} of_val v @ s; E {{ v', ⌜v = v'⌝ }}.
Proof. iIntros "!# _". by iApply wp_value'. Qed.

Lemma ht_vs s E P P' Φ Φ' e :
  (P ={E}=> P') ∧ {{ P' }} e @ s; E {{ Φ' }} ∧ (∀ v, Φ' v ={E}=> Φ v)
  ⊢ {{ P }} e @ s; E {{ Φ }}.
Proof.
  iIntros "(#Hvs & #Hwp & #HΦ) !# HP". iMod ("Hvs" with "HP") as "HP".
  iApply wp_fupd. iApply (wp_wand with "[HP]"); [by iApply "Hwp"|].
  iIntros (v) "Hv". by iApply "HΦ".
Qed.

Lemma ht_atomic s E1 E2 P P' Φ Φ' e `{!Atomic s e} :
  (P ={E1,E2}=> P') ∧ {{ P' }} e @ s; E2 {{ Φ' }} ∧ (∀ v, Φ' v ={E2,E1}=> Φ v)
  ⊢ {{ P }} e @ s; E1 {{ Φ }}.
Proof.
  iIntros "(#Hvs & #Hwp & #HΦ) !# HP". iApply (wp_atomic _ _ E2); auto.
  iMod ("Hvs" with "HP") as "HP". iModIntro.
  iApply (wp_wand with "[HP]"); [by iApply "Hwp"|].
  iIntros (v) "Hv". by iApply "HΦ".
Qed.

Lemma ht_bind `{LanguageCtx Λ K} s E P Φ Φ' e :
  {{ P }} e @ s; E {{ Φ }} ∧ (∀ v, {{ Φ v }} K (of_val v) @ s; E {{ Φ' }})
  ⊢ {{ P }} K e @ s; E {{ Φ' }}.
Proof.
  iIntros "[#Hwpe #HwpK] !# HP". iApply wp_bind.
  iApply (wp_wand with "[HP]"); [by iApply "Hwpe"|].
  iIntros (v) "Hv". by iApply "HwpK".
Qed.

Lemma ht_forget_not_stuck s E P Φ e :
  {{ P }} e @ s; E {{ Φ }} ⊢ {{ P }} e @ E ?{{ Φ }}.
Proof.
  by iIntros "#Hwp !# ?"; iApply wp_forget_not_stuck; iApply "Hwp".
Qed.

Lemma ht_mask_weaken s E1 E2 P Φ e :
  E1 ⊆ E2 → {{ P }} e @ s; E1 {{ Φ }} ⊢ {{ P }} e @ s; E2 {{ Φ }}.
Proof.
  iIntros (?) "#Hwp !# HP". iApply (wp_mask_mono _ E1 E2); try done.
  by iApply "Hwp".
Qed.

Lemma ht_frame_l s E P Φ R e :
  {{ P }} e @ s; E {{ Φ }} ⊢ {{ R ∗ P }} e @ s; E {{ v, R ∗ Φ v }}.
Proof. iIntros "#Hwp !# [$ HP]". by iApply "Hwp". Qed.

Lemma ht_frame_r s E P Φ R e :
  {{ P }} e @ s; E {{ Φ }} ⊢ {{ P ∗ R }} e @ s; E {{ v, Φ v ∗ R }}.
Proof. iIntros "#Hwp !# [HP $]". by iApply "Hwp". Qed.

Lemma ht_frame_step_l s E1 E2 P R1 R2 e Φ :
  to_val e = None → E2 ⊆ E1 →
  (R1 ={E1,E2}=> ▷ |={E2,E1}=> R2) ∧ {{ P }} e @ s; E2 {{ Φ }}
  ⊢ {{ R1 ∗ P }} e @ s; E1 {{ λ v, R2 ∗ Φ v }}.
Proof.
  iIntros (??) "[#Hvs #Hwp] !# [HR HP]".
  iApply (wp_frame_step_l _ E1 E2); try done.
  iSplitL "HR"; [by iApply "Hvs"|by iApply "Hwp"].
Qed.

Lemma ht_frame_step_r s E1 E2 P R1 R2 e Φ :
  to_val e = None → E2 ⊆ E1 →
  (R1 ={E1,E2}=> ▷ |={E2,E1}=> R2) ∧ {{ P }} e @ s; E2 {{ Φ }}
  ⊢ {{ P ∗ R1 }} e @ s; E1 {{ λ v, Φ v ∗ R2 }}.
Proof.
  iIntros (??) "[#Hvs #Hwp] !# [HP HR]".
  iApply (wp_frame_step_r _ E1 E2); try done.
  iSplitR "HR"; [by iApply "Hwp"|by iApply "Hvs"].
Qed.

Lemma ht_frame_step_l' s E P R e Φ :
  to_val e = None →
  {{ P }} e @ s; E {{ Φ }} ⊢ {{ ▷ R ∗ P }} e @ s; E {{ v, R ∗ Φ v }}.
Proof.
  iIntros (?) "#Hwp !# [HR HP]".
  iApply wp_frame_step_l'; try done. iFrame "HR". by iApply "Hwp".
Qed.

Lemma ht_frame_step_r' s E P Φ R e :
  to_val e = None →
  {{ P }} e @ s; E {{ Φ }} ⊢ {{ P ∗ ▷ R }} e @ s; E {{ v, Φ v ∗ R }}.
Proof.
  iIntros (?) "#Hwp !# [HP HR]".
  iApply wp_frame_step_r'; try done. iFrame "HR". by iApply "Hwp".
Qed.
End hoare.