Commit d7107cb8 authored by Ralf Jung's avatar Ralf Jung
Browse files

adjust solutions file syntax to be easier to use

parent b2b410d9
......@@ -111,12 +111,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.
```
......
......@@ -2,12 +2,15 @@ BEGIN {
in_solution = 0;
}
{ # on every line of the input
if (match($0, /^( *)\(\* *BEGIN SOLUTION *\*\)$/, groups)) {
if (match($0, /^( *)\(\* *SOLUTION *\*\) *Proof.$/, groups)) {
print groups[1] "Proof."
in_solution = 1
} else if (match($0, /^( *)\(\* *END SOLUTION *\*\)$/, groups)) {
} else if (in_solution == 1 && match($0, /^( *)Qed.$/, groups)) {
print groups[1] " (* exercise *)"
print groups[1] "Admitted."
in_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)) {
......
......@@ -58,35 +58,28 @@ Section compatibility.
iDestruct 1 as (w1 w2 ->) "[??]". by wp_pures.
Qed.
Lemma Snd_sem_typed Γ e A1 A2 : Γ e : A1 * A2 - Γ Snd e : A2.
Proof.
(* BEGIN SOLUTION *)
(* SOLUTION *) Proof.
iIntros "#H" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H [//])"); iIntros (w).
iDestruct 1 as (w1 w2 ->) "[??]". by wp_pures.
Qed.
(* END SOLUTION *)
Lemma InjL_sem_typed Γ e A1 A2 : Γ e : A1 - Γ InjL e : A1 + A2.
Proof.
(* BEGIN SOLUTION *)
(* SOLUTION *) Proof.
iIntros "#H" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H [//])"); iIntros (w) "#HA".
wp_pures. iLeft. iExists w. auto.
Qed.
(* END SOLUTION *)
Lemma InjR_sem_typed Γ e A1 A2 : Γ e : A2 - Γ InjR e : A1 + A2.
Proof.
(* BEGIN SOLUTION *)
(* SOLUTION *) Proof.
iIntros "#H" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H [//])"); iIntros (w) "#HA".
wp_pures. iRight. iExists w. auto.
Qed.
(* END SOLUTION *)
Lemma Case_sem_typed Γ e e1 e2 A1 A2 B :
Γ e : A1 + A2 - Γ e1 : (A1 B) - Γ e2 : (A2 B) -
Γ Case e e1 e2 : B.
Proof.
(* BEGIN SOLUTION *)
(* SOLUTION *) Proof.
iIntros "#H #H1 #H2" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H [//])"); iIntros (w) "#[HA|HA]".
- iDestruct "HA" as (w1 ->) "HA". wp_pures.
......@@ -94,7 +87,6 @@ Section compatibility.
- iDestruct "HA" as (w2 ->) "HA". wp_pures.
wp_apply (wp_wand with "(H2 [//])"); iIntros (v) "#HAB". by iApply "HAB".
Qed.
(* END SOLUTION *)
(** * Functions *)
Lemma Rec_sem_typed Γ f x e A1 A2 :
......@@ -128,18 +120,15 @@ Section compatibility.
Qed.
Lemma Pack_sem_typed Γ e C A : Γ e : C A - Γ (pack: e) : A, C A.
Proof.
(* BEGIN SOLUTION *)
(* SOLUTION *) Proof.
iIntros "#H" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H [//])"); iIntros (w) "#HB".
wp_lam. by iExists A.
Qed.
(* END SOLUTION *)
Lemma Unpack_sem_typed Γ x e1 e2 C B :
(Γ e1 : A, C A) - ( A, binder_insert x (C A) Γ e2 : B) -
Γ (unpack: x := e1 in e2) : B.
Proof.
(* BEGIN SOLUTION *)
(* SOLUTION *) Proof.
iIntros "#H1 #H2" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H1 [//])"); iIntros (v); iDestruct 1 as (A) "#HC".
rewrite /exist_unpack; wp_pures. rewrite -subst_map_binder_insert.
......@@ -147,7 +136,6 @@ Section compatibility.
{ by iApply env_sem_typed_insert. }
auto.
Qed.
(* END SOLUTION *)
(** ** Heap operations *)
Lemma Alloc_sem_typed Γ e A : Γ e : A - Γ ref e : ref A.
......@@ -168,31 +156,26 @@ Section compatibility.
Qed.
Lemma Store_sem_typed Γ e1 e2 A :
Γ e1 : ref A - Γ e2 : A - Γ (e1 <- e2) : ().
Proof.
(* BEGIN SOLUTION *)
(* SOLUTION *) Proof.
iIntros "#H1 #H2" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H2 [//])"); iIntros (w2) "#HA".
wp_apply (wp_wand with "(H1 [//])"); iIntros (w1); iDestruct 1 as (l ->) "#?".
iInv (tyN.@l) as (v) "[>Hl _]". wp_store. eauto 10.
Qed.
(* END SOLUTION *)
Lemma FAA_sem_typed Γ e1 e2 :
Γ e1 : ref sem_ty_int - Γ e2 : sem_ty_int - Γ FAA e1 e2 : sem_ty_int.
Proof.
(* BEGIN SOLUTION *)
(* SOLUTION *) Proof.
iIntros "#H1 #H2" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H2 [//])"); iIntros (w2); iDestruct 1 as (n) "->".
wp_apply (wp_wand with "(H1 [//])"); iIntros (w1); iDestruct 1 as (l ->) "#?".
iInv (tyN.@l) as (v) "[>Hl Hv]"; iDestruct "Hv" as (n') "> ->".
wp_faa. iModIntro. eauto 10.
Qed.
(* END SOLUTION *)
Lemma CmpXchg_sem_typed Γ A e1 e2 e3 :
SemTyUnboxed A
Γ e1 : ref A - Γ e2 : A - Γ e3 : A -
Γ CmpXchg e1 e2 e3 : A * sem_ty_bool.
Proof.
(* BEGIN SOLUTION *)
(* SOLUTION *) Proof.
intros. iIntros "#H1 #H2 #H3" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H3 [//])"); iIntros (w3) "HA3".
wp_apply (wp_wand with "(H2 [//])"); iIntros (w2) "HA2".
......@@ -201,7 +184,6 @@ Section compatibility.
iInv (tyN.@l) as (v) "[>Hl #Hv]". wp_cmpxchg as ?|?; iModIntro;
(iSplitL; [by eauto 12 with iFrame | iExists _, _; eauto]).
Qed.
(* END SOLUTION *)
(** ** Operators *)
Lemma UnOp_sem_typed Γ e op A B :
......@@ -213,34 +195,28 @@ Section compatibility.
Qed.
Lemma BinOp_sem_typed Γ e1 e2 op A1 A2 B :
SemTyBinOp op A1 A2 B Γ e1 : A1 - Γ e2 : A2 - Γ BinOp op e1 e2 : B.
Proof.
(* BEGIN SOLUTION *)
(* SOLUTION *) Proof.
intros. iIntros "#H1 #H2" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H2 [//])"); iIntros (v2) "#HA2".
wp_apply (wp_wand with "(H1 [//])"); iIntros (v1) "#HA1".
iDestruct (sem_ty_bin_op with "HA1 HA2") as (w ?) "#HB". by wp_binop.
Qed.
(* END SOLUTION *)
Lemma If_sem_typed Γ e e1 e2 B :
Γ e : sem_ty_bool - Γ e1 : B - Γ e2 : B -
Γ (if: e then e1 else e2) : B.
Proof.
(* BEGIN SOLUTION *)
(* SOLUTION *) Proof.
iIntros "#H #H1 #H2" (vs) "!# #HΓ /=".
iSpecialize ("H1" with "HΓ"). iSpecialize ("H2" with "HΓ").
wp_apply (wp_wand with "(H [//])"); iIntros (w). iDestruct 1 as ([]) "->"; by wp_if.
Qed.
(* END SOLUTION *)
(** ** Fork *)
Lemma Fork_sem_typed Γ e : Γ e : () - Γ Fork e : ().
Proof.
(* BEGIN SOLUTION *)
(* SOLUTION *) Proof.
iIntros "#H" (vs) "!# #HΓ /=".
wp_apply wp_fork; last done. by iApply (wp_wand with "(H [//])").
Qed.
(* END SOLUTION *)
(** * Compatibility rules for value typing *)
(** ** Base types *)
......@@ -249,11 +225,9 @@ Section compatibility.
Lemma BoolV_sem_typed (b : bool) : #b : sem_ty_bool.
Proof. by iExists b. Qed.
Lemma IntV_sem_typed (n : Z) : #n : sem_ty_int.
Proof.
(* BEGIN SOLUTION *)
(* SOLUTION *) Proof.
by iExists n.
Qed.
(* END SOLUTION *)
(** ** Products and sums *)
Lemma PairV_sem_typed v1 v2 τ1 τ2 :
......
......@@ -233,11 +233,9 @@ You should prove this lemma.
Hint: [wp_pures] also executes the [+] operator. Carefully check how it affects
the embedded [#] and convince yourself why that makes sense. *)
Proof.
(* BEGIN SOLUTION *)
(* SOLUTION *) Proof.
iIntros. rewrite /swap_and_add. do 2 wp_load. do 2 wp_store. by iFrame.
Qed.
(* END SOLUTION *)
(** ** Reasoning about higher-order functions *)
(** For the next example, let us consider the higher-order function [twice].
......@@ -340,8 +338,7 @@ Lemma wp_add_two_ref `{!heapG Σ} l (x : Z) :
about addition on [Z] (or the [replace] or [rewrite (_ : x = y)] tactic with
[lia]) to turn [2 + x] into [1 + (1 + x)]. Tactics like [replace] and [rewrite]
work operate both on the MoSeL proof goal and the MoSeL proof context. *)
Proof.
(* BEGIN SOLUTION *)
(* SOLUTION *) Proof.
iIntros "Hl".
rewrite /add_two_ref. wp_pures.
iApply wp_twice.
......@@ -351,7 +348,6 @@ Proof.
iFrame.
auto.
Qed.
(* END SOLUTION *)
(** ** Reasoning about higher-order state *)
(** To see how Iris can be used to reason about higher-order state---that is,
......@@ -422,8 +418,7 @@ Definition add_two_fancy : val := λ: "x",
Lemma wp_add_two_fancy `{!heapG Σ} (x : Z) :
WP add_two_fancy #x {{ w, w = #(2 + x) }}.
Proof.
(* BEGIN SOLUTION *)
(* SOLUTION *) Proof.
rewrite /add_two_fancy. wp_pures.
wp_alloc lf as "Hlf".
wp_alloc lx as "Hlx".
......@@ -435,7 +430,6 @@ Proof.
wp_load.
auto with f_equal lia.
Qed.
(* END SOLUTION *)
(** * Reasoning about "unsafe" programs *)
(** Since HeapLang is an untyped language, we can write down arbitrary
......@@ -466,12 +460,10 @@ Definition unsafe_ref : val := λ: <>,
Lemma wp_unsafe_ref `{!heapG Σ} :
WP unsafe_ref #() {{ v, v = #true }}.
Proof.
(* BEGIN SOLUTION *)
(* SOLUTION *) Proof.
rewrite /unsafe_ref. wp_pures.
wp_alloc l.
wp_store.
wp_load.
auto.
Qed.
(* END SOLUTION *)
......@@ -27,8 +27,7 @@ Section parametricity.
( `{!heapG Σ}, e : A, A)
rtc erased_step ([e <_>]%E, σ) (of_val w :: es, σ')
False.
Proof.
(* BEGIN SOLUTION *)
(* SOLUTION *) Proof.
intros He.
change False with ((λ _, False) w).
apply sem_gen_type_safety with (φ := λ _, False)=> ?.
......@@ -41,14 +40,12 @@ Section parametricity.
iIntros (u) "#Hu".
iApply ("Hu" $! T).
Qed.
(* END SOLUTION *)
(** * Exercise (boolean_param, moderate) *)
Lemma boolean_param `{!heapPreG Σ} e (v1 v2 : val) σ w es σ' :
( `{!heapG Σ}, e : A, A A A)
rtc erased_step ([e <_> v1 v2]%E, σ) (of_val w :: es, σ') w = v1 w = v2.
Proof.
(* BEGIN SOLUTION *)
(* SOLUTION *) Proof.
intros He.
apply sem_gen_type_safety with (φ := λ w, w = v1 w = v2)=> ?.
pose (T := SemTy (λ w, w = v1 w = v2)%I : sem_ty Σ).
......@@ -65,15 +62,13 @@ Section parametricity.
iIntros (w'') "#Hw''".
iApply ("Hw''" $! v2). by iRight.
Qed.
(* END SOLUTION *)
(** * Exercise (nat_param, hard) *)
Lemma nat_param `{!heapPreG Σ} e σ w es σ' :
( `{!heapG Σ}, e : A, (A A) A A)
rtc erased_step ([e <_> (λ: "n", "n" + #1)%V #0]%E, σ)
(of_val w :: es, σ') n : nat, w = #n.
Proof.
(* BEGIN SOLUTION *)
(* SOLUTION *) Proof.
intros He.
apply sem_gen_type_safety with (φ := λ w, n : nat, w = #n)=> ?.
set (T := SemTy (λ w, n : nat, w = #n)%I : sem_ty Σ).
......@@ -94,7 +89,6 @@ Section parametricity.
iApply ("Hw''" $! #0).
by iExists 0%nat.
Qed.
(* END SOLUTION *)
(** * Exercise (strong_nat_param, hard) *)
Lemma strong_nat_param `{!heapPreG Σ} e σ w es σ' (vf vz : val) φ :
......@@ -104,8 +98,7 @@ Section parametricity.
( Φ vz)
( w, Φ w - ⌜φ w))
rtc erased_step ([e <_> vf vz]%E, σ) (of_val w :: es, σ') φ w.
Proof.
(* BEGIN SOLUTION *)
(* SOLUTION *) Proof.
intros He.
apply sem_gen_type_safety with (φ0 := φ)=> ?.
set (T := SemTy (λ w, φ w )%I : sem_ty Σ).
......@@ -126,5 +119,4 @@ Section parametricity.
{ iApply "Hw''". iApply Hvz. }
iIntros (v). by iApply Hφ.
Qed.
(* END SOLUTION *)
End parametricity.
......@@ -44,12 +44,10 @@ Lemma wp_swap_poly `{!heapG Σ} l1 l2 v1 v2 :
l1 v1 -
l2 v2 -
WP swap_poly <_> #l1 #l2 {{ v, v = #() l1 v2 l2 v1 }}.
Proof.
(* BEGIN SOLUTION *)
(* SOLUTION *) Proof.
iIntros "Hl1 Hl2".
rewrite /swap_poly.
do 2 wp_load.
do 2 wp_store.
by iFrame.
Qed.
(* END SOLUTION *)
......@@ -267,68 +267,57 @@ of them for both the expression construct and their value counterpart. *)
Lemma Lam_typed Γ x e τ1 τ2 :
binder_insert x τ1 Γ e : τ2
Γ (λ: x, e) : TArr τ1 τ2.
Proof.
(* BEGIN SOLUTION *)
(* SOLUTION *) Proof.
intros He.
apply Rec_typed.
simpl.
done.
Qed.
(* END SOLUTION *)
Lemma LamV_typed x e τ1 τ2 :
binder_insert x τ1 e : τ2
(λ: x, e) : TArr τ1 τ2.
Proof.
(* BEGIN SOLUTION *)
(* SOLUTION *) Proof.
intros He.
apply RecV_typed.
simpl.
done.
Qed.
(* END SOLUTION *)
Lemma Let_typed Γ x e1 e2 τ1 τ2 :
Γ e1 : τ1
binder_insert x τ1 Γ e2 : τ2
Γ (let: x := e1 in e2) : τ2.
Proof.
(* BEGIN SOLUTION *)
(* SOLUTION *) Proof.
intros He1 He2.
apply App_typed with τ1.
- by apply Lam_typed.
- done.
Qed.
(* END SOLUTION *)
Lemma Seq_typed Γ e1 e2 τ1 τ2 :
Γ e1 : τ1
Γ e2 : τ2
Γ (e1;; e2) : τ2.
Proof.
(* BEGIN SOLUTION *)
(* SOLUTION *) Proof.
intros He1 He2.
by apply Let_typed with τ1.
Qed.
(* END SOLUTION *)
Lemma Skip_typed Γ :
Γ Skip : ().
Proof.
(* BEGIN SOLUTION *)
(* SOLUTION *) Proof.
apply App_typed with ()%ty.
- apply Val_typed, RecV_typed. apply Val_typed, UnitV_typed.
- apply Val_typed, UnitV_typed.
Qed.
(* END SOLUTION *)
(** * Typing of concrete programs *)
(** ** Exercise (swap_typed, easy) *)
(** Prove that the non-polymorphic swap function [swap] can be given the type
[ref τ → ref τ → ()] for any [τ]. *)
Lemma swap_typed τ : swap : (ref τ ref τ ()).
Proof.
(* BEGIN SOLUTION *)
(* SOLUTION *) Proof.
rewrite /swap.
apply LamV_typed.
apply Lam_typed.
......@@ -342,14 +331,12 @@ Proof.
- by apply Var_typed.
- by apply Var_typed.
Qed.
(* END SOLUTION *)
(** ** Exercise (swap_poly_typed, easy) *)
(** Prove that [swap_poly] can be typed using the polymorphic type
[∀ X, ref X → ref X → ())], i.e. [∀: ref #0 → ref #0 → ())] in De Bruijn style. *)
Lemma swap_poly_typed : swap_poly : (∀: ref #0 ref #0 ()).
Proof.
(* BEGIN SOLUTION *)
(* SOLUTION *) Proof.
rewrite /swap_poly.
apply TLamV_typed.
do 2 apply Lam_typed.
......@@ -363,14 +350,12 @@ Proof.
- by apply Var_typed.
- by apply Var_typed.
Qed.
(* END SOLUTION *)
(** ** Exercise (not_typed, easy) *)
(** Prove that the programs [unsafe_pure] and [unsafe_ref] from [language.v]
cannot be typed using the syntactic type system. *)
Lemma unsafe_pure_not_typed τ : ¬ ( unsafe_pure : τ).
Proof.
(* BEGIN SOLUTION *)
(* SOLUTION *) Proof.
intros Htyped.
repeat
match goal with
......@@ -378,11 +363,9 @@ Proof.
| H : _ : _ |- _ => inversion H; simplify_eq/=; clear H
end.
Qed.
(* END SOLUTION *)
Lemma unsafe_ref_not_typed τ : ¬ ( unsafe_ref : τ).
Proof.
(* BEGIN SOLUTION *)
(* SOLUTION *) Proof.
intros Htyped.
repeat
match goal with
......@@ -390,4 +373,3 @@ Proof.
| H : _ : _ |- _ => inversion H; simplify_eq/=; clear H
end.
Qed.
(* END SOLUTION *)
Markdown is supported
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