From c0a9dcdb1c4fd3bfabb727b5a186c2f76957b4ef Mon Sep 17 00:00:00 2001
From: Adrien Burgun <adrien.burgun@orange.fr>
Date: Wed, 3 Jan 2024 15:12:46 +0100
Subject: [PATCH] :sparkles: Start exercises 8

---
 theories/program_logics/hoare.v | 355 +++++++++++++++++++++++++-------
 1 file changed, 286 insertions(+), 69 deletions(-)

diff --git a/theories/program_logics/hoare.v b/theories/program_logics/hoare.v
index b355491..2268b23 100644
--- a/theories/program_logics/hoare.v
+++ b/theories/program_logics/hoare.v
@@ -17,8 +17,8 @@ Implicit Types
 Check ent_equiv.
 Check ent_refl.
 Check ent_trans.
-(* NOTE: True = ⌜True⌝ *) 
-(* NOTE: False = ⌜False⌝ *) 
+(* NOTE: True = ⌜True⌝ *)
+(* NOTE: False = ⌜False⌝ *)
 Check ent_prove_pure.
 Check ent_assume_pure.
 Check ent_and_elim_r.
@@ -37,54 +37,84 @@ Lemma ent_weakening P Q R :
   (P ⊢ R) →
   P ∧ Q ⊢ R.
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  intro P_ent_R.
+  eapply ent_trans; [ eapply ent_and_elim_l | assumption ].
+Qed.
 
 
 Lemma ent_true P :
   P ⊢ True.
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  eapply ent_trans.
+  - apply (ent_prove_pure P True).
+    tauto.
+  - exact (ent_refl True).
+Qed.
 
 
 Lemma ent_false P :
   False ⊢ P.
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  apply (ent_assume_pure _ _ _ (ent_refl False)).
+  tauto.
+Qed.
 
 
 Lemma ent_and_comm P Q :
   P ∧ Q ⊢ Q ∧ P.
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  apply ent_and_intro; [ apply ent_and_elim_r | apply ent_and_elim_l ].
+Qed.
 
 
+Definition ent_or_intro_l := ent_or_introl.
+Definition ent_or_intro_r := ent_or_intror.
+
 Lemma ent_or_comm P Q :
   P ∨ Q ⊢ Q ∨ P.
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  apply ent_or_elim; [ apply ent_or_intro_r | apply ent_or_intro_l ].
+Qed.
 
 
 Lemma ent_all_comm {X} (Φ : X → X → iProp) :
   (∀ x y, Φ x y) ⊢ (∀ y x, Φ x y).
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  apply ent_all_intro.
+  intro x.
+  apply ent_all_intro.
+  intro y.
+  eapply ent_trans.
+  - eapply ent_all_elim.
+  - eapply ent_all_elim.
+Qed.
 
 
 Lemma ent_exist_comm {X} (Φ : X → X → iProp) :
   (∃ x y, Φ x y) ⊢ (∃ y x, Φ x y).
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  apply ent_exist_elim.
+  intro x.
+  apply ent_exist_elim.
+  intro y.
+  eapply ent_exist_intro.
+  eapply ent_exist_intro.
+  exact (ent_refl _).
+Qed.
 
 
+Lemma ent_pure_pure {φ ψ : Prop} :
+  (φ → ψ) →
+  bi_entails (PROP := iProp) ⌜φ⌝ ⌜ψ⌝.
+Proof.
+  intro H.
+  apply (ent_assume_pure _ _ _ (ent_refl ⌜φ⌝)); intro Hφ.
+  eapply ent_prove_pure.
+  exact (H Hφ).
+Qed.
+
 (** Derived Hoare rules *)
-Lemma hoare_con_pre P Q Φ e:
+Lemma hoare_con_pre {P Q Φ e}:
   (P ⊢ Q) →
   {{ Q }} e {{ Φ }} →
   {{ P }} e {{ Φ }}.
@@ -92,7 +122,7 @@ Proof.
   intros ??. eapply hoare_con; eauto.
 Qed.
 
-Lemma hoare_con_post P Φ Ψ e:
+Lemma hoare_con_post {P Φ Ψ e}:
   (∀ v, Ψ v ⊢ Φ v) →
   {{ P }} e {{ Ψ }} →
   {{ P }} e {{ Φ }}.
@@ -100,7 +130,7 @@ Proof.
   intros ??. eapply hoare_con; last done; eauto.
 Qed.
 
-Lemma hoare_value_con P Φ v :
+Lemma hoare_value_con {P Φ v} :
   (P ⊢ Φ v) →
   {{ P }} v {{ Φ }}.
 Proof.
