upd template

_CoqProject

@@ -100,6 +100,9 @@ theories/axiomatic/hoare_lib.v
 theories/axiomatic/hoare.v
 theories/axiomatic/ipm.v
 theories/axiomatic/later_löb.v
+theories/axiomatic/ipm_sol.v
+theories/axiomatic/hoare_sol.v
+
 
 
 

theories/axiomatic/hoare_lib.v

@@ -679,13 +679,13 @@ Module hoare.
   Qed.
 
   Lemma ent_later_wp_load l v Φ :
-    ▷ l ↦ v ∗ ▷ (l ↦ v -∗ Φ v) ⊢ WP ! #l {{ Φ }}.
+    l ↦ v ∗ ▷ (l ↦ v -∗ Φ v) ⊢ WP ! #l {{ Φ }}.
   Proof.
     iIntros "[Hl Hp]". wp_load. iApply wp_value. by iApply "Hp".
   Qed.
 
   Lemma ent_later_wp_store l v w Φ :
-    ▷ l ↦ v ∗ ▷ (l ↦ w -∗ Φ #()) ⊢ WP #l <- w {{ Φ }}.
+    l ↦ v ∗ ▷ (l ↦ w -∗ Φ #()) ⊢ WP #l <- w {{ Φ }}.
   Proof.
     iIntros "[Hl Hp]". wp_store. iApply wp_value. by iApply "Hp".
   Qed.

theories/axiomatic/hoare_sol.v

 From iris.prelude Require Import options.
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import lang notation.
-From semantics.axiomatic_semantics Require Export hoare_lib.
+From semantics.axiomatic Require Export hoare_lib.
 
 Import hoare.
 Implicit Types

theories/axiomatic/later_löb.v

@@ -104,7 +104,7 @@ Proof.
 
   Restart.
   iIntros "($ & $)".
-Abort.
+Qed.
 
 Lemma ipm_later_exists_commuting (Φ : nat → iProp) :
   ▷ (∃ n : nat, Φ n) -∗ ∃ n : nat, ▷ Φ n.
@@ -112,8 +112,8 @@ Proof.
   (* automatically commutes the later around the existential *)
   (* note: in general, this relies on the type that is existentially quantified over
     to be [Inhabited]. The IPM tactics will fail if an instance for that cannot be found. *)
-  iIntros "(%n & Hn)".
-Abort.
+  iIntros "(%n & Hn)". eauto with iFrame.
+Qed.
 
 Lemma ipm_later_or_commuting P Q :
   ▷ (P ∨ Q) -∗ ▷ P ∨ ▷ Q.
@@ -123,7 +123,7 @@ Proof.
 
   Restart.
   iIntros "[ $ | $ ]".
-Abort.
+Qed.
 
 Lemma ipm_later_next_1 P Q R `{!Persistent P} :
   ▷ P -∗ ▷ R -∗ ▷ Q.
@@ -138,11 +138,8 @@ Lemma ent_wp_rec v Φ (Ψ : val → val → iProp) e :
   (∀ v, (Φ v ∗ (∀ u, {{ Φ u }} (rec: "f" "x" := e) u {{ Ψ u }}) ⊢ WP subst "x" v (subst "f" (rec: "f" "x" := e) e) {{ Ψ v }})) →
   (Φ v ⊢ WP (rec: "f" "x" := e) v {{ Ψ v }}).
 Proof.
-  iIntros (Hs). iLöb as "IH" forall (v).
-  iIntros "Hv".
-  wp_pures. iApply Hs. iFrame "Hv".
-  iIntros (v') "!> Hv'".
-  by iApply "IH".
+  iIntros (Hs). iLöb as "IH" forall (v). iIntros "Hv".
+  wp_pures. iApply Hs. iFrame "Hv". eauto.
 Qed.
 
 Section Z.
@@ -199,7 +196,7 @@ Lemma infinite_exec_Omega :
   ⊢ infinite_exec Omega.
 Proof.
   iLöb as "IH".
-  rewrite {2}infinite_exec_unfold /infinite_exec_pre /=.
+  rewrite {2} infinite_exec_unfold /infinite_exec_pre /=.
   iExists Omega. iSplitR; last done.
   iPureIntro. apply pure_step_beta.
 Qed.
@@ -245,7 +242,7 @@ Proof.
   (* FIXME: exercise *)
 Admitted.
 
-(** * Impredicate invariants *)
+(** * Impredicative invariants *)
 Import impred_invariants.
 (* [ent_inv_pers] and [ent_inv_alloc] hold unchanged *)
 (* The opening rules that support impredicative invariants put a later ▷ around the contents [F]. *)