materials for this week

_CoqProject

@@ -4,6 +4,8 @@
 # Cannot use non-canonical projections as it causes massive unification failures
 # (https://github.com/coq/coq/issues/6294).
 -arg -w -arg -redundant-canonical-projection
+# we use Restart for demoing purposes, sometimes
+-arg -w -arg -undo-batch-mode
 
 # library stuff
 theories/lib/maps.v
@@ -96,8 +98,7 @@ theories/axiomatic/heap_lang/primitive_laws_nolater.v
 # Program logic chapter
 theories/axiomatic/hoare_lib.v
 theories/axiomatic/hoare.v
-
-
+theories/axiomatic/ipm.v
 
 
 

theories/axiomatic/hoare_lib.v

 From iris.prelude Require Import options.
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import lang notation.
+From iris.base_logic Require Export invariants.
 From semantics.axiomatic.heap_lang Require Export primitive_laws_nolater.
 From semantics.axiomatic.heap_lang Require Import adequacy proofmode.
 
@@ -177,7 +178,6 @@ Module hoare.
   (** Hoare rules *)
   Implicit Types
     (Φ Ψ: val → iProp).
-
   Definition hoare P (e: expr) Φ := P ⊢ WP e {{ Φ }}.
 
   Global Notation "{{ P } } e {{ Φ } }" := (hoare P%I e%E Φ%I)
@@ -460,4 +460,233 @@ Module hoare.
 
   (* Prevent printing of magic wands *)
   Notation "P -∗ Q" := (bi_entails P Q) (only parsing) : stdpp_scope.
