(** Formal Type Theory, Autumn 2009, Exercise set 3 NAME(S) OF SUBMITTER(S): COMMENTS ON THE EXERCISE: Send this file (with the problems solved) to ftt09@cs.helsinki.fi by 2009-11-27 03:00+02 *) (** Our theorems and proofs are getting a little more complex all the time. Once again, you are encouraged to seek a partner with whom to share thoughts and solutions. All the problems are of course solvable alone, but it is more work. There are four problems worth four points each. However, the maximum number of points from this week's exercises is 12. You may choose which problems to solve, or you may solve them all if you like. In many of the exercises a tactic is likely to generate several subgoals that all need somehow similar treatment. In these cases it is practical to use the [tac1 ; tac2] syntax to apply [tac2] at once to all the subgoals that [tac1] generates. Also remember that you can use [try tac1] if [tac1] is only applicable to _some_ subgoals. Then it will fail harmlessly in the other subgoals. Also, in all of the exercises you are free to use the [auto] and [eauto] tactics and you can also use [Hint Constructors] and [Hint Resolve] as you like. However, sometimes it may be easier to solve a task manually instead of spending time to tweak automation. Use your judgement here. In some cases it is possible solve an entire problem with some tactics that are applied to all subgoals after an induction. In these cases the automation tactics may fail simply because there is too much to do and they give up too soon. In these cases, you can give a numeric depth argument for [auto] or [eauto], e.g. [eauto 10]. (A depth of ten should be enough for all of these exercises.) Some tactics that are going to be useful: - use [inversion] to examine the possible ways that a particular proof of an inductively defined proposition may have been constructed. In particular, use [inversion] to prove any goal from an impossible hypothesis. - use [exists] to provide an explicit witness object for an existential goal, or [eexists] to allow the witness to be inferred from the proof of the existentially quantified predicate - use [left] and [right] to choose to prove the left or right hand alternative of a disjunction (these are just short for [apply or_introl] and [apply or_intror]) - use [unfold] to expand a particular defined constant to the body of the definition (often [red] can also be used) - use complex introduction patterns with [induction], [destruct] or [intros] in order to easily destructure e.g. disjunctions, conjunctions and existentials and their combinations. See the Coq manual's description of the [intros] tactic for a more detailed explanation of the introduction patterns. These are especially useful when sequencing tactics with [;] - use [auto] and [eauto] for automation. Remember that the different problems deal with different languages, so you may need to declare different hints for each. Remember to write your name and comments at the start of this file. Good luck! **) Require Import tapl_ch8. Module ex1. Require Import typed_arith_lang. Notation "t1 -->* t2" := (RSC eval t1 t2) : type_scope. (** Problem 1 (4 p) Consider the following terms of the typed arithmetic language: *) Definition term1 : term := (succ (if (iszero (succ 0)) then false else 0))%tm. Definition term2 : term := (if (if (iszero 0) then true else false) then false else true)%tm. (** The task is to show for each of them - whether it is well-typed or not, and - whether it can be evaluated to a value or not Due to the constructive nature of Coq's logic, a positive answer requires an explicit witness: i.e. specifying _which_ type a term has, and _which_ value it evaluates to. Some preliminary definitions. We say that a term [t] is well-typed iff there is some type [T] such that [|- t : T]. *) Definition well_typed (t : term) := exists T : type, |- t : T. (** And [t] evaluates to a value iff there is some term [t'] that is a value and [t] evaluates to it in zero or more steps. *) Definition evals_to_value (t : term) := exists t' : term, val t' /\ t -->* t'. (** Finally, we say that the proposition [P] is decidable if we can show either [P] or its negation, i.e. we know whether it is true or not. *) Definition decidable (P : Prop) := P \/ ~P. (** So the task is simply to decide for both terms whether [well_typed] and [evals_to_value] are true or not. *) (** Problem 1.a (1 p) *) Lemma ex1a : decidable (evals_to_value term1). Proof. (* it evals to 0 *) apply or_introl. exists (succ 0)%tm. split. Case "val (succ 0)". apply Val_NV; apply NV_Succ; apply NV_Zero. Case "term1 -->* (succ 0)". unfold term1. eapply rsc_step. apply E_Succ. apply E_If. apply E_IsZeroSucc. apply NV_Zero. eapply rsc_step. apply E_Succ. apply E_IfFalse. apply rsc_refl. Qed. (** Problem 1.b (1 p) *) Lemma ex1b : decidable (well_typed term1). Proof. (* it's not typeable *) apply or_intror. unfold well_typed. intro WT. destruct WT as (typ, H). (* we use inversions to dig out the contradiction *) inversion H. inversion H1. inversion H8. Qed. (** Problem 1.c (1 p) *) Local Hint Constructors RSC eval : myhint. Lemma ex1c : decidable (evals_to_value term2). Proof with eauto with myhint. (* it evals to false *) apply or_introl. exists false%tm. split. auto with typed_arith. (* compute the evaluation *) unfold term2. eapply rsc_step... Qed. (** Problem 1.d (1 p) *) Lemma ex1d : decidable (well_typed term2). Proof with eauto with typed_arith. (* it has type bool *) apply or_introl. unfold well_typed. unfold term2. exists TyBool... Qed. End ex1. Module ex2. Require Import untyped_wrong_arith_lang. (** Problem 2 (4 p) (Adapted from TAPL 3.5.16) One way of coping with the problem of stuck terms (i.e. terms that are not values but which cannot be evaluated further) is to introduce a new term [wrong] and some new evaluation rules that are intended to make sure that the previously stuck terms will then evaluate to [wrong]. This is a simple formalization of the approach taken by the dynamically checked languages: an operation with incompatible operands can occur at run-time, but the outcome is well-defined. See the formalization of the rules in TAPL 3.5.16, in the file wrong.ott and in untyped_wrong_arith_lang.v. Then prove the progress theorem for this language. The proof is very similar to the progress proof for the plain boolean language [untyped_bool2.progress]. There are simply more cases to consider. There is ample room for automation here, and in fact the whole progress lemma can be proven in just a couple of lines. *) Local Hint Constructors term nv val badnat badbool eval or and ex : myhint. Lemma progress : forall t, t = wrong \/ val t \/ exists t', t --> t'. Proof with eauto 10 with myhint. intro t. induction t... Case "if". destruct IHt1 as [twrong | [ [ | | t' nvt' ] | [t' t1tot'] ]]... SCase "t1 = wrong". rewrite twrong. apply or_intror. apply or_intror. exists wrong. apply E_If_Wrong. apply BB_Wrong. Case "succ". destruct IHt as [twrong | [ [ | | t' nvt' ] | [t' t1tot'] ]]... SCase "t = wrong". rewrite twrong... Case "pred". destruct IHt as [twrong | [ [ | | t' nvt' ] | [t' t1tot'] ]]... SCase "t = wrong". rewrite twrong... SCase "val t". destruct nvt'... Case "iszero". destruct IHt as [twrong | [ [ | | t' nvt' ] | [t' t1tot'] ]]... SCase "t = wrong". rewrite twrong... SCase "val t". destruct nvt'... Qed. End ex2. Module ex34. Require Import untyped_bigstep_arith_lang. Notation "t1 -->* t2" := (RSC eval t1 t2) : type_scope. Local Hint Constructors RSC term nv val eval or and ex : myhint. (** Problem 3 (TAPL 3.5.17) An alternative way of specifying the evaluation rules of a programming language is to use _big-step semantics_, where a single evaluation judgement shows the final result of the computation. The files bigstep.ott and untyped_bigstep_arith_lang.v contain the definition of big-step semantics for the arithmetic language. The task is to prove that if [t ==> v], i.e. [t] evaluates into [v] by the big-step relation, then [t] can also be evaluated into [v] by repeated application of the small-step evaluation, i.e. [t -->* v]. You may have look at the sample solution in TAPL. The formal proof in Coq has a similar structure. *) (** Problem 3.a (1 p) Prove the following congruence lemmas for the many-step evaluation relation. These are all extremely simple inductions, and everything after the induction can be easily automatized. You can follow the example of [untyped_bool3.meval_if_congr] which was previously proven for the boolean language. *) Lemma congr_if : forall t1 t1' t2 t3, t1 -->* t1' -> (if t1 then t2 else t3)%tm -->* (if t1' then t2 else t3)%tm. Proof with eauto with myhint. intros t1 t1' t2 t3 H. induction H as [ a | a b c atob btoc IH ]. apply rsc_refl. eapply rsc_step. apply E_If. apply atob. apply IH. Qed. Lemma congr_succ : forall t1 t1', t1 -->* t1' -> (succ t1)%tm -->* (succ t1')%tm. Proof with eauto with myhint. intros t1 t1' H. induction H... Qed. Lemma congr_pred : forall t1 t1', t1 -->* t1' -> (pred t1)%tm -->* (pred t1')%tm. Proof with eauto with myhint. intros t1 t1' H. induction H... Qed. Lemma congr_iszero : forall t1 t1', t1 -->* t1' -> (iszero t1)%tm -->* (iszero t1')%tm. Proof with eauto with myhint. intros t1 t1' H. induction H... Qed. (** Problem 3.b (3 p) Then prove the actual theorem. As is shown in the sample answer in TAPL, the proof proceeds by induction on the derivation of [t ==> t'], and most of the cases involve chaining the inductive hypotheses together with the congruence lemmas and computation rules. There is an example of similar chaining in the proof of [untyped_bool4.eval_normalizing]. Once again there are opportunities for automation. *) Local Hint Resolve congr_if congr_succ congr_pred congr_iszero (*rsc_trans eval*): myhint. Theorem beval_then_meval : forall t t', val t' -> (t ==> t') -> (t -->* t'). Proof with eauto with myhint. assert (val 0). eauto with myhint. assert (forall t, nv t -> val t -> val (succ t)). eauto with myhint. intros t t' valt' ttot'. induction ttot'; eauto 10 with myhint. Case "iftrue". eapply rsc_trans. eapply congr_if. apply (IHttot'1 Val_True). eapply rsc_step. apply E_IfTrue. apply IHttot'2. exact valt'. Case "iffalse". eapply rsc_trans. eapply congr_if. apply (IHttot'1 Val_False). eapply rsc_step... Case "predzero". eapply rsc_trans. eapply congr_pred. apply IHttot'... eapply rsc_step... Case "predsucc". eapply rsc_trans. eapply congr_pred. apply IHttot'... eapply rsc_step... Case "iszero zero". eapply rsc_trans. eapply congr_iszero. apply IHttot'... eapply rsc_step... Case "iszero succ". eapply rsc_trans. eapply congr_iszero. apply IHttot'... eapply rsc_step... Qed. (** Problem 4. (4 p) So far we have only discussed evaluation as an abstract relation, but the actual computational aspect of evaluation has been left implicit (although a constructive normalization proof actually contains a method for finding the normal form of each term). Note that it is impossible to begin solving 4.b without first having completed 4.a. Problem 4.a (2 p) Write a recursive function [evaluate : term -> option term] such that [t ==> t' <-> evaluate t = Some t']. That is, it should return the result of evaluating the argument term with big-step evaluation. The function is a relatively straightforward combination of structural recursion and pattern matching. A stub is provided below. Hint: think very carefully about what the exact semantics of the [succ] operation is, and consider when your function should return [None]. *) Fixpoint evaluate (t : term) : option term := match t with | true%tm => Some true%tm | false%tm => Some false%tm | (if t1 then t2 else t3)%tm => match evaluate t1 with | Some true%tm => evaluate t2 | Some false%tm => evaluate t3 | _ => None end | 0%tm => Some 0%tm | (succ t1)%tm => match evaluate t1 with | Some x => Some (succ x)%tm | _ => None end | (pred t1)%tm => match evaluate t1 with | Some (succ n)%tm => Some n | Some 0%tm => Some 0%tm | _ => None end | (iszero t1)%tm => match evaluate t1 with | Some 0%tm => Some true%tm | Some (succ _)%tm => Some false%tm | _ => None end end. (** Problem 4.b (2 p) Show one direction of the equivalence between the big-step semantics and your function: if [t ==> t'] then [evaluate t = Some t']. The proof once again proceeds by induction on the proof of [t ==> t']. The basic principle is to use the inductive hypothesis to rewrite a subterm in the goal. An important tactic here is [simpl], which often converts goal into a form where the right subterm appears. It is best to use [simpl] immediately after induction. Once again, there is ample opportunity for automation. *) Local Hint Constructors term nv val eval or and ex : myhint. Lemma evaluate_faithful : forall t t', (t ==> t') -> evaluate t = Some t'. Proof with auto with myhint. intros t t' tBt'. (* rewriting IHtBt' takes care of the simple cases, unfortunately in the cases for If we have _two_ inductive hypotheses which requires us to do a renaming trick. *) induction tBt'; simpl; try rename IHtBt'1 into IHtBt'; try rewrite IHtBt'... Case "val t". destruct H; simpl... SCase "nv t". induction H; simpl... SSCase "succ". rewrite IHnv... Qed. End ex34.