@@ -122,8 +152,9 @@ Lemma hoare_rec P Φ f x e v:
   ({{ P }} subst' x v (subst' f (rec: f x := e) e) {{Φ}}) →
   {{ P }} (rec: f x := e)%V v {{Φ}}.
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  intro H_subst.
+  eapply hoare_pure_step; [ apply pure_step_beta | assumption ].
+Qed.
 
 
 Lemma hoare_let P Φ x e v:
@@ -138,58 +169,95 @@ Proof.
   apply pure_step_beta.
 Qed.
 
-Lemma hoare_eq_num (n m: Z):
-  {{ ⌜n = m⌝ }} #n = #m {{ u, ⌜u = #true⌝ }}.
+Lemma hoare_value_exact P v :
+  {{ P }} v {{ w, ⌜w = v⌝ }}.
 Proof.
-  eapply hoare_pure; first reflexivity.
-  intros ->. eapply hoare_pure_step.
-  { apply pure_step_eq. done. }
   apply hoare_value_con.
   by apply ent_prove_pure.
 Qed.
 
+Ltac by_hoare_pred H := eapply hoare_pure; first reflexivity; intro H.
+
+Lemma hoare_eq_num (n m: Z):
+  {{ ⌜n = m⌝ }} #n = #m {{ u, ⌜u = #true⌝ }}.
+Proof.
+  by_hoare_pred Heq; subst.
+  eapply hoare_pure_step; [ apply pure_step_eq; done | apply hoare_value_exact ].
+Qed.
+
 Lemma hoare_neq_num (n m: Z):
   {{ ⌜n ≠ m⌝ }} #n = #m {{ u, ⌜u = #false⌝ }}.
 Proof.
