(** * Simple imperative programs Version of 2/25/2009 Please include the pennkey of every member of your group (* FILL IN HERE *) *) Require Export Logicsol. (* ------------------------------------------------------- *) (** * Informal proofs, again *) (* Q: What is the relation between a formal proof of a proposition P and an informal proof of the same proposition P? A: The latter should *teach* the reader how to produce the former. Q: How much detail is needed? A: There is no single right answer; rather, there is a range of choices. At one end of the spectrum, we can essentially give the reader the whole formal proof (i.e., the informal proof amounts to just transcribing the formal one into words). This gives the reader the *ability* to reproduce the formal one for themselves, but it doesn't *teach* them anything. At the other end of the spectrum, we can say "The theorem is true and you can figure out why for yourself if you think about it hard enough." This is also not a good teaching strategy, because usually writing the proof requires some deep insights into the thing we're proving, and most readers will give up before they rediscover all the same insights as we did. In the middle is the golden mean -- a proof that includes all of the essential insights (saving the reader the hard part of work that we went through to find the proof in the first place) and clear high-level suggestions for the more routine parts to save the reader from spending too much time reconstructing these parts (e.g., what the IH says and what must be shown in each case of an inductive proof), but not so much detail that the main ideas are obscured. ----------------- Another key point: if we're talking about a formal proof of a proposition P and an informal proof of P, the proposition P doesn't change. That is, formal and informal proofs are TALKING ABOUT THE SAME WORLD and they must PLAY BY THE SAME RULES. In particular, whether we are talking about formal or informal proofs, propositions and booleans are different things! * Booleans are VALUES in the COMPUTATIONAL world. Every expression of type [bool] (with no free variables) can be simplified to either [true] or [false]. * Propositions are TYPES in the LOGICAL world. They are either PROVABLE (i.e., there is some expression that has this type) or not (there is no such expression). It doesn't make sense to say that a proposition is "equivalent to [true]," and it is not necessarily the case that, if a proposition [P] is not provable, then [~P] is provable. We do sometimes use the words "true" and "false" when referring to propositions. Strictly speaking, we should not: a proposition is either provable or it is not. *) (* ------------------------------------------------------- *) (** * Templates for informal proofs by induction *) (* In the real world of mathematical communication, written proofs range from extremely longwinded and pedantic to extremely brief and telegraphic. The ideal is probably somewhere in between, but while you are getting used to the style it is better to go more toward the pedantic end. Also, during the learning phase, it is probably helpful to have a clear standard to compare against. So... For the rest of the course, ALL your inductive proofs should match one of the two following templates. 1) TEMPLATE FOR INFORMAL PROOFS BY INDUCTION OVER AN INDUCTIVELY DEFINED SET: THEOREM: PROOF: By induction on n. * Suppose n = c a1 ... ak, where <...and here we state the IH for each of the a's that has type S, if any>. We must show <...and here we restate P(c a1 ... ak)>. * [] EXAMPLE THEOREM: For all sets X, lists l : list X, and numbers n, if length l = n then index (S n) l = None. PROOF: By induction on l. * Suppose l = []. We must show, for all numbers n, that, if length [] = n, then index (S n) [] = None. This follows immediately from the definition of index. * Suppose l = x :: l' for some x and l', where length l' = n' implies index (S n') l' = None, for any number n'. We must show, for all n, that, if length (x::l') = n then index (S n) (x::l') = None. Let n be a number with length l = n. Since length l = length (x::l') = S (length l'), it suffices to show that index (S (length l')) l' = None. But this follows directly from the induction hypothesis, picking n' to be length l'. [] 2) TEMPLATE FOR INFORMAL PROOFS BY INDUCTION OVER AN INDUCTIVELY DEFINED PROPOSITION (I.E., "INDUCTION ON DERIVATIONS"): THEOREM: P," where Q is some inductively defined proposition. (More generally, "For all x y z, (Q x y z) -> (P x y z),"> PROOF: By induction on a derivation of Q. * Suppose the final rule used to show Q is c. Then <...and here we state the types of all of the a's together with any equalities that follow from the definition of the constructor and the IH for each of the a's that has type Q, if there are any>. We must show <...and here we restate P>. * [] EXAMPLE THEOREM: The <= relation is transitive -- i.e., for all numbers n, m, and o, if n <= m and m <= o, then n <= o. PROOF: By induction on a derivation of m <= o. * Suppose the final rule used to show m <= o is le_n. Then m = o and the result is immediate. * Suppose the final rule used to show m <= o is le_S. Then o = S o' for some o' with m <= o'. By induction hypothesis, n <= o'. But then, by le_S, n <= o. [] *) (* ------------------------------------------------------- *) (* ------------------------------------------------------- *) (* ------------------------------------------------------- *) (** * Evaluating arithmetic expressions *) Module AExp. Inductive aexp : Set := | ANum : nat -> aexp | APlus : aexp -> aexp -> aexp | AMinus : aexp -> aexp -> aexp | AMult : aexp -> aexp -> aexp. Definition two_plus_two := APlus (ANum 2) (ANum 2). (* Since we're going to be writing a lot of these arithmetic expressions, let's introduce some concrete syntax that's nicer to look at. *) Notation "a1 '+++' a2" := (APlus a1 a2) (at level 50). Notation "a1 '---' a2" := (AMinus a1 a2) (at level 50). Notation "a1 '***' a2" := (AMult a1 a2) (at level 40). Notation A0 := (ANum 0). Notation A1 := (ANum 1). Notation A2 := (ANum 2). Notation A3 := (ANum 3). Notation A4 := (ANum 4). Notation A5 := (ANum 5). Definition two_plus_two' := A2 +++ A2. Fixpoint aeval (e : aexp) {struct e} : nat := match e with | ANum n => n | APlus a1 a2 => plus (aeval a1) (aeval a2) | AMinus a1 a2 => minus (aeval a1) (aeval a2) | AMult a1 a2 => mult (aeval a1) (aeval a2) end. Example test_aeval1: aeval two_plus_two = 4. Proof. reflexivity. Qed. Inductive bexp : Set := | BTrue : bexp | BFalse : bexp | BEq : aexp -> aexp -> bexp | BLtEq : aexp -> aexp -> bexp | BNot : bexp -> bexp | BAnd : bexp -> bexp -> bexp | BOr : bexp -> bexp -> bexp. Fixpoint beval (e : bexp) {struct e} : bool := match e with | BTrue => true | BFalse => false | BEq a1 a2 => beq_nat (aeval a1) (aeval a2) | BLtEq a1 a2 => ble_nat (aeval a1) (aeval a2) | BNot b1 => negb (beval b1) | BAnd b1 b2 => andb (beval b1) (beval b2) | BOr b1 b2 => orb (beval b1) (beval b2) end. Notation "b1 '===' b2" := (BEq b1 b2) (at level 60). Notation "b1 '<<=' b2" := (BLtEq b1 b2) (at level 60). (* ------------------------------------------------------- *) (** * Correctness of a simple optimization *) Fixpoint optimize_0plus (e:aexp) {struct e} : aexp := match e with | ANum n => ANum n | APlus (ANum 0) e2 => optimize_0plus e2 | APlus e1 e2 => APlus (optimize_0plus e1) (optimize_0plus e2) | AMinus e1 e2 => AMinus (optimize_0plus e1) (optimize_0plus e2) | AMult e1 e2 => AMult (optimize_0plus e1) (optimize_0plus e2) end. Example test_optimize_0plus: optimize_0plus (A2 +++ (A0 +++ (A0 +++ A1))) = A2 +++ A1. Proof. reflexivity. Qed. Theorem optimize_0plus_sound: forall e, aeval (optimize_0plus e) = aeval e. Proof. intros e. induction e. Case "ANum". reflexivity. Case "APlus". destruct e1. SCase "e1 = ANum n". destruct n. SSCase "n = 0". simpl. apply IHe2. SSCase "n <> 0". simpl. rewrite IHe2. reflexivity. SCase "e1 = APlus e1_1 e1_2". simpl. simpl in IHe1. rewrite IHe1. rewrite IHe2. reflexivity. SCase "e1 = AMinus e1_1 e1_2". simpl. simpl in IHe1. rewrite IHe1. rewrite IHe2. reflexivity. SCase "e1 = AMult e1_1 e1_2". simpl. simpl in IHe1. rewrite IHe1. rewrite IHe2. reflexivity. Case "AMinus". simpl. rewrite IHe1. rewrite IHe2. reflexivity. Case "AMult". simpl. rewrite IHe1. rewrite IHe2. reflexivity. Qed. (* ------------------------------------------------------- *) (* ------------------------------------------------------- *) (* ------------------------------------------------------- *) (** * Tacticals *) (* The repetition in this last proof is starting to be a little annoying. It's still bearable here, but clearly, if either the language of arithmetic expressions or the optimization being proved sound were significantly more complex, it would start to be a real problem. So far, we've been doing all our proofs using just a small handful of Coq's tactics and completely ignoring its very powerful facilities for constructing proofs automatically. This section introduces some of these facilities, and we will see more over the next several chapters. Getting used to them will take some energy -- Coq's automation is a power tool -- but it will allow us to scale up our efforts to more complex definitions and more interesting properties without becoming overwhelmed by boring, repetitive, or low-level details. *) (* ------------------------------------------------------- *) (** ** The [try] tactical *) (* "Tactical" is Coq's term for operations that manipulate tactics as data -- higher-order tactics, if you will. *) (* One very simple tactical is [try]: If [T] is a tactic, then [try T] is a tactic that is just like [T] except that, if [T] fails, [try T] does nothing at all (instead of failing). *) (* ------------------------------------------------------- *) (** ** The [;] tactical *) (* Another very basic tactical is written [;]. If [T], [T1], ..., [Tn] are tactics, then T; [T1 | T2 | ... | Tn] is a tactic that first performs [T] and then performs [T1] on the first subgoal generated by [T], performs [T2] on the second subgoal, etc. In the special case where all of the [Ti]s are the same tactic [T'], we can just write [T;T'] instead of: T; [T' | T' | ... | T'] That is, if [T] and [T'] are tactics, then [T;T'] is a tactic that first performs [T] and then performs [T'] on EACH SUBGOAL generated by [T]. This is the form of [;] that is used most often in practice. *) (* Using [try] and [;] together, we can get rid of the repetition in the above proof. *) Theorem optimize_0plus_sound': forall e, aeval (optimize_0plus e) = aeval e. Proof. intros e. induction e; (* Most cases follow directly by the IH *) try (simpl; rewrite IHe1; rewrite IHe2; reflexivity). Case "ANum". reflexivity. Case "APlus". destruct e1; (* Most cases follow directly by the IH *) try (simpl; simpl in IHe1; rewrite IHe1; rewrite IHe2; reflexivity). (* The interesting case is when e1 = ANum n *) SCase "e1 = ANum n". destruct n. SSCase "n = 0". apply IHe2. SSCase "n <> 0". simpl. rewrite IHe2. reflexivity. Qed. (* In practice, Coq experts often use [try] with a tactic like [induction] to take care of many similar "straightforward" cases all at once. Naturally, this practice has an analog in informal proofs. Here is an informal proof of our example theorem that matches the structure of the formal one: THEOREM: For all arithmetic expressions e, aeval (optimize_0plus e) = aeval e. PROOF: By induction on e. The AMinus and AMult cases follow directly from the IH. The remaining cases are as follows: * Suppose e = ANum n for some n. We must show aeval (optimize_0plus (ANum n)) = aeval (ANum n). This is immediate from the definition of optimize_0plus. * Suppose e = APlus e1 e2 for some e1 and e2. We must show aeval (optimize_0plus (APlus e1 e2)) = aeval (APlus e1 e2). Consider the possible forms of e1. For most of them, optimize_0plus simply calls itself recursively for the subexpressions and rebuilds a new expression of the same form as e1; in these cases, the result follows directly from the IH. The interesting case is when e1 = ANum n for some n. If n = ANum 0, then optimize_0plus (APlus e1 e2) = optimize_0plus e2 and the IH for e2 is exactly what we need. On the other hand, if n = S n' for some n', then again optimize_0plus simply calls itself recursively, and the result follows from the IH. [] This proof can still be improved: the first case (for e = ANum n) is very trivial -- even more trivial than the cases that we said simply followed from the IH -- yet we have chosen to write it out in full. It would be better and clearer to drop it and just say, at the top, "Most cases are either immediate or direct from the IH. The only interesting case is the one for APlus..." Of course, we'd like to do the same thing in our formal proof too! Here's how this looks: *) Theorem optimize_0plus_sound'': forall e, aeval (optimize_0plus e) = aeval e. Proof. intros e. induction e; (* Most cases follow directly by the IH *) try (simpl; rewrite IHe1; rewrite IHe2; reflexivity); (* ... or are immediate by definition *) try (reflexivity). (* The interesting case is when e = APlus (ANum 0) e2. *) Case "APlus". destruct e1; try (simpl; simpl in IHe1; rewrite IHe1; rewrite IHe2; reflexivity). SCase "e1 = ANum n". destruct n. SSCase "n = 0". apply IHe2. SSCase "n <> 0". simpl. rewrite IHe2. reflexivity. Qed. (* ------------------------------------------------------- *) (** ** Defining new tactic notations *) (* Coq also provides some handy ways to define "shorthand tactics" that, when invoked, apply several tactics at the same time. *) Tactic Notation "simpl_and_try" tactic(c) := simpl; try c. (* Here's a more interesting use of this feature... *) (* ------------------------------------------------------- *) (** ** Bulletproofing case analyses *) (* Being able to deal with most of the cases of an [induction] or [destruct] all at the same time is very convenient, but it can also be a little confusing. One problem that often comes up is that MAINTAINING proofs written in this style can be difficult. For example, suppose that, later, we extended the definition of [aexp] with another constructor that also required a special argument. The above proof might break because Coq generated the subgoals for this constructor before the one for APlus, so that, at the point when we start working on the [APlus] case, Coq is actually expecting the argument for a completely different constructor. What we'd like is to get a sensible error message saying "I was expecting the [AFoo] case at this point, but the proof script is talking about [APlus]." Here's a nice little trick that smoothly achieves this. *) Tactic Notation "aexp_cases" tactic(first) tactic(c) := first; [ c "ANum" | c "APlus" | c "AMinus" | c "AMult" ]. (* If [e] is a variable of type [aexp], then doing aexp_cases (induction e) (Case) will perform an induction on [e] (the same as if we had just typed [induction e]) and ALSO add a "Case" tag to each subgoal labeling which constructor it comes from. *) (* Exercise: 3 stars (optimize_0plus_b) *) (* Since the optimize_0plus tranformation doesn't change the value of aexps, we should be able to apply it to all the aexps that appear in a bexp without changing the bexp's value. Write a function which performs that transformation on bexps, and prove it is sound. Use the tacticals we've just seen to make the proof as elegant as possible. *) (* FILL IN HERE *) (* Exercise: 4 stars (optimizer) *) (* DESIGN EXERCISE: The optimization implemented by our optimize_0plus function is only one of many imaginable optimizations on arithmetic and boolean expressions. Write a more sophisticated optimizer and prove it correct. FILL IN HERE *) End AExp. (* ------------------------------------------------------- *) (** * A couple more handy tactics *) (* clear H remove hypothesis H from the context subst x find an assumption [x = e] or [e = x] in the context, replace x with e throughout the context and current goal, and clear the assumption subst substitute away ALL assumptions of the form [x = e] or [e = x] assumption tries to find a hypothesis [H] in the context that exactly matches the goal; if one is found, behaves just like [apply H] *) (* We'll see many examples of these in the proofs below... *) (* ------------------------------------------------------- *) (* ------------------------------------------------------- *) (* ------------------------------------------------------- *) (** * While programs *) (* ----------------------------------------------------- *) (** ** Mappings *) (* In the rest of the course, we'll often need to talk about "identifiers," such as program variables. We could use strings for this, or (as in a real compiler) some kind of fancier structures like symbols from a symbol table. For simplicity, though, let's just use natural numbers as identifiers. *) Definition id := nat. (* Now, a [mapping] is a partial function from identifiers to members of some other type, [X]. We use an [option] in the result type to represent partiality: A result of [None] means that the mapping is not defined for the given id. *) Definition mapping (X : Set) := id -> option X. Definition lookup (X : Set) (k : id) (f : mapping X) : option X := f k. Implicit Arguments lookup [X]. Definition empty_mapping (X:Set) : (mapping X) := constfun None. Definition extend (X : Set) (f : mapping X) (k:id) (x:X) := override f k (Some x). Implicit Arguments extend [X]. Definition remove (X : Set) (f : mapping X) (k:id) := override f k None. Implicit Arguments remove [X]. (* Since the critical functions on mappings, [extend] and [remove], are implemented in terms of the [override] operator that we studied before, their properties can also be derived from those of [override]. *) Theorem extend_eq : forall X x x' k (f : mapping X), x = x' -> lookup k (extend f k x) = Some x'. Proof. intros X x x' k f Heq. rewrite Heq. unfold lookup, extend. apply override_eq. Qed. (* Exercise: 2 stars *) Theorem extend_neq : forall X o1 x2 k1 k2 (f : mapping X), lookup k1 f = o1 -> beq_nat k2 k1 = false -> lookup k1 (extend f k2 x2) = o1. Proof. (* FILL IN HERE (and delete "Admitted") *) Admitted. (* Exercise: 2 stars, optional *) Theorem extend_example : forall (X:Set) (b:bool), lookup 3 (extend (empty_mapping _) 2 b) = None. Proof. (* Before starting to play with tactics, make sure you understand exactly what the theorem is saying! *) (* OPTIONAL EXERCISE *) Admitted. (* Exercise: 2 stars, optional *) Theorem extend_shadow : forall X x1 x2 k1 k2 (f : mapping X), lookup k1 (extend (extend f k2 x1) k2 x2) = lookup k1 (extend f k2 x2). Proof. (* OPTIONAL EXERCISE *) Admitted. (* Exercise: 2 stars, optional *) Theorem extend_same : forall X x1 k1 k2 (f : mapping X), lookup k1 f = Some x1 -> lookup k2 (extend f k1 x1) = lookup k2 f. Proof. (* OPTIONAL EXERCISE *) Admitted. (* Exercise: 2 stars, optional *) Theorem extend_permute : forall X x1 x2 k1 k2 k3 (f : mapping X), false = beq_nat k2 k1 -> lookup k3 (extend (extend f k2 x1) k1 x2) = lookup k3 (extend (extend f k1 x2) k2 x1). Proof. (* OPTIONAL EXERCISE *) Admitted. (* --------------------------------------------------- *) (** ** WHILE program syntax *) Definition state := (mapping nat). Definition empty_state := empty_mapping nat. (* Adding variables to what we had before *) Inductive aexp : Set := | ANum : nat -> aexp | AId : id -> aexp | APlus : aexp -> aexp -> aexp | AMinus : aexp -> aexp -> aexp | AMult : aexp -> aexp -> aexp. Tactic Notation "aexp_cases" tactic(first) tactic(c) := first; [ c "ANum" | c "AId" | c "APlus" | c "AMinus" | c "AMult" ]. (* Same notations as before... *) Notation A0 := (ANum 0). Notation A1 := (ANum 1). Notation A2 := (ANum 2). Notation A3 := (ANum 3). Notation A4 := (ANum 4). Notation A5 := (ANum 5). Notation A6 := (ANum 6). Notation "a1 '***' a2" := (AMult a1 a2) (at level 50). Notation "a1 '---' a2" := (AMinus a1 a2) (at level 40). Notation "a1 '+++' a2" := (APlus a1 a2) (at level 40). (* ...plus one more: *) Notation "'!' X" := (AId X) (at level 30). (* Shorthands for variables: *) Definition X : id := 0. Definition Y : id := 1. Definition Z : id := 2. (* Note that the choice of variable names (X, Y, Z) clashes a bit with our earlier use of uppercase letters for Sets. Since we're not using polymorphism heavily in this section, this overloading will hopefully not cause confusion. *) (* Same bexps as before (using the new aexps) *) Inductive bexp : Set := | BTrue : bexp | BFalse : bexp | BEq : aexp -> aexp -> bexp | BLtEq : aexp -> aexp -> bexp | BNot : bexp -> bexp | BAnd : bexp -> bexp -> bexp | BOr : bexp -> bexp -> bexp. Notation "b1 '===' b2" := (BEq b1 b2) (at level 60). Notation "b1 '<<=' b2" := (BLtEq b1 b2) (at level 60). Tactic Notation "bexp_cases" tactic(first) tactic(c) := first; [ c "BTrue" | c "BFalse" | c "BEq" | c "BLtEq" | c "BNot" | c "BAnd" | c "BOr" ]. Inductive com : Set := | CSkip : com | CAss : id -> aexp -> com | CSeq : com -> com -> com | CIf : bexp -> com -> com -> com | CWhile : bexp -> com -> com. Tactic Notation "com_cases" tactic(first) tactic(c) := first; [ c "CSkip" | c "CAss" | c "CSeq" | c "CIf" | c "CWhile" ]. Notation "'skip'" := CSkip. Notation "c1 ; c2" := (CSeq c1 c2) (at level 80, right associativity). Notation "l '::=' a" := (CAss l a) (at level 60). Notation "'while' b 'do' c" := (CWhile b c) (at level 80, right associativity). Notation "'testif' e1 'then' e2 'else' e3" := (CIf e1 e2 e3) (at level 80, right associativity). (* Note that [CIf] is written [testif...then...else...] to avoid confusion with Coq's existing [if...then...else...] syntactic sugar. *) (* ------------------------------------------------------- *) (* Some programs... *) Definition plus2 : com := X ::= !X +++ A2. (* Note that the notations we introduced make it easy to write down commands that look close to how they would in a real imperative programming language; for example, here's what [plus2] looks like fully expanded: *) Example plus2_notation : plus2 = CAss 0 (APlus (AId 0) (ANum 2)). Proof. reflexivity. Qed. Definition XtimesYinZ : com := Z ::= !X *** !Y. (* loops *) Definition subtract_slowly_body : com := Z ::= !Z --- A1; X ::= !X --- A1. Definition subtract_X_slowly : com := while BNot (!X === A0) do subtract_slowly_body. Definition subtract_3_from_5_slowly : com := X ::= A3; Z ::= A5; while BNot (!X === A0) do subtract_slowly_body. (* an infinite loop *) Definition loop : com := while BTrue do skip. (* factorial *) Definition fact_body : com := Z ::= !Z *** !X; X ::= !X --- A1. Definition pfactorial : com := while BLtEq A1 (!X) do fact_body. (* Note that pfactorial should be run in a state where Z is 1 We could enforce this with the following program: *) Definition pfactorial' : com := Z ::= ANum 1; pfactorial. (* exponentiation *) Definition exp_body : com := Z ::= !Z *** !X; Y ::= !Y --- A1. Definition pexp : com := while BNot (!Y === (ANum 0)) do exp_body. (* Note that pexp should be run in a state where Z is 1 *) (* Exercise: 2 stars *) (* Write a While program that sums the numbers from 1 to X (inclusive: 1 + 2 + ... + X) in the variable Y. *) (* FILL IN HERE *) (* Exercise: 2 stars *) (* Write a While program that sets Z to 0 if X is even and sets Z to 1 otherwise. *) (* FILL IN HERE *) (* --------------------------------------------------- *) (** ** Evaluation *) Fixpoint aeval (st : state) (e : aexp) {struct e} : nat := match e with | ANum n => n | AId l => match lookup l st with | Some n => n | None => O end | APlus a1 a2 => plus (aeval st a1) (aeval st a2) | AMinus a1 a2 => minus (aeval st a1) (aeval st a2) | AMult a1 a2 => mult (aeval st a1) (aeval st a2) end. Fixpoint beval (st : state) (e : bexp) {struct e} : bool := match e with | BTrue => true | BFalse => false | BEq a1 a2 => beq_nat (aeval st a1) (aeval st a2) | BLtEq a1 a2 => ble_nat (aeval st a1) (aeval st a2) | BNot b1 => negb (beval st b1) | BAnd b1 b2 => andb (beval st b1) (beval st b2) | BOr b1 b2 => orb (beval st b1) (beval st b2) end. (* First try at an evaluator for commands, omitting CWhile *) Fixpoint ceval_step1 (st : state) (c : com) {struct c} : state := match c with | CSkip => st | CAss l a1 => extend st l (aeval st a1) | CSeq c1 c2 => let st' := ceval_step1 st c1 in ceval_step1 st' c2 | CIf b c1 c2 => if (beval st b) then ceval_step1 st c1 else ceval_step1 st c2 | CWhile b1 c1 => st (* bogus *) end. (* Second try, using an extra "step index" to ensure that evaluation always terminates *) Fixpoint ceval_step2 (st : state) (c : com) (i : nat) {struct i} : state := match i with | O => empty_state | S i' => match c with | CSkip => st | CAss l a1 => extend st l (aeval st a1) | CSeq c1 c2 => let st' := ceval_step2 st c1 i' in ceval_step2 st' c2 i' | CIf b c1 c2 => if (beval st b) then ceval_step2 st c1 i' else ceval_step2 st c2 i' | CWhile b1 c1 => if (beval st b1) then let st' := ceval_step2 st c1 i' in ceval_step2 st' (CWhile b1 c1) i' else st end end. (* NOTE: It is tempting to think that the index [i] here is counting the "number of steps of evaluation." But if you look closely you'll see that this is not the case: for example, in the [CSeq] rule, the same [i] is passed to both recursive calls. Understanding the exact way that [i] is treated will be important in the proof of [ceval__ceval_step], which is given as an exercise below. *) Definition bind_option (X Y : Set) (xo : option X) (f : X -> option Y) : option Y := match xo with | None => None | Some x => f x end. Implicit Arguments bind_option [X Y]. (* Third try, returning an [option state] instead of just a [state] so that we can distinguish between normal and abnormal termination. *) Fixpoint ceval_step (st : state) (c : com) (i : nat) {struct i} : option state := match i with | O => None | S i' => match c with | CSkip => Some st | CAss l a1 => Some (extend st l (aeval st a1)) | CSeq c1 c2 => bind_option (ceval_step st c1 i') (fun st' => ceval_step st' c2 i') | CIf b c1 c2 => if (beval st b) then ceval_step st c1 i' else ceval_step st c2 i' | CWhile b1 c1 => if (beval st b1) then bind_option (ceval_step st c1 i') (fun st' => ceval_step st' (CWhile b1 c1) i') else Some st end end. (* A better way: define [ceval] as a RELATION, rather than a (total) FUNCTION. *) Inductive ceval : state -> com -> state -> Prop := | CESkip : forall st, ceval st CSkip st | CEAss : forall st a1 n l, aeval st a1 = n -> ceval st (CAss l a1) (extend st l n) | CESeq : forall c1 c2 st st' st'', ceval st c1 st' -> ceval st' c2 st'' -> ceval st (CSeq c1 c2) st'' | CEIfTrue : forall st st' b1 c1 c2, beval st b1 = true -> ceval st c1 st' -> ceval st (CIf b1 c1 c2) st' | CEIfFalse : forall st st' b1 c1 c2, beval st b1 = false -> ceval st c2 st' -> ceval st (CIf b1 c1 c2) st' | CEWhileEnd : forall b1 st c1, beval st b1 = false -> ceval st (CWhile b1 c1) st | CEWhileLoop : forall st st' st'' b1 c1, beval st b1 = true -> ceval st c1 st' -> ceval st' (CWhile b1 c1) st'' -> ceval st (CWhile b1 c1) st''. (* Exercise: 3 stars (aeval_beval_rel) *) (* Write relations [aeval_rel] and [beval_rel] in the same style as [ceval], and prove that they are equivalent to [aeval] and [beval]. *) (* FILL IN HERE *) Tactic Notation "ceval_cases" tactic(first) tactic(c) := first; [ c "CESkip" | c "CEAss" | c "CESeq" | c "CEIfTrue" | c "CEIfFalse" | c "CEWhileEnd" | c "CEWhileLoop" ]. Example ceval_example1: ceval empty_state (X ::= A2; testif !X <<= A1 then Y ::= A3 else Z ::= A4) (extend (extend empty_state X 2) Z 4). Proof. apply CESeq with (extend empty_state X 2). Case "assignment command". apply CEAss. reflexivity. Case "if command". apply CEIfFalse. reflexivity. apply CEAss. reflexivity. Qed. (* And here's the similar output of ceval_step *) Eval compute in (ceval_step empty_state (X ::= A2; testif !X <<= A1 then Y ::= A3 else Z ::= A4) 500). Eval compute in (match ceval_step empty_state (X ::= A2; testif !X <<= A1 then Y ::= A3 else Z ::= A4) 500 with | None => (None,None) (* shouldn't happen, if 500 is big enough *) | Some st => (lookup X st, lookup Z st) end). (* Exercise: 2 stars *) Example ceval_example2: ceval empty_state (X ::= A0; Y ::= A1; Z ::= A2) (extend (extend (extend empty_state X 0) Y 1) Z 2). Proof. (* FILL IN HERE (and delete "Admitted") *) Admitted. (* ------------------------------------------------------- *) (** ** Equivalence of step-indexed and relational evaluation *) Theorem ceval_step__ceval: forall c st st', (exists i, ceval_step st c i = Some st') -> ceval st c st'. Proof. intros c st st' H. inversion H as [i E]. clear H. generalize dependent st'. generalize dependent st. generalize dependent c. induction i as [| i' ]. Case "i = 0 -- contradictory". intros c st st' H. inversion H. Case "i = S i'". intros c st st' H. (com_cases (destruct c) SCase); simpl in H; inversion H; subst; clear H. SCase "CSkip". apply CESkip. SCase "CAss". apply CEAss. reflexivity. SCase "CSeq". remember (ceval_step st c1 i') as r1. destruct r1. SSCase "Evaluation of r1 terminates normally". apply CESeq with s. apply IHi'. rewrite Heqr1. reflexivity. apply IHi'. simpl in H1. apply H1. SSCase "Evaluation of r1 terminates abnormally -- contradiction". inversion H1. SCase "CIf". remember (beval st b) as r. destruct r. SSCase "r = true". apply CEIfTrue. rewrite Heqr. reflexivity. apply IHi'. apply H1. SSCase "r = false". apply CEIfFalse. rewrite Heqr. reflexivity. apply IHi'. apply H1. SCase "CWhile". remember (beval st b) as r. destruct r. SSCase "r = true". remember (ceval_step st c i') as r1. destruct r1. SSSCase "r1 = Some s". apply CEWhileLoop with s. rewrite Heqr. reflexivity. apply IHi'. rewrite Heqr1. reflexivity. apply IHi'. simpl in H1. apply H1. SSSCase "r1 = None". inversion H1. SSCase "r = false". inversion H1. apply CEWhileEnd. rewrite Heqr. subst. reflexivity. Qed. (* Exercise: 4 stars (ceval_step__ceval_inf) *) (* Write an informal proof of [ceval_step__ceval], following the template at the top of the file. (The template for case analysis on an inductively defined value should look the same as for induction, except that there are no induction hypothesis.) Make your proof communicate the main ideas to a human reader; do *not* simply transcribe the steps of the formal proof. (* FILL IN HERE *) *) Theorem ceval_step_more: forall i1 i2 st st' c, i1 <= i2 -> ceval_step st c i1 = Some st' -> ceval_step st c i2 = Some st'. Proof. induction i1 as [|i1']; intros i2 st st' c Hle Hceval. Case "i1 = 0". inversion Hceval. Case "i1 = S i1'". destruct i2 as [|i2']. inversion Hle. com_cases (destruct c) SCase. SCase "CSkip". simpl in Hceval. inversion Hceval. reflexivity. SCase "CAss". simpl in Hceval. inversion Hceval. reflexivity. SCase "CSeq". simpl in Hceval. simpl. apply le_S_n in Hle. remember (ceval_step st c1 i1') as i1'o. destruct i1'o. SSCase "i1'o = Some". apply sym_eq in Heqi1'o. apply (IHi1' i2') in Heqi1'o; try assumption. rewrite Heqi1'o. simpl. simpl in Hceval. apply (IHi1' i2') in Hceval; try assumption. SSCase "i1'o = None". inversion Hceval. SCase "CIf". simpl in Hceval. simpl. apply le_S_n in Hle. remember (beval st b) as bval. destruct bval; apply (IHi1' i2') in Hceval; assumption. SCase "CWhile". simpl in Hceval. simpl. destruct (beval st b); try assumption. apply le_S_n in Hle. remember (ceval_step st c i1') as i1'o. destruct i1'o. SSCase "i1'o = Some". apply sym_eq in Heqi1'o. apply (IHi1' i2') in Heqi1'o; try assumption. rewrite -> Heqi1'o. simpl. simpl in Hceval. apply (IHi1' i2') in Hceval; try assumption. SSCase "i1'o = None". simpl in Hceval. inversion Hceval. Qed. (* Exercise: 4 stars *) (* Finish the following proof. You'll need [ceval_step_more] in a few places, as well as some basic facts about [<=] and [plus]. *) Theorem ceval__ceval_step: forall c st st', ceval st c st' -> exists i, ceval_step st c i = Some st'. Proof. intros c st st' Hce. ceval_cases (induction Hce) Case. (* FILL IN HERE (and delete "Admitted") *) Admitted. Theorem ceval_and_ceval_step_coincide: forall c st st', ceval st c st' <-> exists i, ceval_step st c i = Some st'. Proof. intros c st st'. split. apply ceval__ceval_step. apply ceval_step__ceval. Qed. (* ------------------------------------------------------- *) (** ** Reasoning about programs *) Theorem plus2_spec : forall st n st', lookup X st = Some n -> ceval st plus2 st' -> lookup X st' = Some (plus n 2). Proof. intros st n st' HX Heval. (* inverting Heval essentially forces coq to expand one step of the ceval computation - in this case revealing that st' must be st extended with the new value of X, since plus2 is an assignment *) inversion Heval. subst. apply extend_eq. simpl. rewrite -> HX. reflexivity. Qed. (* Exercise: 3 stars (XtimesYinZ_spec) *) (* State and prove a specification of the XtimesYinZ while program *) (* FILL IN HERE *) (* Exercise: 3 stars *) Theorem loop_never_stops : forall st st', ~(ceval st loop st'). Proof. intros st st' contra. unfold loop in contra. remember (while BTrue do skip) as loopdef. (* Proceed by induction on the assumed derivation showing that loopdef terminates. Most of the cases are immediately contradictory (and so can be solved in one step with [inversion]). *) (* FILL IN HERE (and delete "Admitted") *) Admitted. Fixpoint no_whiles (c : com) {struct c} : bool := match c with | CSkip => true | CAss _ _ => true | CSeq c1 c2 => andb (no_whiles c1) (no_whiles c2) | CIf _ ct cf => andb (no_whiles ct) (no_whiles cf) | CWhile _ _ => false end. (* Exercise: 4 stars *) (* On the other hand, programs that don't involve while loops always terminate. State and prove a theorem that says this. *) (* FILL IN HERE *)