From 8d480a49c72b3f0a296bfe4e7cb312e9ed9171b1 Mon Sep 17 00:00:00 2001
From: Adrien Burgun <adrien.burgun@orange.fr>
Date: Wed, 10 Jan 2024 15:31:45 +0100
Subject: [PATCH] :tada: Finish exercises 9 (with IPM cheating)

---
 theories/program_logics/ipm.v | 302 +++++++++++++++++++++++++++-------
 1 file changed, 240 insertions(+), 62 deletions(-)

diff --git a/theories/program_logics/ipm.v b/theories/program_logics/ipm.v
index 90b7b39..310c1ee 100644
--- a/theories/program_logics/ipm.v
+++ b/theories/program_logics/ipm.v
@@ -25,28 +25,63 @@ Qed.
 (** Exercise 1 *)
 
 Lemma ent_carry_res P Q :
-  P ⊢ Q -∗ P ∗ Q.
+  P ⊢ Q -∗ (P ∗ Q).
 Proof.
-(* don't use the IPM *)
-  (* TODO: exercise *)
-Admitted.
-
-
+  apply ent_wand_intro.
+  reflexivity.
+Qed.
 
 Lemma ent_comm_premise P Q R :
   (Q -∗ P -∗ R) ⊢ P -∗ Q -∗ R.
 Proof.
-(* don't use the IPM *)
-  (* TODO: exercise *)
-Admitted.
+  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.
-(* don't use the IPM *)
-  (* TODO: exercise *)
-Admitted.
+  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.
 
@@ -62,7 +97,8 @@ Lemma or_elim P Q R:
   (P ∨ Q) ⊢ R.
 Proof.
   iIntros (H1 H2) "[P|Q]".
-  - by iApply H1.
+  - iApply H1.
+    iExact "P".
   - by iApply H2.
 Qed.
 
@@ -135,7 +171,7 @@ Lemma destruct_ex {X} (p : X → Prop) (Φ : X → iProp) : (∃ x : X, ⌜p x
 Proof.
   (* we can lead the identifier with a [%] to introduce to the Coq context *)
   iIntros "[%w Hw]".
-  iDestruct "Hw" as  "[%Hw1 Hw2]".
+  iDestruct "Hw" as "[%Hw1 Hw2]".
 
   (* more compactly: *)
   Restart.
@@ -163,6 +199,7 @@ Proof.
   iIntros "HP HR Hw".
   iSpecialize ("Hw" with "[HR HP]").
   { iFrame. }
+  iAssumption.
 
   Restart.
   iIntros "HP HR Hw".
@@ -253,44 +290,55 @@ Section without_ipm.
   Lemma ent_lem1 P Q :
     True ⊢ P -∗ Q -∗ P ∗ Q.
   Proof.
-    (* TODO: exercise *)
-  Admitted.
+    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.
-    (* TODO: exercise *)
-  Admitted.
+    rewrite ent_sep_comm.
+    apply ent_wand_elim.
+    reflexivity.
+  Qed.
 
 
   Lemma ent_lem3 P Q R :
     (P ∨ Q) ⊢ R -∗ (P ∗ R) ∨ (Q ∗ R).
   Proof.
-    (* TODO: exercise *)
-  Admitted.
-
+    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.
-  (* TODO: exercise *)
-Admitted.
-
+  iIntros "_ HP HQ".
+  iSplitL "HP".
+  all: iAssumption.
+Qed.
 
 Lemma ent_lem2_ipm P Q :
   P ∗ (P -∗ Q) ⊢ Q.
 Proof.
-  (* TODO: exercise *)
-Admitted.
-
+  iIntros "[HP HPQ]".
+  iSpecialize ("HPQ" with "HP").
+  iAssumption.
+Qed.
 
 Lemma ent_lem3_ipm P Q R :
   (P ∨ Q) ⊢ R -∗ (P ∗ R) ∨ (Q ∗ R).
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  iIntros "[HP | HQ] HR".
+  - iLeft.
+    iFrame.
+  - iRight.
+    iFrame.
+Qed.
 
 
 
@@ -322,38 +370,59 @@ Lemma hoare_frame' P R Φ e :
   {{ P }} e {{ Φ }} →
   {{ P ∗ R }} e {{ v, Φ v ∗ R }}.
 Proof.
-(* don't use the IPM *)
-  (* TODO: exercise *)
-Admitted.
-
+  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.
-(* don't use the IPM *)
-  (* TODO: exercise *)
-Admitted.
+  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.
-(* don't use the IPM *)
-  (* TODO: exercise *)
-Admitted.
+  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.
-(* don't use the IPM *)
-  (* TODO: exercise *)
-Admitted.
-
-
-
+  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 *)
 
@@ -417,40 +486,149 @@ Qed.
 Lemma new_ll_correct :
   {{ True }} new_ll #() {{ v, is_ll [] v }}.
 Proof.
-(* don't use the IPM *)
-  (* TODO: exercise *)
-Admitted.
+  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.
-(* don't use the IPM *)
-  (* TODO: exercise *)
-Admitted.
+  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.
-(* don't use the IPM *)
-  (* TODO: exercise *)
-Admitted.
-
+  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.
-(* don't use the IPM *)
-  (* TODO: exercise *)
-Admitted.
-
+  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.
-(* don't use the IPM *)
-  (* TODO: exercise *)
-Admitted.
 
+  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.