From 04f1502ff52ed0e074f21190e41b2351e5c1af6d Mon Sep 17 00:00:00 2001
From: Benjamin Peters <bpeters@mpi-sws.org>
Date: Thu, 4 Jan 2024 17:10:11 +0100
Subject: [PATCH] release exercise 9

---
 _CoqProject                   |   1 +
 theories/program_logics/ipm.v | 456 ++++++++++++++++++++++++++++++++++
 2 files changed, 457 insertions(+)
 create mode 100644 theories/program_logics/ipm.v

diff --git a/_CoqProject b/_CoqProject
index 3b529fc..c069d2c 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -93,6 +93,7 @@ theories/program_logics/heap_lang/primitive_laws_nolater.v
 theories/program_logics/hoare_lib.v
 theories/program_logics/hoare.v
 theories/program_logics/hoare_sol.v
+theories/program_logics/ipm.v
 
 # By removing the # below, you can add the exercise sheets to make
 #theories/type_systems/warmup/warmup.v
diff --git a/theories/program_logics/ipm.v b/theories/program_logics/ipm.v
new file mode 100644
index 0000000..90b7b39
--- /dev/null
+++ b/theories/program_logics/ipm.v
@@ -0,0 +1,456 @@
+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.
+(* don't use the IPM *)
+  (* TODO: exercise *)
+Admitted.
+
+
+
+Lemma ent_comm_premise P Q R :
+  (Q -∗ P -∗ R) ⊢ P -∗ Q -∗ R.
+Proof.
+(* don't use the IPM *)
+  (* TODO: exercise *)
+Admitted.
+
+
+Lemma ent_sep_or_disj2 P Q R :
+  (P ∨ R) ∗ (Q ∨ R) ⊢ (P ∗ Q) ∨ R.
+Proof.
+(* don't use the IPM *)
+  (* TODO: exercise *)
+Admitted.
+
+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]".
+  - by iApply H1.
+  - 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. }
+
+  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.
+    (* TODO: exercise *)
+  Admitted.
+
+
+  Lemma ent_lem2 P Q :
+    P ∗ (P -∗ Q) ⊢ Q.
+  Proof.
+    (* TODO: exercise *)
+  Admitted.
+
+
+  Lemma ent_lem3 P Q R :
+    (P ∨ Q) ⊢ R -∗ (P ∗ R) ∨ (Q ∗ R).
+  Proof.
+    (* TODO: exercise *)
+  Admitted.
+
+End without_ipm.
+
+Lemma ent_lem1_ipm P Q :
+  True ⊢ P -∗ Q -∗ P ∗ Q.
+Proof.
+  (* TODO: exercise *)
+Admitted.
+
+
+Lemma ent_lem2_ipm P Q :
+  P ∗ (P -∗ Q) ⊢ Q.
+Proof.
+  (* TODO: exercise *)
+Admitted.
+
+
+Lemma ent_lem3_ipm P Q R :
+  (P ∨ Q) ⊢ R -∗ (P ∗ R) ∨ (Q ∗ R).
+Proof.
+  (* TODO: exercise *)
+Admitted.
+
+
+
+(** 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.
+(* don't use the IPM *)
+  (* TODO: exercise *)
+Admitted.
+
+
+(** Exercise 4 *)
+
+Lemma hoare_load l v :
+  {{ l ↦ v }} !#l {{ w, ⌜w = v⌝ ∗ l ↦ v }}.
+Proof.
+(* don't use the IPM *)
+  (* TODO: exercise *)
+Admitted.
+
+
+Lemma hoare_store l (v w : val) :
+  {{ l ↦ v }} #l <- w {{ _, l ↦ w }}.
+Proof.
+(* don't use the IPM *)
+  (* TODO: exercise *)
+Admitted.
+
+
+Lemma hoare_new (v : val) :
+  {{ True }} ref v {{ w, ∃ l : loc, ⌜w = #l⌝ ∗ l ↦ v }}.
+Proof.
+(* don't use the IPM *)
+  (* TODO: exercise *)
+Admitted.
+
+
+
+
+(** 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.
+(* don't use the IPM *)
+  (* TODO: exercise *)
+Admitted.
+
+
+Lemma cons_ll_correct (v x : val) xs :
+  {{ is_ll xs v }} cons_ll x v {{ u, is_ll (x :: xs) u }}.
+Proof.
+(* don't use the IPM *)
+  (* TODO: exercise *)
+Admitted.
+
+
+Lemma head_ll_correct (v x : val) xs :
+  {{ is_ll (x :: xs) v }} head_ll v {{ w, ⌜w = x⌝ }}.
+Proof.
+(* don't use the IPM *)
+  (* TODO: exercise *)
+Admitted.
+
+
+Lemma tail_ll_correct v x xs :
+  {{ is_ll (x :: xs) v }} tail_ll v {{ w, is_ll xs w }}.
+Proof.
+(* don't use the IPM *)
+  (* TODO: exercise *)
+Admitted.
+
+
+Lemma len_ll_correct v xs :
+  {{ is_ll xs v }} len_ll v {{ w, ⌜w = #(length xs)⌝ ∗ is_ll xs v }}.
+Proof.
+(* don't use the IPM *)
+  (* TODO: exercise *)
+Admitted.
+
+