(* iris_deprecated/program_logic/hoare.v *)
From iris.proofmode Require Import proofmode
From iris.deprecated.base_logic Require Export viewshifts
From iris.program_logic Require Export weakestpre
From iris.prelude Require Import options

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

Global Instance: Params (@ht) 5 := {}.

Global Instanceht_ne s E n :
  Proper (dist n ==> eq ==> pointwise_relation _ (dist n) ==> dist n) (ht s E).
Proof. solve_proper. Qed.

Global Instanceht_proper s E :
  Proper ((≡) ==> eq ==> pointwise_relation _ (≡) ==> (≡)) (ht s E).
Proof. solve_proper. Qed.

Lemma ht_monos E P P' Φ Φ' e :
  (P ⊢ P') → (∀ v, Φ' v ⊢ Φ v) → {{ P' }} e @ s; E {{ Φ' }} ⊢ {{ P }} e @ s; E {{ Φ }}.
Proof. by intros; apply affinely_mono, persistently_mono, wand_mono, wp_mono. Qed.

Lemma ht_stuck_monos1 s2 E P Φ e :
  s1 ⊑ s2 → {{ P }} e @ s1; E {{ Φ }} ⊢ {{ P }} e @ s2; E {{ Φ }}.
Proof. by intros; apply affinely_mono, persistently_mono, wand_mono, wp_stuck_mono. Qed.

Global Instanceht_mono' s E :
  Proper (flip (⊢) ==> eq ==> pointwise_relation _ (⊢) ==> (⊢)) (ht s E).
Proof. solve_proper. Qed.

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

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

Lemma ht_vss 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 "(Hwp HP)").
  iIntros (v) "Hv". by iApply "HΦ".
Qed.

Lemma ht_atomics E1 E2 P P' Φ Φ' e `{!Atomic (stuckness_to_atomicity 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 "(Hwp HP)").
  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 "(Hwpe HP)").
  iIntros (v) "Hv". by iApply "HwpK".
Qed.

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

Lemma ht_mask_weakens 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_ls 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_rs 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_ls E1 E2 P R1 R2 e Φ :
  TCEq (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_rs E1 E2 P R1 R2 e Φ :
  TCEq (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 Φ :
  TCEq (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 :
  TCEq (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.

Lemma ht_exists(T : Type) s E (P : T → iProp Σ) Φ e :
  (∀ x, {{ P x }} e @ s; E {{ Φ }}) ⊢ {{ ∃ x, P x }} e @ s; E {{ Φ }}.
Proof. iIntros "#HT !> HP". iDestruct "HP" as (x) "HP". by iApply "HT". Qed.