From a565eb10c3452cbb27327af7c5a748364bbd0027 Mon Sep 17 00:00:00 2001 From: Benjamin Peters Date: Thu, 4 Jan 2024 11:54:14 +0100 Subject: [PATCH 1/2] solution for exercise 08 --- _CoqProject | 1 + theories/program_logics/hoare_sol.v | 1037 +++++++++++++++++++++++++++ 2 files changed, 1038 insertions(+) create mode 100644 theories/program_logics/hoare_sol.v diff --git a/_CoqProject b/_CoqProject index a7ea32a..3b529fc 100644 --- a/_CoqProject +++ b/_CoqProject @@ -92,6 +92,7 @@ theories/program_logics/heap_lang/primitive_laws_nolater.v # Program logic chapter theories/program_logics/hoare_lib.v theories/program_logics/hoare.v +theories/program_logics/hoare_sol.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/hoare_sol.v b/theories/program_logics/hoare_sol.v new file mode 100644 index 0000000..2b2948f --- /dev/null +++ b/theories/program_logics/hoare_sol.v @@ -0,0 +1,1037 @@ +From iris.prelude Require Import options. +From iris.proofmode Require Import tactics. +From iris.heap_lang Require Import lang notation. +From semantics.pl Require Export hoare_lib. + +Import hoare. +Implicit Types + (P Q: iProp) + (φ ψ: Prop) + (e: expr) + (v: val). + + +(** * Hoare logic *) + +(** Entailment rules *) + + +(** Derived entailment rules *) +Lemma ent_weakening P Q R : + (P ⊢ R) → + P ∧ Q ⊢ R. +Proof. + intros HP. eapply ent_trans. + - apply ent_and_elim_l. + - done. +Qed. + +Lemma ent_true P : + P ⊢ True. +Proof. + by apply ent_prove_pure. +Qed. + +Lemma ent_false P : + False ⊢ P. +Proof. + eapply ent_assume_pure. + - apply ent_refl. + - done. +Qed. + +Lemma ent_and_comm P Q : + P ∧ Q ⊢ Q ∧ P. +Proof. + apply ent_and_intro. + - apply ent_and_elim_r. + - apply ent_and_elim_l. +Qed. + +Lemma ent_or_comm P Q : + P ∨ Q ⊢ Q ∨ P. +Proof. + apply ent_or_elim. + - apply ent_or_intror. + - apply ent_or_introl. +Qed. + +Lemma ent_all_comm {X} (Φ : X → X → iProp) : + (∀ x y, Φ x y) ⊢ (∀ y x, Φ x y). +Proof. + apply ent_all_intro. intros y. + apply ent_all_intro. intros x. + etrans. + - 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. + eapply ent_exist_elim. intros x. + eapply ent_exist_elim. intros y. + eapply ent_exist_intro. eapply ent_exist_intro. + apply ent_refl. +Qed. + +(** Derived Hoare rules *) +Lemma hoare_con_pre P Q Φ e: + (P ⊢ Q) → + {{ Q }} e {{ Φ }} → + {{ P }} e {{ Φ }}. +Proof. + intros ??. eapply hoare_con; eauto. +Qed. + +Lemma hoare_con_post P Φ Ψ e: + (∀ v, Ψ v ⊢ Φ v) → + {{ P }} e {{ Ψ }} → + {{ P }} e {{ Φ }}. +Proof. + intros ??. eapply hoare_con; last done; eauto. +Qed. + +Lemma hoare_value_con P Φ v : + (P ⊢ Φ v) → + {{ P }} v {{ Φ }}. +Proof. + intros H. eapply hoare_con; last apply hoare_value. + - apply H. + - eauto. +Qed. + +Lemma hoare_value' P v : + {{ P }} v {{ w, P ∗ ⌜w = v⌝}}. +Proof. + eapply hoare_con; last apply hoare_value with (Φ := (λ v', P ∗ ⌜v' = v⌝)%I). + - etrans; first apply ent_sep_true. rewrite ent_sep_comm. apply ent_sep_split; first done. + by apply ent_prove_pure. + - done. +Qed. + +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. + intros Ha. eapply hoare_pure_step; last done. + apply pure_step_beta. +Qed. + +Lemma hoare_let P Φ x e v: + ({{ P }} subst' x v e {{Φ}}) → + {{ P }} let: x := v in e {{Φ}}. +Proof. + intros Ha. eapply hoare_pure_steps. + { eapply (rtc_pure_step_fill [AppLCtx _]). + apply pure_step_val. done. + } + eapply hoare_pure_step; last done. + apply pure_step_beta. +Qed. + +Lemma hoare_eq_num (n m: Z): + {{ ⌜n = m⌝ }} #n = #m {{ u, ⌜u = #true⌝ }}. +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. + +Lemma hoare_neq_num (n m: Z): + {{ ⌜n ≠ m⌝ }} #n = #m {{ u, ⌜u = #false⌝ }}. +Proof. + eapply hoare_pure; first reflexivity. + intros Hneq. eapply hoare_pure_step. + { apply pure_step_neq. done. } + apply hoare_value_con. + by apply ent_prove_pure. +Qed. + +Lemma hoare_sub (z1 z2: Z): + {{ True }} #z1 - #z2 {{ v, ⌜v = #(z1 - z2)⌝ }}. +Proof. + eapply hoare_pure_step. + { apply pure_step_sub. } + apply hoare_value_con. by apply ent_prove_pure. +Qed. + +Lemma hoare_add (z1 z2: Z): + {{ True }} #z1 + #z2 {{ v, ⌜v = #(z1 + z2)⌝ }}. +Proof. + eapply hoare_pure_step. + { apply pure_step_add. } + apply hoare_value_con. by apply ent_prove_pure. +Qed. + +Lemma hoare_if_false P e1 e2 Φ: + {{ P }} e2 {{ Φ }} → + ({{ P }} if: #false then e1 else e2 {{ Φ }}). +Proof. + intros H. eapply hoare_pure_step. + { apply pure_step_if_false. } + done. +Qed. + +Lemma hoare_if_true P e1 e2 Φ: + {{ P }} e1 {{ Φ }} → + ({{ P }} if: #true then e1 else e2 {{ Φ }}). +Proof. + intros H. eapply hoare_pure_step. + { apply pure_step_if_true. } + done. +Qed. + +Lemma hoare_pure_pre φ Φ e: + {{ ⌜φ⌝ }} e {{ Φ }} ↔ (φ → {{ True }} e {{ Φ }}). +Proof. + split. + - intros Hh Hφ. eapply hoare_con; last done. + + eapply ent_prove_pure. done. + + intros v. eapply ent_refl. + - intros Hh. eapply hoare_pure; first eapply ent_refl. + intros ?. eapply hoare_con; last by eapply Hh. + + eapply ent_prove_pure; done. + + intros ?. eapply ent_refl. +Qed. + +(** Example: Fibonacci *) +Definition fib: val := + rec: "fib" "n" := + if: "n" = #0 then #0 + else if: "n" = #1 then #1 + else "fib" ("n" - #1) + "fib" ("n" - #2). + +Lemma fib_zero: + {{ True }} fib #0 {{ v, ⌜v = #0⌝ }}. +Proof. + unfold fib. + eapply hoare_pure_steps. + { econstructor 2. + { apply pure_step_beta. } + simpl. econstructor 2. + { apply (pure_step_fill [IfCtx _ _]). apply pure_step_eq. done. } + simpl. econstructor 2. + { apply pure_step_if_true. } + reflexivity. + } + apply hoare_value_con. apply ent_prove_pure. done. +Qed. + +Lemma fib_one: + {{ True }} fib #1 {{ v, ⌜v = #1⌝ }}. +Proof. + unfold fib. + eapply hoare_pure_steps. + { econstructor 2. + { apply pure_step_beta. } + simpl. econstructor 2. + { apply (pure_step_fill [IfCtx _ _ ]). apply pure_step_neq. done. } + simpl. econstructor 2. + { apply pure_step_if_false. } + econstructor 2. + { apply (pure_step_fill [IfCtx _ _]). apply pure_step_eq. done. } + econstructor 2. + { apply pure_step_if_true. } + reflexivity. + } + eapply hoare_value_con. apply ent_prove_pure. done. +Qed. + +Lemma fib_succ (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. + intros H1 H2. eapply hoare_pure_pre. intros Hgt. + unfold fib. + eapply hoare_pure_steps. + { econstructor 2. + { apply pure_step_beta. } + simpl. econstructor 2. { apply (pure_step_fill [IfCtx _ _]). apply pure_step_neq. lia. } + simpl. econstructor 2. { apply pure_step_if_false. } + econstructor 2. { apply (pure_step_fill [IfCtx _ _]). apply pure_step_neq. lia. } + simpl. econstructor 2. { apply pure_step_if_false. } + fold fib. reflexivity. + } + eapply (hoare_bind [BinOpRCtx _ _]). + { eapply (hoare_bind [AppRCtx _]). { apply hoare_sub. } + intros v. eapply hoare_pure_pre. intros ->. apply H2. + } + intros v. apply hoare_pure_pre. intros ->. simpl. + eapply (hoare_bind [BinOpLCtx _ _]). + { eapply (hoare_bind [AppRCtx _]). { apply hoare_sub. } + intros v. eapply hoare_pure_pre. intros ->. apply H1. + } + intros v. apply hoare_pure_pre. intros ->. simpl. + eapply hoare_pure_step. { apply pure_step_add. } + eapply hoare_value_con. by apply ent_prove_pure. +Qed. + +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. + intros H1 H2. eapply hoare_pure_pre. intros Hgt. + rewrite /fib. + eapply hoare_rec; simpl. fold fib. + eapply hoare_bind with (K := [IfCtx _ _]). + { eapply hoare_con; last eapply hoare_neq_num; eauto with lia. } + intros v; simpl. apply hoare_pure_pre. + intros ->. eapply hoare_if_false. + eapply hoare_bind with (K := [IfCtx _ _]). + { eapply hoare_con; last eapply hoare_neq_num; eauto with lia. } + intros w; simpl. apply hoare_pure_pre. + intros ->. eapply hoare_if_false. + eapply hoare_bind with (K := [AppRCtx _; BinOpRCtx _ _]). + { eapply hoare_sub. } + simpl. intros w. eapply hoare_pure_pre. intros ->. + eapply hoare_bind with (K := [BinOpRCtx _ _]); first eapply H2. + simpl. intros w. eapply hoare_pure_pre. intros ->. + eapply hoare_bind with (K := [BinOpLCtx _ _]). + - eapply hoare_bind with (K := [AppRCtx _]); first by eapply hoare_sub. + simpl. intros v. eapply hoare_pure_pre. + intros ->. eapply H1. + - simpl. intros v. eapply hoare_pure_pre. + intros ->. eapply hoare_add. +Qed. + +Fixpoint Fib (n: nat) := + match n with + | 0 => 0 + | S n => + match n with + | 0 => 1 + | S m => Fib n + Fib m + end + end. + +Lemma fib_computes_Fib (n: nat): + {{ True }} fib #n {{ v, ⌜v = #(Fib n)⌝ }}. +Proof. + induction (lt_wf n) as [n _ IH]. + destruct n as [|[|n]]. + - simpl. eapply fib_zero. + - simpl. eapply fib_one. + - replace (Fib (S (S n)): Z) with (Fib (S n) + Fib n)%Z by (simpl; lia). + edestruct (hoare_pure_pre (S (S n) > 1))%Z as [H1 _]; eapply H1; last lia. + eapply fib_succ. + + replace (S (S n) - 1)%Z with (S n: Z) by lia. eapply IH. lia. + + replace (S (S n) - 2)%Z with (n: Z) by lia. eapply IH. lia. +Qed. + +(** ** Example: gcd *) +Definition mod_val : val := + λ: "a" "b", "a" - ("a" `quot` "b") * "b". +Definition euclid: val := + rec: "euclid" "a" "b" := + if: "b" = #0 then "a" else "euclid" "b" (mod_val "a" "b"). + +Lemma quot_diff a b : + (0 ≤ a)%Z → (0 < b)%Z → (0 ≤ a - a `quot` b * b < b)%Z. +Proof. + intros. split. + - rewrite Z.mul_comm -Z.rem_eq; last lia. apply Z.rem_nonneg; lia. + - rewrite Z.mul_comm -Z.rem_eq; last lia. + specialize (Z.rem_bound_pos_pos a b ltac:(lia) ltac:(lia)). lia. +Qed. +Lemma Z_nonneg_ind (P : Z → Prop) : + (∀ x, (0 ≤ x)%Z → (∀ y, (0 ≤ y < x)%Z → P y) → P x) → + ∀ x, (0 ≤ x)%Z → P x. +Proof. + intros IH x Hle. generalize Hle. + revert x Hle. refine (Z_lt_induction (λ x, (0 ≤ x)%Z → P x) _). + naive_solver. +Qed. + +Lemma mod_spec (a b : Z) : + {{ ⌜(b > 0)%Z⌝ ∧ ⌜(a >= 0)%Z⌝ }} + mod_val #a #b + {{ cv, ∃ (c k : Z), ⌜cv = #c ∧ (0 <= k)%Z ∧ (a = b * k + c)%Z ∧ (0 <= c < b)%Z⌝ }}. +Proof. + eapply (hoare_pure _ (b > 0 ∧ a >= 0)%Z). + { eapply ent_assume_pure. { eapply ent_and_elim_l. } + intros ?. eapply ent_assume_pure. { eapply ent_and_elim_r. } + intros ?. eapply ent_assume_pure. { eapply ent_and_elim_l. } + intros ?. apply ent_prove_pure. done. + } + intros (? & ?). + unfold mod_val. eapply hoare_pure_step. + { apply pure_step_fill with (K := [AppLCtx _]). apply pure_step_beta. } + fold mod_val. simpl. + apply hoare_let. simpl. + eapply hoare_pure_step. + { apply pure_step_fill with (K := [BinOpLCtx _ _; BinOpRCtx _ _]). + apply pure_step_quot. lia. + } + simpl. eapply hoare_pure_step. + { apply pure_step_fill with (K := [BinOpRCtx _ _]). apply pure_step_mul. } + simpl. eapply hoare_pure_step. + { apply pure_step_sub. } + eapply hoare_value_con. + eapply ent_exist_intro. apply ent_exist_intro with (x := (a `quot` b)%Z). + (* MATH *) + apply ent_prove_pure. split; last split; last split. + - reflexivity. + - apply Z.quot_pos; lia. + - lia. + - apply quot_diff; lia. +Qed. + +Lemma gcd_step (b c k : Z) : + Z.gcd b c = Z.gcd (b * k + c) b. +Proof. + rewrite Z.add_comm (Z.gcd_comm _ b) Z.mul_comm Z.gcd_add_mult_diag_r. done. +Qed. + +Lemma euclid_step_gt0 (a b : Z) : + (∀ c : Z, + {{ ⌜(0 ≤ c < b)%Z⌝}} + euclid #b #c + {{ d, ⌜d = #(Z.gcd b c)⌝ }}) → + {{ ⌜(b > 0)%Z⌝ ∧ ⌜(a >= 0)%Z⌝}} euclid #a #b {{ c, ⌜c = #(Z.gcd a b)⌝ }}. +Proof. + intros Ha. + eapply (hoare_pure _ (a >= 0 ∧ b > 0)%Z). + { eapply ent_assume_pure. { eapply ent_and_elim_l. } + intros ?. eapply ent_assume_pure. { eapply ent_and_elim_r. } + intros ?. eapply ent_assume_pure. { eapply ent_and_elim_l. } + intros ?. apply ent_prove_pure. done. + } + intros (? & ?). + unfold euclid. eapply hoare_pure_step. + { apply (pure_step_fill [AppLCtx _]). apply pure_step_beta. } + fold euclid. simpl. apply hoare_let. simpl. + eapply hoare_pure_step. + { apply (pure_step_fill [IfCtx _ _]). apply pure_step_neq. lia. } + simpl. apply hoare_if_false. + + eapply hoare_bind with (K := [AppRCtx _]). + { apply mod_spec. } + intros v. simpl. + apply hoare_exist_pre. intros d. + apply hoare_exist_pre. intros k. + apply hoare_pure_pre. + intros (-> & ? & -> & ?). + eapply hoare_con; last apply Ha. + { apply ent_prove_pure. split_and!; lia. } + { simpl. intros v. eapply ent_assume_pure; first done. intros ->. + apply ent_prove_pure. f_equiv. f_equiv. apply gcd_step. + } +Qed. + +Lemma euclid_step_0 (a : Z) : + {{ True }} euclid #a #0 {{ v, ⌜v = #a⌝ }}. +Proof. + unfold euclid. eapply hoare_pure_step. + { apply (pure_step_fill [AppLCtx _]). apply pure_step_beta. } + fold euclid. simpl. apply hoare_let. simpl. + eapply hoare_pure_step. + { apply (pure_step_fill [IfCtx _ _]). apply pure_step_eq. lia. } + simpl. apply hoare_if_true. + apply hoare_value_con. by apply ent_prove_pure. +Qed. + +Lemma euclid_proof (a b : Z) : + {{ ⌜(0 ≤ a ∧ 0 ≤ b)%Z⌝ }} euclid #a #b {{ c, ⌜c = #(Z.gcd a b)⌝ }}. +Proof. + eapply hoare_pure_pre. intros (Ha & Hb). + revert b Hb a Ha. refine (Z_nonneg_ind _ _). + intros b Hb IH a Ha. + destruct (decide (b = 0)) as [ -> | Hneq0]. + - eapply hoare_con; last apply euclid_step_0. + { done. } + { intros v. simpl. eapply ent_assume_pure; first done. intros ->. + apply ent_prove_pure. + rewrite Z.gcd_0_r Z.abs_eq; first done. lia. + } + - (* use a mod b < b *) + eapply hoare_con; last apply euclid_step_gt0. + { apply ent_and_intro; apply ent_prove_pure; lia. } + { done. } + intros c. apply hoare_pure_pre. intros. + eapply hoare_con; last eapply IH; [ done | done | lia.. ]. +Qed. + +(** Exercise: Factorial *) +Definition fac : val := + rec: "fac" "n" := + if: "n" = #0 then #1 + else "n" * "fac" ("n" - #1). + +Lemma fac_zero : + {{ True }} fac #0 {{ v, ⌜v = #1⌝ }}. +Proof. + unfold fac. apply hoare_rec. simpl. + eapply hoare_pure_steps. + { econstructor 2. + { eapply pure_step_fill with (K := [IfCtx _ _]). by apply pure_step_eq. } + simpl. econstructor 2. { apply pure_step_if_true. } + reflexivity. + } + eapply hoare_value_con. by apply ent_prove_pure. +Qed. + +Lemma fac_succ (n m : Z) : + {{ True }} fac #(n - 1) {{ v, ⌜v = #m⌝ }} → + {{ ⌜(n > 0)%Z⌝ }} fac #n {{ v, ⌜v = #(n * m)⌝ }}. +Proof. + intros Hs. unfold fac. apply hoare_rec. simpl. + apply hoare_pure_pre. intros Hn. + eapply hoare_pure_steps. + { econstructor 2. + { eapply pure_step_fill with (K := [IfCtx _ _]). + apply pure_step_neq. lia. } + simpl. econstructor 2. { apply pure_step_if_false. } + fold fac. econstructor 2. + { eapply pure_step_fill with (K := [AppRCtx _; BinOpRCtx _ _]). + apply pure_step_sub. + } + simpl. reflexivity. + } + eapply hoare_bind with (K := [BinOpRCtx _ _]). { apply Hs. } + intros v. apply hoare_pure_pre. intros ->. + simpl. eapply hoare_pure_step. { apply pure_step_mul. } + eapply hoare_value_con. by apply ent_prove_pure. +Qed. + +Fixpoint Fac (n : nat) := + match n with + | 0 => 1 + | S n => (S n) * Fac n + end. +Lemma fac_computes_Fac (n : nat) : + {{ True }} fac #n {{ v, ⌜v = #(Fac n)⌝ }}. +Proof. + induction n as [ | n IH]; simpl. + - apply fac_zero. + - eapply hoare_con; first last. + + apply fac_succ. + replace (Z.of_nat (S n) - 1)%Z with (Z.of_nat n) by lia. + apply IH. + + intros v. simpl. eapply ent_assume_pure; first reflexivity. + intros ->. apply ent_prove_pure. f_equiv. f_equiv. lia. + + apply ent_prove_pure; done. +Qed. + +(** * Separation Logic *) + + +(* Note: The separating conjunction can usually be typed with \ast or \sep *) + + +Lemma ent_pointsto_disj l l' v w : + l ↦ v ∗ l' ↦ w ⊢ ⌜l ≠ l'⌝. +Proof. + destruct (decide (l = l')) as [ -> | Hneq]. + - etrans. { apply ent_pointsto_sep. } + apply ent_false. + - by apply ent_prove_pure. +Qed. + +Lemma ent_sep_exists {X} (Φ : X → iProp) P : + (∃ x : X, Φ x ∗ P) ⊣⊢ (∃ x : X, Φ x) ∗ P. +Proof. + apply ent_equiv. split. + - apply ent_exist_elim. intros x. + apply ent_sep_split; last done. + by eapply ent_exist_intro. + - apply ent_exists_sep. +Qed. + + +(** ** Example: Chains *) +Fixpoint chain_pre n l r : iProp := + match n with + | 0 => ⌜l = r⌝ + | S n => ∃ t : loc, l ↦ #t ∗ chain_pre n t r + end. +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. + unfold chain. eapply ent_exist_intro with (x := 1). + etrans; first apply ent_sep_true. apply ent_sep_split. + - apply ent_prove_pure. lia. + - eapply ent_exist_intro. etrans; first apply ent_sep_true. + rewrite ent_sep_comm. apply ent_sep_split; first done. + apply ent_prove_pure; done. +Qed. + +Lemma chain_cons (l r t : loc) : + l ↦ #r ∗ chain r t ⊢ chain l t. +Proof. + unfold chain. rewrite ent_sep_comm -ent_sep_exists. + apply ent_exist_elim. intros n. + apply ent_exist_intro with (x := S n). rewrite -ent_sep_assoc. + eapply ent_assume_pure. + { etrans; first apply ent_sep_weaken. done. } + intros ?. apply ent_sep_split. + { apply ent_prove_pure. lia. } + simpl. apply ent_exist_intro with (x := r). + rewrite ent_sep_comm. apply ent_sep_split; done. +Qed. + +Lemma chain_trans (l r t : loc) : + chain l r ∗ chain r t ⊢ chain l t. +Proof. + unfold chain. rewrite -ent_sep_exists. + apply ent_exist_elim. intros n. + rewrite ent_sep_comm -ent_sep_exists. + apply ent_exist_elim. intros m. + eapply ent_assume_pure. + { etrans; first apply ent_sep_weaken. etrans; first apply ent_sep_weaken; done. } + intros ?. + eapply ent_assume_pure. + { rewrite ent_sep_comm. etrans; first apply ent_sep_weaken. etrans; first apply ent_sep_weaken; done. } + intros Hn. + apply ent_exist_intro with (x := n + m). rewrite -ent_sep_assoc. + apply ent_sep_split. + { apply ent_prove_pure; lia. } + induction n as [ | n IH] in l, Hn |-*; first lia. + simpl. + setoid_rewrite ent_sep_comm at 2. rewrite -ent_sep_exists. + rewrite ent_sep_comm -ent_sep_exists. + apply ent_exist_elim. intros l'. apply ent_exist_intro with (x := l'). + rewrite -!ent_sep_assoc. apply ent_sep_split; first done. + destruct n as [ | n]. + - simpl. eapply ent_assume_pure. { apply ent_sep_weaken. } + intros ->. rewrite ent_sep_comm. rewrite (ent_sep_comm _ (chain_pre _ _ _)) -ent_sep_assoc. + apply ent_sep_weaken. + - etrans; last apply IH; last lia. + rewrite ent_sep_comm. rewrite ent_sep_assoc. apply ent_sep_split; last done. + rewrite ent_sep_comm. apply ent_sep_split; first done. + apply ent_prove_pure. lia. +Qed. + +Lemma chain_sep_false (l r t : loc) : + chain l r ∗ chain l t ⊢ False. +Proof. + unfold chain. rewrite -ent_sep_exists. + apply ent_exist_elim. intros n. + rewrite ent_sep_comm -ent_sep_exists. + apply ent_exist_elim. intros m. + eapply ent_assume_pure. + { etrans; first apply ent_sep_weaken. etrans; first apply ent_sep_weaken; done. } + intros ?. + eapply ent_assume_pure. + { rewrite ent_sep_comm. etrans; first apply ent_sep_weaken. etrans; first apply ent_sep_weaken; done. } + intros Hn. + destruct n as [ | n]; first lia. + destruct m as [ | m]; first lia. + simpl. + setoid_rewrite ent_sep_comm at 2. rewrite -ent_sep_exists -ent_sep_exists. + apply ent_exist_elim. intros l'. + rewrite ent_sep_comm. setoid_rewrite ent_sep_comm at 2. + rewrite -ent_sep_exists -ent_sep_exists. + apply ent_exist_elim. intros l''. + rewrite !ent_sep_assoc. etrans; first apply ent_sep_weaken. + etrans; first apply ent_sep_weaken. + rewrite -ent_sep_assoc. rewrite ent_sep_comm ent_sep_assoc. + etrans; first apply ent_sep_weaken. + rewrite -ent_sep_assoc ent_sep_comm. etrans; first apply ent_sep_weaken. + apply ent_pointsto_sep. +Qed. + +Definition cycle l := chain l l. +Lemma chain_cycle l r : + chain l r ∗ chain r l ⊢ cycle l. +Proof. + apply chain_trans. +Qed. + + +(** New Hoare rules *) +(*Check hoare_frame.*) +(*Check hoare_new.*) +(*Check hoare_store.*) +(*Check hoare_load.*) + +Lemma hoare_pure_pre_sep_l (ϕ : Prop) Q Φ e : + (ϕ → {{ Q }} e {{ Φ }}) → + {{ ⌜ϕ⌝ ∗ Q }} e {{ Φ }}. +Proof. + intros He. + eapply hoare_pure. + { apply ent_sep_weaken. } + intros ?. + eapply hoare_con; last by apply He. + - rewrite ent_sep_comm. apply ent_sep_weaken. + - done. +Qed. + +(* Enables rewriting with equivalences ⊣⊢ in pre/post condition *) +#[export] Instance hoare_proper : + Proper (equiv ==> eq ==> (pointwise_relation val (⊢)) ==> impl) hoare. +Proof. + intros P1 P2 HP%ent_equiv e1 e2 <- Φ1 Φ2 HΦ Hp. + eapply hoare_con; last done. + - apply HP. + - done. +Qed. + +Definition assert e := (if: e then #() else #0 #0)%E. + +Lemma hoare_assert P e : + {{ P }} e {{ v, ⌜v = #true⌝ }} → + {{ P }} assert e {{ v, ⌜v = #()⌝ }}. +Proof. + intros He. + eapply hoare_bind with (K := [IfCtx _ _]); first done. + intros v. simpl. apply hoare_pure_pre. intros ->. + eapply hoare_pure_step. + { apply pure_step_if_true. } + apply hoare_value_con. by apply ent_prove_pure. +Qed. + +Lemma frame_example (f : val) : + (∀ l l' : loc, {{ l ↦ #0 }} f #l #l' {{ _, l ↦ #42 }}) → + {{ True }} + let: "x" := ref #0 in + let: "y" := ref #42 in + (f "x" "y";; + assert (!"x" = !"y")) + {{ _, True }}. +Proof. + intros Hf. + eapply hoare_bind with (K := [AppRCtx _]). + { apply hoare_new. } + intros v. simpl. + apply hoare_exist_pre. intros l. + apply hoare_pure_pre_sep_l. intros ->. + eapply hoare_let. simpl. + + eapply hoare_bind with (K := [AppRCtx _]). + { eapply hoare_con_pre. { apply ent_sep_true. } + eapply hoare_frame. apply hoare_new. } + intros v. simpl. + + rewrite -ent_sep_exists. apply hoare_exist_pre. intros l'. + rewrite -ent_sep_assoc. eapply hoare_pure_pre_sep_l. intros ->. + eapply hoare_let. simpl. + eapply hoare_bind with (K := [AppRCtx _]). + { rewrite ent_sep_comm. eapply hoare_frame. apply Hf. } + intros v. simpl. + + apply hoare_let. simpl. + eapply hoare_con_post; first last. + { apply hoare_assert. + eapply hoare_bind with (K := [BinOpRCtx _ _]). + { rewrite ent_sep_comm. apply hoare_frame. apply hoare_load. } + intros v'. simpl. rewrite -ent_sep_assoc. apply hoare_pure_pre_sep_l. + intros ->. + + eapply hoare_bind with (K := [BinOpLCtx _ _]). + { rewrite ent_sep_comm. apply hoare_frame. apply hoare_load. } + intros v'. simpl. rewrite -ent_sep_assoc. apply hoare_pure_pre_sep_l. + intros ->. + + eapply hoare_pure_step. { by apply pure_step_eq. } + eapply hoare_value_con. by apply ent_prove_pure. + } + intros. apply ent_true. +Qed. + +(** Exercise: swap *) +Definition swap : val := + λ: "l" "r", let: "t" := ! "r" in "r" <- !"l";; "l" <- "t". + +Lemma swap_correct (l r: loc) (v w: val): + {{ l ↦ v ∗ r ↦ w }} swap #l #r {{ _, l ↦ w ∗ r ↦ v }}. +Proof. + rewrite /swap. + (* we execute the first application *) + eapply hoare_bind with (K := [AppLCtx _]). + { eapply hoare_rec; simpl. + eapply hoare_pure_steps. + { eapply pure_step_val. constructor. } + eapply hoare_value'. + } + + (* we remove the equality over f *) + simpl; intros f. rewrite ent_sep_comm. + eapply hoare_pure_pre_sep_l. intros ->. + eapply hoare_rec. simpl. + + (* we execute the load *) + eapply hoare_bind with (K := [AppRCtx _]). + { rewrite ent_sep_comm. apply hoare_frame. apply hoare_load. } + intros v'. simpl. rewrite -ent_sep_assoc. apply hoare_pure_pre_sep_l. intros ->. + + (* we execute the let *) + eapply hoare_let; simpl. + + (* we execute the next load *) + eapply hoare_bind with (K := [StoreRCtx _; AppRCtx _]). + { rewrite ent_sep_comm. apply hoare_frame. apply hoare_load. } + intros t; simpl. rewrite -ent_sep_assoc. apply hoare_pure_pre_sep_l. intros ->. + + (* we execute the store *) + eapply hoare_bind with (K := [AppRCtx _]). + { rewrite ent_sep_comm. apply hoare_frame. apply hoare_store. } + simpl. intros ?. apply hoare_let. simpl. + + (* we execute the store *) + rewrite ent_sep_comm. apply hoare_frame. apply hoare_store. +Qed. + + + +(** ** Case study: lists *) +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. + induction xs as [ | x xs IH] in v |-*. + - simpl. apply hoare_pure_pre_sep_l. intros ->. + eapply hoare_bind with (K := [AppLCtx _]). + { apply hoare_rec. simpl. + eapply hoare_pure_steps. + { apply pure_step_val. done. } + eapply hoare_value'. + } + intros v'. simpl. rewrite ent_sep_comm. apply hoare_pure_pre_sep_l. intros ->. + + apply hoare_rec. simpl. + eapply hoare_pure_step. { apply pure_step_match_injl. } + apply hoare_let. simpl. apply hoare_value. + - simpl. rewrite -ent_sep_exists. apply hoare_exist_pre. + intros l. rewrite -ent_sep_exists. apply hoare_exist_pre. + intros w'. rewrite -ent_sep_assoc. apply hoare_pure_pre_sep_l. intros ->. + + eapply hoare_bind with (K := [AppLCtx _ ]). + { apply hoare_rec. simpl. + eapply hoare_pure_steps. {apply pure_step_val. done. } + eapply hoare_value'. + } + intros v'. simpl. rewrite ent_sep_comm. apply hoare_pure_pre_sep_l. intros ->. + + apply hoare_rec. simpl. + eapply hoare_pure_step. {apply pure_step_match_injr. } + apply hoare_let. simpl. + eapply hoare_bind with (K := [AppRCtx _]). + { apply hoare_frame. apply hoare_frame. apply hoare_load. } + intros v. simpl. + rewrite -!ent_sep_assoc. apply hoare_pure_pre_sep_l. intros ->. + apply hoare_let. simpl. + + eapply hoare_bind with (K := [PairRCtx _; StoreRCtx _; AppRCtx _]). + { eapply hoare_bind with (K := [AppRCtx _; AppLCtx _]). + { eapply hoare_pure_step. { apply pure_step_snd. } + apply hoare_value'. + } + intros v. simpl. fold app_ll. + rewrite ent_sep_comm. apply hoare_pure_pre_sep_l. intros ->. + rewrite ent_sep_comm. eapply hoare_frame. + apply IH. + } + intros v. simpl. + eapply hoare_bind with (K := [PairLCtx _; StoreRCtx _; AppRCtx _]). + { eapply hoare_pure_step. { apply pure_step_fst. } + apply hoare_value'. + } + intros v'. simpl. rewrite ent_sep_comm. apply hoare_pure_pre_sep_l. intros ->. + eapply hoare_bind with (K := [AppRCtx _]). + { rewrite ent_sep_comm. apply hoare_frame. + eapply hoare_bind with (K := [StoreRCtx _]). + { eapply hoare_pure_steps. + { eapply pure_step_val. eauto. } + eapply hoare_value'. + } + intros v'. simpl. rewrite ent_sep_comm. apply hoare_pure_pre_sep_l. intros ->. + apply hoare_store. + } + intros v'. simpl. apply hoare_let. simpl. + eapply hoare_pure_steps. + { eapply pure_step_val. eauto. } + eapply hoare_value_con. + eapply ent_exist_intro. eapply ent_exist_intro. + etrans. { apply ent_sep_true. } + eapply ent_sep_split. + { apply ent_prove_pure. done. } + apply ent_sep_split; reflexivity. +Qed. + +(** Exercise: linked lists *) +Lemma new_ll_correct : + {{ True }} new_ll #() {{ v, is_ll [] v }}. +Proof. + unfold new_ll. apply hoare_rec. simpl. + apply hoare_value_con. + by apply ent_prove_pure. +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 cons_ll. + eapply hoare_bind with (K := [AppLCtx _]). + { apply hoare_rec. simpl. + eapply hoare_pure_steps. + { eapply pure_step_val. eauto. } + eapply hoare_value'. + } + intros v'. simpl. rewrite ent_sep_comm. apply hoare_pure_pre_sep_l. intros ->. + eapply hoare_rec. simpl. + eapply hoare_bind with (K := [InjRCtx]). + { eapply hoare_bind with (K := [AllocNRCtx _]). + { eapply hoare_pure_steps. { eapply pure_step_val; eauto. } + eapply hoare_value'. + } + intros v'. simpl. rewrite ent_sep_comm. apply hoare_pure_pre_sep_l. + intros ->. + eapply hoare_con_pre; first apply ent_sep_true. + apply hoare_frame. apply hoare_new. + } + intros v'. simpl. rewrite -ent_sep_exists. + apply hoare_exist_pre. intros l. + rewrite -ent_sep_assoc. apply hoare_pure_pre_sep_l. intros ->. + eapply hoare_pure_steps. + { apply pure_step_val; eauto. } + apply hoare_value_con. + + eapply ent_exist_intro. eapply ent_exist_intro. + etrans. { apply ent_sep_true. } + eapply ent_sep_split. + { apply ent_prove_pure. done. } + apply ent_sep_split; reflexivity. +Qed. + +Lemma head_ll_correct (v x : val) xs : + {{ is_ll (x :: xs) v }} head_ll v {{ w, ⌜w = x⌝ }}. +Proof. + unfold head_ll. + apply hoare_rec. simpl. + apply hoare_exist_pre. intros l. + apply hoare_exist_pre. intros w. + apply hoare_pure_pre_sep_l. intros ->. + eapply hoare_pure_step. + { apply pure_step_match_injr. } + apply hoare_let. simpl. + eapply hoare_bind with (K := [FstCtx]). + { apply hoare_frame. apply hoare_load. } + intros v. simpl. rewrite -ent_sep_assoc. apply hoare_pure_pre_sep_l. intros ->. + eapply hoare_pure_step. { apply pure_step_fst. } + eapply hoare_value_con. + apply ent_prove_pure. done. +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. + apply hoare_rec. simpl. + apply hoare_exist_pre. intros l. + apply hoare_exist_pre. intros w. + apply hoare_pure_pre_sep_l. intros ->. + eapply hoare_pure_step. + { apply pure_step_match_injr. } + apply hoare_let. simpl. + eapply hoare_bind with (K := [SndCtx]). + { apply hoare_frame. apply hoare_load. } + intros v. simpl. rewrite -ent_sep_assoc. apply hoare_pure_pre_sep_l. intros ->. + eapply hoare_pure_step. { apply pure_step_snd. } + eapply hoare_value_con. + rewrite ent_sep_comm. + apply ent_sep_weaken. +Qed. + + +Lemma len_ll_correct v xs : + {{ is_ll xs v }} len_ll v {{ w, ⌜w = #(length xs)⌝ ∗ is_ll xs v }}. +Proof. + induction xs as [ | x xs IH] in v |-*. + - simpl. eapply hoare_pure_pre. intros ->. + apply hoare_rec. simpl. + eapply hoare_pure_step. { apply pure_step_match_injl. } + apply hoare_let. simpl. apply hoare_value_con. + etrans; first apply ent_sep_true. + apply ent_sep_split; by apply ent_prove_pure. + - simpl. apply hoare_exist_pre. intros l. + apply hoare_exist_pre. intros w. apply hoare_pure_pre_sep_l. intros ->. + + apply hoare_rec. simpl. fold len_ll. + eapply hoare_pure_step. {apply pure_step_match_injr. } + apply hoare_let. simpl. + eapply hoare_bind with (K := [SndCtx; AppRCtx _; BinOpRCtx _ _]). + { apply hoare_frame. apply hoare_load. } + intros v. simpl. + rewrite -ent_sep_assoc. apply hoare_pure_pre_sep_l. intros ->. + eapply hoare_bind with (K := [AppRCtx _; BinOpRCtx _ _]). + { eapply hoare_pure_step; first apply pure_step_snd. apply hoare_value'. } + intros v. simpl. rewrite ent_sep_comm. apply hoare_pure_pre_sep_l. intros ->. + + eapply hoare_bind with (K := [BinOpRCtx _ _]). + { rewrite ent_sep_comm. apply hoare_frame. apply IH. } + intros v. simpl. rewrite -ent_sep_assoc. apply hoare_pure_pre_sep_l. intros ->. + + eapply hoare_pure_step. { apply pure_step_add. } + eapply hoare_value_con. + + etrans; first apply ent_sep_true. + apply ent_sep_split. + { apply ent_prove_pure. f_equiv. f_equiv. lia. } + eapply ent_exist_intro. + eapply ent_exist_intro. + etrans; first apply ent_sep_true. + apply ent_sep_split. { by apply ent_prove_pure. } + rewrite ent_sep_comm. apply ent_sep_split; done. +Qed. + +(** Exercise: State and prove a strengthened specification for [tail]. *) + +Lemma tail_ll_strengthened v x xs : + {{ is_ll (x :: xs) v }} tail_ll v {{ w, (∃ l : loc, ⌜v = SOMEV #l⌝ ∗ l ↦ (x, w)) ∗ is_ll xs w }}. +Proof. + unfold tail_ll. + apply hoare_rec. simpl. + apply hoare_exist_pre. intros l. + apply hoare_exist_pre. intros w. + apply hoare_pure_pre_sep_l. intros ->. + eapply hoare_pure_step. + { apply pure_step_match_injr. } + apply hoare_let. simpl. + eapply hoare_bind with (K := [SndCtx]). + { apply hoare_frame. apply hoare_load. } + intros v. simpl. rewrite -ent_sep_assoc. apply hoare_pure_pre_sep_l. intros ->. + eapply hoare_pure_step. { apply pure_step_snd. } + eapply hoare_value_con. + apply ent_sep_split; last done. + eapply ent_exist_intro. etrans; first apply ent_sep_true. + apply ent_sep_split; last done. + by apply ent_prove_pure. +Qed. From 04f1502ff52ed0e074f21190e41b2351e5c1af6d Mon Sep 17 00:00:00 2001 From: Benjamin Peters Date: Thu, 4 Jan 2024 17:10:11 +0100 Subject: [PATCH 2/2] 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. + +