Commit 7c3c983f authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'ralf/auto-ex' into 'master'

update to more automatic solution syntax

See merge request tutorial-popl18!5
parents d00179c4 35826abd
Pipeline #33370 passed with stage
in 20 minutes and 48 seconds
......@@ -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.
```
......
......@@ -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
......
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
}
......
......@@ -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.
......@@ -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.
......@@ -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.
......@@ -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.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment