From 35826abdbd70643c69eebb3b528c3836768022fc Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Fri, 28 Aug 2020 12:01:05 +0200 Subject: [PATCH] update to more automatic solution syntax --- README.md | 5 +++-- exercises/ex_03_spinlock.v | 3 ++- gen-exercises.awk | 16 ++++++++++------ solutions/ex_01_swap.v | 4 +--- solutions/ex_02_sumlist.v | 16 ++++------------ solutions/ex_03_spinlock.v | 14 +++++++------- solutions/ex_05_parallel_add_mul.v | 4 +--- 7 files changed, 28 insertions(+), 34 deletions(-) diff --git a/README.md b/README.md index 944f7c6..396b408 100644 --- a/README.md +++ b/README.md @@ -69,12 +69,13 @@ macOS). The syntax for the solution files is as follows: ``` -(* BEGIN SOLUTION *) +(* SOLUTION *) Proof. solution here. -(* END SOLUTION *) +Qed. ``` is replaced by ``` +Proof. (* exercise *) Admitted. ``` diff --git a/exercises/ex_03_spinlock.v b/exercises/ex_03_spinlock.v index 2d6a0ad..e724855 100644 --- a/exercises/ex_03_spinlock.v +++ b/exercises/ex_03_spinlock.v @@ -102,7 +102,8 @@ Section proof. - wp_cmpxchg_fail. iMod ("Hclose" with "[Hl]") as "_". { iNext. iExists true. iFrame. } iModIntro. wp_proj. - (* exercise *) + (* exercise *) admit. + - (* exercise *) admit. Admitted. (** *Exercise*: prove the spec of [acquire]. Since [acquire] is a recursive diff --git a/gen-exercises.awk b/gen-exercises.awk index 5abe3cb..895f1e9 100644 --- a/gen-exercises.awk +++ b/gen-exercises.awk @@ -1,18 +1,22 @@ BEGIN { - in_solution = 0; + in_solution = 0; # for the advanced solution syntax + in_auto_solution = 0; # for the simple solution syntax that recognizes `Qed.` } { # on every line of the input - if (match($0, /^( *)\(\* *BEGIN SOLUTION *\*\)$/, groups)) { - in_solution = 1 - } else if (match($0, /^( *)\(\* *END SOLUTION *\*\)$/, groups)) { + if (match($0, /^( *)\(\* *SOLUTION *\*\) *Proof.$/, groups)) { + print groups[1] "Proof." + in_auto_solution = 1 + } else if (in_auto_solution == 1 && match($0, /^( *)Qed.$/, groups)) { print groups[1] " (* exercise *)" print groups[1] "Admitted." - in_solution = 0 + in_auto_solution = 0 + } else if (match($0, /^( *)\(\* *BEGIN SOLUTION *\*\)$/, groups)) { + in_solution = 1 } else if (match($0, /^( *)\(\* *END SOLUTION BEGIN TEMPLATE *$/, groups)) { in_solution = 0 } else if (match($0, /^( *)END TEMPLATE *\*\)$/, groups)) { # Nothing to do, just do not print this line. - } else if (in_solution == 0) { + } else if (in_solution == 0 && in_auto_solution == 0) { gsub("From solutions Require", "From exercises Require") print } diff --git a/solutions/ex_01_swap.v b/solutions/ex_01_swap.v index a3e3e50..7675773 100644 --- a/solutions/ex_01_swap.v +++ b/solutions/ex_01_swap.v @@ -136,12 +136,10 @@ Lemma rotate_l_spec x y z v1 v2 v3 : {{{ x ↦ v1 ∗ y ↦ v2 ∗ z ↦ v3 }}} rotate_l #x #y #z {{{ RET #(); x ↦ v2 ∗ y ↦ v3 ∗ z ↦ v1 }}}. -Proof. -(* BEGIN SOLUTION *) +(* SOLUTION *) Proof. iIntros (Φ) "(Hx & Hy & Hz) Post". unfold rotate_l. wp_lam. do 2 wp_let. wp_apply (swap_spec with "[$Hx $Hy]"); iIntros "[Hx Hy]"; wp_seq. wp_apply (swap_spec with "[$Hy $Hz]"); iIntros "[Hy Hz]". iApply ("Post" with "[$]"). Qed. -(* END SOLUTION *) End proof. diff --git a/solutions/ex_02_sumlist.v b/solutions/ex_02_sumlist.v index 54d60e4..1a9d9e3 100644 --- a/solutions/ex_02_sumlist.v +++ b/solutions/ex_02_sumlist.v @@ -116,8 +116,7 @@ Lemma inc_list_spec_induction n l v : {{{ is_list l v }}} inc_list #n v {{{ RET #(); is_list (map (Z.add n) l) v }}}. -Proof. -(* BEGIN SOLUTION *) +(* SOLUTION *) Proof. iIntros (Φ) "Hl Post". iInduction l as [|x l] "IH" forall (v Φ); simpl. - iDestruct "Hl" as %->. @@ -134,15 +133,13 @@ Proof. iExists p. iSplitR; [done|]. iExists v. iSplitR "Hl"; [iApply "Hp"|iApply "Hl"]. Qed. -(* END SOLUTION *) (** *Exercise*: Now do the proof again using Löb induction. *) Lemma inc_list_spec_löb n l v : {{{ is_list l v }}} inc_list #n v {{{ RET #(); is_list (map (Z.add n) l) v }}}. -Proof. -(* BEGIN SOLUTION *) +(* SOLUTION *) Proof. iIntros (Φ) "Hl Post". iLöb as "IH" forall (l v Φ). destruct l as [|x l]; simpl; wp_rec; wp_let. - iDestruct "Hl" as %->. wp_match. by iApply "Post". @@ -151,7 +148,6 @@ Proof. wp_apply ("IH" with "Hl"). iIntros "Hl". iApply "Post". eauto with iFrame. Qed. -(* END SOLUTION *) (** *Exercise*: Do the proof of [sum_inc_list] by making use of the lemmas of [sum_list] and [inc_list] we just proved. Make use of [wp_apply]. *) @@ -159,13 +155,11 @@ Lemma sum_inc_list_spec n l v : {{{ is_list l v }}} sum_inc_list #n v {{{ RET #(sum_list_coq (map (Z.add n) l)); is_list (map (Z.add n) l) v }}}. -Proof. -(* BEGIN SOLUTION *) +(* SOLUTION *) Proof. iIntros (Φ) "Hl Post". wp_lam. wp_let. wp_apply (inc_list_spec_induction with "Hl"); iIntros "Hl /="; wp_seq. wp_apply (sum_list_spec_induction with "Hl"); auto. Qed. -(* END SOLUTION *) (** *Optional exercise*: Prove the following spec of [map_list] which makes use of a nested Texan triple, This spec is rather weak, as it requires [f] to be @@ -173,8 +167,7 @@ pure, if you like, you can try to make it more general. *) Lemma map_list_spec_induction (f : val) (f_coq : Z → Z) l v : (∀ n, {{{ True }}} f #n {{{ RET #(f_coq n); True }}}) -∗ {{{ is_list l v }}} map_list f v {{{ RET #(); is_list (map f_coq l) v }}}. -Proof. -(* BEGIN SOLUTION *) +(* SOLUTION *) Proof. iIntros "#Hf" (Φ) "!# Hl Post". iLöb as "IH" forall (l v Φ). destruct l as [|x l]; simpl; wp_rec; wp_let. - iDestruct "Hl" as %->. wp_match. by iApply "Post". @@ -185,5 +178,4 @@ Proof. wp_apply ("IH" with "Hl"). iIntros "Hl". iApply "Post". eauto with iFrame. Qed. -(* END SOLUTION *) End proof. diff --git a/solutions/ex_03_spinlock.v b/solutions/ex_03_spinlock.v index dcd4986..769a9a1 100644 --- a/solutions/ex_03_spinlock.v +++ b/solutions/ex_03_spinlock.v @@ -109,21 +109,23 @@ Section proof. { iNext. iExists true. iFrame. } iModIntro. wp_proj. by iApply ("HΦ" $! true with "HR"). Qed. - (* END SOLUTION *) + (* END SOLUTION BEGIN TEMPLATE + (* exercise *) admit. + - (* exercise *) admit. + Admitted. + END TEMPLATE *) (** *Exercise*: prove the spec of [acquire]. Since [acquire] is a recursive function, you should use the tactic [iLöb] for Löb induction. Use the tactic [wp_apply] to use [try_acquire_spec] when appropriate. *) Lemma acquire_spec lk R : {{{ is_lock lk R }}} acquire lk {{{ RET #(); R }}}. - Proof. - (* BEGIN SOLUTION *) + (* SOLUTION *) Proof. iIntros (Φ) "#Hl HΦ". iLöb as "IH". wp_rec. wp_apply (try_acquire_spec with "Hl"). iIntros ([]). - iIntros "HR". wp_if. by iApply "HΦ". - iIntros "_". wp_if. iApply ("IH" with "HΦ"). Qed. - (* END SOLUTION *) (** *Exercise*: prove the spec of [release]. At a certain point in this proof, you need to open the invariant. For this you can use: @@ -134,12 +136,10 @@ Section proof. invariant. *) Lemma release_spec lk R : {{{ is_lock lk R ∗ R }}} release lk {{{ RET #(); True }}}. - Proof. - (* BEGIN SOLUTION *) + (* SOLUTION *) Proof. iIntros (Φ) "(Hlock & HR) HΦ". iDestruct "Hlock" as (l ->) "#Hinv /=". wp_lam. iInv lockN as (b) "[Hl _]" "Hclose". wp_store. iApply "HΦ". iApply "Hclose". iNext. iExists false. iFrame. Qed. - (* END SOLUTION *) End proof. diff --git a/solutions/ex_05_parallel_add_mul.v b/solutions/ex_05_parallel_add_mul.v index cb28294..ff5c75a 100644 --- a/solutions/ex_05_parallel_add_mul.v +++ b/solutions/ex_05_parallel_add_mul.v @@ -73,8 +73,7 @@ Section proof. Lemma parallel_add_mul_spec : {{{ True }}} parallel_add_mul {{{ z, RET #z; ⌜ z = 2%Z ∨ z = 4%Z ⌝ }}}. - Proof. - (* BEGIN SOLUTION *) + (* SOLUTION *) Proof. iIntros (Φ) "_ Post". unfold parallel_add_mul. wp_alloc r as "Hr". wp_let. iMod (ghost_var_alloc false) as (γ1) "[Hγ1● Hγ1◯]". @@ -107,5 +106,4 @@ Section proof. iDestruct (ghost_var_agree with "Hγ2● Hγ2◯") as %->. auto. Qed. - (* END SOLUTION *) End proof. -- GitLab