From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import lang primitive_laws notation.
From iris.base_logic Require Import invariants.
From semantics.pl.heap_lang Require Import adequacy proofmode primitive_laws_nolater.
From semantics.pl Require Import hoare_lib.
From semantics.pl.program_logic Require Import notation.

(** ** Magic is in the air *)
Import hoare.
Check ent_wand_intro.
Check ent_wand_elim.

Section primitive.
Implicit Types (P Q R: iProp).

Lemma ent_or_sep_dist P Q R :
  (P ∨ Q) ∗ R ⊢ (P ∗ R) ∨ (Q ∗ R).
Proof.
  apply ent_wand_elim.
  apply ent_or_elim.
  - apply ent_wand_intro. apply ent_or_introl.
  - apply ent_wand_intro. apply ent_or_intror.
Qed.

(** Exercise 1 *)

Lemma ent_carry_res P Q :
  P ⊢ Q -∗ (P ∗ Q).
Proof.
  apply ent_wand_intro.
  reflexivity.
Qed.

Lemma ent_comm_premise P Q R :
  (Q -∗ P -∗ R) ⊢ P -∗ Q -∗ R.
Proof.
  apply ent_wand_intro.
  apply ent_wand_intro.
  rewrite <-ent_sep_assoc.
  rewrite (ent_sep_comm P Q).
  rewrite ent_sep_assoc.
  apply ent_wand_elim.
  apply ent_wand_elim.
  reflexivity.
Qed.

Lemma ent_or_comm P Q :
  P ∨ Q ⊣⊢ Q ∨ P.
Proof.
  apply bi.equiv_entails; constructor.
  - apply ent_or_elim.
    + apply ent_or_intror.
    + apply ent_or_introl.
  - apply ent_or_elim.
    + apply ent_or_intror.
    + apply ent_or_introl.
Qed.

