pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2025-02-26 03:22:13 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Revising OperationalSemantics

Browse source
This commit is contained in:
Adam Chlipala 2020-02-29 16:10:37 -05:00
parent 254e2aedc6
commit d6e8cebdc9
2 changed files with 1018 additions and 1097 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

417
OperationalSemantics.v
View file

@ -18,38 +18,16 @@ Inductive arith : Set :=
| Minus (e1 e2 : arith) | Minus (e1 e2 : arith)
| Times (e1 e2 : arith). | Times (e1 e2 : arith).
Inductive cmd :=
| Skip
| Assign (x : var) (e : arith)
| Sequence (c1 c2 : cmd)
| If (e : arith) (then_ else_ : cmd)
| While (e : arith) (body : cmd).
(* Important differences: we added [If] and switched [Repeat] to general
* [While]. *)
(* Here are some notations for the language, which again we won't really
* explain. *)
Coercion Const : nat >-> arith. Coercion Const : nat >-> arith.
Coercion Var : var >-> arith. Coercion Var : var >-> arith.
Infix "+" := Plus : arith_scope. Infix "+" := Plus : arith_scope.
Infix "-" := Minus : arith_scope. Infix "-" := Minus : arith_scope.
Infix "*" := Times : arith_scope. Infix "*" := Times : arith_scope.
Delimit Scope arith_scope with arith. Delimit Scope arith_scope with arith.
Notation "x <- e" := (Assign x e%arith) (at level 75).
Infix ";;" := Sequence (at level 76). (* This one changed slightly, to avoid parsing clashes. *)
Notation "'when' e 'then' then_ 'else' else_ 'done'" := (If e%arith then_ else_) (at level 75, e at level 0).
Notation "'while' e 'loop' body 'done'" := (While e%arith body) (at level 75).
(* Here's an adaptation of our factorial example from Chapter 3. *) Definition valuation := fmap var nat.
Example factorial :=
"output" <- 1;;
while "input" loop
"output" <- "output" * "input";;
"input" <- "input" - 1
done.
(* Recall our use of a recursive function to interpret expressions. *) (* Recall our use of a recursive function to interpret expressions. *)
Definition valuation := fmap var nat.
Fixpoint interp (e : arith) (v : valuation) : nat := Fixpoint interp (e : arith) (v : valuation) : nat :=
match e with match e with
| Const n => n | Const n => n
@ -63,41 +41,66 @@ Fixpoint interp (e : arith) (v : valuation) : nat :=
| Times e1 e2 => interp e1 v * interp e2 v | Times e1 e2 => interp e1 v * interp e2 v
end. end.
(* Our old trick of interpreters won't work for this new language, because of Module Simple.
Inductive cmd :=
| Skip
| Assign (x : var) (e : arith)
| Sequence (c1 c2 : cmd)
| If (e : arith) (then_ else_ : cmd)
| While (e : arith) (body : cmd).
(* Important differences: we added [If] and switched [Repeat] to general
* [While]. *)
(* Here are some notations for the language, which again we won't really
* explain. *)
Notation "x <- e" := (Assign x e%arith) (at level 75).
Infix ";;" := Sequence (at level 76). (* This one changed slightly, to avoid parsing clashes. *)
Notation "'when' e 'then' then_ 'else' else_ 'done'" := (If e%arith then_ else_) (at level 75, e at level 0).
Notation "'while' e 'loop' body 'done'" := (While e%arith body) (at level 75).
(* Here's an adaptation of our factorial example from Chapter 3. *)
Example factorial :=
"output" <- 1;;
while "input" loop
"output" <- "output" * "input";;
"input" <- "input" - 1
done.
(* Our old trick of interpreters won't work for this new language, because of
* the general "while" loops. No such interpreter could terminate for all * the general "while" loops. No such interpreter could terminate for all
* programs. Instead, we will use inductive predicates to explain program * programs. Instead, we will use inductive predicates to explain program
* meanings. First, let's apply the most intuitive method, called * meanings. First, let's apply the most intuitive method, called
* *big-step operational semantics*. *) * *big-step operational semantics*. *)
Inductive eval : valuation -> cmd -> valuation -> Prop := Inductive eval : valuation -> cmd -> valuation -> Prop :=
| EvalSkip : forall v, | EvalSkip : forall v,
eval v Skip v eval v Skip v
| EvalAssign : forall v x e, | EvalAssign : forall v x e,
eval v (Assign x e) (v $+ (x, interp e v)) eval v (Assign x e) (v $+ (x, interp e v))
| EvalSeq : forall v c1 v1 c2 v2, | EvalSeq : forall v c1 v1 c2 v2,
eval v c1 v1 eval v c1 v1
-> eval v1 c2 v2 -> eval v1 c2 v2
-> eval v (Sequence c1 c2) v2 -> eval v (Sequence c1 c2) v2
| EvalIfTrue : forall v e then_ else_ v', | EvalIfTrue : forall v e then_ else_ v',
interp e v <> 0 interp e v <> 0
-> eval v then_ v' -> eval v then_ v'
-> eval v (If e then_ else_) v' -> eval v (If e then_ else_) v'
| EvalIfFalse : forall v e then_ else_ v', | EvalIfFalse : forall v e then_ else_ v',
interp e v = 0 interp e v = 0
-> eval v else_ v' -> eval v else_ v'
-> eval v (If e then_ else_) v' -> eval v (If e then_ else_) v'
| EvalWhileTrue : forall v e body v' v'', | EvalWhileTrue : forall v e body v' v'',
interp e v <> 0 interp e v <> 0
-> eval v body v' -> eval v body v'
-> eval v' (While e body) v'' -> eval v' (While e body) v''
-> eval v (While e body) v'' -> eval v (While e body) v''
| EvalWhileFalse : forall v e body, | EvalWhileFalse : forall v e body,
interp e v = 0 interp e v = 0
-> eval v (While e body) v. -> eval v (While e body) v.
(* Let's run the factorial program on a few inputs. *) (* Let's run the factorial program on a few inputs. *)
Theorem factorial_2 : exists v, eval ($0 $+ ("input", 2)) factorial v Theorem factorial_2 : exists v, eval ($0 $+ ("input", 2)) factorial v
/\ v $? "output" = Some 2. /\ v $? "output" = Some 2.
Proof. Proof.
eexists; propositional. eexists; propositional.
(* [eexists]: to prove [exists x, P(x)], switch to proving [P(?y)], for a new (* [eexists]: to prove [exists x, P(x)], switch to proving [P(?y)], for a new
* existential variable [?y]. *) * existential variable [?y]. *)
@ -124,53 +127,53 @@ Proof.
simplify. simplify.
equality. equality.
Qed. Qed.
(* That was rather repetitive. It's easy to automate. *) (* That was rather repetitive. It's easy to automate. *)
Ltac eval1 := Ltac eval1 :=
apply EvalSkip || apply EvalAssign || eapply EvalSeq apply EvalSkip || apply EvalAssign || eapply EvalSeq
|| (apply EvalIfTrue; [ simplify; equality | ]) || (apply EvalIfTrue; [ simplify; equality | ])
|| (apply EvalIfFalse; [ simplify; equality | ]) || (apply EvalIfFalse; [ simplify; equality | ])
|| (eapply EvalWhileTrue; [ simplify; equality | | ]) || (eapply EvalWhileTrue; [ simplify; equality | | ])
|| (apply EvalWhileFalse; [ simplify; equality ]). || (apply EvalWhileFalse; [ simplify; equality ]).
Ltac evaluate := simplify; try equality; repeat eval1. Ltac evaluate := simplify; try equality; repeat eval1.
Theorem factorial_2_snazzy : exists v, eval ($0 $+ ("input", 2)) factorial v Theorem factorial_2_snazzy : exists v, eval ($0 $+ ("input", 2)) factorial v
/\ v $? "output" = Some 2. /\ v $? "output" = Some 2.
Proof. Proof.
eexists; propositional. eexists; propositional.
evaluate. evaluate.
evaluate. evaluate.
Qed. Qed.
Theorem factorial_3 : exists v, eval ($0 $+ ("input", 3)) factorial v Theorem factorial_3 : exists v, eval ($0 $+ ("input", 3)) factorial v
/\ v $? "output" = Some 6. /\ v $? "output" = Some 6.
Proof. Proof.
eexists; propositional. eexists; propositional.
evaluate. evaluate.
evaluate. evaluate.
Qed. Qed.
(* Instead of chugging through these relatively slow individual executions, (* Instead of chugging through these relatively slow individual executions,
* let's prove once and for all that [factorial] is correct. *) * let's prove once and for all that [factorial] is correct. *)
Fixpoint fact (n : nat) : nat := Fixpoint fact (n : nat) : nat :=
match n with match n with
| O => 1 | O => 1
| S n' => n * fact n' | S n' => n * fact n'
end. end.
Example factorial_loop := Example factorial_loop :=
while "input" loop while "input" loop
"output" <- "output" * "input";; "output" <- "output" * "input";;
"input" <- "input" - 1 "input" <- "input" - 1
done. done.
Lemma factorial_loop_correct : forall n v out, v $? "input" = Some n Lemma factorial_loop_correct : forall n v out, v $? "input" = Some n
-> v $? "output" = Some out -> v $? "output" = Some out
-> exists v', eval v factorial_loop v' -> exists v', eval v factorial_loop v'
/\ v' $? "output" = Some (fact n * out). /\ v' $? "output" = Some (fact n * out).
Proof. Proof.
induct n; simplify. induct n; simplify.
exists v; propositional. exists v; propositional.
@ -205,12 +208,12 @@ Proof.
rewrite H2. rewrite H2.
f_equal. f_equal.
ring. ring.
Qed. Qed.
Theorem factorial_correct : forall n v, v $? "input" = Some n Theorem factorial_correct : forall n v, v $? "input" = Some n
-> exists v', eval v factorial v' -> exists v', eval v factorial v'
/\ v' $? "output" = Some (fact n). /\ v' $? "output" = Some (fact n).
Proof. Proof.
simplify. simplify.
assert (exists v', eval (v $+ ("output", 1)) factorial_loop v' assert (exists v', eval (v $+ ("output", 1)) factorial_loop v'
/\ v' $? "output" = Some (fact n * 1)). /\ v' $? "output" = Some (fact n * 1)).
@ -226,42 +229,42 @@ Proof.
rewrite H1. rewrite H1.
f_equal. f_equal.
ring. ring.
Qed. Qed.
(** * Small-step semantics *) (** * Small-step semantics *)
(* Big-step semantics only tells us something about the behavior of terminating (* Big-step semantics only tells us something about the behavior of terminating
* programs. Our imperative language clearly supports nontermination, thanks to * programs. Our imperative language clearly supports nontermination, thanks to
* the inclusion of general "while" loops. A switch to *small-step* semantics * the inclusion of general "while" loops. A switch to *small-step* semantics
* lets us also explain what happens with nonterminating executions, and this * lets us also explain what happens with nonterminating executions, and this
* style will also come in handy for more advanced features like concurrency. *) * style will also come in handy for more advanced features like concurrency. *)
Inductive step : valuation * cmd -> valuation * cmd -> Prop := Inductive step : valuation * cmd -> valuation * cmd -> Prop :=
| StepAssign : forall v x e, | StepAssign : forall v x e,
step (v, Assign x e) (v $+ (x, interp e v), Skip) step (v, Assign x e) (v $+ (x, interp e v), Skip)
| StepSeq1 : forall v c1 c2 v' c1', | StepSeq1 : forall v c1 c2 v' c1',
step (v, c1) (v', c1') step (v, c1) (v', c1')
-> step (v, Sequence c1 c2) (v', Sequence c1' c2) -> step (v, Sequence c1 c2) (v', Sequence c1' c2)
| StepSeq2 : forall v c2, | StepSeq2 : forall v c2,
step (v, Sequence Skip c2) (v, c2) step (v, Sequence Skip c2) (v, c2)
| StepIfTrue : forall v e then_ else_, | StepIfTrue : forall v e then_ else_,
interp e v <> 0 interp e v <> 0
-> step (v, If e then_ else_) (v, then_) -> step (v, If e then_ else_) (v, then_)
| StepIfFalse : forall v e then_ else_, | StepIfFalse : forall v e then_ else_,
interp e v = 0 interp e v = 0
-> step (v, If e then_ else_) (v, else_) -> step (v, If e then_ else_) (v, else_)
| StepWhileTrue : forall v e body, | StepWhileTrue : forall v e body,
interp e v <> 0 interp e v <> 0
-> step (v, While e body) (v, Sequence body (While e body)) -> step (v, While e body) (v, Sequence body (While e body))
| StepWhileFalse : forall v e body, | StepWhileFalse : forall v e body,
interp e v = 0 interp e v = 0
-> step (v, While e body) (v, Skip). -> step (v, While e body) (v, Skip).
(* Here's a small-step factorial execution. *) (* Here's a small-step factorial execution. *)
Theorem factorial_2_small : exists v, step^* ($0 $+ ("input", 2), factorial) (v, Skip) Theorem factorial_2_small : exists v, step^* ($0 $+ ("input", 2), factorial) (v, Skip)
/\ v $? "output" = Some 2. /\ v $? "output" = Some 2.
Proof. Proof.
eexists; propositional. eexists; propositional.
econstructor. econstructor.
@ -309,33 +312,33 @@ Proof.
simplify. simplify.
equality. equality.
Qed. Qed.
Ltac step1 := Ltac step1 :=
apply TrcRefl || eapply TrcFront apply TrcRefl || eapply TrcFront
|| apply StepAssign || apply StepSeq2 || eapply StepSeq1 || apply StepAssign || apply StepSeq2 || eapply StepSeq1
|| (apply StepIfTrue; [ simplify; equality ]) || (apply StepIfTrue; [ simplify; equality ])
|| (apply StepIfFalse; [ simplify; equality ]) || (apply StepIfFalse; [ simplify; equality ])
|| (eapply StepWhileTrue; [ simplify; equality ]) || (eapply StepWhileTrue; [ simplify; equality ])
|| (apply StepWhileFalse; [ simplify; equality ]). || (apply StepWhileFalse; [ simplify; equality ]).
Ltac stepper := simplify; try equality; repeat step1. Ltac stepper := simplify; try equality; repeat step1.
Theorem factorial_2_small_snazzy : exists v, step^* ($0 $+ ("input", 2), factorial) (v, Skip) Theorem factorial_2_small_snazzy : exists v, step^* ($0 $+ ("input", 2), factorial) (v, Skip)
/\ v $? "output" = Some 2. /\ v $? "output" = Some 2.
Proof. Proof.
eexists; propositional. eexists; propositional.
stepper. stepper.
stepper. stepper.
Qed. Qed.
(* It turns out that these two semantics styles are equivalent. Let's prove (* It turns out that these two semantics styles are equivalent. Let's prove
* it. *) * it. *)
Lemma step_star_Seq : forall v c1 c2 v' c1', Lemma step_star_Seq : forall v c1 c2 v' c1',
step^* (v, c1) (v', c1') step^* (v, c1) (v', c1')
-> step^* (v, Sequence c1 c2) (v', Sequence c1' c2). -> step^* (v, Sequence c1 c2) (v', Sequence c1' c2).
Proof. Proof.
induct 1. induct 1.
constructor. constructor.
@ -347,11 +350,11 @@ Proof.
apply IHtrc. apply IHtrc.
equality. equality.
equality. equality.
Qed. Qed.
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).
Proof. Proof.
induct 1; simplify. induct 1; simplify.
constructor. constructor.
@ -391,12 +394,12 @@ Proof.
apply StepWhileFalse. apply StepWhileFalse.
assumption. assumption.
constructor. constructor.
Qed. Qed.
Lemma small_big'' : forall v c v' c', step (v, c) (v', c') Lemma small_big'' : forall v c v' c', step (v, c) (v', c')
-> forall v'', eval v' c' v'' -> forall v'', eval v' c' v''
-> eval v c v''. -> eval v c v''.
Proof. Proof.
induct 1; simplify. induct 1; simplify.
invert H. invert H.
@ -429,12 +432,12 @@ Proof.
invert H0. invert H0.
apply EvalWhileFalse. apply EvalWhileFalse.
assumption. assumption.
Qed. Qed.
Lemma small_big' : forall v c v' c', step^* (v, c) (v', c') Lemma small_big' : forall v c v' c', step^* (v, c) (v', c')
-> forall v'', eval v' c' v'' -> forall v'', eval v' c' v''
-> eval v c v''. -> eval v c v''.
Proof. Proof.
induct 1; simplify. induct 1; simplify.
trivial. trivial.
@ -446,92 +449,92 @@ Proof.
equality. equality.
equality. equality.
assumption. assumption.
Qed. Qed.
Theorem small_big : forall v c v', step^* (v, c) (v', Skip) Theorem small_big : forall v c v', step^* (v, c) (v', Skip)
-> eval v c v'. -> eval v c v'.
Proof. Proof.
simplify. simplify.
eapply small_big'. eapply small_big'.
eassumption. eassumption.
constructor. constructor.
Qed. Qed.
(* 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. 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')
-> step^* (v, Sequence c1 c2) (v', Sequence c1' c2). -> step^* (v, Sequence c1 c2) (v', Sequence c1' c2).
Proof. Proof.
induct 1; eauto. induct 1; eauto.
cases y; eauto. cases y; eauto.
Qed. Qed.
Hint Resolve step_star_Seq_snazzy. 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).
Proof. Proof.
induct 1; eauto 6 using trc_trans. induct 1; eauto 6 using trc_trans.
Qed. Qed.
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''
-> eval v c v''. -> eval v c v''.
Proof. Proof.
induct 1; simplify; induct 1; simplify;
repeat match goal with repeat match goal with
| [ H : eval _ _ _ |- _ ] => invert1 H | [ H : eval _ _ _ |- _ ] => invert1 H
end; eauto. end; eauto.
Qed. Qed.
Hint Resolve small_big''_snazzy. 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''
-> eval v c v''. -> eval v c v''.
Proof. Proof.
induct 1; eauto. induct 1; eauto.
cases y; eauto. cases y; eauto.
Qed. Qed.
Hint Resolve small_big'_snazzy. 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'.
Proof. Proof.
eauto. eauto.
Qed. Qed.
(** * Small-step semantics gives rise to transition systems. *) (** * Small-step semantics gives rise to transition systems. *)
Definition trsys_of (v : valuation) (c : cmd) : trsys (valuation * cmd) := {| Definition trsys_of (v : valuation) (c : cmd) : trsys (valuation * cmd) := {|
Initial := {(v, c)}; Initial := {(v, c)};
Step := step Step := step
|}. |}.
Theorem simple_invariant : Theorem simple_invariant :
invariantFor (trsys_of ($0 $+ ("a", 1)) ("b" <- "a" + 1;; "c" <- "b" + "b")) invariantFor (trsys_of ($0 $+ ("a", 1)) ("b" <- "a" + 1;; "c" <- "b" + "b"))
(fun s => snd s = Skip -> fst s $? "c" = Some 4). (fun s => snd s = Skip -> fst s $? "c" = Some 4).
Proof. Proof.
model_check. model_check.
Qed. Qed.
Inductive isEven : nat -> Prop := Inductive isEven : nat -> Prop :=
| EvenO : isEven 0 | EvenO : isEven 0
| EvenSS : forall n, isEven n -> isEven (S (S n)). | EvenSS : forall n, isEven n -> isEven (S (S n)).
Definition my_loop := Definition my_loop :=
while "n" loop while "n" loop
"a" <- "a" + "n";; "a" <- "a" + "n";;
"n" <- "n" - 2 "n" <- "n" - 2
done. done.
Definition all_programs := { Definition all_programs := {
(while "n" loop (while "n" loop
"a" <- "a" + "n";; "a" <- "a" + "n";;
"n" <- "n" - 2 "n" <- "n" - 2
@ -564,23 +567,23 @@ Definition all_programs := {
"n" <- "n" - 2 "n" <- "n" - 2
done), done),
Skip Skip
}. }.
Lemma isEven_minus2 : forall n, isEven n -> isEven (n - 2). Lemma isEven_minus2 : forall n, isEven n -> isEven (n - 2).
Proof. Proof.
induct 1; simplify. induct 1; simplify.
constructor. constructor.
replace (n - 0) with n by linear_arithmetic. replace (n - 0) with n by linear_arithmetic.
assumption. assumption.
Qed. Qed.
Lemma isEven_plus : forall n m, Lemma isEven_plus : forall n m,
isEven n isEven n
-> isEven m -> isEven m
-> isEven (n + m). -> isEven (n + m).
Proof. Proof.
induct 1; simplify. induct 1; simplify.
assumption. assumption.
@ -588,9 +591,9 @@ Proof.
constructor. constructor.
apply IHisEven. apply IHisEven.
assumption. assumption.
Qed. Qed.
Lemma manually_proved_invariant' : forall n, Lemma manually_proved_invariant' : forall n,
isEven n isEven n
-> invariantFor (trsys_of ($0 $+ ("n", n) $+ ("a", 0)) (while "n" loop "a" <- "a" + "n";; "n" <- "n" - 2 done)) -> invariantFor (trsys_of ($0 $+ ("n", n) $+ ("a", 0)) (while "n" loop "a" <- "a" + "n";; "n" <- "n" - 2 done))
(fun s => all_programs (snd s) (fun s => all_programs (snd s)
@ -598,7 +601,7 @@ Lemma manually_proved_invariant' : forall n,
/\ fst s $? "a" = Some a /\ fst s $? "a" = Some a
/\ isEven n /\ isEven n
/\ isEven a). /\ isEven a).
Proof. Proof.
simplify. simplify.
apply invariant_induction; simplify. apply invariant_induction; simplify.
@ -682,13 +685,13 @@ Proof.
unfold all_programs in *; simplify; propositional; try equality. unfold all_programs in *; simplify; propositional; try equality.
invert H1. invert H1.
do 2 eexists; propositional; try eassumption. do 2 eexists; propositional; try eassumption.
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. Hint Constructors isEven : core.
Hint Resolve isEven_minus2 isEven_plus. 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
-> invariantFor (trsys_of ($0 $+ ("n", n) $+ ("a", 0)) (while "n" loop "a" <- "a" + "n";; "n" <- "n" - 2 done)) -> invariantFor (trsys_of ($0 $+ ("n", n) $+ ("a", 0)) (while "n" loop "a" <- "a" + "n";; "n" <- "n" - 2 done))
(fun s => all_programs (snd s) (fun s => all_programs (snd s)
@ -696,7 +699,7 @@ Lemma manually_proved_invariant'_snazzy : forall n,
/\ fst s $? "a" = Some a /\ fst s $? "a" = Some a
/\ isEven n /\ isEven n
/\ isEven a). /\ isEven a).
Proof. Proof.
simplify; apply invariant_induction; simplify; unfold all_programs in *; first_order; subst; simplify; simplify; apply invariant_induction; simplify; unfold all_programs in *; first_order; subst; simplify;
try match goal with try match goal with
| [ H : step _ _ |- _ ] => invert H; simplify | [ H : step _ _ |- _ ] => invert H; simplify
@ -707,77 +710,77 @@ Proof.
| [ H : @eq cmd (_ _ _ _) _ |- _ ] => invert H | [ H : @eq cmd (_ _ _ _) _ |- _ ] => invert H
| [ H : step _ _ |- _ ] => invert2 H | [ H : step _ _ |- _ ] => invert2 H
end; simplify); equality || eauto 7. end; simplify); equality || eauto 7.
Qed. Qed.
Theorem manually_proved_invariant : forall n, Theorem manually_proved_invariant : forall n,
isEven n isEven n
-> invariantFor (trsys_of ($0 $+ ("n", n) $+ ("a", 0)) (while "n" loop "a" <- "a" + "n";; "n" <- "n" - 2 done)) -> invariantFor (trsys_of ($0 $+ ("n", n) $+ ("a", 0)) (while "n" loop "a" <- "a" + "n";; "n" <- "n" - 2 done))
(fun s => exists a, fst s $? "a" = Some a /\ isEven a). (fun s => exists a, fst s $? "a" = Some a /\ isEven a).
Proof. Proof.
simplify. simplify.
eapply invariant_weaken. eapply invariant_weaken.
apply manually_proved_invariant'; assumption. apply manually_proved_invariant'; assumption.
first_order. first_order.
Qed. Qed.
(* We'll return to these systems and their abstractions in the next few (* We'll return to these systems and their abstractions in the next few
* chapters. *) * chapters. *)
(** * Contextual small-step semantics *) (** * Contextual small-step semantics *)
(* There is a common way to factor a small-step semantics into different parts, (* There is a common way to factor a small-step semantics into different parts,
* to make the semantics easier to understand and extend. First, we define a * to make the semantics easier to understand and extend. First, we define a
* notion of *evaluation contexts*, which are commands with *holes* in them. *) * notion of *evaluation contexts*, which are commands with *holes* in them. *)
Inductive context := Inductive context :=
| Hole | Hole
| CSeq (C : context) (c : cmd). | CSeq (C : context) (c : cmd).
(* This relation explains how to plug the hole in a context with a specific (* This relation explains how to plug the hole in a context with a specific
* term. Note that we use an inductive relation instead of a recursive * term. Note that we use an inductive relation instead of a recursive
* definition, because Coq's proof automation is better at working with * definition, because Coq's proof automation is better at working with
* relations. *) * relations. *)
Inductive plug : context -> cmd -> cmd -> Prop := Inductive plug : context -> cmd -> cmd -> Prop :=
| PlugHole : forall c, plug Hole c c | PlugHole : forall c, plug Hole c c
| PlugSeq : forall c C c' c2, | PlugSeq : forall c C c' c2,
plug C c c' plug C c c'
-> plug (CSeq C c2) c (Sequence c' c2). -> plug (CSeq C c2) c (Sequence c' c2).
(* Now we define almost the same step relation as before, with one omission: (* Now we define almost the same step relation as before, with one omission:
* only the more trivial of the [Sequence] rules remains. *) * only the more trivial of the [Sequence] rules remains. *)
Inductive step0 : valuation * cmd -> valuation * cmd -> Prop := Inductive step0 : valuation * cmd -> valuation * cmd -> Prop :=
| Step0Assign : forall v x e, | Step0Assign : forall v x e,
step0 (v, Assign x e) (v $+ (x, interp e v), Skip) step0 (v, Assign x e) (v $+ (x, interp e v), Skip)
| Step0Seq : forall v c2, | Step0Seq : forall v c2,
step0 (v, Sequence Skip c2) (v, c2) step0 (v, Sequence Skip c2) (v, c2)
| Step0IfTrue : forall v e then_ else_, | Step0IfTrue : forall v e then_ else_,
interp e v <> 0 interp e v <> 0
-> step0 (v, If e then_ else_) (v, then_) -> step0 (v, If e then_ else_) (v, then_)
| Step0IfFalse : forall v e then_ else_, | Step0IfFalse : forall v e then_ else_,
interp e v = 0 interp e v = 0
-> step0 (v, If e then_ else_) (v, else_) -> step0 (v, If e then_ else_) (v, else_)
| Step0WhileTrue : forall v e body, | Step0WhileTrue : forall v e body,
interp e v <> 0 interp e v <> 0
-> step0 (v, While e body) (v, Sequence body (While e body)) -> step0 (v, While e body) (v, Sequence body (While e body))
| Step0WhileFalse : forall v e body, | Step0WhileFalse : forall v e body,
interp e v = 0 interp e v = 0
-> step0 (v, While e body) (v, Skip). -> step0 (v, While e body) (v, Skip).
(* We recover the meaning of the original with one top-level rule, combining (* We recover the meaning of the original with one top-level rule, combining
* plugging of contexts with basic steps. *) * plugging of contexts with basic steps. *)
Inductive cstep : valuation * cmd -> valuation * cmd -> Prop := Inductive cstep : valuation * cmd -> valuation * cmd -> Prop :=
| CStep : forall C v c v' c' c1 c2, | CStep : forall C v c v' c' c1 c2,
plug C c c1 plug C c c1
-> step0 (v, c) (v', c') -> step0 (v, c) (v', c')
-> plug C c' c2 -> plug C c' c2
-> cstep (v, c1) (v', c2). -> cstep (v, c1) (v', c2).
(* We can prove equivalence between the two formulations. *) (* We can prove equivalence between the two formulations. *)
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')
-> cstep (v, c) (v', c'). -> cstep (v, c) (v', c').
Proof. Proof.
induct 1. induct 1.
econstructor. econstructor.
@ -821,21 +824,21 @@ Proof.
apply Step0WhileFalse. apply Step0WhileFalse.
assumption. assumption.
constructor. constructor.
Qed. Qed.
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')
-> step (v, c) (v', c'). -> step (v, c) (v', c').
Proof. Proof.
invert 1; constructor; assumption. invert 1; constructor; assumption.
Qed. Qed.
Lemma cstep_step' : forall C c0 c, Lemma cstep_step' : forall C c0 c,
plug C c0 c plug C c0 c
-> forall v' c'0 v c', step0 (v, c0) (v', c'0) -> forall v' c'0 v c', step0 (v, c0) (v', c'0)
-> plug C c'0 c' -> plug C c'0 c'
-> step (v, c) (v', c'). -> step (v, c) (v', c').
Proof. Proof.
induct 1; simplify. induct 1; simplify.
invert H0. invert H0.
@ -847,75 +850,75 @@ Proof.
eapply IHplug. eapply IHplug.
eassumption. eassumption.
assumption. assumption.
Qed. Qed.
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')
-> step (v, c) (v', c'). -> step (v, c) (v', c').
Proof. Proof.
invert 1. invert 1.
eapply cstep_step'. eapply cstep_step'.
eassumption. eassumption.
eassumption. eassumption.
assumption. assumption.
Qed. Qed.
(* 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. 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')
-> cstep (v, c) (v', c'). -> cstep (v, c) (v', c').
Proof. Proof.
induct 1; repeat match goal with induct 1; repeat match goal with
| [ H : cstep _ _ |- _ ] => invert H | [ H : cstep _ _ |- _ ] => invert H
end; eauto. end; eauto.
Qed. Qed.
Hint Resolve step_cstep_snazzy. 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')
-> step (v, c) (v', c'). -> step (v, c) (v', c').
Proof. Proof.
invert 1; eauto. invert 1; eauto.
Qed. Qed.
Hint Resolve step0_step_snazzy. 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
-> forall v' c'0 v c', step0 (v, c0) (v', c'0) -> forall v' c'0 v c', step0 (v, c0) (v', c'0)
-> plug C c'0 c' -> plug C c'0 c'
-> step (v, c) (v', c'). -> step (v, c) (v', c').
Proof. Proof.
induct 1; simplify; repeat match goal with induct 1; simplify; repeat match goal with
| [ H : plug _ _ _ |- _ ] => invert1 H | [ H : plug _ _ _ |- _ ] => invert1 H
end; eauto. end; eauto.
Qed. Qed.
Hint Resolve cstep_step'_snazzy. 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')
-> step (v, c) (v', c'). -> step (v, c) (v', c').
Proof. Proof.
invert 1; eauto. invert 1; eauto.
Qed. Qed.
(** * Determinism *) (** * Determinism *)
(* Each of the relations we have defined turns out to be deterministic. Let's (* Each of the relations we have defined turns out to be deterministic. Let's
* prove it. *) * prove it. *)
Theorem eval_det : forall v c v1, Theorem eval_det : forall v c v1,
eval v c v1 eval v c v1
-> forall v2, eval v c v2 -> forall v2, eval v c v2
-> v1 = v2. -> v1 = v2.
Proof. Proof.
induct 1; invert 1; try first_order. induct 1; invert 1; try first_order.
apply IHeval2. apply IHeval2.
@ -927,13 +930,13 @@ Proof.
apply IHeval1 in H7. apply IHeval1 in H7.
subst. subst.
assumption. assumption.
Qed. Qed.
Theorem step_det : forall s out1, Theorem step_det : forall s out1,
step s out1 step s out1
-> forall out2, step s out2 -> forall out2, step s out2
-> out1 = out2. -> out1 = out2.
Proof. Proof.
induct 1; invert 1; try first_order. induct 1; invert 1; try first_order.
apply IHstep in H5. apply IHstep in H5.
@ -942,13 +945,13 @@ Proof.
invert H. invert H.
invert H4. invert H4.
Qed. Qed.
Theorem cstep_det : forall s out1, Theorem cstep_det : forall s out1,
cstep s out1 cstep s out1
-> forall out2, cstep s out2 -> forall out2, cstep s out2
-> out1 = out2. -> out1 = out2.
Proof. Proof.
simplify. simplify.
cases s; cases out1; cases out2. cases s; cases out1; cases out2.
eapply step_det. eapply step_det.
@ -956,8 +959,8 @@ Proof.
eassumption. eassumption.
apply cstep_step. apply cstep_step.
eassumption. eassumption.
Qed. Qed.
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 *)
@ -1041,7 +1044,7 @@ Module Concurrent.
|| ("b" <- "n";; || ("b" <- "n";;
"n" <- "b" + 1). "n" <- "b" + 1).
Hint Constructors plug step0 cstep. 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)
@ -1146,7 +1149,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. 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! *)
@ -1160,7 +1163,7 @@ Module Concurrent.
end; eauto. end; eauto.
Qed. Qed.
Hint Resolve step_cstep. 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')
@ -1169,7 +1172,7 @@ Module Concurrent.
invert 1; eauto. invert 1; eauto.
Qed. Qed.
Hint Resolve step0_step. 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
@ -1182,7 +1185,7 @@ Module Concurrent.
end; eauto. end; eauto.
Qed. Qed.
Hint Resolve cstep_step'. 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')