+
+
+  (** Weakest precondition rules *)
+  Lemma ent_wp_value Φ v :
+    Φ v ⊢ WP of_val v {{ w, Φ w }}.
+  Proof.
+    iIntros "Hv". by iApply wp_value.
+  Qed.
+
+  Lemma ent_wp_wand' Φ Ψ e :
+    (∀ v, Φ v -∗ Ψ v) -∗ WP e {{ Φ }} -∗ WP e {{ Ψ }}.
+  Proof.
+    iIntros "Hp Hwp". iApply (wp_wand with "Hwp Hp").
+  Qed.
+
+  Lemma ent_wp_wand Φ Ψ e :
+    (∀ v, Φ v -∗ Ψ v) ∗ WP e {{ Φ }} ⊢ WP e {{ Ψ }}.
+  Proof.
+    iIntros "[Hp Hwp]". iApply (wp_wand with "Hwp Hp").
+  Qed.
+
+  Lemma ent_wp_bind e K Φ :
+    WP e {{ v, WP fill K (Val v) {{ Φ }} }} ⊢ WP fill K e {{ Φ }}.
+  Proof.
+    iApply wp_bind.
+  Qed.
+
+  Lemma ent_wp_pure_step e e' Φ :
+    pure_step e e' →
+    WP e' {{ Φ }} ⊢ WP e {{ Φ }}.
+  Proof.
+    iIntros (Hpure) "Hwp". iApply (lifting.wp_pure_step_later _ _ _ _ _ True 1); last iApply "Hwp"; last done.
+    intros _. apply nsteps_once. apply Hpure.
+  Qed.
+
+  Lemma ent_wp_new v Φ :
+    (∀ l : loc, l ↦ v -∗ Φ #l) ⊢ WP ref (Val v) {{ Φ }}.
+  Proof.
+    iIntros "Hs". wp_alloc l as "Hl". wp_value_head. by iApply "Hs".
+  Qed.
+
+  Lemma ent_wp_load l v Φ :
+    l ↦ v ∗ (l ↦ v -∗ Φ v) ⊢ WP !#l {{ Φ }}.
+  Proof.
+    iIntros "(Hl & Hp)". wp_load. wp_value_head. by iApply "Hp".
+  Qed.
+
+  Lemma ent_wp_store l v w Φ :
+    l ↦ w ∗ (l ↦ v -∗ Φ #()) ⊢ WP #l <- Val v {{ Φ }}.
+  Proof.
+    iIntros "(Hl & Hp)". wp_store. wp_value_head. by iApply "Hp".
+  Qed.
+
+
+  (** Persistency *)
+  Lemma ent_pers_dup P :
+    □ P ⊢ (□ P) ∗ (□ P).
+  Proof.
+    iIntros "#HP". eauto.
+  Qed.
+
+  Lemma ent_pers_elim P :
+    □ P ⊢ P.
+  Proof.
+    iIntros "#$".
+  Qed.
+
+  Lemma ent_pers_mono P Q :
+    (P ⊢ Q) →
+    □ P ⊢ □ Q.
+  Proof.
+    iIntros (HPQ) "#HP !>". by iApply HPQ.
+  Qed.
+
+  Lemma ent_pers_pure (ϕ : Prop) :
+    ⌜ϕ⌝ ⊢ (□ ⌜ϕ⌝ : iProp).
+  Proof.
+    iIntros "#$".
+  Qed.
+
+  Lemma ent_pers_and_sep P Q :
+    (□ P) ∧ Q ⊢ (□ P) ∗ Q.
+  Proof.
+    iIntros "(#$ & $)".
+  Qed.
+
+  Lemma ent_pers_idemp P :
+    □ P ⊢ □ □ P.
+  Proof.
+    iIntros "#$".
+  Qed.
+
+  Lemma ent_pers_all {X} (Φ : X → iProp) :
+    (∀ x : X, □ Φ x) ⊢ □ ∀ x : X, Φ x.
+  Proof.
+    iIntros "#Hx" (x). iApply "Hx".
+  Qed.
+
+  Lemma ent_pers_exists {X} (Φ : X → iProp) :
+    (□ ∃ x : X, Φ x) ⊢ ∃ x : X, □ Φ x.
+  Proof.
+    iIntros "(%x & #Hx)". iExists x. done.
+  Qed.
+
+  (** Invariants *)
+  Implicit Type
+    (F : iProp)
+    (N : namespace)
+    (E : coPset)
+  .
+  Lemma ent_inv_pers F N :
+    inv N F ⊢ □ inv N F.
+  Proof.
+    iIntros "#$".
+  Qed.
+  Lemma ent_inv_alloc F P N E e Φ :
+    (P ∗ inv N F ⊢ WP e @ E {{ Φ }}) →
+    (P ∗ F ⊢ WP e @ E {{ Φ }}).
+  Proof.
+    iIntros (Ha) "[HP HF]".
+    iMod (inv_alloc N with "HF") as "#Hinv".
+    iApply Ha. iFrame "Hinv ∗".
+  Qed.
+  Lemma inv_alloc N F E e Φ :
+    F -∗
+    (inv N F -∗ WP e @ E {{ Φ }}) -∗
+    WP e @ E {{ Φ }}.
+  Proof.
+    iIntros "HF Hs".
+    iMod (inv_alloc N with "HF") as "#Hinv".
+    by iApply "Hs".
+  Qed.
+
+  (** We require a sidecondition here, namely that [F] is "timeless". All propositions we have seen up to now are in fact timeless.
+    We will see propositions that do not satisfy this requirement and which need a stronger rule for invariants soon.
+  *)
+  Lemma ent_inv_open `{!Timeless F} P N E e Φ :
+    (P ∗ F ⊢ WP e @ (E ∖ ↑N) {{ v, F ∗ Φ v }}) →
+    ↑N ⊆ E →
+    (P ∗ inv N F ⊢ WP e @ E {{ Φ }}).
+  Proof.
+    iIntros (Ha Hincl) "(HP & #Hinv)".
+    iMod (inv_acc_timeless with "Hinv") as "(HF & Hcl)"; first done.
+    iApply wp_fupd'. iApply wp_wand_r.
+    iSplitR "Hcl". { iApply Ha. iFrame. }
+    iIntros (v) "[HF Hphi]". iMod ("Hcl" with "HF"). done.
+  Qed.
+  Lemma inv_open `{!Timeless F} N E e Φ :
+    ↑N ⊆ E →
+    inv N F -∗
+    (F -∗ WP e @ (E ∖ ↑N) {{ v, F ∗ Φ v }})%I -∗
+    WP e @ E {{ Φ }}.
+  Proof.
+    iIntros (Hincl) "#Hinv Hs".
+    iMod (inv_acc_timeless with "Hinv") as "(HF & Hcl)"; first done.
+    iApply wp_fupd'. iApply wp_wand_r.
+    iSplitR "Hcl". { iApply "Hs". iFrame. }
+    iIntros (v) "[HF Hphi]". iMod ("Hcl" with "HF"). done.
+  Qed.
+
+
+  (** Later *)
+  Lemma ent_later_intro P :
+    P ⊢ ▷ P.
+  Proof.
+    iIntros "$".
+  Qed.
+
+  Lemma ent_later_mono P Q :
+    (P ⊢ Q) →
+    (▷ P ⊢ ▷ Q).
+  Proof.
+    iIntros (Hs) "HP!>". by iApply Hs.
+  Qed.
+
+  Lemma ent_löb P :
+    (▷ P ⊢ P) →
+    True ⊢ P.
+  Proof.
+    iIntros (Hs) "_".
+    iLöb as "IH". by iApply Hs.
+  Qed.
+
+  Lemma ent_later_sep P Q :
+    ▷ (P ∗ Q) ⊣⊢ (▷ P) ∗ (▷ Q).
+  Proof.
+    iSplit; iIntros "[$ $]".
+  Qed.
+
+  Lemma ent_later_exists `{Inhabited X} (Φ : X → iProp) :
+    (▷ (∃ x : X, Φ x)) ⊣⊢ ∃ x : X, ▷ Φ x.
+  Proof. apply bi.later_exist. Qed.
+
+  Lemma ent_later_all {X} (Φ : X → iProp) :
+    ▷ (∀ x : X, Φ x) ⊣⊢ ∀ x : X, ▷ Φ x.
+  Proof. apply bi.later_forall. Qed.
+
+  Lemma ent_later_pers P :
+    ▷ □ P ⊣⊢ □ ▷ P.
+  Proof.
+    iSplit; iIntros "#H !> !>"; done.
+  Qed.
+
+  Lemma ent_later_wp_pure_step e e' Φ :
+    pure_step e e' →
+    ▷ WP e' {{ Φ }} ⊢ WP e {{ Φ }}.
+  Proof.
+    iIntros (Hpure%PureExec_1_equiv) "Hwp".
+    destruct Hpure as (ϕ & Hphi & Hpure).
+    iApply (lifting.wp_pure_step_later _ _ _ _ _ _ 1); done.
+  Qed.
+
+  Lemma ent_later_wp_new v Φ :
+    ▷ (∀ l : loc, l ↦ v -∗ Φ #l) ⊢ WP ref v {{ Φ }}.
+  Proof.
+    iIntros "Hp". wp_alloc l as "Hl". iApply wp_value. by iApply "Hp".
+  Qed.
+
+  Lemma ent_later_wp_load l v Φ :
+    ▷ l ↦ v ∗ ▷ (l ↦ v -∗ Φ v) ⊢ WP ! #l {{ Φ }}.
+  Proof.
+    iIntros "[Hl Hp]". wp_load. iApply wp_value. by iApply "Hp".
+  Qed.
+
+  Lemma ent_later_wp_store l v w Φ :
+    ▷ l ↦ v ∗ ▷ (l ↦ w -∗ Φ #()) ⊢ WP #l <- w {{ Φ }}.
+  Proof.
+    iIntros "[Hl Hp]". wp_store. iApply wp_value. by iApply "Hp".
+  Qed.
 End hoare.

theories/axiomatic/ipm.v

+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.axiomatic.heap_lang Require Import adequacy proofmode primitive_laws_nolater.
+From semantics.axiomatic Require Import hoare_lib.
+From semantics.axiomatic.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.
+
+Lemma ent_carry_res P Q :
+  P ⊢ Q -∗ P ∗ Q.
+Proof.
+  (* FIXME: exercise, don't use the IPM *)
+Admitted.
+
+Lemma ent_comm_premise P Q R :
+  (Q -∗ P -∗ R) ⊢ P -∗ Q -∗ R.
+Proof.
+  (* FIXME: exercise, don't use the IPM *)
+Admitted.
+
+Lemma ent_sep_or_disj2 P Q R :
+  (P ∨ R) ∗ (Q ∨ R) ⊢ (P ∗ Q) ∨ R.
+Proof.
+  (* FIXME: exercise, don't use the IPM *)
+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) "[HP | HQ]".
+  - 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. *)
+
+  Lemma ent_lem1 P Q :
+    True ⊢ P -∗ Q -∗ P ∗ Q.
+  Proof.
+    (* FIXME: exercise *)
+  Admitted.
+
+  Lemma ent_lem2 P Q :
+    P ∗ (P -∗ Q) ⊢ Q.
+  Proof.
+    (* FIXME: exercise *)
+  Admitted.
+
+  Lemma ent_lem3 P Q R :
+    (P ∨ Q) ⊢ R -∗ (P ∗ R) ∨ (Q ∗ R).
+  Proof.
+    (* FIXME: exercise *)
+  Admitted.
+End without_ipm.
+
+Lemma ent_lem1_ipm P Q :
+  True ⊢ P -∗ Q -∗ P ∗ Q.
+Proof.
+  (* FIXME: exercise *)
+Admitted.
+
+Lemma ent_lem2_ipm P Q :
+  P ∗ (P -∗ Q) ⊢ Q.
+Proof.
+  (* FIXME: exercise *)
+Admitted.
+
+
+Lemma ent_lem3_ipm P Q R :
+  (P ∨ Q) ⊢ R -∗ (P ∗ R) ∨ (Q ∗ R).
+Proof.
+  (* FIXME: 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.
+(** 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.
+  (* FIXME: exercise, don't use the IPM *)
+Admitted.
+
+Lemma hoare_load l v :
+  {{ l ↦ v }} !#l {{ w, ⌜w = v⌝ ∗ l ↦ v }}.
+Proof.