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.