266
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. 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. Hint Constructors isEven : core.
Hint Resolve isEven_minus2 isEven_plus. 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. 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')
@ -614,176 +614,6 @@ Admitted.
(** * Example of how easy it is to add concurrency to a contextual semantics *)
Module Concurrent.
(* Let's add a construct for *parallel execution* of two commands. Such
* parallelism may be nested arbitrarily. *)
Inductive cmd :=
| Skip
| Assign (x : var) (e : arith)
| Sequence (c1 c2 : cmd)
| If (e : arith) (then_ else_ : cmd)
| While (e : arith) (body : cmd)
| Parallel (c1 c2 : cmd).
Notation "x <- e" := (Assign x e%arith) (at level 75).
Infix ";;" := Sequence (at level 76). (* This one changed slightly, to avoid parsing clashes. *)
Notation "'when' e 'then' then_ 'else' else_ 'done'" := (If e%arith then_ else_) (at level 75, e at level 0).
Notation "'while' e 'loop' body 'done'" := (While e%arith body) (at level 75).
Infix "||" := Parallel.
(* We need surprisingly few changes to the contextual semantics, to explain
* this new feature. First, we allow a hole to appear on *either side* of a
* [Parallel]. In other words, the "scheduler" may choose either "thread" to
* run next. *)
Inductive context :=
| Hole
| CSeq (C : context) (c : cmd)
| CPar1 (C : context) (c : cmd)
| CPar2 (c : cmd) (C : context).
(* We explain the meaning of plugging the new contexts in the obvious way. *)
Inductive plug : context -> cmd -> cmd -> Prop :=
| PlugHole : forall c, plug Hole c c
| PlugSeq : forall c C c' c2,
plug C c c'
-> plug (CSeq C c2) c (Sequence c' c2)
| PlugPar1 : forall c C c' c2,
plug C c c'
-> plug (CPar1 C c2) c (Parallel c' c2)
| PlugPar2 : forall c C c' c1,
plug C c c'
-> plug (CPar2 c1 C) c (Parallel c1 c').
(* The only new step rules are for "cleaning up" finished "threads," which
* have reached the point of being [Skip] commands. *)
Inductive step0 : valuation * cmd -> valuation * cmd -> Prop :=
| Step0Assign : forall v x e,
step0 (v, Assign x e) (v $+ (x, interp e v), Skip)
| Step0Seq : forall v c2,
step0 (v, Sequence Skip c2) (v, c2)
| Step0IfTrue : forall v e then_ else_,
interp e v <> 0
-> step0 (v, If e then_ else_) (v, then_)
| Step0IfFalse : forall v e then_ else_,
interp e v = 0
-> step0 (v, If e then_ else_) (v, else_)
| Step0WhileTrue : forall v e body,
interp e v <> 0
-> step0 (v, While e body) (v, Sequence body (While e body))
| Step0WhileFalse : forall v e body,
interp e v = 0
-> step0 (v, While e body) (v, Skip)
| Step0Par1 : forall v c,
step0 (v, Parallel Skip c) (v, c).
Inductive cstep : valuation * cmd -> valuation * cmd -> Prop :=
| CStep : forall C v c v' c' c1 c2,
plug C c c1
-> step0 (v, c) (v', c')
-> plug C c' c2
-> cstep (v, c1) (v', c2).
(** Example: stepping a specific program. *)
(* Here's the classic cautionary-tale program about remembering to lock your
* concurrent threads. *)
Definition prog :=
("a" <- "n";;
"n" <- "a" + 1)
|| ("b" <- "n";;
"n" <- "b" + 1).
Hint Constructors plug step0 cstep.
(* The naive "expected" answer is attainable. *)
Theorem correctAnswer : forall n, exists v, cstep^* ($0 $+ ("n", n), prog) (v, Skip)
/\ v $? "n" = Some (n + 2).
Proof.
eexists; propositional.
unfold prog.
econstructor.
eapply CStep with (C := CPar1 (CSeq Hole _) _); eauto.
econstructor.
eapply CStep with (C := CPar1 Hole _); eauto.
econstructor.
eapply CStep with (C := CPar1 Hole _); eauto.
econstructor.
eapply CStep with (C := Hole); eauto.
econstructor.
eapply CStep with (C := CSeq Hole _); eauto.
econstructor.
eapply CStep with (C := Hole); eauto.
econstructor.
eapply CStep with (C := Hole); eauto.
econstructor.
simplify.
f_equal.
ring.
Qed.
(* But so is the "wrong" answer! *)
Theorem wrongAnswer : forall n, exists v, cstep^* ($0 $+ ("n", n), prog) (v, Skip)
/\ v $? "n" = Some (n + 1).
Proof.
eexists; propositional.
unfold prog.
Admitted.
(** Proving equivalence with non-contextual semantics *)
(* To give us something interesting to prove, let's also define a
* non-contextual small-step semantics. Note how we have to do some more
* explicit threading of mutable state through recursive invocations. *)
Inductive step : valuation * cmd -> valuation * cmd -> Prop :=
| StepAssign : forall v x e,
step (v, Assign x e) (v $+ (x, interp e v), Skip)
| StepSeq1 : forall v c1 c2 v' c1',
step (v, c1) (v', c1')
-> step (v, Sequence c1 c2) (v', Sequence c1' c2)
| StepSeq2 : forall v c2,
step (v, Sequence Skip c2) (v, c2)
| StepIfTrue : forall v e then_ else_,
interp e v <> 0
-> step (v, If e then_ else_) (v, then_)
| StepIfFalse : forall v e then_ else_,
interp e v = 0
-> step (v, If e then_ else_) (v, else_)
| StepWhileTrue : forall v e body,
interp e v <> 0
-> step (v, While e body) (v, Sequence body (While e body))
| StepWhileFalse : forall v e body,
interp e v = 0
-> step (v, While e body) (v, Skip)
| StepParSkip1 : forall v c,
step (v, Parallel Skip c) (v, c)
| StepPar1 : forall v c1 c2 v' c1',
step (v, c1) (v', c1')
-> step (v, Parallel c1 c2) (v', Parallel c1' c2)
| StepPar2 : forall v c1 c2 v' c2',
step (v, c2) (v', c2')
-> step (v, Parallel c1 c2) (v', Parallel c1 c2').
Hint Constructors step.
(* Now, an automated proof of equivalence. Actually, it's *exactly* the same
* proof we used for the old feature set! For full dramatic effect, copy and
* paste here from above. *)
End Concurrent.
(** * Determinism *) (** * Determinism *)
@ -837,3 +667,91 @@ Proof.
apply cstep_step. apply cstep_step.
eassumption. eassumption.
Qed. Qed.
(** * Example of how easy it is to add concurrency to a contextual semantics *)
(** At this point, we add concurrency to the code we already wrote above. *)
(*
(* Here's the classic cautionary-tale program about remembering to lock your
* concurrent threads. *)
Definition prog :=
("a" <- "n";;
"n" <- "a" + 1)
|| ("b" <- "n";;
"n" <- "b" + 1).
Hint Constructors plug step0 cstep : core.
(* The naive "expected" answer is attainable. *)
Theorem correctAnswer : forall n, exists v, cstep^* ($0 $+ ("n", n), prog) (v, Skip)
/\ v $? "n" = Some (n + 2).
Proof.
eexists; propositional.
unfold prog.
econstructor.
eapply CStep with (C := CPar1 (CSeq Hole _) _); eauto.
econstructor.
eapply CStep with (C := CPar1 Hole _); eauto.
econstructor.
eapply CStep with (C := CPar1 Hole _); eauto.
econstructor.
eapply CStep with (C := Hole); eauto.
econstructor.
eapply CStep with (C := CSeq Hole _); eauto.
econstructor.
eapply CStep with (C := Hole); eauto.
econstructor.
eapply CStep with (C := Hole); eauto.
econstructor.
simplify.
f_equal.
ring.
Qed.
(* But so is the "wrong" answer! *)
Theorem wrongAnswer : forall n, exists v, cstep^* ($0 $+ ("n", n), prog) (v, Skip)
/\ v $? "n" = Some (n + 1).
Proof.
eexists; propositional.
unfold prog.
Admitted.
*)