pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-09-19 19:57:13 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Revising for Monday's lecture

Browse source
This commit is contained in:
Adam Chlipala 2022-02-26 15:58:03 -05:00
parent e3f0ada30e
commit 52e47df705
2 changed files with 21 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

31
OperationalSemantics.v
View file

@ -463,7 +463,7 @@ Module Simple.
(* Bonus material: here's how to make these proofs much more automatic. We (* Bonus material: here's how to make these proofs much more automatic. We
* won't explain the features being used here. *) * won't explain the features being used here. *)
Hint Constructors trc step eval : core. Local Hint Constructors trc step eval : core.
Lemma step_star_Seq_snazzy : forall v c1 c2 v' c1', Lemma step_star_Seq_snazzy : forall v c1 c2 v' c1',
step^* (v, c1) (v', c1') step^* (v, c1) (v', c1')
@ -473,7 +473,7 @@ Module Simple.
cases y; eauto. cases y; eauto.
Qed. Qed.
Hint Resolve step_star_Seq_snazzy : core. Local Hint Resolve step_star_Seq_snazzy : core.
Theorem big_small_snazzy : forall v c v', eval v c v' Theorem big_small_snazzy : forall v c v', eval v c v'
-> step^* (v, c) (v', Skip). -> step^* (v, c) (v', Skip).
@ -491,7 +491,7 @@ Module Simple.
end; eauto. end; eauto.
Qed. Qed.
Hint Resolve small_big''_snazzy : core. Local Hint Resolve small_big''_snazzy : core.
Lemma small_big'_snazzy : forall v c v' c', step^* (v, c) (v', c') Lemma small_big'_snazzy : forall v c v' c', step^* (v, c) (v', c')
-> forall v'', eval v' c' v'' -> forall v'', eval v' c' v''
@ -501,7 +501,7 @@ Module Simple.
cases y; eauto. cases y; eauto.
Qed. Qed.
Hint Resolve small_big'_snazzy : core. Local Hint Resolve small_big'_snazzy : core.
Theorem small_big_snazzy : forall v c v', step^* (v, c) (v', Skip) Theorem small_big_snazzy : forall v c v', step^* (v, c) (v', Skip)
-> eval v c v'. -> eval v c v'.
@ -688,8 +688,8 @@ Module Simple.
Qed. Qed.
(* That manual proof was quite a pain. Here's a bonus automated proof. *) (* That manual proof was quite a pain. Here's a bonus automated proof. *)
Hint Constructors isEven : core. Local Hint Constructors isEven : core.
Hint Resolve isEven_minus2 isEven_plus : core. Local Hint Resolve isEven_minus2 isEven_plus : core.
Lemma manually_proved_invariant'_snazzy : forall n, Lemma manually_proved_invariant'_snazzy : forall n,
isEven n isEven n
@ -866,7 +866,7 @@ Module Simple.
(* Bonus material: here's how to make these proofs much more automatic. We (* Bonus material: here's how to make these proofs much more automatic. We
* won't explain the features being used here. *) * won't explain the features being used here. *)
Hint Constructors plug step0 cstep : core. Local Hint Constructors plug step0 cstep : core.
Theorem step_cstep_snazzy : forall v c v' c', Theorem step_cstep_snazzy : forall v c v' c',
step (v, c) (v', c') step (v, c) (v', c')
@ -877,7 +877,7 @@ Module Simple.
end; eauto. end; eauto.
Qed. Qed.
Hint Resolve step_cstep_snazzy : core. Local Hint Resolve step_cstep_snazzy : core.
Lemma step0_step_snazzy : forall v c v' c', Lemma step0_step_snazzy : forall v c v' c',
step0 (v, c) (v', c') step0 (v, c) (v', c')
@ -886,7 +886,7 @@ Module Simple.
invert 1; eauto. invert 1; eauto.
Qed. Qed.
Hint Resolve step0_step_snazzy : core. Local Hint Resolve step0_step_snazzy : core.
Lemma cstep_step'_snazzy : forall C c0 c, Lemma cstep_step'_snazzy : forall C c0 c,
plug C c0 c plug C c0 c
@ -899,7 +899,7 @@ Module Simple.
end; eauto. end; eauto.
Qed. Qed.
Hint Resolve cstep_step'_snazzy : core. Local Hint Resolve cstep_step'_snazzy : core.
Theorem cstep_step_snazzy : forall v c v' c', Theorem cstep_step_snazzy : forall v c v' c',
cstep (v, c) (v', c') cstep (v, c) (v', c')
@ -962,6 +962,7 @@ Module Simple.
Qed. Qed.
End Simple. End Simple.
(** * Example of how easy it is to add concurrency to a contextual semantics *) (** * Example of how easy it is to add concurrency to a contextual semantics *)
Module Concurrent. Module Concurrent.
@ -1044,7 +1045,7 @@ Module Concurrent.
|| ("b" <- "n";; || ("b" <- "n";;
"n" <- "b" + 1). "n" <- "b" + 1).
Hint Constructors plug step0 cstep : core. Local Hint Constructors plug step0 cstep : core.
(* The naive "expected" answer is attainable. *) (* The naive "expected" answer is attainable. *)
Theorem correctAnswer : forall n, exists v, cstep^* ($0 $+ ("n", n), prog) (v, Skip) Theorem correctAnswer : forall n, exists v, cstep^* ($0 $+ ("n", n), prog) (v, Skip)
@ -1149,7 +1150,7 @@ Module Concurrent.
step (v, c2) (v', c2') step (v, c2) (v', c2')
-> step (v, Parallel c1 c2) (v', Parallel c1 c2'). -> step (v, Parallel c1 c2) (v', Parallel c1 c2').
Hint Constructors step : core. Local Hint Constructors step : core.
(* Now, an automated proof of equivalence. Actually, it's *exactly* the same (* Now, an automated proof of equivalence. Actually, it's *exactly* the same
* proof we used for the old feature set! *) * proof we used for the old feature set! *)
@ -1163,7 +1164,7 @@ Module Concurrent.
end; eauto. end; eauto.
Qed. Qed.
Hint Resolve step_cstep : core. Local Hint Resolve step_cstep : core.
Lemma step0_step : forall v c v' c', Lemma step0_step : forall v c v' c',
step0 (v, c) (v', c') step0 (v, c) (v', c')
@ -1172,7 +1173,7 @@ Module Concurrent.
invert 1; eauto. invert 1; eauto.
Qed. Qed.
Hint Resolve step0_step : core. Local Hint Resolve step0_step : core.
Lemma cstep_step' : forall C c0 c, Lemma cstep_step' : forall C c0 c,
plug C c0 c plug C c0 c
@ -1185,7 +1186,7 @@ Module Concurrent.
end; eauto. end; eauto.
Qed. Qed.
Hint Resolve cstep_step' : core. Local Hint Resolve cstep_step' : core.
Theorem cstep_step : forall v c v' c', Theorem cstep_step : forall v c v' c',
cstep (v, c) (v', c') cstep (v, c) (v', c')