-  (* TODO: exercise *)
-Admitted.
-
+  by_hoare_pred n_ne_m.
+  eapply hoare_pure_step; [ apply (pure_step_neq _ _ n_ne_m) | apply hoare_value_exact ].
+Qed.
 
 Lemma hoare_sub (z1 z2: Z):
   {{ True }} #z1 - #z2 {{ v, ⌜v = #(z1 - z2)⌝ }}.
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  eapply hoare_pure_step; [ apply pure_step_sub | apply hoare_value_exact ].
+Qed.
 
 
 Lemma hoare_add (z1 z2: Z):
   {{ True }} #z1 + #z2 {{ v, ⌜v = #(z1 + z2)⌝ }}.
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  eapply hoare_pure_step; [ apply pure_step_add | apply hoare_value_exact ].
+Qed.
+
+Lemma hoare_mul (z1 z2: Z):
+  {{ True }} #z1 * #z2 {{ v, ⌜v = #(z1 * z2)⌝ }}.
+Proof.
+  eapply hoare_pure_step; [ apply pure_step_mul | apply hoare_value_exact ].
+Qed.
+
+Lemma hoare_mul_nat (n1 n2: nat):
+  {{ True }} #n1 * #n2 {{ v, ⌜v = #((n1 * n2)%nat)⌝ }}.
+Proof.
+  eapply hoare_con_post; [ | apply hoare_mul ].
+  intro v.
+  apply ent_pure_pure.
+  intros ->.
+  have n_eq : (n1 * n2)%Z = (n1 * n2)%nat.
+  {
+    lia.
+  }
+  rewrite n_eq.
+  reflexivity.
+Qed.
 
 
 Lemma hoare_if_false P e1 e2 Φ:
   {{ P }} e2 {{ Φ }} →
   ({{ P }} if: #false then e1 else e2 {{ Φ }}).
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  eapply hoare_pure_step. apply pure_step_if_false.
+Qed.
 
 
 Lemma hoare_if_true P e1 e2 Φ:
   {{ P }} e1 {{ Φ }} →
   ({{ P }} if: #true then e1 else e2 {{ Φ }}).
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  eapply hoare_pure_step. apply pure_step_if_true.
+Qed.
 
 
-Lemma hoare_pure_pre φ Φ e:
-  {{ ⌜φ⌝ }} e {{ Φ }} ↔ (φ → {{ True }} e {{ Φ }}).
-Proof.
-  (* TODO: exercise *)
-Admitted.
+Lemma hoare_pure_pre φ (ψ : val → iProp) e:
+  {{ ⌜φ⌝ }} e {{ ψ }} ↔ (φ → {{ True }} e {{ ψ }}).
+Proof.
+  constructor.
+  - intros He Hφ.
+    (* For yet another ungodly reason,
+      now coq has been messed up and requires multiple goals to be proven inside of focus groups,
+      and if you fail to prove something in an apply, it just gets shelved away.
+    *)
+    eapply (hoare_con_pre (ent_prove_pure _ _ Hφ) He).
+  - intro He.
+    by_hoare_pred Hφ.
+    specialize (He Hφ).
+    by eapply (hoare_con_pre (ent_true _) He).
+Qed.
 
 
 (** Example: Fibonacci *)
@@ -199,18 +267,50 @@ Definition fib: val :=
     else if: "n" = #1 then #1
     else "fib" ("n" - #1) + "fib" ("n" - #2).
 
+Ltac by_pure_step H := eapply hoare_pure_step; first apply H; simpl.
+
 Lemma fib_zero:
   {{ True }} fib #0 {{ v, ⌜v = #0⌝ }}.
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  unfold fib.
+  by_pure_step pure_step_beta.
+  eapply hoare_pure_step.
+  {
+    eapply (pure_step_fill [IfCtx _ _]).
+    apply pure_step_eq; reflexivity.
+  }
+  simpl.
+  by_pure_step pure_step_if_true.
+  apply hoare_value_exact.
+Qed.
 
 
 Lemma fib_one:
   {{ True }} fib #1 {{ v, ⌜v = #1⌝ }}.
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  unfold fib.
+  by_pure_step pure_step_beta.
+
+  eapply hoare_pure_step.
+  {
+    eapply (pure_step_fill [IfCtx _ _]).
+    apply pure_step_neq. auto.
+  }
+  simpl.
+
+  by_pure_step pure_step_if_false.
+
+  eapply hoare_pure_step.
+  {
+    eapply (pure_step_fill [IfCtx _ _]).
+    apply pure_step_eq; reflexivity.
+  }
+  simpl.
+
+  by_pure_step pure_step_if_true.
+
+  apply hoare_value_exact.
+Qed.
 
 
 Lemma fib_succ (z n m: Z):
@@ -243,13 +343,58 @@ Proof.
   eapply hoare_value_con. by apply ent_prove_pure.
 Qed.
 
+Ltac hoare_erase_pre := eapply (hoare_con_pre (Q := True)); [ apply ent_prove_pure; tauto | ].
+Ltac hoare_bind_cleanup :=
+  let v := fresh "v" in
+  let H := fresh "H" in
+  intro v; simpl; by_hoare_pred H; subst v; hoare_erase_pre.
+
 Lemma fib_succ_oldschool (z n m: Z):
   {{ True }} fib #(z - 1)%Z {{ v, ⌜v = #n⌝ }} →
   {{ True }} fib #(z - 2)%Z {{ v, ⌜v = #m⌝ }} →
   {{ ⌜z > 1⌝%Z }} fib #z {{ v, ⌜v = #(n + m)⌝ }}.
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  intros Hf1 Hf2.
+  by_hoare_pred z_gt_one.
+
+  unfold fib.
+  eapply hoare_rec.
+  simpl.
+
+  eapply (hoare_bind [IfCtx _ _]).
+  {
+    eapply hoare_con_pre; [ eapply ent_prove_pure | eapply hoare_neq_num ].
+    lia.
+  }
+  hoare_bind_cleanup.
+
+  eapply hoare_if_false.
+
+  eapply (hoare_bind [IfCtx _ _]).
+  {
+    eapply hoare_con_pre; [ eapply ent_prove_pure | eapply hoare_neq_num ].
+    lia.
+  }
+  hoare_bind_cleanup.
+  eapply hoare_if_false.
+  fold fib.
+
+  eapply (hoare_bind [BinOpRCtx PlusOp _]).
+  {
+    eapply (hoare_bind [AppRCtx _]); [ apply hoare_sub | hoare_bind_cleanup ].
+    exact Hf2.
+  }
+  hoare_bind_cleanup.
+
+  eapply (hoare_bind [BinOpLCtx PlusOp _]).
+  {
+    eapply (hoare_bind [AppRCtx _]); [ apply hoare_sub | hoare_bind_cleanup ].
+    exact Hf1.
+  }
+  hoare_bind_cleanup.
+
+  apply hoare_add.
+Qed.
 
 
 Fixpoint Fib (n: nat) :=
@@ -415,7 +560,19 @@ Definition fac : val :=
     if: "n" = #0 then #1
     else "n" * "fac" ("n" - #1).
 
+Ltac hoare_simpl_if_neq :=
+  eapply (hoare_bind [IfCtx _ _]); [(
+    eapply hoare_con_pre; [ eapply ent_prove_pure | eapply hoare_neq_num ];
+    try lia
+  ) |
+  hoare_bind_cleanup; eapply hoare_if_false].
 
+Ltac hoare_simpl_if_eq :=
+  eapply (hoare_bind [IfCtx _ _]); [(
+    eapply hoare_con_pre; [ eapply ent_prove_pure | eapply hoare_eq_num ];
+    try lia
+  ) |
+  hoare_bind_cleanup; eapply hoare_if_true].
 
 Fixpoint Fac (n : nat) :=
   match n with
@@ -425,18 +582,46 @@ Fixpoint Fac (n : nat) :=
 Lemma fac_computes_Fac (n : nat) :
   {{ True }} fac #n {{ v, ⌜v = #(Fac n)⌝ }}.
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  induction n.
+  - unfold fac.
+    eapply hoare_rec; simpl.
+    hoare_simpl_if_eq.
+    apply hoare_value_exact.
+  - unfold fac.
+    eapply hoare_rec; simpl.
+    hoare_simpl_if_neq.
+    fold fac.
+
+    eapply (hoare_bind [BinOpRCtx _ _]).
+    {
+      eapply (hoare_bind [AppRCtx _]); [ apply hoare_sub | hoare_bind_cleanup ].
+      have h₁ : (S n - 1)%Z = n.
+      {
+        lia.
+      }
+      rewrite h₁.
+      exact IHn.
+    }
+    hoare_bind_cleanup.
+
+    have h₂ : (Fac n) + n * (Fac n) = (S n) * (Fac n).
+    {
+      lia.
+    }
+
+    rewrite h₂.
+    apply (hoare_mul_nat (S n) (Fac n)).
+Qed.
 
 
 (** * Separation Logic *)
-(*Check ent_sep_weaken.*)
-(*Check ent_sep_true.*)
-(*Check ent_sep_comm.*)
-(*Check ent_sep_split.*)
-(*Check ent_sep_assoc.*)
-(*Check ent_pointsto_sep.*)
-(*Check ent_exists_sep.*)
+Check ent_sep_weaken.
+Check ent_sep_true.
+Check ent_sep_comm.
+Check ent_sep_split.
+Check ent_sep_assoc.
+Check ent_pointsto_sep.
+Check ent_exists_sep.
 
 (* Note: The separating conjunction can usually be typed with \ast or \sep *)
 
@@ -444,15 +629,23 @@ Admitted.
 Lemma ent_pointsto_disj l l' v w :
   l ↦ v ∗ l' ↦ w ⊢ ⌜l ≠ l'⌝.
 Proof.
-  (* TODO: exercise *)
-Admitted.
-
+  destruct (decide (l = l')) as [l_eq | l_neq].
+  - rewrite l_eq.
+    eapply ent_trans; [ apply ent_pointsto_sep | apply ent_false ].
+  - apply ent_prove_pure.
+    assumption.
+Qed.
 
 Lemma ent_sep_exists {X} (Φ : X → iProp) P :
   (∃ x : X, Φ x ∗ P) ⊣⊢ (∃ x : X, Φ x) ∗ P.
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  rewrite ent_equiv.
+  constructor.
+  - eapply ent_trans; [ apply ent_exist_elim; intro x | reflexivity ].
+    eapply ent_sep_split; [ | reflexivity ].
+    eapply ent_exist_intro; reflexivity.
+  - eapply ent_exists_sep.
+Qed.
 
 
 
@@ -467,15 +660,36 @@ Definition chain l r : iProp := ∃ n, ⌜n > 0⌝ ∗ chain_pre n l r.
 Lemma chain_single (l r : loc) :
   l ↦ #r ⊢ chain l r.
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  eapply (ent_trans _ (∃ t : loc, l ↦ #t ∗ ⌜t = r⌝) _); [ | eapply (ent_exist_intro 1); unfold chain_pre].
+  - eapply (ent_exist_intro r).
+    etransitivity; first apply ent_sep_true.
+    rewrite ent_sep_comm.
+    apply ent_sep_split; first reflexivity.
+    apply ent_prove_pure.
+    reflexivity.
+  - etrans; first apply ent_sep_true.
+    apply ent_sep_split; last reflexivity.
+    apply ent_prove_pure.
+    lia.
+Qed.
 
 
 Lemma chain_cons (l r t : loc) :
   l ↦ #r ∗ chain r t ⊢ chain l t.
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  unfold chain.
+  rewrite ent_sep_comm.
+  rewrite <-ent_sep_exists.
+  apply ent_exist_elim; intro x.
+
+  rewrite <-ent_sep_assoc.
+  rewrite (ent_sep_comm _ (l ↦ #r)).
+  eapply (ent_exist_intro (S x)).
+  unfold chain_pre; fold chain_pre.
+  apply ent_sep_split; [ apply ent_pure_pure; intro; lia | ].
+  eapply (ent_exist_intro r).
+  reflexivity.
+Qed.
 
 
 Lemma chain_trans (l r t : loc) :
@@ -535,8 +749,12 @@ Lemma hoare_assert P e :
   {{ P }} e {{ v, ⌜v = #true⌝ }} →
   {{ P }} assert e {{ v, ⌜v = #()⌝ }}.
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  intro He.
+  unfold assert.
+  eapply (hoare_bind [IfCtx _ _]); [ exact He | hoare_bind_cleanup ].
+  apply hoare_if_true.
+  apply hoare_value_exact.
+Qed.
 
 
 Lemma frame_example (f : val) :
@@ -748,4 +966,3 @@ Lemma tail_ll_strengthened v x xs :
 Proof.
   (* FIXME: exercise *)
 Abort.
-