Lemma ent_or_cancel_left P Q Q' :
  (Q ⊢ Q') → P ∨ Q ⊢ P ∨ Q'.
Proof.
  intro H.
  apply ent_or_elim.
  - apply ent_or_introl.
  - etrans; [ apply H | apply ent_or_intror ].
Qed.

Lemma ent_sep_or_disj2 P Q R :
  (P ∨ R) ∗ (Q ∨ R) ⊢ (P ∗ Q) ∨ R.
Proof.
  apply ent_wand_elim.
  apply ent_or_elim.
  - apply ent_wand_intro.
    rewrite ent_sep_comm.
    etrans; [ apply ent_or_sep_dist | ].
    rewrite ent_sep_comm.
    apply ent_or_cancel_left.
    apply ent_sep_weaken.
  - apply ent_wand_intro.
    rewrite ent_sep_comm.
    etrans; [ apply ent_or_sep_dist | ].
    rewrite ent_sep_comm.
    etrans; first apply ent_or_elim; [ apply ent_sep_weaken | apply ent_sep_weaken | apply ent_or_intror ].
Qed.

End primitive.

(** ** Using the IPM *)
Implicit Types
  (P Q R: iProp)
  (Φ Ψ : val → iProp)
.

Lemma or_elim P Q R:
  (P ⊢ R) →
  (Q ⊢ R) →
  (P ∨ Q) ⊢ R.
Proof.
  iIntros (H1 H2) "[P|Q]".
  - iApply H1.
    iExact "P".
  - by iApply H2.
Qed.

Lemma or_intro_l P Q:
  P ⊢ P ∨ Q.
Proof.
  iIntros "P". iLeft. iFrame "P".

  (* [iExact] corresponds to Coq's [exact] *)
  Restart.
  iIntros "P". iLeft. iExact "P".

  (* [iAssumption] can solve the goal if there is an exact match in the context *)
  Restart.
  iIntros "P". iLeft. iAssumption.

  (* This directly frames the introduced proposition. The IPM will automatically try to pick a disjunct. *)
  Restart.
  iIntros "$".
Qed.

Lemma or_sep P Q R: (P ∨ Q) ∗ R ⊢ (P ∗ R) ∨ (Q ∗ R).
Proof.
  (* we first introduce, destructing the separating conjunction *)
  iIntros "[HPQ HR]".
  iDestruct "HPQ" as "[HP | HQ]".
  - iLeft. iFrame.
  - iRight. iFrame.

  (* we can also split more explicitly *)
  Restart.
  iIntros "[HPQ HR]".
  iDestruct "HPQ" as "[HP | HQ]".
  - iLeft.
    (* [iSplitL] uses the given hypotheses to prove the left conjunct and the rest for the right conjunct *)
    (* symmetrically, [iSplitR] gives the specified hypotheses to the right *)
    iSplitL "HP". all: iAssumption.
  - iRight.
    (* if we don't give any hypotheses, everything will go to the left. *)
    iSplitL. (* now we're stuck... *)

  (* alternative: directly destruct the disjunction *)
  Restart.
  (* iFrame will also directly pick the disjunct *)
  iIntros "[[HP | HQ] HR]"; iFrame.
Abort.

(* Using entailments *)
Lemma or_sep P Q R: (P ∨ Q) ∗ R ⊢ (P ∗ R) ∨ (Q ∗ R).
Proof.
  iIntros "[HPQ HR]". iDestruct "HPQ" as "[HP | HQ]".
  - (* this will make the entailment ⊢ into a wand *)
    iPoseProof (ent_or_introl (P ∗ R) (Q ∗ R)) as "-#Hor".
    iApply "Hor". iFrame.
  - (* we can also directly apply the entailment *)
    iApply ent_or_intror.
    iFrame.
Abort.

(* Proving pure Coq propositions *)
Lemma prove_pure P : P ⊢ ⌜42 > 0⌝.
Proof.
  iIntros "HP".
  (* [iPureIntro] will switch to a Coq goal, of course losing access to the Iris context *)
  iPureIntro. lia.
Abort.

(* Destructing assumptions *)
Lemma destruct_ex {X} (p : X → Prop) (Φ : X → iProp) : (∃ x : X, ⌜p x⌝ ∗ Φ x) ⊢ False.
Proof.
  (* we can lead the identifier with a [%] to introduce to the Coq context *)
  iIntros "[%w Hw]".
  iDestruct "Hw" as "[%Hw1 Hw2]".

  (* more compactly: *)
  Restart.
  iIntros "(%w & %Hw1 & Hw2)".

  Restart.
  (* we cannot introduce an existential to the Iris context *)
  Fail iIntros "(w & Hw)".

  Restart.
  iIntros "(%w & Hw1 & Hw2)".
  (* if we first introduce a pure proposition into the Iris context,
    we can later move it to the Coq context *)
  iDestruct "Hw1" as "%Hw1".
Abort.

(* Specializing assumptions *)
Lemma specialize_assum P Q R :
  ⊢
  P -∗
  R -∗
  (P ∗ R -∗ (P ∗ R) ∨ (Q ∗ R)) -∗
  (P ∗ R) ∨ (Q ∗ R).
Proof.
  iIntros "HP HR Hw".
  iSpecialize ("Hw" with "[HR HP]").
  { iFrame. }
  iAssumption.

  Restart.
  iIntros "HP HR Hw".
  (* we can also directly frame it *)
  iSpecialize ("Hw" with "[$HR $HP]").

  Restart.
  iIntros "HP HR Hw".
  (* we can let it frame all hypotheses *)
  iSpecialize ("Hw" with "[$]").

  Restart.
  (* we can also use [iPoseProof], and introduce the generated hypothesis with [as] *)
  iIntros "HP HR Hw".
  iPoseProof ("Hw" with "[$HR $HP]") as "$".

  Restart.
  iIntros "HP HR Hw".
  (* [iApply] can similarly be specialized *)
  iApply ("Hw" with "[$HP $HR]").

Abort.

(* Nested specialization *)
Lemma specialize_nested P Q R :
  ⊢
  P -∗
  (P -∗ R) -∗
  (R -∗ Q) -∗
  Q.
Proof.
  iIntros "HP HPR HRQ".
  (* we can use the pattern with round parentheses to specialize a hypothesis in a nested way *)
  iSpecialize ("HRQ" with "(HPR HP)").
  (* can finish the proof with [iExact] *)
  iExact "HRQ".

  (* of course, this also works for [iApply] *)
  Restart.
  iIntros "HP HPR HRQ". iApply ("HRQ" with "(HPR HP)").
Abort.

(* Existentials *)
Lemma prove_existential (Φ : nat → iProp) :
  ⊢ Φ 1337 -∗ ∃ n m, ⌜n > 41⌝ ∗ Φ m.
Proof.
  (* [iExists] can instantiate existentials *)
  iIntros "Ha".
  iExists 42.
  iExists 1337. iSplitR. { iPureIntro. lia. } iFrame.

  Restart.
  iIntros "Ha". iExists 42, 1337.
  (* [iSplit] works if the goal is a conjunction or one of the separating conjuncts is pure.
     In that case, the hypotheses will be available for both sides.  *)
  iSplit.

  Restart.
  iIntros "Ha". iExists 42, 1337. iSplitR; iFrame; iPureIntro. lia.
Abort.

(* specializing universals *)
Lemma specialize_universal (Φ : nat → iProp) :
  ⊢ (∀ n, ⌜n = 42⌝ -∗ Φ n) -∗ Φ 42.
Proof.
  iIntros "Hn".
  (* we can use [$!] to specialize Iris hypotheses with pure Coq terms *)
  iSpecialize ("Hn" $! 42).
  iApply "Hn". done.

  Restart.
  iIntros "Hn".
  (* we can combine this with [with] patterns. The [%] pattern will generate a pure Coq goal. *)
  iApply ("Hn" $! 42 with "[%]").
  done.

  Restart.
  iIntros "Hn".
  (* ...and ending the pattern with // will call done *)
  iApply ("Hn" $! 42 with "[//]").
Abort.

Section without_ipm.
  (** Prove the following entailments without using the IPM. *)

  (** Exercise 2 *)

  Lemma ent_lem1 P Q :
    True ⊢ P -∗ Q -∗ P ∗ Q.
  Proof.
    repeat apply ent_wand_intro.
    rewrite <-ent_sep_assoc.
    rewrite ent_sep_comm.
    apply ent_sep_weaken.
  Qed.


  Lemma ent_lem2 P Q :
    P ∗ (P -∗ Q) ⊢ Q.
  Proof.
    rewrite ent_sep_comm.
    apply ent_wand_elim.
    reflexivity.
  Qed.


  Lemma ent_lem3 P Q R :
    (P ∨ Q) ⊢ R -∗ (P ∗ R) ∨ (Q ∗ R).
  Proof.
    apply ent_wand_intro.
    apply ent_or_sep_dist.
  Qed.
End without_ipm.

Lemma ent_lem1_ipm P Q :
  True ⊢ P -∗ Q -∗ P ∗ Q.
Proof.
  iIntros "_ HP HQ".
  iSplitL "HP".
  all: iAssumption.
Qed.

Lemma ent_lem2_ipm P Q :
  P ∗ (P -∗ Q) ⊢ Q.
Proof.
  iIntros "[HP HPQ]".
  iSpecialize ("HPQ" with "HP").
  iAssumption.
Qed.

Lemma ent_lem3_ipm P Q R :
  (P ∨ Q) ⊢ R -∗ (P ∗ R) ∨ (Q ∗ R).
Proof.
  iIntros "[HP | HQ] HR".
  - iLeft.
    iFrame.
  - iRight.
    iFrame.
Qed.



(** Weakest precondition rules *)

Check ent_wp_value.
Check ent_wp_wand.
Check ent_wp_bind.
Check ent_wp_pure_step.
Check ent_wp_new.
Check ent_wp_load.
Check ent_wp_store.

Lemma ent_wp_pure_steps e e' Φ :
  rtc pure_step e e' →
  WP e' {{ Φ }} ⊢ WP e {{ Φ }}.
Proof.
  iIntros (Hpure) "Hwp".
  iInduction Hpure as [|] "IH"; first done.
  iApply ent_wp_pure_step; first done. by iApply "IH".
Qed.

Print hoare.

(** Exercise 3 *)

(** We can re-derive the Hoare rules from the weakest pre rules. *)
Lemma hoare_frame' P R Φ e :
  {{ P }} e {{ Φ }} →
  {{ P ∗ R }} e {{ v, Φ v ∗ R }}.
Proof.
  intro HP.
  unfold hoare in *.
  etrans; first apply ent_sep_split; [ exact HP | reflexivity | ].
  etrans; last apply ent_wp_wand.
  simpl.
  rewrite ent_sep_comm.
  apply ent_sep_split; [ apply ent_all_intro; intro v | reflexivity ].
  apply ent_wand_intro.
  rewrite ent_sep_comm.
  reflexivity.
Qed.

(** Exercise 4 *)

Lemma hoare_load l v :
  {{ l ↦ v }} !#l {{ w, ⌜w = v⌝ ∗ l ↦ v }}.
Proof.
  unfold hoare.
  etrans; last apply ent_wp_load; simpl.
  etrans; [ apply ent_sep_true | rewrite ent_sep_comm; apply ent_sep_split ].
  1: reflexivity.
  apply ent_wand_intro; rewrite ent_sep_comm.
  etrans; [ apply ent_sep_weaken | etrans; first apply ent_sep_true ].
  apply ent_sep_split; [ | reflexivity ].
  apply ent_prove_pure.
  reflexivity.
Qed.


Lemma hoare_store l (v w : val) :
  {{ l ↦ v }} #l <- w {{ _, l ↦ w }}.
Proof.
  unfold hoare.
  etrans; last apply ent_wp_store; simpl.
  etrans; first apply ent_sep_true.
  rewrite ent_sep_comm; apply ent_sep_split; first reflexivity.
  apply ent_wand_intro.
  rewrite ent_sep_comm; apply ent_sep_weaken.
Qed.


Lemma hoare_new (v : val) :
  {{ True }} ref v {{ w, ∃ l : loc, ⌜w = #l⌝ ∗ l ↦ v }}.
Proof.
  unfold hoare.
  etrans; last apply ent_wp_new; simpl.
  apply ent_all_intro; intro l.
  apply ent_wand_intro.
  etrans; first apply ent_sep_split; [ apply ent_prove_pure | reflexivity | ].
  exact (eq_refl #l).
  eapply ent_exist_intro.
  reflexivity.
Qed.

(** Exercise 5 *)

(** Linked lists using the IPM *)
Fixpoint is_ll (xs : list val) (v : val) : iProp :=
  match xs with
  | [] => ⌜v = NONEV⌝
  | x :: xs =>
    ∃ (l : loc) (w : val),
      ⌜v = SOMEV #l⌝ ∗ l ↦ (x, w) ∗ is_ll xs w
  end.

Definition new_ll : val :=
  λ: <>, NONEV.

Definition cons_ll : val :=
  λ: "h" "l", SOME (ref ("h", "l")).

Definition head_ll : val :=
  λ: "x", match: "x" with NONE => #() | SOME "r" => Fst (!"r") end.
Definition tail_ll : val :=
  λ: "x", match: "x" with NONE => #() | SOME "r" => Snd (!"r") end.

Definition len_ll : val :=
  rec: "len" "x" := match: "x" with NONE => #0 | SOME "r" => #1 + "len" (Snd !"r") end.

Definition app_ll : val :=
  rec: "app" "x" "y" :=
    match: "x" with NONE => "y" | SOME "r" =>
        let: "rs" := !"r" in
        "r" <- (Fst "rs", "app" (Snd "rs") "y");;
        SOME "r"
    end.

Lemma app_ll_correct xs ys v w :
  {{ is_ll xs v ∗ is_ll ys w }} app_ll v w {{ u, is_ll (xs ++ ys) u }}.
Proof.
  iIntros "[Hv Hw]".
  iRevert (v) "Hv Hw".
  (* We use the [iInduction] tactic which lifts Coq's induction into Iris.
    ["IH"] is the name the inductive hypothesis should get in the Iris context.
    Note that the inductive hypothesis is printed above another line [-----□].
    This is another kind of context which you will learn about soon; for now, just
    treat it the same as any other elements of the Iris context.
  *)
  iInduction xs as [ | x xs] "IH"; simpl; iIntros (v) "Hv Hw".
  Restart.
  (* simpler: use the [forall] clause of [iInduction] to let it quantify over [v] *)
  iIntros "[Hv Hw]".
  iInduction xs as [ | x xs] "IH" forall (v); simpl.
  - iDestruct "Hv" as "->". unfold app_ll. wp_pures. iApply wp_value. done.
  - iDestruct "Hv" as "(%l & %w' & -> & Hl & Hv)".
    (* Note: [wp_pures] does not unfold the definition *)
    wp_pures.
    unfold app_ll. wp_pures. fold app_ll. wp_load. wp_pures.
    wp_bind (app_ll _ _). iApply (ent_wp_wand' with "[Hl] [Hv Hw]"); first last.
    { iApply ("IH" with "Hv Hw"). }
    simpl. iIntros (v) "Hv". wp_store. wp_pures. iApply wp_value. eauto with iFrame.
Qed.

Lemma new_ll_correct :
  {{ True }} new_ll #() {{ v, is_ll [] v }}.
Proof.
  unfold new_ll.
  unfold is_ll.
  iIntros "_".
  wp_pures.
  iApply (ent_wp_value).
  iPureIntro.
  reflexivity.
Qed.


Lemma cons_ll_correct (v x : val) xs :
  {{ is_ll xs v }} cons_ll x v {{ u, is_ll (x :: xs) u }}.
Proof.
  unfold hoare, cons_ll, is_ll.
  fold is_ll.
  etrans; last eapply ent_wp_pure_steps.
  2: {
    eapply rtc_l.
    {
      apply (pure_step_fill [AppLCtx _]).
      apply pure_step_beta.
    }
    simpl.
    etrans.
    {
      apply (rtc_pure_step_fill [AppLCtx _]).
      apply pure_step_val; eauto.
    }
    simpl.
    eapply rtc_l; last reflexivity.
    apply pure_step_beta.
  }
  simpl.
  etrans; last eapply (hoare_bind [InjRCtx]); [
    apply ent_sep_true
    | apply hoare_frame
    | intro w
  ].
  eapply hoare_pure_steps.
  {
    apply (rtc_pure_step_fill [AllocNRCtx _]).
    apply pure_step_val.
    eauto.
  }
  simpl.

  1: apply hoare_new.
  simpl.
  unfold hoare.
  etrans; first apply ent_exists_sep.
  apply ent_exist_elim; intro l.

  etrans; last eapply hoare_pure_steps; [ | apply pure_step_val; eauto | apply ent_wp_value ].

  apply (ent_exist_intro l).
  apply (ent_exist_intro v).

  (* My patience is up. *)
  iIntros "[[%w_eq HL] HV]".
  rewrite w_eq.
  iSplitR.
  { iPureIntro; reflexivity. }
  iFrame.
Qed.


Lemma head_ll_correct (v x : val) xs :
  {{ is_ll (x :: xs) v }} head_ll v {{ w, ⌜w = x⌝ }}.
Proof.
  unfold head_ll, is_ll; fold is_ll.
  iIntros "(%l & %w & %eq & HL & HW)".
  subst.
  wp_pures.
  iApply (ent_wp_bind _ [FstCtx]).
  iApply ent_wp_load.
  iFrame.
  simpl.
  iIntros "_".
  wp_pures.
  iApply wp_value.
  iPureIntro; reflexivity.
Qed.

Lemma tail_ll_correct v x xs :
  {{ is_ll (x :: xs) v }} tail_ll v {{ w, is_ll xs w }}.
Proof.
  unfold tail_ll, is_ll; fold is_ll.
  iIntros "(%l & %w & %eq & HL & HW)".
  subst.
  wp_pures.
  iApply (ent_wp_bind _ [SndCtx]).
  iApply ent_wp_load.
  iFrame.
  simpl.
  iIntros "_".
  wp_pures.
  iApply wp_value.
  iAssumption.
Qed.

Lemma len_ll_correct v xs :
  {{ is_ll xs v }} len_ll v {{ w, ⌜w = #(length xs)⌝ ∗ is_ll xs v }}.
Proof.

  iInduction xs as [ | w xs ] "IH" forall (v); simpl.
  - iIntros "%eq".
    subst.
    unfold len_ll.
    wp_pures.
    iApply wp_value.
    iSplit; iPureIntro; reflexivity.
  - iIntros "(%l & %x & %eq & HL & HX)".
    subst.
    unfold len_ll.
    wp_pures.
    iApply (ent_wp_bind _ [BinOpRCtx _ #1]).
    simpl.

    iApply (ent_wp_bind _ [SndCtx; AppRCtx _]).
    iApply ent_wp_load.
    iSplitL "HL"; [ iExact "HL" | iIntros "HL"; simpl ].
    iApply (ent_wp_bind _ [AppRCtx _]).
    wp_pures.
    iApply (ent_wp_value).
    simpl.

    iSpecialize ("IH" $! x).
    iSpecialize ("IH" with "HX").
    iApply (ent_wp_wand' with "[HL]"); last iExact "IH".
    iIntros "%v [%eq HX]".
    subst.
    wp_pures.
    iApply (ent_wp_value).
    iSplitR.
    {
      iPureIntro.
      have h : (1 + length xs = S (length xs))%Z.
      lia.
      rewrite h.
      reflexivity.
    }
    iExists l, x.
    iSplitR.
    { iPureIntro; reflexivity. }
    iFrame.
Qed.