(** * Smallstep: Small-step Operational Semantics *) Require Export Imp. (** Evaluation relations come in two flavors... _Big-step_ style: evaluation rules take an expression (or command) to a final answer "all in one step": 2 + 2 + 3 * 4 || 16 _Small-step_ style: Rules show how to "reduce" an expression by performing a single step of computation: 2 + 2 + 3 * 4 ==> 2 + 2 + 12 ==> 4 + 12 ==> 16 Advantages of the small-step style include: - Finer-grained "abstract machine" is closer to real implementations - Extends to concurrent languages - Separates _divergence_ (nontermination) from _stuckness_ (run-time error) *) (* ########################################################### *) (** * Relations *) (** A _relation_ on a set [X] is a family of propositions parameterized by two elements of [X] -- i.e., a proposition about pairs of elements of [X]. *) Definition relation (X: Type) := X->X->Prop. (* ########################################################### *) (** * A Toy Language *) (** The world's simplest programming language: *) Inductive tm : Type := | C : nat -> tm (* Constant *) | P : tm -> tm -> tm. (* Plus *) Tactic Notation "tm_cases" tactic(first) ident(c) := first; [ Case_aux c "C" | Case_aux c "P" ]. (** *** Big-step evaluation as a function *) Fixpoint evalF (t : tm) : nat := match t with | C n => n | P a1 a2 => evalF a1 + evalF a2 end. (** *** Big-step evaluation as a relation *) (** -------- (E_Const) C n || n t1 || n1 t2 || n2 ---------------------- (E_Plus) P t1 t2 || C (n1 + n2) *) Reserved Notation " t '||' n " (at level 50, left associativity). Inductive eval : tm -> nat -> Prop := | E_Const : forall n, C n || n | E_Plus : forall t1 t2 n1 n2, t1 || n1 -> t2 || n2 -> P t1 t2 || (n1 + n2) where " t '||' n " := (eval t n). Tactic Notation "eval_cases" tactic(first) ident(c) := first; [ Case_aux c "E_Const" | Case_aux c "E_Plus" ]. Module SimpleArith1. (** *** Small-step evaluation relation *) (** ------------------------------- (ST_PlusConstConst) P (C n1) (C n2) ==> C (n1 + n2) t1 ==> t1' -------------------- (ST_Plus1) P t1 t2 ==> P t1' t2 t2 ==> t2' --------------------------- (ST_Plus2) P (C n1) t2 ==> P (C n1) t2' *) Reserved Notation " t '==>' t' " (at level 40). Inductive step : tm -> tm -> Prop := | ST_PlusConstConst : forall n1 n2, P (C n1) (C n2) ==> C (n1 + n2) | ST_Plus1 : forall t1 t1' t2, t1 ==> t1' -> P t1 t2 ==> P t1' t2 | ST_Plus2 : forall n1 t2 t2', t2 ==> t2' -> P (C n1) t2 ==> P (C n1) t2' where " t '==>' t' " := (step t t'). Tactic Notation "step_cases" tactic(first) ident(c) := first; [ Case_aux c "ST_PlusConstConst" | Case_aux c "ST_Plus1" | Case_aux c "ST_Plus2" ]. (** Notice: - each step reduces the _leftmost_ [P] node that is ready to go - first rule tells how to rewrite this node - second and third rules tell where to find it - constants are not related to anything *) (** *** Examples *) (** If [t1] can take a step to [t1'], then [P t1 t2] steps to [P t1' t2]: *) Example test_step_1 : P (P (C 0) (C 3)) (P (C 2) (C 4)) ==> P (C (0 + 3)) (P (C 2) (C 4)). Proof. apply ST_Plus1. apply ST_PlusConstConst. Qed. (* QUIZ *) (** What does the following term step to? P (P (C 1) (C 2)) (P (C 1) (C 2)) (1) [C 6] (2) [P (C 3) (P (C 1) (C 2))] (3) [P (P (C 1) (C 2)) (C 3)] (4) [P (C 3) (C 3)] (5) None of the above *) (* /QUIZ *) (* QUIZ *) (** What about this one? C 1 (1) [C 1] (2) [P (C 0) (C 1)] (3) None of the above *) (* /QUIZ *) (** *** Determinism *) (** One simple property of the [==>] relation is that, like the evaluation relation for our language of Imp programs, it is _deterministic_. _Theorem_: For each [t], there is at most one [t'] such that [t] steps to [t'] ([t ==> t'] is provable). Formally, this is the same as saying that [==>] is deterministic. *) (** Formally: *) Definition deterministic {X: Type} (R: relation X) := forall x y1 y2 : X, R x y1 -> R x y2 -> y1 = y2. Theorem step_deterministic: deterministic step. Proof. unfold deterministic. intros x y1 y2 Hy1 Hy2. generalize dependent y2. step_cases (induction Hy1) Case; intros y2 Hy2. Case "ST_PlusConstConst". step_cases (inversion Hy2) SCase. SCase "ST_PlusConstConst". reflexivity. SCase "ST_Plus1". inversion H2. SCase "ST_Plus2". inversion H2. Case "ST_Plus1". step_cases (inversion Hy2) SCase. SCase "ST_PlusConstConst". rewrite <- H0 in Hy1. inversion Hy1. SCase "ST_Plus1". rewrite <- (IHHy1 t1'0). reflexivity. assumption. SCase "ST_Plus2". rewrite <- H in Hy1. inversion Hy1. Case "ST_Plus2". step_cases (inversion Hy2) SCase. SCase "ST_PlusConstConst". rewrite <- H1 in Hy1. inversion Hy1. SCase "ST_Plus1". inversion H2. SCase "ST_Plus2". rewrite <- (IHHy1 t2'0). reflexivity. assumption. Qed. End SimpleArith1. (* ########################################################### *) (** ** Values *) (** It is useful to think of the [==>] relation as defining an _abstract machine_: - At any moment, the _state_ of the machine is a term. - A _step_ of the machine is an atomic unit of computation -- here, a single "add" operation. - The _halting states_ of the machine are ones where there is no more computation to be done. We can then execute a term [t] as follows: - Take [t] as the starting state of the machine. - Repeatedly use the [==>] relation to find a sequence of machine states, starting with [t], where each state steps to the next. - When no more reduction is possible, "read out" the final state of the machine as the result of execution. *) (** Final states of the machine are terms of the form [C n] for some [n]. We call such terms _values_. *) Inductive value : tm -> Prop := v_const : forall n, value (C n). (** This gives a more elegant way of writing the [ST_Plus2] rule: *) (** ------------------------------- (ST_PlusConstConst) P (C n1) (C n2) ==> C (n1 + n2) t1 ==> t1' -------------------- (ST_Plus1) P t1 t2 ==> P t1' t2 value v1 t2 ==> t2' -------------------- (ST_Plus2) P v1 t2 ==> P v1 t2' *) (** Again, variable names carry important information: - [v1] ranges only over values - [t1] and [t2] range over arbitrary terms So the [value] hypothesis in the last rule is actually redundant. We'll keep it for now, but in later chapters we'll elide it. Here are the formal rules: *) Reserved Notation " t '==>' t' " (at level 40). Inductive step : tm -> tm -> Prop := | ST_PlusConstConst : forall n1 n2, P (C n1) (C n2) ==> C (n1 + n2) | ST_Plus1 : forall t1 t1' t2, t1 ==> t1' -> P t1 t2 ==> P t1' t2 | ST_Plus2 : forall v1 t2 t2', value v1 -> (* <----- n.b. *) t2 ==> t2' -> P v1 t2 ==> P v1 t2' where " t '==>' t' " := (step t t'). Tactic Notation "step_cases" tactic(first) ident(c) := first; [ Case_aux c "ST_PlusConstConst" | Case_aux c "ST_Plus1" | Case_aux c "ST_Plus2" ]. (* ########################################################### *) (** ** Strong Progress and Normal Forms *) (** _Theorem_ (_Strong Progress_): If [t] is a term, then either [t] is a value, or there exists a term [t'] such that [t ==> t']. *) (** Or, formally: *) Theorem strong_progress : forall t, value t \/ (exists t', t ==> t'). Proof. tm_cases (induction t) Case. Case "C". left. apply v_const. Case "P". right. inversion IHt1. SCase "l". inversion IHt2. SSCase "l". inversion H. inversion H0. exists (C (n + n0)). apply ST_PlusConstConst. SSCase "r". inversion H0 as [t' H1]. exists (P t1 t'). apply ST_Plus2. apply H. apply H1. SCase "r". inversion H as [t' H0]. exists (P t' t2). apply ST_Plus1. apply H0. Qed. (** *** Normal forms *) (** The idea of "making progress" can be extended to tell us something interesting about [value]s: in this language [value]s are exactly the terms that _cannot_ make progress in this sense. To state this observation formally, let's begin by giving a name to terms that cannot make progress. We'll call them _normal forms_. *) Definition normal_form {X:Type} (R:relation X) (t:X) : Prop := ~ exists t', R t t'. (** *** Values vs. normal forms *) (** In this language, normal forms and values coincide: *) Lemma value_is_nf : forall v, value v -> normal_form step v. Proof. unfold normal_form. intros v H. inversion H. intros contra. inversion contra. inversion H1. Qed. Lemma nf_is_value : forall t, normal_form step t -> value t. Proof. (* a corollary of [strong_progress]... *) unfold normal_form. intros t H. assert (G : value t \/ exists t', t ==> t'). SCase "Proof of assertion". apply strong_progress. inversion G. SCase "l". apply H0. SCase "r". apply ex_falso_quodlibet. apply H. assumption. Qed. Corollary nf_same_as_value : forall t, normal_form step t <-> value t. Proof. split. apply nf_is_value. apply value_is_nf. Qed. (** Why is this interesting? Because [value] is a syntactic concept -- it is defined by looking at the form of a term -- while [normal_form] is a semantic one -- it is defined by looking at how the term steps. It is not obvious that these concepts should coincide! Indeed, we could easily have written the definitions so that they would not coincide... *) (* ##################################################### *) (** *** *) (** We might, for example, mistakenly define [value] so that it includes some terms that are not finished reducing. *) Module Temp1. Inductive value : tm -> Prop := | v_const : forall n, value (C n) | v_funny : forall t1 n2, (* <---- *) value (P t1 (C n2)). Reserved Notation " t '==>' t' " (at level 40). Inductive step : tm -> tm -> Prop := | ST_PlusConstConst : forall n1 n2, P (C n1) (C n2) ==> C (n1 + n2) | ST_Plus1 : forall t1 t1' t2, t1 ==> t1' -> P t1 t2 ==> P t1' t2 | ST_Plus2 : forall v1 t2 t2', value v1 -> t2 ==> t2' -> P v1 t2 ==> P v1 t2' where " t '==>' t' " := (step t t'). (* QUIZ *) (** How many different terms does the following term [step] to? P (P (C 1) (C 2)) (C 3) *) (* /QUIZ *) (* QUIZ *) (** How many different terms does the following term [step] to? P (P (C 1) (C 2)) (P (C 3) (C 4)) *) (* /QUIZ *) (** *) Lemma value_not_same_as_normal_form : exists v, value v /\ ~ normal_form step v. Proof. exists (P (C 0) (C 0)). split. constructor. unfold normal_form. intros hip. assert (H: exists t, (P (C 0) (C 0)) ==> t) by ((exists (C 0)); constructor). apply hip in H. assumption. Qed. End Temp1. (* ##################################################### *) (** *** *) (** Alternatively, we might mistakenly define [step] so that it permits something designated as a value to reduce further. *) Module Temp2. Inductive value : tm -> Prop := | v_const : forall n, value (C n). Reserved Notation " t '==>' t' " (at level 40). Inductive step : tm -> tm -> Prop := | ST_Funny : forall n, (* <---- *) C n ==> P (C n) (C 0) | ST_PlusConstConst : forall n1 n2, P (C n1) (C n2) ==> C (n1 + n2) | ST_Plus1 : forall t1 t1' t2, t1 ==> t1' -> P t1 t2 ==> P t1' t2 | ST_Plus2 : forall v1 t2 t2', value v1 -> t2 ==> t2' -> P v1 t2 ==> P v1 t2' where " t '==>' t' " := (step t t'). (* QUIZ *) (** How many terms does the following term step to? P (C 1) (C 3) *) (* /QUIZ *) (** *) Lemma value_not_same_as_normal_form : exists v, value v /\ ~ normal_form step v. Proof. (* FILL IN HERE *) Admitted. End Temp2. (* ########################################################### *) (** *** *) (** Finally, we might define [value] and [step] so that there is some term that is not a value but that cannot take a step in the [step] relation. Such terms are said to be _stuck_. In this case this is caused by a mistake in the semantics, but we will also see situations where, even in a correct language definition, it makes sense to allow some terms to be stuck. *) Module Temp3. Inductive value : tm -> Prop := | v_const : forall n, value (C n). Reserved Notation " t '==>' t' " (at level 40). Inductive step : tm -> tm -> Prop := | ST_PlusConstConst : forall n1 n2, P (C n1) (C n2) ==> C (n1 + n2) | ST_Plus1 : forall t1 t1' t2, t1 ==> t1' -> P t1 t2 ==> P t1' t2 where " t '==>' t' " := (step t t'). (** (Note that [ST_Plus2] is missing.) *) (* QUIZ *) (** How many terms does the following term step to? P (C 1) (P (C 1) (C 2)) *) (* /QUIZ *) (** *) Lemma value_not_same_as_normal_form : exists t, ~ value t /\ normal_form step t. Proof. exists (P (C 0) (P (C 0) (C 0))). split; intros hip; inversion hip. inversion H; subst. inversion H3. Qed. End Temp3. (* ########################################################### *) (** * Multi-Step Reduction *) (** We can now use the single-step relation and the concept of value to formalize an entire _execution_ of an abstract machine. First, we define a _multi-step reduction relation_ [==>*] to capture the intermediate results of a computation. *) (* ########################################################### *) (** *** *) (** Since we'll want to reuse the idea of multi-step reduction many times in this and future chapters, let's take a little extra trouble here and define it generically. Given a relation [R], we define a relation [multi R], called the _multi-step closure of [R]_ as follows: *) Inductive multi {X:Type} (R: relation X) : relation X := | multi_refl : forall (x : X), multi R x x | multi_step : forall (x y z : X), R x y -> multi R y z -> multi R x z. (** The effect of this definition is that [multi R] relates two elements [x] and [y] if either - [x = y], or else - there is some sequence [z1], [z2], ..., [zn] such that R x z1 R z1 z2 ... R zn y. Thus, if [R] describes a single-step of computation, [z1], ... [zn] is the sequence of intermediate steps of computation between [x] and [y]. *) Tactic Notation "multi_cases" tactic(first) ident(c) := first; [ Case_aux c "multi_refl" | Case_aux c "multi_step" ]. (** *** *) (** We write [==>*] for the [multi step] relation -- i.e., the relation that relates two terms [t] and [t'] if we can get from [t] to [t'] using the [step] relation zero or more times. *) Definition multistep := multi step. Notation " t '==>*' t' " := (multistep t t') (at level 40). (** *** *) (** The relation [multi R] has several crucial properties. First, it is obviously _reflexive_ (that is, [forall x, multi R x x]). In the case of the [==>*] (i.e. [multi step]) relation, the intuition is that a term can execute to itself by taking zero steps of execution. Second, it contains [R] -- that is, single-step executions are a particular case of multi-step executions. (It is this fact that justifies the word "closure" in the term "multi-step closure of [R].") *) Theorem multi_R : forall (X:Type) (R:relation X) (x y : X), R x y -> (multi R) x y. Proof. intros X R x y H. apply multi_step with y. apply H. apply multi_refl. Qed. (* QUIZ *) (** Which of the following relations on numbers _cannot_ be expressed as [multi R] for some [R]? (1) less then or equal (2) strictly less than (3) equal (4) none of the above *) (* /QUIZ *) (** Third, [multi R] is _transitive_. *) Theorem multi_trans : forall (X:Type) (R: relation X) (x y z : X), multi R x y -> multi R y z -> multi R x z. Proof. intros X R x y z G H. multi_cases (induction G) Case. Case "multi_refl". assumption. Case "multi_step". apply multi_step with y. assumption. apply IHG. assumption. Qed. (** That is, if [t1==>*t2] and [t2==>*t3], then [t1==>*t3]. *) (* ########################################################### *) (** ** Examples *) Lemma test_multistep_1: P (P (C 0) (C 3)) (P (C 2) (C 4)) ==>* C ((0 + 3) + (2 + 4)). Proof. apply multi_step with (P (C (0 + 3)) (P (C 2) (C 4))). apply ST_Plus1. apply ST_PlusConstConst. apply multi_step with (P (C (0 + 3)) (C (2 + 4))). apply ST_Plus2. apply v_const. apply ST_PlusConstConst. apply multi_R. apply ST_PlusConstConst. Qed. (** **** Exercises: ***) Lemma test_multistep_2: C 3 ==>* C 3. Proof. (* FILL IN HERE *) Admitted. (** [] *) Lemma test_multistep_3: P (C 0) (C 3) ==>* P (C 0) (C 3). Proof. (* FILL IN HERE *) Admitted. (** [] *) Lemma test_multistep_4: P (C 0) (P (C 2) (P (C 0) (C 3))) ==>* P (C 0) (C (2 + (0 + 3))). Proof. (* FILL IN HERE *) Admitted. (* ########################################################### *) (** ** Normal Forms Again *) (** If [t] reduces to [t'] in zero or more steps and [t'] is a normal form, we say that "[t'] is a normal form of [t]." *) Definition step_normal_form := normal_form step. Definition normal_form_of (t t' : tm) := (t ==>* t' /\ step_normal_form t'). (** Notice: - single-step reduction is deterministic - so, if [t] can reach a normal form, then this normal form is unique - so we can pronounce [normal_form t t'] as "[t'] is _the_ normal form of [t]." *) (** Indeed, something stronger is true (for this language): - the reduction of _any_ term [t] will eventually reach a normal form - i.e., [normal_form_of] is a _total_ function Formally, we say the [step] relation is _normalizing_. *) Definition normalizing {X:Type} (R:relation X) := forall t, exists t', (multi R) t t' /\ normal_form R t'. (** To prove that [step] is normalizing, we need a couple of lemmas. First, we observe that, if [t] reduces to [t'] in many steps, then the same sequence of reduction steps within [t] is also possible when [t] appears as the left-hand child of a [P] node, and similarly when [t] appears as the right-hand child of a [P] node whose left-hand child is a value. *) Lemma multistep_congr_1 : forall t1 t1' t2, t1 ==>* t1' -> P t1 t2 ==>* P t1' t2. Proof. intros t1 t1' t2 H. multi_cases (induction H) Case. Case "multi_refl". apply multi_refl. Case "multi_step". apply multi_step with (P y t2). apply ST_Plus1. apply H. apply IHmulti. Qed. Lemma multistep_congr_2 : forall t1 t2 t2', value t1 -> t2 ==>* t2' -> P t1 t2 ==>* P t1 t2'. Proof. (* FILL IN HERE *) Admitted. (** _Theorem_: The [step] function is normalizing -- i.e., for every [t] there exists some [t'] such that [t] steps to [t'] and [t'] is a normal form. _Proof sketch_: By induction on terms. There are two cases to consider: - [t = C n] for some [n]. Here [t] doesn't take a step, and we have [t' = t]. We can derive the left-hand side by reflexivity and the right-hand side by observing (a) that values are normal forms (by [nf_same_as_value]) and (b) that [t] is a value (by [v_const]). - [t = P t1 t2] for some [t1] and [t2]. By the IH, [t1] and [t2] have normal forms [t1'] and [t2']. Recall that normal forms are values (by [nf_same_as_value]); we know that [t1' = C n1] and [t2' = C n2], for some [n1] and [n2]. We can combine the [==>*] derivations for [t1] and [t2] to prove that [P t1 t2] reduces in many steps to [C (n1 + n2)]. It is clear that our choice of [t' = C (n1 + n2)] is a value, which is in turn a normal form. [] *) Theorem step_normalizing : normalizing step. Proof. unfold normalizing. tm_cases (induction t) Case. Case "C". exists (C n). split. SCase "l". apply multi_refl. SCase "r". (* We can use [rewrite] with "iff" statements, not just equalities: *) rewrite nf_same_as_value. apply v_const. Case "P". inversion IHt1 as [t1' H1]; clear IHt1. inversion IHt2 as [t2' H2]; clear IHt2. inversion H1 as [H11 H12]; clear H1. inversion H2 as [H21 H22]; clear H2. rewrite nf_same_as_value in H12. rewrite nf_same_as_value in H22. inversion H12 as [n1]. inversion H22 as [n2]. rewrite <- H in H11. rewrite <- H0 in H21. exists (C (n1 + n2)). split. SCase "l". apply multi_trans with (P (C n1) t2). apply multistep_congr_1. apply H11. apply multi_trans with (P (C n1) (C n2)). apply multistep_congr_2. apply v_const. apply H21. apply multi_R. apply ST_PlusConstConst. SCase "r". rewrite nf_same_as_value. apply v_const. Qed. (* ########################################################### *) (** ** Equivalence of Big-Step and Small-Step Reduction *) (** Having defined the operational semantics of our tiny programming language in two different styles, it makes sense to ask whether these definitions actually define the same thing! They do, though it takes a little work to show it. (The details are left as an exercise). *) Theorem eval__multistep : forall t n, t || n -> t ==>* C n. (** The key idea behind the proof comes from the following picture: P t1 t2 ==> (by ST_Plus1) P t1' t2 ==> (by ST_Plus1) P t1'' t2 ==> (by ST_Plus1) ... P (C n1) t2 ==> (by ST_Plus2) P (C n1) t2' ==> (by ST_Plus2) P (C n1) t2'' ==> (by ST_Plus2) ... P (C n1) (C n2) ==> (by ST_PlusConstConst) C (n1 + n2) That is, the multistep reduction of a term of the form [P t1 t2] proceeds in three phases: - First, we use [ST_Plus1] some number of times to reduce [t1] to a normal form, which must (by [nf_same_as_value]) be a term of the form [C n1] for some [n1]. - Next, we use [ST_Plus2] some number of times to reduce [t2] to a normal form, which must again be a term of the form [C n2] for some [n2]. - Finally, we use [ST_PlusConstConst] one time to reduce [P (C n1) (C n2)] to [C (n1 + n2)]. *) Proof. (* FILL IN HERE *) Admitted. (** For the other direction, we need one lemma, which establishes a relation between single-step reduction and big-step evaluation. *) Lemma step__eval : forall t t' n, t ==> t' -> t' || n -> t || n. Proof. intros t t' n Hs. generalize dependent n. (* FILL IN HERE *) Admitted. (** The fact that small-step reduction implies big-step is now straightforward to prove, once it is stated correctly. The proof proceeds by induction on the multip-step reduction sequence that is buried in the hypothesis [normal_form_of t t']. *) Theorem multistep__eval : forall t t', normal_form_of t t' -> exists n, t' = C n /\ t || n. Proof. (* FILL IN HERE *) Admitted. (* ########################################################### *) (** * Small-Step Imp *) (** For a more serious example, here is the small-step version of the Imp operational semantics. *) Inductive aval : aexp -> Prop := av_num : forall n, aval (ANum n). Reserved Notation " t '/' st '==>a' t' " (at level 40, st at level 39). Inductive astep : state -> aexp -> aexp -> Prop := | AS_Id : forall st i, AId i / st ==>a ANum (st i) | AS_Plus : forall st n1 n2, APlus (ANum n1) (ANum n2) / st ==>a ANum (n1 + n2) | AS_Plus1 : forall st a1 a1' a2, a1 / st ==>a a1' -> (APlus a1 a2) / st ==>a (APlus a1' a2) | AS_Plus2 : forall st v1 a2 a2', aval v1 -> a2 / st ==>a a2' -> (APlus v1 a2) / st ==>a (APlus v1 a2') | AS_Minus : forall st n1 n2, (AMinus (ANum n1) (ANum n2)) / st ==>a (ANum (minus n1 n2)) | AS_Minus1 : forall st a1 a1' a2, a1 / st ==>a a1' -> (AMinus a1 a2) / st ==>a (AMinus a1' a2) | AS_Minus2 : forall st v1 a2 a2', aval v1 -> a2 / st ==>a a2' -> (AMinus v1 a2) / st ==>a (AMinus v1 a2') | AS_Mult : forall st n1 n2, (AMult (ANum n1) (ANum n2)) / st ==>a (ANum (mult n1 n2)) | AS_Mult1 : forall st a1 a1' a2, a1 / st ==>a a1' -> (AMult (a1) (a2)) / st ==>a (AMult (a1') (a2)) | AS_Mult2 : forall st v1 a2 a2', aval v1 -> a2 / st ==>a a2' -> (AMult v1 a2) / st ==>a (AMult v1 a2') where " t '/' st '==>a' t' " := (astep st t t'). Reserved Notation " t '/' st '==>b' t' " (at level 40, st at level 39). Inductive bstep : state -> bexp -> bexp -> Prop := | BS_Eq : forall st n1 n2, (BEq (ANum n1) (ANum n2)) / st ==>b (if (beq_nat n1 n2) then BTrue else BFalse) | BS_Eq1 : forall st a1 a1' a2, a1 / st ==>a a1' -> (BEq a1 a2) / st ==>b (BEq a1' a2) | BS_Eq2 : forall st v1 a2 a2', aval v1 -> a2 / st ==>a a2' -> (BEq v1 a2) / st ==>b (BEq v1 a2') | BS_LtEq : forall st n1 n2, (BLe (ANum n1) (ANum n2)) / st ==>b (if (ble_nat n1 n2) then BTrue else BFalse) | BS_LtEq1 : forall st a1 a1' a2, a1 / st ==>a a1' -> (BLe a1 a2) / st ==>b (BLe a1' a2) | BS_LtEq2 : forall st v1 a2 a2', aval v1 -> a2 / st ==>a a2' -> (BLe v1 a2) / st ==>b (BLe v1 (a2')) | BS_NotTrue : forall st, (BNot BTrue) / st ==>b BFalse | BS_NotFalse : forall st, (BNot BFalse) / st ==>b BTrue | BS_NotStep : forall st b1 b1', b1 / st ==>b b1' -> (BNot b1) / st ==>b (BNot b1') | BS_AndTrueTrue : forall st, (BAnd BTrue BTrue) / st ==>b BTrue | BS_AndTrueFalse : forall st, (BAnd BTrue BFalse) / st ==>b BFalse | BS_AndFalse : forall st b2, (BAnd BFalse b2) / st ==>b BFalse | BS_AndTrueStep : forall st b2 b2', b2 / st ==>b b2' -> (BAnd BTrue b2) / st ==>b (BAnd BTrue b2') | BS_AndStep : forall st b1 b1' b2, b1 / st ==>b b1' -> (BAnd b1 b2) / st ==>b (BAnd b1' b2) where " t '/' st '==>b' t' " := (bstep st t t'). (** The semantics of commands is the interesting part. We need two small tricks to make it work: - We use [SKIP] as a "command value" -- i.e., a command that has reached a normal form. - An assignment command reduces to [SKIP] (and an updated state). - The sequencing command waits until its left-hand subcommand has reduced to [SKIP], then throws it away so that reduction can continue with the right-hand subcommand. - We reduce a [WHILE] command by transforming it into a conditional followed by the same [WHILE]. *) Reserved Notation " t '/' st '==>' t' '/' st' " (at level 40, st at level 39, t' at level 39). Inductive cstep : (com * state) -> (com * state) -> Prop := | CS_AssStep : forall st i a a', a / st ==>a a' -> (i ::= a) / st ==> (i ::= a') / st | CS_Ass : forall st i n, (i ::= (ANum n)) / st ==> SKIP / (update st i n) | CS_SeqStep : forall st c1 c1' st' c2, c1 / st ==> c1' / st' -> (c1 ; c2) / st ==> (c1' ; c2) / st' | CS_SeqFinish : forall st c2, (SKIP ; c2) / st ==> c2 / st | CS_IfTrue : forall st c1 c2, IFB BTrue THEN c1 ELSE c2 FI / st ==> c1 / st | CS_IfFalse : forall st c1 c2, IFB BFalse THEN c1 ELSE c2 FI / st ==> c2 / st | CS_IfStep : forall st b b' c1 c2, b / st ==>b b' -> IFB b THEN c1 ELSE c2 FI / st ==> (IFB b' THEN c1 ELSE c2 FI) / st | CS_While : forall st b c1, (WHILE b DO c1 END) / st ==> (IFB b THEN (c1; (WHILE b DO c1 END)) ELSE SKIP FI) / st where " t '/' st '==>' t' '/' st' " := (cstep (t,st) (t',st')). (* ########################################################### *) (** * Concurrent Imp *) (** Finally, let's define a _concurrent_ extension of Imp, to show off the power of our new tools... *) Module CImp. Inductive com : Type := | CSkip : com | CAss : id -> aexp -> com | CSeq : com -> com -> com | CIf : bexp -> com -> com -> com | CWhile : bexp -> com -> com (* New: *) | CPar : com -> com -> com. Tactic Notation "com_cases" tactic(first) ident(c) := first; [ Case_aux c "SKIP" | Case_aux c "::=" | Case_aux c ";" | Case_aux c "IFB" | Case_aux c "WHILE" | Case_aux c "PAR" ]. Notation "'SKIP'" := CSkip. Notation "x '::=' a" := (CAss x a) (at level 60). Notation "c1 ; c2" := (CSeq c1 c2) (at level 80, right associativity). Notation "'WHILE' b 'DO' c 'END'" := (CWhile b c) (at level 80, right associativity). Notation "'IFB' b 'THEN' c1 'ELSE' c2 'FI'" := (CIf b c1 c2) (at level 80, right associativity). Notation "'PAR' c1 'WITH' c2 'END'" := (CPar c1 c2) (at level 80, right associativity). Inductive cstep : (com * state) -> (com * state) -> Prop := (* Old part *) | CS_AssStep : forall st i a a', a / st ==>a a' -> (i ::= a) / st ==> (i ::= a') / st | CS_Ass : forall st i n, (i ::= (ANum n)) / st ==> SKIP / (update st i n) | CS_SeqStep : forall st c1 c1' st' c2, c1 / st ==> c1' / st' -> (c1 ; c2) / st ==> (c1' ; c2) / st' | CS_SeqFinish : forall st c2, (SKIP ; c2) / st ==> c2 / st | CS_IfTrue : forall st c1 c2, (IFB BTrue THEN c1 ELSE c2 FI) / st ==> c1 / st | CS_IfFalse : forall st c1 c2, (IFB BFalse THEN c1 ELSE c2 FI) / st ==> c2 / st | CS_IfStep : forall st b b' c1 c2, b /st ==>b b' -> (IFB b THEN c1 ELSE c2 FI) / st ==> (IFB b' THEN c1 ELSE c2 FI) / st | CS_While : forall st b c1, (WHILE b DO c1 END) / st ==> (IFB b THEN (c1; (WHILE b DO c1 END)) ELSE SKIP FI) / st (* New part: *) | CS_Par1 : forall st c1 c1' c2 st', c1 / st ==> c1' / st' -> (PAR c1 WITH c2 END) / st ==> (PAR c1' WITH c2 END) / st' | CS_Par2 : forall st c1 c2 c2' st', c2 / st ==> c2' / st' -> (PAR c1 WITH c2 END) / st ==> (PAR c1 WITH c2' END) / st' | CS_ParDone : forall st, (PAR SKIP WITH SKIP END) / st ==> SKIP / st where " t '/' st '==>' t' '/' st' " := (cstep (t,st) (t',st')). Definition cmultistep := multi cstep. Notation " t '/' st '==>*' t' '/' st' " := (multi cstep (t,st) (t',st')) (at level 40, st at level 39, t' at level 39). (** *** *) (* QUIZ *) (** Which state cannot be obtained as a result of executing the following program? PAR Y ::= ANum 1; WITH Y ::= Y+1; END; X ::= Y. (1) Y=1; X=1 (2) Y=0; X=1 (3) Y=n; X=n (4) None of the above *) (* /QUIZ *) (* QUIZ *) (** How about this one? PAR Y ::= ANum 0; X ::= Y+1 WITH Y ::= Y+1; X ::= ANum 1 END. (1) Y=0; X=1 (2) Y=1; X=1 (3) Y=0; X=0 (4) None of the above *) (* /QUIZ *) (** *** *) (** Among the many interesting properties of this language is the fact that the following program can terminate with the variable [X] set to any value... *) Definition par_loop : com := PAR Y ::= ANum 1 WITH WHILE BEq (AId Y) (ANum 0) DO X ::= APlus (AId X) (ANum 1) END END. (** In particular, it can terminate with [X] set to [0]: *) Example par_loop_example_0: exists st', par_loop / empty_state ==>* SKIP / st' /\ st' X = 0. Proof. eapply ex_intro. split. unfold par_loop. eapply multi_step. apply CS_Par1. apply CS_Ass. eapply multi_step. apply CS_Par2. apply CS_While. eapply multi_step. apply CS_Par2. apply CS_IfStep. apply BS_Eq1. apply AS_Id. eapply multi_step. apply CS_Par2. apply CS_IfStep. apply BS_Eq. simpl. eapply multi_step. apply CS_Par2. apply CS_IfFalse. eapply multi_step. apply CS_ParDone. eapply multi_refl. reflexivity. Qed. (** It can also terminate with [X] set to [2]: *) Example par_loop_example_2: exists st', par_loop / empty_state ==>* SKIP / st' /\ st' X = 2. Proof. eapply ex_intro. split. eapply multi_step. apply CS_Par2. apply CS_While. eapply multi_step. apply CS_Par2. apply CS_IfStep. apply BS_Eq1. apply AS_Id. eapply multi_step. apply CS_Par2. apply CS_IfStep. apply BS_Eq. simpl. eapply multi_step. apply CS_Par2. apply CS_IfTrue. eapply multi_step. apply CS_Par2. apply CS_SeqStep. apply CS_AssStep. apply AS_Plus1. apply AS_Id. eapply multi_step. apply CS_Par2. apply CS_SeqStep. apply CS_AssStep. apply AS_Plus. eapply multi_step. apply CS_Par2. apply CS_SeqStep. apply CS_Ass. eapply multi_step. apply CS_Par2. apply CS_SeqFinish. eapply multi_step. apply CS_Par2. apply CS_While. eapply multi_step. apply CS_Par2. apply CS_IfStep. apply BS_Eq1. apply AS_Id. eapply multi_step. apply CS_Par2. apply CS_IfStep. apply BS_Eq. simpl. eapply multi_step. apply CS_Par2. apply CS_IfTrue. eapply multi_step. apply CS_Par2. apply CS_SeqStep. apply CS_AssStep. apply AS_Plus1. apply AS_Id. eapply multi_step. apply CS_Par2. apply CS_SeqStep. apply CS_AssStep. apply AS_Plus. eapply multi_step. apply CS_Par2. apply CS_SeqStep. apply CS_Ass. eapply multi_step. apply CS_Par1. apply CS_Ass. eapply multi_step. apply CS_Par2. apply CS_SeqFinish. eapply multi_step. apply CS_Par2. apply CS_While. eapply multi_step. apply CS_Par2. apply CS_IfStep. apply BS_Eq1. apply AS_Id. eapply multi_step. apply CS_Par2. apply CS_IfStep. apply BS_Eq. simpl. eapply multi_step. apply CS_Par2. apply CS_IfFalse. eapply multi_step. apply CS_ParDone. eapply multi_refl. reflexivity. Qed. Lemma par_body_n__Sn : forall n st, st X = n /\ st Y = 0 -> par_loop / st ==>* par_loop / (update st X (S n)). Proof. (* FILL IN HERE *) Admitted. (** [] *) Lemma par_body_n : forall n st, st X = 0 /\ st Y = 0 -> exists st', par_loop / st ==>* par_loop / st' /\ st' X = n /\ st' Y = 0. Proof. (* FILL IN HERE *) Admitted. (** [] *) (** ... the above loop can exit with [X] having any value whatsoever. *) Theorem par_loop_any_X: forall n, exists st', par_loop / empty_state ==>* SKIP / st' /\ st' X = n. Proof. intros n. destruct (par_body_n n empty_state). split; unfold update; reflexivity. rename x into st. inversion H as [H' [HX HY]]; clear H. exists (update st Y 1). split. eapply multi_trans with (par_loop,st). apply H'. eapply multi_step. apply CS_Par1. apply CS_Ass. eapply multi_step. apply CS_Par2. apply CS_While. eapply multi_step. apply CS_Par2. apply CS_IfStep. apply BS_Eq1. apply AS_Id. rewrite update_eq. eapply multi_step. apply CS_Par2. apply CS_IfStep. apply BS_Eq. simpl. eapply multi_step. apply CS_Par2. apply CS_IfFalse. eapply multi_step. apply CS_ParDone. apply multi_refl. rewrite update_neq. assumption. reflexivity. Qed. End CImp.