10
OperationalSemantics_template.v
View file

@ -360,7 +360,7 @@ Qed.
(* Automated proofs used here, if only to save time in class. (* Automated proofs used here, if only to save time in class.
* See book code for more manual proofs, too. *) * See book code for more manual proofs, too. *)
Hint Constructors trc step eval : core. Local Hint Constructors trc step eval : core.
Theorem big_small : forall v c v', eval v c v' Theorem big_small : forall v c v', eval v c v'
-> step^* (v, c) (v', Skip). -> step^* (v, c) (v', Skip).
@ -430,8 +430,8 @@ Proof.
assumption. assumption.
Qed. Qed.
Hint Constructors isEven : core. Local Hint Constructors isEven : core.
Hint Resolve isEven_minus2 isEven_plus : core. Local Hint Resolve isEven_minus2 isEven_plus : core.
Definition my_loop := Definition my_loop :=
while "n" loop while "n" loop
@ -581,7 +581,7 @@ Inductive cstep : valuation * cmd -> valuation * cmd -> Prop :=
(* We can prove equivalence between the two formulations. *) (* We can prove equivalence between the two formulations. *)
Hint Constructors plug step0 cstep : core. Local Hint Constructors plug step0 cstep : core.
Theorem step_cstep : forall v c v' c', Theorem step_cstep : forall v c v' c',
step (v, c) (v', c') step (v, c) (v', c')
@ -710,7 +710,7 @@ Definition prog :=
|| ("b" <- "n";; || ("b" <- "n";;
"n" <- "b" + 1). "n" <- "b" + 1).
Hint Constructors plug step0 cstep : core. Local Hint Constructors plug step0 cstep : core.
(* The naive "expected" answer is attainable. *) (* The naive "expected" answer is attainable. *)
Theorem correctAnswer : forall n, exists v, cstep^* ($0 $+ ("n", n), prog) (v, Skip) Theorem correctAnswer : forall n, exists v, cstep^* ($0 $+ ("n", n), prog) (v, Skip)