diff --git a/_CoqProject b/_CoqProject
index e05bcb7..0d7cfdc 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -92,6 +92,8 @@ 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
+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/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.
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.
+
+