diff --git a/README.md b/README.md index 0a01304..ff11cf6 100644 --- a/README.md +++ b/README.md @@ -1,17 +1,26 @@ # A Short Introduction to Coq -You can try it [online in Binder](https://mybinder.org/v2/git/https%3A%2F%2Fc4science.ch%2Fdiffusion%2F9452%2Fcoq-project.git/master?filepath=demo.ipynb) +You can try it online in Binder: + +- [demo](https://mybinder.org/v2/git/https%3A%2F%2Fc4science.ch%2Fdiffusion%2F9452%2Fcoq-project.git/master?filepath=demo.ipynb) +- [advanced](https://mybinder.org/v2/git/https%3A%2F%2Fc4science.ch%2Fdiffusion%2F9452%2Fcoq-project.git/master?filepath=advanced.ipynb) ## Install ```shell brew install coq # or something similar for your OS pip install --user coq_jupyter==1.5.0 python -m coq_jupyter.install ``` +Depending on your system, you may also need to run: + +```shell +pip install --user notebook +``` + ## Run ```shell jupyter notebook -``` \ No newline at end of file +``` diff --git a/advanced.ipynb b/advanced.ipynb new file mode 100644 index 0000000..1904811 --- /dev/null +++ b/advanced.ipynb @@ -0,0 +1,3819 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Adapted from a workshop given at [POPL\n", + "2008](https://www.cis.upenn.edu/~plclub/popl08-tutorial/).\n", + "\n", + "The NB language, back again\n", + "===========================\n", + "\n", + "In this notebook, we will be working with a language very similar to the\n", + "NB language from the first assignment.\n", + "\n", + "Definitions\n", + "-----------\n", + "\n", + "### Grammar and terms\n", + "\n", + "The grammar of our language would be defined as follows:\n", + "\n", + " t ::= \"true\" terms\n", + " | \"false\"\n", + " | \"if\" t \"then\" t \"else\" t\n", + " | 0\n", + " | \"succ\" t\n", + " | \"pred\" t\n", + " | \"iszero\" t\n", + "\n", + "To represent the terms of this language in Coq, we will define `tm`, an\n", + "`Inductive` data type:" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Inductive tm : Set :=\n", + "| tm_true : tm\n", + "| tm_false : tm\n", + "| tm_if : tm -> tm -> tm -> tm\n", + "| tm_zero : tm\n", + "| tm_succ : tm -> tm\n", + "| tm_pred : tm -> tm\n", + "| tm_iszero : tm -> tm." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Compare the two definitions. For every rule in the grammar, there is a\n", + "corresponding *constructor*. Each constructor is a value in Coq that\n", + "allows us to obtain values of type `tm`. In contrast to the previous\n", + "notebook, here we annotate every constructor with a type. `tm_true` is a\n", + "constructor corresponding to the terminal rule `\"true\"` - it takes no\n", + "arguments and is therefore annotated with the simple type `tm`.\n", + "`tm_succ` is a constructor corresponding to the `\"succ\" t` rule - since\n", + "the rule has a single subterm, the constructor is a function from `tm`\n", + "to `tm`.\n", + "\n", + "Using the above definition, we can create values corresponding to the\n", + "terms in our language:" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Check (tm_if (tm_iszero tm_zero) tm_false tm_true)." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "### Definition of value\n", + "\n", + "Next, we want to define what it means to be a *value* in our language.\n", + "While in the original NB language we did so through grammar rules, it’s\n", + "equally valid to define a judgment which tells us which terms are\n", + "boolean and numeric values (correspondingly, `bvalue` and `nvalue`):\n", + "\n", + " --------------- (b_true)\n", + " ⊢ bvalue (true)\n", + "\n", + " ---------------- (b_false)\n", + " ⊢ bvalue (false)\n", + "\n", + " \n", + " ---------- (n_zero)\n", + " ⊢ nvalue 0\n", + " \n", + " ⊢ nvalue t\n", + " ----------------- (n_succ)\n", + " ⊢ nvalue (succ t)\n", + "\n", + "Recall that from Curry-Howard correspondence we know that types\n", + "correspond to propositions and values correspond to proofs. Therefore,\n", + "we can represent the above judgements in Coq by defining a type\n", + "corresponding to each judgement. Then, begin able to create a value of\n", + "type `nvalue` is the same as being able to construct a proof that a\n", + "given term is an `nvalue`.\n", + "\n", + "The definitions are as follows:" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Inductive bvalue : tm -> Prop := \n", + "| b_true : bvalue tm_true \n", + "| b_false : bvalue tm_false.\n", + "\n", + "Inductive nvalue : tm -> Prop :=\n", + "| n_zero : nvalue tm_zero\n", + "| n_succ : forall t,\n", + " nvalue t ->\n", + " nvalue (tm_succ t)." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Those definitions should look similar to the inference rules above,\n", + "although they may also look slightly confusing. Before trying to\n", + "understand their every part, it may help to see how they are meant to be\n", + "used.\n", + "\n", + "The *type* `nvalue t` represents the *proposition* that `t` is a numeric\n", + "value. For instance, `nvalue (tm_succ tm_zero)` represents the\n", + "proposition that the successor of zero (or simply one) is a numeric\n", + "value. To show that this proposition is true, we need to construct a\n", + "value of said type. We can do that as follows:" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Check (n_succ tm_zero n_zero)." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "You should now go back to the definitions and try to understand how they\n", + "represent their corresponding inference rules.\n", + "\n", + "One thing that may still be puzzling are the `Set` and `tm -> Prop`\n", + "annotation. If you are suspecting that the second one mentions `tm ->`\n", + "because the corresponding type is a *type-level function* from `tm` to\n", + "`Prop`, you’d be correct:" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Check nvalue.\n", + "Check nvalue tm_zero." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "The difference between `Set` and `Prop` is much more subtle and\n", + "fundamental. To put it briefly, types annotated as `Set` are meant to be\n", + "used as data types, while those annotated as `Prop` are meant to be used\n", + "as propositions. Fully explaining this distinction is beyond the scope\n", + "of this course, but the above intuition should serve you well enough.\n", + "\n", + "As the last thing in this section, we will (finally) define what it\n", + "means to be a value. If you recall that `T \\/ S` is the data type\n", + "corresponding to the proof that either `T` or `S`, the definition is\n", + "simple enough:" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Definition value (t : tm) : Prop :=\n", + " bvalue t \\/ nvalue t." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "### Operational semantics\n", + "\n", + "Having defined `tm`s and `value`s, we can define call-by-value\n", + "operational semantics for our language. We will define an inductive data\n", + "type `eval (t : tm) (t' : tm) : Prop` corresponding to the proposition\n", + "that `t` evaluates to `t'` in a single step. The definition is as\n", + "follows:" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Inductive eval : tm -> tm -> Prop :=\n", + "| e_iftrue : forall t2 t3,\n", + " eval (tm_if tm_true t2 t3) t2\n", + "| e_iffalse : forall t2 t3,\n", + " eval (tm_if tm_false t2 t3) t3\n", + "| e_if : forall t1 t1' t2 t3,\n", + " eval t1 t1' ->\n", + " eval (tm_if t1 t2 t3) (tm_if t1' t2 t3)\n", + "| e_succ : forall t t',\n", + " eval t t' ->\n", + " eval (tm_succ t) (tm_succ t')\n", + "| e_predzero :\n", + " eval (tm_pred tm_zero) tm_zero\n", + "| e_predsucc : forall t,\n", + " nvalue t ->\n", + " eval (tm_pred (tm_succ t)) t\n", + "| e_pred : forall t t',\n", + " eval t t' ->\n", + " eval (tm_pred t) (tm_pred t')\n", + "| e_iszerozero :\n", + " eval (tm_iszero tm_zero) tm_true\n", + "| e_iszerosucc : forall t,\n", + " nvalue t ->\n", + " eval (tm_iszero (tm_succ t)) tm_false\n", + "| e_iszero : forall t t',\n", + " eval t t' ->\n", + " eval (tm_iszero t) (tm_iszero t')." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "If you don’t feel comfortable with Coq syntax yet, compare the above\n", + "with the definition of beta-reduction from our first assignment.\n", + "\n", + "Next, we define the multi-step evaluation relation `eval_many`:" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Inductive eval_many : tm -> tm -> Prop :=\n", + "| m_refl : forall t,\n", + " eval_many t t\n", + "| m_step : forall t t' u,\n", + " eval t t' ->\n", + " eval_many t' u ->\n", + " eval_many t u." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "We say that a term is a `normal_form` if there is no term to which it\n", + "can step. We can define this in Coq as follows:" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Definition normal_form (t : tm) : Prop :=\n", + " ~ exists t', eval t t'." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "### Exercises\n", + "\n", + "**Exercise** Multi-step evaluation is often defined as the “reflexive,\n", + "transitive closure” of single-step evaluation. Write an inductively\n", + "defined relation `eval_rtc` that corresponds to that verbal description.\n", + "\n", + "In case you get stuck or need a hint, you can find solutions to all the\n", + "exercises near the bottom of the file.\n", + "\n", + "**Exercise** Sometimes it is more convenient to use a big-step semantics\n", + "for a language. Add the remaining constructors to finish the inductive\n", + "definition `full_eval` for the big-step semantics that corresponds to\n", + "the small-step semantics defined by `eval`. Build the inference rules so\n", + "that `full_eval t v` logically implies both `eval_many t v` and\n", + "`value v`. In order to do this, you may need to add the premise\n", + "`nvalue v` to the appropriate cases.\n", + "\n", + "Hint: You should end up with a total of 8 cases.\n", + "\n", + " Inductive full_eval : tm -> tm -> Prop :=\n", + " | f_value : forall v,\n", + " value v ->\n", + " full_eval v v\n", + " | f_iftrue : forall t1 t2 t3 v,\n", + " full_eval t1 tm_true ->\n", + " full_eval t2 v ->\n", + " full_eval (tm_if t1 t2 t3) v\n", + " | f_succ : forall t v,\n", + " nvalue v ->\n", + " full_eval t v ->\n", + " full_eval (tm_succ t) (tm_succ v).\n", + "\n", + "Proofs\n", + "------\n", + "\n", + "So far, we’ve only seen proofs represented in Coq as\n", + "manually-constructed values. For any non-trivial proof value, it’s\n", + "rather inconvenient to manually construct it.\n", + "\n", + "Proof values are most easily built interactively, using tactics to\n", + "manipulate a proof state. A proof state consists of a set of goals\n", + "(propositions or types for which you must produce an inhabitant), each\n", + "with a context of hypotheses (inhabitants of propositions or types you\n", + "are allowed to use). A proof state begins initially with one goal (the\n", + "statement of the lemma you are tying to prove) and no hypotheses. A goal\n", + "can be solved, and thereby eliminated, when it exactly matches one of\n", + "hypotheses in the context. A proof is completed when all goals are\n", + "solved.\n", + "\n", + "Tactics can be used for forward reasoning (which, roughly speaking,\n", + "means modifying the hypotheses of a context while leaving the goal\n", + "unchanged) or backward reasoning (replacing the current goal with one or\n", + "more new goals in simpler contexts). Given the level of detail required\n", + "in a formal proof, it would be ridiculously impractical to complete a\n", + "proof using forward reasoning alone. However it is usually both possible\n", + "and practical to complete a proof using backward reasoning alone.\n", + "Therefore, we focus almost exclusively on backward reasoning in this\n", + "tutorial. Of course, most people naturally a significant amount of\n", + "forward reasoning in their thinking process, so it may take you a while\n", + "to become accustomed to getting by without it.\n", + "\n", + "We use the keyword `Lemma` to state a new proposition we wish to prove.\n", + "(`Theorem` and `Fact` are exact synonyms for `Lemma`.) The keyword\n", + "`Proof`, immediately following the statement of the proposition,\n", + "indicates the beginning of a proof script. A proof script is a sequence\n", + "of tactic expressions, each concluding with a `.`. Once all of the goals\n", + "are solved, we use the keyword `Qed` to record the completed proof. If\n", + "the proof is incomplete, we may tell Coq to accept the lemma on faith by\n", + "using `Admitted` instead of `Qed`.\n", + "\n", + "We now proceed to introduce the specific proof tactics.\n", + "\n", + "### Implication and universal quantification\n", + "\n", + " - [intros]\n", + " - [apply]\n", + " - [apply with (x := ...)]\n", + "\n", + "Recall that both implication and universal quantification correspond to\n", + "function types and values. Accordingly, we can use the `intros` tactic\n", + "to move universally quantified variables and implication antecedents\n", + "from the goal into the context as hypotheses.\n", + "\n", + "If our current goal corresponds to a conclusion of some implication `P`,\n", + "we can use the `apply P` tactic to prove our goal by proving the\n", + "antecedents of `P`. If you’d suspect from the name of the tactic that\n", + "this corresponds to applying a function, you’d be correct. Using `apply`\n", + "allows building a proof value from the bottom up.\n", + "\n", + "#### Example 1\n", + "\n", + "In the following example, our proof script will build a value\n", + "corresponding to the following proof tree:\n", + "\n", + " nvalue t\n", + " ---------------------------- (e_predsucc)\n", + " eval (tm_pred (tm_succ t)) t\n", + " ------------------------------------------------ (e_succ)\n", + " eval (tm_succ (tm_pred (tm_succ t))) (tm_succ t)\n", + "\n", + "Step through every cell below to see how this tree is constructed." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma e_succ_pred_succ : forall t,\n", + " nvalue t ->\n", + " eval (tm_succ (tm_pred (tm_succ t))) (tm_succ t).\n", + "Proof." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " (** Let [t] be a [tm]. *)\n", + " intros t." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " (** Assume that [t] is an [nvalue] (and let's call that\n", + " assumption [Hn] for future reference). *)\n", + " intros Hn." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " (** By [e_succ], in order to prove our conclusion, it suffices\n", + " to prove that [eval (tm_pred (tm_succ t)) t]. *)\n", + " Check e_succ.\n", + " apply e_succ." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " (** That, in turn, can be shown by [e_predsucc], if we are\n", + " able to show that [nvalue t]. *)\n", + " Check e_predsucc.\n", + " apply e_predsucc." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " (** But, in fact, we assumed [nvalue t]. *)\n", + " apply Hn." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "You can see below that there is no magic happening at this point:\n", + "`e_succ_pred_succ` is a value that can be used like any other value we\n", + "have seen so far. We can ask Coq for its type:" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Check e_succ_pred_succ." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "And we can see the value we have constructed with tactics:" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Print e_succ_pred_succ." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Compare the value to the proof script above. Observe how function\n", + "application in the value corresponds to usages of `apply` tactic.\n", + "\n", + "#### Example 2\n", + "\n", + "Now consider, for a moment, the rule `m_step`:\n", + "\n", + " eval t t' eval_many t' u\n", + " ------------------------- (m_step)\n", + " eval_many t u\n", + "\n", + "If we have a goal such as `eval_many e1 e2`, we should be able to use\n", + "`apply m_step` in order to replace it with the goals `eval e1 t'` and\n", + "`eval_many t' e2`. But what exactly is `t'` here? When and how is it\n", + "chosen? It stands to reason the conclusion is justified if we can come\n", + "up with any `t'` for which the premises can be justified.\n", + "\n", + "Now we note that, in the Coq syntax for the type of `m_step`, all three\n", + "variables `t`, `t'`, and `u` are universally quantified. The tactic\n", + "`apply m_step` will use pattern matching between our goal and the\n", + "conclusion of `m_step` to find the only possible instantiation of `t`\n", + "and `u`. However, `apply m_step` will raise an error since it does not\n", + "know how it should instantiate `t'`. In this case, the `apply` tactic\n", + "takes a `with` clause that allows us to provide this instantiation. This\n", + "is demonstrated in the proof below.\n", + "\n", + "Observe how this works in the proof script below. The proof tree here\n", + "gives a visual representation of the proof term we are going to\n", + "construct and the proof script has again been annotated with the steps\n", + "in English.\n", + "\n", + " Letting s = tm_succ\n", + " p = tm_pred\n", + " lem = e_succ_pred_succ,\n", + "\n", + " nvalue t\n", + " - - - - - - - - - - - - (lem) --------------------- (m_refl)\n", + " eval (s (p (s t))) (s t) eval_many (s t) (s t)\n", + " ------------------------------------------------------ (m_step)\n", + " eval_many (s (p (s t))) (s t)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma m_succ_pred_succ : forall t,\n", + " nvalue t ->\n", + " eval_many (tm_succ (tm_pred (tm_succ t))) (tm_succ t).\n", + "Proof." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " (** Let [t] be a [tm], and assume [nvalue t]. *)\n", + " intros t Hn." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " (** By [m_step], to show our conclusion, it suffices to find\n", + " some [t'] for which\n", + " [eval (tm_succ (tm_pred (tm_succ t))) t']\n", + " and\n", + " [eval t' (tm_succ t)].\n", + " Let us choose [t'] to be [tm_succ t]. *)\n", + " Check m_step.\n", + " apply m_step with (t' := tm_succ t)." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " (** By the lemma [e_succ_pred_succ], to show\n", + " [eval (tm_succ (tm_pred (tm_succ t))) (tm_succ t)],\n", + " it suffices to show [nvalue t]. *)\n", + " Check e_succ_pred_succ.\n", + " apply e_succ_pred_succ." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " (** And, in fact, we assumed [nvalue t]. *)\n", + " apply Hn." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " (** Moreover, by the rule [m_refl], we also may conclude\n", + " [eval (tm_succ t) (tm_succ t)]. *)\n", + " Check m_refl.\n", + " apply m_refl." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "#### Example 3\n", + "\n", + "Any tactic like `apply` that takes the name of a constructor or lemma as\n", + "an argument can just as easily be given a more complicated expression as\n", + "an argument. Thus, we may use function application to construct proof\n", + "objects on the fly in these cases. Observe how this technique can be\n", + "used to rewrite the proof of the previous lemma.\n", + "\n", + "Although, we have eliminated one use of `apply`, this is not necessarily\n", + "an improvement over the previous proof. However, there are cases where\n", + "this technique is quite valuable." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma m_succ_pred_succ_alt : forall t,\n", + " nvalue t ->\n", + " eval_many (tm_succ (tm_pred (tm_succ t))) (tm_succ t).\n", + "Proof.\n", + " intros t Hn." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " Check m_step.\n", + " apply (m_step\n", + " (tm_succ (tm_pred (tm_succ t)))\n", + " (tm_succ t)\n", + " (tm_succ t)\n", + " )." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " Check e_succ_pred_succ.\n", + " apply (e_succ_pred_succ t Hn)." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " apply t." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " Check m_refl.\n", + " apply (m_refl (tm_succ t))." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "#### Lab 1\n", + "\n", + "Write proof scripts for the following lemmas, following the plain\n", + "language descriptions.\n", + "\n", + "These lemmas will be useful in later proofs." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma m_one : forall t1 t2,\n", + " eval t1 t2 ->\n", + " eval_many t1 t2." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " (** Let [t1] and [t2] be terms, and assume [eval t1 t2]. We\n", + " may conclude [eval_many t1 t2] by [m_step] if we can find\n", + " a term [t'] such that [eval t1 t'] and [eval_many t' t2].\n", + " We will choose [t'] to be [t2]. Now we can show\n", + " [eval t1 t2] by our assumption, and we can show\n", + " [eval_many t2 t2] by [m_refl]. *)\n", + "Proof." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " (* to finish *)\n", + "Admitted." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma m_two : forall t1 t2 t3,\n", + " eval t1 t2 ->\n", + " eval t2 t3 ->\n", + " eval_many t1 t3." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " (** Let [t1], [t2], and [t3] be terms. Assume [eval t1 t2]\n", + " and [eval t2 t3]. By [m_step], we may conclude that\n", + " [eval_many t1 t3] if we can find a term [t'] such that\n", + " [eval t1 t'] and [eval_many t' t3]. Let's choose [t'] to\n", + " be [t2]. We know [eval t1 t2] holds by assumption. In\n", + " the other case, by the lemma [m_one], to show [eval_many\n", + " t2 t3], it suffices to show [eval t2 t3], which is one of\n", + " our assumptions. *)\n", + "Proof." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " (* to finish *)\n", + "Admitted." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma m_iftrue_step : forall t t1 t2 u,\n", + " eval t tm_true ->\n", + " eval_many t1 u ->\n", + " eval_many (tm_if t t1 t2) u." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " (** Let [t], [t1], [t2], and [u] be terms. Assume that\n", + " [eval t tm_true] and [eval_many t1 u]. To show\n", + " [eval_many (tm_if t t1 t2) u], by [m_step], it suffices to\n", + " find a [t'] for which [eval (tm_if t t1 t2) t'] and\n", + " [eval_many t' u]. Let us choose [t'] to be\n", + " [tm_if tm_true t1 t2]. Now we can use [e_if] to show that\n", + " [eval (tm_if t t1 t2) (tm_if tm_true t1 t2)] if we can\n", + " show [eval t tm_true], which is actually one of our\n", + " assumptions. Moreover, using [m_step] once more, we can\n", + " show [eval_many (tm_if tm_true t1 t2) u] where [t'] is\n", + " chosen to be [t1]. Doing so leaves us to show\n", + " [eval (tm_if tm_true t1 t2) t1] and [eval_many t1 u]. The\n", + " former holds by [e_iftrue] and the latter holds by\n", + " assumption. *)\n", + "Proof." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " (* to finish *)\n", + "Admitted." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "### Working with Definitions\n", + "\n", + " - [unfold]\n", + "\n", + "There is a notion of equivalence on Coq terms that arises from the\n", + "conversion rules of the underlying calculus of constructions. It is\n", + "sometimes useful to be able to replace one term in a proof with an\n", + "equivalent one. For instance, we may want to replace a defined name with\n", + "its definition. This sort of replacement can be done the tactic\n", + "`unfold`. This tactic can be used to manipulate the goal or the\n", + "hypotheses." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Definition strongly_diverges t :=\n", + " forall u, eval_many t u -> ~ normal_form u." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma unfold_example : forall t t',\n", + " strongly_diverges t ->\n", + " eval t t' ->\n", + " strongly_diverges t'.\n", + "Proof.\n", + " intros t t' Hd He.\n", + " unfold strongly_diverges. intros u Hm.\n", + " unfold strongly_diverges in Hd.\n", + " apply Hd. apply m_step with (t' := t').\n", + " apply He.\n", + " apply Hm.\n", + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Exercise** In reality, many tactics will perform conversion\n", + "automatically as necessary. Try removing the uses of `unfold` from the\n", + "above proof to check which ones were necessary.\n", + "\n", + "### Working with Conjunction and Disjunction\n", + "\n", + " - [split]\n", + " - [left]\n", + " - [right]\n", + " - [destruct] (for conjunction and disjunction)\n", + "\n", + "**Example** If `H` is the name of a conjunctive hypothesis, then\n", + "`destruct H as p` will replace the hypothesis `H` with its components\n", + "using the names in the pattern `p`. Observe the pattern in the example\n", + "below." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma m_two_conj : forall t t' t'',\n", + " eval t t' /\\ eval t' t'' ->\n", + " eval_many t t''.\n", + "Proof.\n", + " intros t t' t'' H.\n", + " destruct H as [ He1 He2 ].\n", + " apply m_two with (t2 := t').\n", + " apply He1.\n", + " apply He2.\n", + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Example** Patterns may be nested to break apart nested structures.\n", + "Note that infix conjunction is right-associative, which is significant\n", + "when trying to write nested patterns. We will later see how to use\n", + "`destruct` on many different sorts of hypotheses." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma m_three_conj : forall t t' t'' t''',\n", + " eval t t' /\\ eval t' t'' /\\ eval t'' t''' ->\n", + " eval_many t t'''.\n", + "Proof.\n", + " intros t t' t'' t''' H.\n", + " destruct H as [ He1 [ He2 He3 ] ].\n", + " apply m_step with (t' := t').\n", + " apply He1.\n", + " apply m_two with (t2 := t'').\n", + " apply He2.\n", + " apply He3.\n", + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Example** If your goal is a conjunction, use `split` to break it apart\n", + "into two separate subgoals." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma m_three : forall t t' t'' t''',\n", + " eval t t' ->\n", + " eval t' t'' ->\n", + " eval t'' t''' ->\n", + " eval_many t t'''.\n", + "Proof.\n", + " intros t t' t'' t''' He1 He2 He3.\n", + " apply m_three_conj with (t' := t') (t'' := t'').\n", + " split.\n", + " apply He1.\n", + " split.\n", + " apply He2.\n", + " apply He3.\n", + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Exercise** Hint: You might find lemma `m_three` useful here." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma m_if_iszero_conj : forall v t2 t2' t3 t3',\n", + " nvalue v /\\ eval t2 t2' /\\ eval t3 t3' ->\n", + " eval_many (tm_if (tm_iszero tm_zero) t2 t3) t2' /\\\n", + " eval_many (tm_if (tm_iszero (tm_succ v)) t2 t3) t3'.\n", + "Proof." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " (* to finish *)\n", + "Admitted." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Example** If the goal is a disjunction, we can use the `left` or\n", + "`right` tactics to solve it by proving the left or right side of the\n", + "conclusion." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma true_and_succ_zero_values :\n", + " value tm_true /\\ value (tm_succ tm_zero).\n", + "Proof.\n", + " unfold value. split.\n", + " left. apply b_true.\n", + " right. apply n_succ. apply n_zero.\n", + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Example** If we have a disjunction in the context, we can use\n", + "`destruct` to reason by cases on the hypothesis. Note the syntax of the\n", + "associated pattern." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma e_if_true_or_false : forall t1 t2,\n", + " eval t1 tm_true \\/ eval t1 tm_false ->\n", + " eval_many (tm_if t1 t2 t2) t2.\n", + "Proof.\n", + " intros t1 t2 H. destruct H as [ He1 | He2 ].\n", + " apply m_two with (t2 := tm_if tm_true t2 t2).\n", + " apply e_if. apply He1.\n", + " apply e_iftrue.\n", + " apply m_two with (t2 := tm_if tm_false t2 t2).\n", + " apply e_if. apply He2.\n", + " apply e_iffalse.\n", + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "#### Lab 2\n", + "\n", + "Work on the following exercise.\n", + "\n", + "**Exercise**" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma two_values : forall t u,\n", + " value t /\\ value u ->\n", + " bvalue t \\/\n", + " bvalue u \\/\n", + " (nvalue t /\\ nvalue u)." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " (** We know [value t] and [value u], which means either\n", + " [bvalue t] or [nvalue t], and either [bvalue u] or\n", + " [nvalue u]. Consider the case in which\n", + " [bvalue t] holds. Then one of the disjuncts of our\n", + " conclusion is proved. Next, consider the case in which\n", + " [nvalue t] holds. Now consider the subcase where\n", + " [bvalue u] holds. ... *)\n", + "Proof." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " (* to finish *)\n", + "Admitted." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Example** `destruct` can be used on propositions with implications.\n", + "This will have the effect of performing `destruct` on the conclusion of\n", + "the implication, while leaving the hypotheses of the implication as\n", + "additional subgoals." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma destruct_example : forall bv t t' t'',\n", + " bvalue bv ->\n", + " (value bv -> eval t t' /\\ eval t' t'') ->\n", + " eval_many t t''.\n", + "Proof.\n", + " intros bv t t' t'' Hbv H. destruct H as [ H1 H2 ].\n", + " Show 2.\n", + " unfold value. left. apply Hbv.\n", + " apply m_two with (t2 := t').\n", + " apply H1.\n", + " apply H2.\n", + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Tip** After applying a tactic that introduces multiple subgoals, it is\n", + "sometimes useful to see not only the subgoals themselves but also their\n", + "hypotheses. Adding the command `Show n.` to your proof script to cause\n", + "Coq to display the nth subgoal in full.\n", + "\n", + "Reasoning by Cases and Induction\n", + "--------------------------------" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " - [destruct] (for inductively defined propositions)\n", + " - [induction]" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Example** Use `destruct` to reason by cases on an inductively defined\n", + "datatype or proposition.\n", + "\n", + "Note: It is possible to supply `destruct` with a pattern in these\n", + "instances also. However, the patterns become increasingly complex for\n", + "bigger inductive definitions; so it is often more practical to omit the\n", + "pattern (thereby letting Coq choose the names of the terms and\n", + "hypotheses in each case), in spite of the fact that this adds an element\n", + "of fragility to the proof script (since the proof script will mention\n", + "names that were system-generated)." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma e_iszero_nvalue : forall v,\n", + " nvalue v ->\n", + " eval (tm_iszero v) tm_true \\/\n", + " eval (tm_iszero v) tm_false.\n", + "Proof.\n", + " intros v Hn." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " destruct Hn." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " (* Case [n_zero].\n", + " Note how [v] becomes [tm_zero] in the goal. *)\n", + " left." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " apply e_iszerozero." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " (* Case [n_succ].\n", + " Note how [v] becomes [tm_succ v] in the goal. *)\n", + " right." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " apply e_iszerosucc. apply Hn.\n", + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Example** You can use `induction` to reason by induction on an\n", + "inductively defined datatype or proposition. This is the same as\n", + "`destruct`, except that it also introduces an induction hypothesis in\n", + "the inductive cases." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma m_iszero : forall t u,\n", + " eval_many t u ->\n", + " eval_many (tm_iszero t) (tm_iszero u).\n", + "Proof.\n", + " intros t u Hm. induction Hm.\n", + " apply m_refl.\n", + " apply m_step with (t' := tm_iszero t').\n", + " apply e_iszero. apply H.\n", + " apply IHHm.\n", + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "#### Lab 3\n", + "\n", + "Work on the following exercise.\n", + "\n", + "**Exercise**" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma m_trans : forall t t' u,\n", + " eval_many t t' ->\n", + " eval_many t' u ->\n", + " eval_many t u." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " (** We proceed by induction on the derivation of\n", + " [eval_many t t'].\n", + " Case [m_refl]: Since [t] and [t'] must be the same, our\n", + " conclusion holds by assumption.\n", + " Case [m_step]: Now let's rename the [t'] from the lemma\n", + " statement to [u0] (as Coq likely will) and observe that\n", + " there must be some [t'] (from above the line of the\n", + " [m_step] rule) such that [eval t t'] and\n", + " [eval_many t' u0]. Our conclusion follows from from\n", + " an application of [m_step] with our new [t'] and our\n", + " induction hypothesis, which allows us to piece together\n", + " [eval_many t' u0] and [eval_many u0 u] to get\n", + " [eval_many t' u]. *)\n", + "Proof." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " (* to finish *)\n", + "Admitted." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Example** It is possible to use `destruct` not just on hypotheses but\n", + "on any lemma we have proved. If we have a lemma\n", + "\n", + " lemma1 : P /\\ Q\n", + "\n", + "then we can use the tactic\n", + "\n", + " destruct lemma1 as [ H1 H2 ].\n", + "\n", + "to continue our proof with `H1 : P` and `H2 : Q` in our context. This\n", + "works even if the lemma has antecedents (they become new subgoals);\n", + "however it fail if the lemma has a universal quantifier, such as this:\n", + "\n", + " lemma2 : forall x, P(x) /\\ Q(x)\n", + "\n", + "However, remember that we can build a proof of `P(e) /\\ Q(e)` (which can\n", + "be destructed) using the Coq expression `lemma2 e`. So we need to phrase\n", + "our tactic as\n", + "\n", + " destruct (lemma2 e) as [ H1 H2 ].\n", + "\n", + "An example of this technique is below." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma m_iszero_nvalue : forall t v,\n", + " nvalue v ->\n", + " eval_many t v ->\n", + " eval_many (tm_iszero t) tm_true \\/\n", + " eval_many (tm_iszero t) tm_false.\n", + "Proof.\n", + " intros t v Hnv Hm.\n", + " destruct (e_iszero_nvalue v) as [ H1 | H2 ].\n", + " apply Hnv.\n", + " left. apply m_trans with (t' := tm_iszero v).\n", + " apply m_iszero. apply Hm.\n", + " apply m_one. apply H1.\n", + " right. apply m_trans with (t' := tm_iszero v).\n", + " apply m_iszero. apply Hm.\n", + " apply m_one. apply H2.\n", + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Exercise** Prove the following lemma.\n", + "\n", + "Hint: You may be interested in some previously proved lemmas, such as\n", + "`m_one` and `m_trans`.\n", + "\n", + "Note: Even though this lemma is in a comment, its solution is also at\n", + "the bottom. (Coq will give an error if we leave it uncommented since it\n", + "mentions the `eval_rtc` relation, which was the solution to another\n", + "exercise.)\n", + "\n", + " Lemma eval_rtc_many : forall t u,\n", + " eval_rtc t u ->\n", + " eval_many t u.\n", + "\n", + "**Exercise** Prove the following lemma.\n", + "\n", + " Lemma eval_many_rtc : forall t u,\n", + " eval_many t u ->\n", + " eval_rtc t u.\n", + "\n", + "**Exercise** Prove the following lemma.\n", + "\n", + " Lemma full_eval_to_value : forall t v,\n", + " full_eval t v ->\n", + " value v.\n", + "\n", + "Working with Existential Quantification\n", + "---------------------------------------" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " - [exists]\n", + " - [destruct] (for existential propositions)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Example** Use `exists` to give the witness for an existential\n", + "quantifier in your goal." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma if_bvalue : forall t1 t2 t3,\n", + " bvalue t1 ->\n", + " exists u, eval (tm_if t1 t2 t3) u.\n", + "Proof.\n", + " intros t1 t2 t3 Hb. destruct Hb.\n", + " exists t2. apply e_iftrue.\n", + " exists t3. apply e_iffalse.\n", + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Example** You may use `destruct` to break open an existential\n", + "hypothesis." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma m_two_exists : forall t u,\n", + " (exists w, eval t w /\\ eval w u) ->\n", + " eval_many t u.\n", + "Proof.\n", + " intros t u H.\n", + " destruct H as [ w He ].\n", + " destruct He as [ He1 He2 ].\n", + " apply m_two with (t2 := w).\n", + " apply He1.\n", + " apply He2.\n", + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Example** Tip: We can combine patterns that destruct existentials with\n", + "patterns that destruct other logical connectives.\n", + "\n", + "Here is the same proof with just one use of `destruct`." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma m_two_exists' : forall t u,\n", + " (exists w, eval t w /\\ eval w u) ->\n", + " eval_many t u.\n", + "Proof.\n", + " intros t u H. destruct H as [ w [ He1 He2 ] ].\n", + " apply m_two with (t2 := w).\n", + " apply He1.\n", + " apply He2.\n", + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Example** Tip: We give patterns to the `intros` tactic to destruct\n", + "hypotheses as we introduce them.\n", + "\n", + "Here is the same proof again without any uses of `destruct`." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma m_two_exists'' : forall t u,\n", + " (exists w, eval t w /\\ eval w u) ->\n", + " eval_many t u.\n", + "Proof.\n", + " intros t u [ w [ He1 He2 ] ].\n", + " apply m_two with (t2 := w).\n", + " apply He1.\n", + " apply He2.\n", + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Exercise**" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma value_can_expand : forall v,\n", + " value v ->\n", + " exists u, eval u v.\n", + "Proof.\n", + " (* to finish *)\n", + "Admitted." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "#### Lab 4\n", + "\n", + " Work on the following exercise.\n", + "\n", + "**Exercise** Tip: You should find the lemma `m_iszero` useful. Use\n", + "`Check m_iszero.` if you’ve forgotten its statement." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma exists_iszero_nvalue : forall t,\n", + " (exists nv, nvalue nv /\\ eval_many t nv) ->\n", + " exists bv, eval_many (tm_iszero t) bv.\n", + "Proof.\n", + " (** There exists some [nv] such that [nvalue nv]. Consider\n", + " the case where [nv] is [tm_zero]. Then choose [bv] to\n", + " be [tm_true]. By [m_trans], we can show that\n", + " [eval_many (tm_iszero t) tm_true] by showing\n", + " [eval_many (tm_iszero t) (tm_iszero tm_zero)] and\n", + " [eval_many (tm_iszero tm_zero) tm_true]. The former\n", + " follows from [m_iszero] and our assumption. The latter\n", + " follows from [m_one] and the rule [e_iszerozero]. On the\n", + " other hand, in the case where [nv] is built from\n", + " [tm_succ], we choose [bv] to be [tm_false] and the proof\n", + " follows similarly. *)\n", + "\n", + " (* to finish *)\n", + "Admitted." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Working with Negation\n", + "---------------------" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " - [unfold not]\n", + " - [destruct] (for negation)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Example** The standard library defines an uninhabited type `False` and\n", + "defines `not P` to stand for `P -> False`. Furthermore, Coq defines the\n", + "notation `~ P` to stand for `not P`. (Such notations only affect parsing\n", + "and printing – Coq views `not P` and `~ P` as being syntactically\n", + "equal.)\n", + "\n", + "The most basic way to work with negated statements is to unfold `not`\n", + "and treat `False` just as any other proposition.\n", + "\n", + "(Note how multiple definitions can be unfolded with one use of `unfold`.\n", + "Also, as noted earlier, many uses of `unfold` are not strictly\n", + "necessary. You can try deleting the uses from the proof below to check\n", + "that the proof script still works.)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma normal_form_succ : forall t,\n", + " normal_form (tm_succ t) ->\n", + " normal_form t.\n", + "Proof.\n", + " intros t Hnf.\n", + " unfold normal_form. unfold not.\n", + " unfold normal_form, not in Hnf.\n", + " intros [ t' H' ]. apply Hnf.\n", + " exists (tm_succ t'). apply e_succ. apply H'.\n", + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Exercise**" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma normal_form_to_forall : forall t,\n", + " normal_form t ->\n", + " forall u, ~ eval t u.\n", + "Proof.\n", + " (* to finish *)\n", + "Admitted." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Exercise**" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma normal_form_from_forall : forall t,\n", + " (forall u, ~ eval t u) ->\n", + " normal_form t.\n", + "Proof.\n", + " (* to finish *)\n", + "Admitted." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Example** If you happen to have `False` as a hypothesis, you may use\n", + "`destruct` on that hypothesis to solve your goal." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma False_hypothesis : forall v,\n", + " False ->\n", + " value v.\n", + "Proof.\n", + " intros v H. destruct H.\n", + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Example** Recalling that `destruct` can be used on propositions with\n", + "antecedents and that negation is simply an abbreviation for an\n", + "implication, using `destruct` on a negated hypothesis has the derived\n", + "behavior of replacing our goal with the proposition that was negated in\n", + "our context.\n", + "\n", + "Tip: We actually don’t even need to do the unfolding below because\n", + "`destruct` would have done it for us." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma destruct_negation_example : forall t v,\n", + " value v ->\n", + " eval t tm_zero ->\n", + " (value v -> normal_form t) ->\n", + " eval tm_true tm_false.\n", + "Proof.\n", + " intros t v Hnv He Hnf.\n", + " unfold normal_form, not in Hnf.\n", + " (* As usual, unfolding was optional here. *)\n", + " destruct Hnf.\n", + " apply Hnv.\n", + " exists tm_zero. apply He.\n", + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Exercise** This one may be a bit tricky. Start by using `destruct` on\n", + "one of your hypotheses." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma negation_exercise : forall v1 v2,\n", + " ~ (value v1 \\/ value v2) ->\n", + " ~ (~ bvalue v1 /\\ ~ bvalue v2) ->\n", + " eval tm_true tm_false.\n", + "Proof.\n", + " (* to finish *)\n", + "Admitted." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Working with Equality\n", + "---------------------" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " - [reflexivity]\n", + " - [subst]\n", + " - [rewrite]\n", + " - [inversion] (on equalities)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Example** If you have an equality in your context, there are several\n", + "ways to substitute one side of the equality for the other in your goal\n", + "or in other hypotheses.\n", + "\n", + "If one side of the equality is a variable `x`, then the tactic `subst x`\n", + "will replace all occurrences of `x` in the context and goal with the\n", + "other side of the quality and will remove `x` from your context.\n", + "\n", + "Use `reflexivity` to solve a goal of the form `e = e`." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma equality_example_1 : forall t1 t2 t3 u1 u2,\n", + " t1 = tm_iszero u1 ->\n", + " t2 = tm_succ u2 ->\n", + " t3 = tm_succ t2 ->\n", + " tm_if t1 t2 t3 =\n", + " tm_if (tm_iszero u1) (tm_succ u2) (tm_succ (tm_succ u2)).\n", + "Proof.\n", + " intros t1 t2 t3 u1 u2 Heq1 Heq2 Heq3.\n", + " subst t1. subst t2. subst t3. reflexivity.\n", + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Example** If neither side of the equality in your context is a\n", + "variable (or if you don’t want to discard the hypothesis), you can use\n", + "the `rewrite` tactic to perform a substitution. The arrow after\n", + "`rewrite` indicates the direction of the substitution. As demonstrated,\n", + "you may perform rewriting in the goal or in a hypothesis." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma equality_example_2a : forall t u v,\n", + " tm_succ t = tm_succ u ->\n", + " eval (tm_succ u) v ->\n", + " eval (tm_succ t) v.\n", + "Proof.\n", + " intros t u v Heq He. rewrite -> Heq. apply He.\n", + "Qed." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma equality_example_2b : forall t u v,\n", + " tm_succ t = tm_succ u ->\n", + " eval (tm_succ u) v ->\n", + " eval (tm_succ t) v.\n", + "Proof.\n", + " intros t u v Heq He. rewrite <- Heq in He. apply He.\n", + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Example** We also note that, analogously with `destruct`, we may use\n", + "`rewrite` even with a hypothesis (or lemma) that has antecedents." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma equality_example_2c : forall t u v,\n", + " nvalue v ->\n", + " (nvalue v -> tm_succ t = tm_succ u) ->\n", + " eval (tm_succ u) v ->\n", + " eval (tm_succ t) v.\n", + "Proof.\n", + " intros t u v Hnv Heq He. rewrite <- Heq in He.\n", + " apply He.\n", + " apply Hnv.\n", + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Example** If you need to derive additional equalities implied by an\n", + "equality in your context (e.g., by the principle of constructor\n", + "injectivity), you may use `inversion`. `inversion` is a powerful tactic\n", + "that uses unification to introduce more equalities into your context.\n", + "(You will observe that it also performs some substitutions in your\n", + "goal.)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma equality_example_3 : forall t u,\n", + " tm_succ t = tm_succ u ->\n", + " t = u.\n", + "Proof.\n", + " intros t u Heq. inversion Heq. reflexivity.\n", + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Exercise**" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma equality_exercise : forall t1 t2 t3 u1 u2 u3 u4,\n", + " tm_if t1 t2 t3 = tm_if u1 u2 u2 ->\n", + " tm_if t1 t2 t3 = tm_if u3 u3 u4 ->\n", + " t1 = u4.\n", + "Proof.\n", + " (* to finish *)\n", + "Admitted." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Example** `inversion` will also solve a goal when unification fails on\n", + "a hypothesis. (Internally, Coq can construct a proof of `False` from\n", + "contradictory equalities.)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma equality_example_4 :\n", + " tm_zero = tm_true ->\n", + " eval tm_true tm_false.\n", + "Proof.\n", + " intros Heq. inversion Heq.\n", + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "#### Lab 5\n", + "\n", + "Work on `equality_exercise` above and `succ_not_circular` below.\n", + "\n", + "**Exercise** Note: `e1 <> e2` is a notation for `~ e1 = e2`, i.e., the\n", + "two are treated as syntactically equal.\n", + "\n", + "Note: This is fairly trivial to prove if we have a size function on\n", + "terms and some automation. With just the tools we have described so far,\n", + "it requires just a little bit of work.\n", + "\n", + "Hint: The proof requires induction on `t`. (This is the first example of\n", + "induction on datatypes, but it is even more straightforward than\n", + "induction on propositions.) In each case, unfold the negation, pull the\n", + "equality into the context, and use `inversion` to eliminate\n", + "contradictory equalities." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma succ_not_circular : forall t,\n", + " t <> tm_succ t.\n", + "Proof.\n", + " (* to finish *)\n", + "Admitted." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Reasoning by Inversion\n", + "----------------------" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " - [inversion] (on propositions)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Example** The `inversion` tactic also allows you to reason by\n", + "inversion on an inductively defined proposition as in paper proofs: we\n", + "try to match some proposition with the conclusion of each inference rule\n", + "and only consider the cases (possibly none) where there is a successful\n", + "unification. In those cases, we may use the premises of the inference\n", + "rule in our reasoning.\n", + "\n", + "Since `inversion` may generate many equalities between variables, it is\n", + "useful to know that using `subst` without an argument will perform all\n", + "possible substitutions for variables. It is a little difficult to\n", + "predict which variables will be eliminated and which will be kept by\n", + "this tactic, but this is a typical sort of trade-off when using powerful\n", + "tactics.\n", + "\n", + "(The use of `subst` in this proof is superfluous, but you can observe\n", + "that it simplifies the context.)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma value_succ_nvalue : forall t,\n", + " value (tm_succ t) ->\n", + " nvalue t.\n", + "Proof.\n", + " intros t H. unfold value in H. destruct H as [ H1 | H2 ].\n", + " (* No unification is possible -- [inversion] solves goal. *)\n", + " inversion H1.\n", + " (* Just the [n_succ] cases unifies with H2. *)\n", + " inversion H2. subst. apply H0.\n", + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "#### Lab 6\n", + "\n", + "Work on the exercise below.\n", + "\n", + "**Exercise**" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma inversion_exercise : forall t,\n", + " normal_form t ->\n", + " eval_many (tm_pred t) tm_zero ->\n", + " nvalue t.\n", + "Proof.\n", + " (** By inversion on the [eval_many] relation, then conclusion\n", + " [eval_many (tm_pred t) tm_zero] must have been derived by\n", + " the rule [m_step], which means there is some [t'] for\n", + " which [eval (tm_pred t) t'] and [eval_many t' tm_zero].\n", + " Now, by inversion on the [eval] relation, there are only\n", + " three ways that [eval (tm_pred t) t'] could have been\n", + " derived:\n", + " * By [e_predzero], with [t] and [t'] both being equal to\n", + " [tm_zero]. Our conclusion follows from [n_zero].\n", + " * By [e_predsucc], with [t] being [tm_succ t0] where we\n", + " have [nvalue t0]. In this case, our conclusion is\n", + " provable with [n_succ].\n", + " * By [e_pred], with [t] taking an evaluation step. This\n", + " contradicts our assumption that [t] is a normal form\n", + " (which can be shown by using [destruct] on that\n", + " assumption). *)\n", + "\n", + " (* to finish *)\n", + "Admitted." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Exercise** Tip: Nested patterns will be useful here." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma contradictory_equalities_exercise :\n", + " (exists t, exists u, exists v,\n", + " value t /\\\n", + " t = tm_succ u /\\\n", + " u = tm_pred v) ->\n", + " eval tm_true tm_false.\n", + "Proof.\n", + " (* to finish *)\n", + "Admitted." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Exercise**" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma eval_fact_exercise : forall t1 t2,\n", + " eval (tm_iszero (tm_pred t1)) t2 ->\n", + " eval t2 tm_false ->\n", + " exists u, t1 = tm_succ u.\n", + "Proof.\n", + " (* to finish *)\n", + "Admitted." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Exercise**" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma normal_form_if : forall t1 t2 t3,\n", + " normal_form (tm_if t1 t2 t3) ->\n", + " t1 <> tm_true /\\ t1 <> tm_false /\\ normal_form t1.\n", + "Proof.\n", + " (* to finish *)\n", + "Admitted." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Additional Important Tactics\n", + "----------------------------" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " - [generalize dependent]\n", + " - [assert]\n", + " - [;]\n", + " - [clear]" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Example** Sometimes we need to have a tactic that moves hypotheses\n", + "from our context back into our goal. Often this is because we want to\n", + "perform induction in the middle of a proof and will not get a\n", + "sufficiently general induction hypothesis without a goal of the correct\n", + "form. (To be specific, if we need to have an induction hypothesis with a\n", + "`forall` quantifier in front, then we must make sure our goal has a\n", + "`forall` quantifier in front at the time we invoke the `induction`\n", + "tactic.) Observe how `generalize dependent` achieves this in the proof\n", + "below, moving the variable `t` and all dependent hypotheses back into\n", + "the goal. You may want to remove the use of `generalize dependent` to\n", + "convince yourself that it is performing an essential role here." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma value_is_normal_form : forall v,\n", + " value v ->\n", + " normal_form v.\n", + "Proof.\n", + " intros v [ Hb | Hn ] [ t He ].\n", + " destruct Hb.\n", + " inversion He.\n", + " inversion He.\n", + " generalize dependent t. induction Hn.\n", + " intros t He. inversion He.\n", + " intros u He. inversion He. subst. destruct (IHHn t').\n", + " apply H0.\n", + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Exercise** Coq has many operations (called “tacticals”) to combine\n", + "smaller tactics into larger ones.\n", + "\n", + "If `t1` and `t2` are tactics, then `t1; t2` is a tactic that executes\n", + "`t1`, and then executes `t2` on subgoals left by or newly generated by\n", + "`t1`. This can help to eliminate repetitious use of tactics. Two\n", + "idiomatic uses are performing `subst` after `inversion` and performing\n", + "`intros` after `induction`. More opportunities to use this tactical can\n", + "usually be discovered after writing a proof. (It is worth noting that\n", + "some uses of this tactical can make proofs less readable or more\n", + "difficult to maintain. Alternatively, some uses can make proofs more\n", + "readable or easier to maintain. It is always good to think about your\n", + "priorities when writing a proof script.)\n", + "\n", + "Revise the proof for `value_is_normal_form` to include uses of the `;`\n", + "tactical.\n", + "\n", + "**Example** Sometimes it is helpful to be able to use forward reasoning\n", + "in a proof. One form of forward reasoning can be done with the tactic\n", + "`assert`. `assert` adds a new hypothesis to the context but asks us to\n", + "first justify it." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma nvalue_is_normal_form : forall v,\n", + " nvalue v ->\n", + " normal_form v.\n", + "Proof.\n", + " intros v Hnv.\n", + " assert (value v) as Hv. right. apply Hnv.\n", + " apply value_is_normal_form. apply Hv.\n", + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Example** `assert` can also be supplied with a tactic that proves the\n", + "assertion. We rewrite the above proof using this form." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma nvalue_is_normal_form' : forall v,\n", + " nvalue v ->\n", + " normal_form v.\n", + "Proof.\n", + " intros v Hnv.\n", + " assert (value v) as Hv by (right; apply Hnv).\n", + " apply value_is_normal_form. apply Hv.\n", + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Example** The proof below introduces two new, simple tactics. First,\n", + "the tactic `replace e1 with e2` performs a substitution in the goal and\n", + "then requires that you prove `e2 = e1` as a new subgoal. This often\n", + "allows us to avoid more cumbersome forms of forward reasoning. Second,\n", + "the `clear` tactic discards a hypothesis from the context. Of course,\n", + "this tactic is never needed, but it can be nice to use when there are\n", + "complicated, irrelevant hypotheses in the context." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma single_step_to_multi_step_determinacy :\n", + " (forall t u1 u2, eval t u1 -> eval t u2 -> u1 = u2) ->\n", + " forall t v1 v2,\n", + " eval_many t v1 -> normal_form v1 ->\n", + " eval_many t v2 -> normal_form v2 ->\n", + " v1 = v2.\n", + "Proof.\n", + " intros H t v1 v2 Hm1 Hnf1 Hm2 Hnf2. induction Hm1.\n", + " clear H. destruct Hm2.\n", + " reflexivity.\n", + " destruct Hnf1. exists t'. apply H.\n", + " destruct Hm2.\n", + " destruct Hnf2. exists t'. apply H0.\n", + " apply IHHm1; clear IHHm1.\n", + " apply Hnf1.\n", + " replace t' with t'0.\n", + " apply Hm2.\n", + " apply H with (t := t).\n", + " apply H1.\n", + " apply H0.\n", + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Exercise** This proof is lengthy and thus somewhat challenging. All of\n", + "the techniques from this section will be useful; some will be essential.\n", + "In particular, you will need to use `generalize dependent` at the\n", + "beginning of the proof. You will find `assert` helpful in the cases\n", + "where your assumptions are contradictory but none of them are in a\n", + "negative form. In that situation, you can assert a negative statement\n", + "that follows from your hypotheses (recall that `normal_form` is a\n", + "negative statement). Finally, you will want to use the above lemma\n", + "`nvalue_is_normal_form`. Good luck!" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Theorem eval_deterministic : forall t t' t'',\n", + " eval t t' ->\n", + " eval t t'' ->\n", + " t' = t''.\n", + "Proof.\n", + " (* to finish *)\n", + "Admitted." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Exercise** Prove the following lemmas. The last is quite long, and you\n", + "may wish to wait until you know more about automation.\n", + "\n", + " Lemma full_eval_from_value : forall v w,\n", + " value v ->\n", + " full_eval v w ->\n", + " v = w.\n", + "\n", + " Lemma eval_full_eval : forall t t' v,\n", + " eval t t' ->\n", + " full_eval t' v ->\n", + " full_eval t v.\n", + "\n", + " Lemma full_eval_complete : forall t v,\n", + " value v ->\n", + " eval_many t v ->\n", + " full_eval t v.\n", + "\n", + "Basic Automation\n", + "----------------" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " - [eapply], [esplit]\n", + " - [auto], [eauto]" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Example** You can use `eapply e` instead of `apply e with (x := e1)`.\n", + "This will generate subgoals containing unification variables that will\n", + "get unified during subsequent uses of `apply`." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma m_if : forall t1 u1 t2 t3,\n", + " eval_many t1 u1 ->\n", + " eval_many (tm_if t1 t2 t3) (tm_if u1 t2 t3).\n", + "Proof.\n", + " intros t1 u1 t2 t3 Hm. induction Hm.\n", + " apply m_refl.\n", + " eapply m_step.\n", + " apply e_if. apply H.\n", + " apply IHHm.\n", + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Example** You can use `esplit` to turn an existentially quantified\n", + "variable in your goal into a unification variable." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma exists_pred_zero :\n", + " exists u, eval (tm_pred tm_zero) u.\n", + "Proof.\n", + " esplit. apply e_predzero.\n", + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Example** The `auto` tactic solves goals that are solvable by any\n", + "combination of\n", + "\n", + "- `intros`\n", + "- `apply` (used on some local hypothesis)\n", + "- `split`, `left`, `right`\n", + "- `reflexivity`\n", + "\n", + "If `auto` cannot solve the goal, it will leave the proof state\n", + "completely unchanged (without generating any errors).\n", + "\n", + "The lemma below is a proposition that has been contrived for the sake of\n", + "demonstrating the scope of the `auto` tactic and does not say anything\n", + "of practical interest. So instead of thinking about what it means, you\n", + "should think about the operations that `auto` had to perform to solve\n", + "the goal.\n", + "\n", + "Note: It is important to remember that `auto` does not destruct\n", + "hypotheses! There are more advanced forms of automation available that\n", + "do destruct hypotheses in some specific ways." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma auto_example : forall t t' t'',\n", + " eval t t' ->\n", + " eval t' t'' ->\n", + " (forall u, eval t t' -> eval t' u -> eval_many t u) ->\n", + " eval t' t \\/ t = t /\\ eval_many t t''.\n", + "Proof.\n", + " auto.\n", + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Example** The `eauto` tactic solves goals that are solvable by some\n", + "combination of\n", + "\n", + "- `intros`\n", + "- `eapply` (used on some local hypothesis)\n", + "- `split`, `left`, `right`\n", + "- `esplit`\n", + "- `reflexivity`\n", + "\n", + "lemma has two significantly differences from the previous one, both of\n", + "which render `auto` useless." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma eauto_example : forall t t' t'',\n", + " eval t t' ->\n", + " eval t' t'' ->\n", + " (forall u, eval t u -> eval u t'' -> eval_many t t'') ->\n", + " eval t' t \\/ (exists u, t = u) /\\ eval_many t t''.\n", + "Proof.\n", + " eauto.\n", + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Example** You can enhance `auto` (or `eauto`) by appending\n", + "`using x_1, ..., x_n`, where each `x_i` is the name of some constructor\n", + "or lemma. Then `auto` will attempt to apply those constructors or lemmas\n", + "in addition to the assumptions in the local context." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma eauto_using_example : forall t t' t'',\n", + " eval t t' ->\n", + " eval t' t'' ->\n", + " eval t' t \\/ t = t /\\ eval_many t t''.\n", + "Proof.\n", + " eauto using m_step, m_one.\n", + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "#### Lab 7\n", + "\n", + "**Exercise** Go back and rewrite your proofs for `m_one`, `m_two`, and\n", + "`m_iftrue_step`. You should be able to make them very succinct given\n", + "what you know now.\n", + "\n", + "**Exercise** See how short you can make these proofs.\n", + "\n", + "Note: This is an exercise. We are not making the claim that shorter\n", + "proofs are necessarily better!\n", + "\n", + "Hint: Remember that we can connect tactics in sequence with `;`.\n", + "However, as you can imagine, figuring out the best thing to write after\n", + "a `;` usually involves some trial and error." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma pred_not_circular : forall t,\n", + " t <> tm_pred t.\n", + "Proof.\n", + " (* to finish *)\n", + "Admitted." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma m_succ : forall t u,\n", + " eval_many t u ->\n", + " eval_many (tm_succ t) (tm_succ u).\n", + "Proof.\n", + " (* to finish *)\n", + "Admitted." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma m_pred : forall t u,\n", + " eval_many t u ->\n", + " eval_many (tm_pred t) (tm_pred u).\n", + "Proof.\n", + " (* to finish *)\n", + "Admitted." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Exercise** Go back and rewrite your proofs for `m_trans` and\n", + "`two_values`. Pulling together several tricks you’ve learned, you should\n", + "be able to prove `two_values` in one (short) line. Since this is a\n", + "notebook, the easiest way for you to do that may be to copy the cells\n", + "here.\n", + "\n", + "**Note** Sometimes there are lemmas or constructors that are so\n", + "frequently needed by `auto` that we don’t want to have to add them to\n", + "our `using` clause each time. Coq allows us to request that certain\n", + "propositions that always be considered by `auto` and `eauto`.\n", + "\n", + "The following command adds four lemmas to the default search procedure\n", + "of `auto`." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Hint Resolve m_if m_succ m_pred m_iszero." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Constructors of inductively defined propositions are some of the most\n", + "frequently needed by `auto`. Instead of writing\n", + "\n", + " Hint Resolve b_true b_false.\n", + "\n", + "we may simply write\n", + "\n", + " Hint Constructors bvalue.\n", + "\n", + "Let’s add all our constructors to `auto`." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Hint Constructors bvalue nvalue eval eval_many." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "By default `auto` will never try to unfold definitions to see if a lemma\n", + "or constructor can be applied. With the `Hint Unfold` command, we can\n", + "instruct `auto` to try unfold definitions in the goal as it is working." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Hint Unfold value normal_form." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "There are a few more variants on the `Hint` command that can be used to\n", + "further customize `auto`. You can learn about them in the Coq reference\n", + "manual.\n", + "\n", + "Functions and Conversion\n", + "------------------------" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + " - [Fixpoint/struct]\n", + " - [match ... end]\n", + " - [if ... then ... else ...]\n", + " - [simpl]\n", + " - [remember]" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "In this section we start to use Coq as a programming language and learn\n", + "how to reason about programs defined within Coq.\n", + "\n", + "**Example** Coq defines many datatypes in its standard libraries. Have a\n", + "quick look now through the library `Datatypes` to see some of the basic\n", + "ones, in particular `bool` and `nat`. (Note that constructors of the\n", + "datatype `nat` are the letter `O` and the letter `S`. However, Coq will\n", + "parse and print `nat`s using a standard decimal representation.)\n", + "\n", + "We define two more datatypes here that will be useful later." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Inductive bool_option : Set :=\n", + "| some_bool : bool -> bool_option\n", + "| no_bool : bool_option." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Inductive nat_option : Set :=\n", + "| some_nat : nat -> nat_option\n", + "| no_nat : nat_option." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Example** We can define simple (non-recursive) functions from one\n", + "datatype to another using the `Definition` keyword. The `match`\n", + "construct allows us to do case analysis on a datatype. The `match`\n", + "expression has a first-match semantics and allows nested patterns;\n", + "however, Coq’s type checker demands that pattern-matching be exhaustive.\n", + "\n", + "We define functions below for converting between Coq `bool`s and boolean\n", + "values in our object language." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Definition tm_to_bool (t : tm) : bool_option :=\n", + " match t with\n", + " | tm_true => some_bool true\n", + " | tm_false => some_bool false\n", + " | _ => no_bool\n", + " end." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Definition bool_to_tm (b : bool) : tm :=\n", + " match b with\n", + " | true => tm_true\n", + " | false => tm_false\n", + " end." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Example** Coq also has an `if/then/else` expression. It can be used,\n", + "not just with the type `bool` but, in fact, with any datatype having\n", + "exactly two constructors (the first constructor corresponding to the\n", + "`then` branch and the second to the `else` branch). Thus, we can define\n", + "a function `is_bool` as below." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Definition is_bool (t : tm) : bool :=\n", + " if tm_to_bool t then true else false." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Example** To define a recursive function, use `Fixpoint` instead of\n", + "`Definition`.\n", + "\n", + "The type system will only allow us to write functions that terminate.\n", + "The annotation `{struct t}` here informs the type-checker that\n", + "termination is guaranteed because the function is being defined by\n", + "structural recursion on `t`." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Fixpoint tm_to_nat (t : tm) {struct t} : nat_option :=\n", + " match t with\n", + " | tm_zero => some_nat O\n", + " | tm_succ t1 =>\n", + " match tm_to_nat t1 with\n", + " | some_nat n => some_nat (S n)\n", + " | no_nat => no_nat\n", + " end\n", + " | _ => no_nat\n", + " end.\n", + "\n", + "Fixpoint nat_to_tm (n : nat) {struct n} : tm :=\n", + " match n with\n", + " | O => tm_zero\n", + " | S m => tm_succ (nat_to_tm m)\n", + " end." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Exercise** Write a function `interp : tm -> tm` that returns the\n", + "normal form of its argument according to the small-step semantics given\n", + "by `eval`.\n", + "\n", + "Hint: You will want to use `tm_to_nat` (or another auxiliary function)\n", + "to prevent stuck terms from stepping in the cases `e_predsucc` and\n", + "`e_iszerosucc`.\n", + "\n", + "**Example** The tactic `simpl` (recursively) reduces the application of\n", + "a function defined by pattern-matching to an argument with a constructor\n", + "at its head. You can supply `simpl` with a particular expression if you\n", + "want to prevent it from simplifying elsewhere." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma bool_tm_bool : forall b,\n", + " tm_to_bool (bool_to_tm b) = some_bool b.\n", + "Proof.\n", + " intros b. destruct b.\n", + " simpl (bool_to_tm true). simpl. reflexivity.\n", + " (* It turns out that [simpl] is unnecessary above, since\n", + " [reflexivity] can automatically check that two terms are\n", + " convertible. *)\n", + " reflexivity.\n", + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Example** We can also apply the tactic `simpl` in our hypotheses." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma tm_bool_tm :forall t b,\n", + " tm_to_bool t = some_bool b ->\n", + " bool_to_tm b = t.\n", + "Proof.\n", + " intros t b Heq. destruct t.\n", + " simpl in Heq. inversion Heq.\n", + " simpl. reflexivity.\n", + " (* As with [reflexivity], [inversion] can automatically\n", + " perform reduction on terms as necessary, so the above use\n", + " of [simpl] was optional. *)\n", + " inversion Heq. reflexivity.\n", + " simpl in Heq. inversion Heq.\n", + " (* Again, the above use of [simpl] was optional. *)\n", + " inversion Heq.\n", + " inversion Heq.\n", + " inversion Heq.\n", + " inversion Heq.\n", + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Exercise**" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma tm_to_bool_dom_includes_bvalue : forall bv,\n", + " bvalue bv -> exists b, tm_to_bool bv = some_bool b.\n", + "Proof.\n", + " (* to finish *)\n", + "Admitted." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Exercise**" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma tm_to_bool_dom_only_bvalue : forall bv b,\n", + " tm_to_bool bv = some_bool b -> bvalue bv.\n", + "Proof.\n", + " (* to finish *)\n", + "Admitted." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Example** Not all uses of `simpl` are optional. Sometimes they are\n", + "necessary so that we can use the `rewrite` tactic. Observe, also, how\n", + "using `rewrite` can automatically trigger a reduction if it creates a\n", + "redex." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma nat_tm_nat : forall n,\n", + " tm_to_nat (nat_to_tm n) = some_nat n.\n", + "Proof.\n", + " intros n. induction n.\n", + " reflexivity.\n", + " simpl. rewrite -> IHn. reflexivity.\n", + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Example** Here’s an example where it is necessary to use `simpl` on a\n", + "hypothesis. To trigger a reduction of a `match` expression in a\n", + "hypothesis, we use the `destruct` tactic on the expression being\n", + "matched." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma tm_nat_tm : forall t n,\n", + " tm_to_nat t = some_nat n ->\n", + " nat_to_tm n = t.\n", + "Proof.\n", + " intros t. induction t; intros n Heq.\n", + " inversion Heq.\n", + " inversion Heq.\n", + " inversion Heq.\n", + " inversion Heq. reflexivity.\n", + " simpl in Heq. destruct (tm_to_nat t).\n", + " inversion Heq. simpl. rewrite -> IHt.\n", + " (* Note how we may use [rewrite] even on an equation\n", + " that is preceded by some other hypotheses. *)\n", + " reflexivity.\n", + " reflexivity.\n", + " inversion Heq.\n", + " inversion Heq.\n", + " inversion Heq.\n", + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Exercise**" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma tm_to_nat_dom_includes_nvalue : forall v,\n", + " nvalue v -> exists n, tm_to_nat v = some_nat n.\n", + "Proof.\n", + " (* to finish *)\n", + "Admitted." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Exercise**" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma tm_to_nat_dom_only_nvalue : forall v n,\n", + " tm_to_nat v = some_nat n -> nvalue v.\n", + "Proof.\n", + " (* to finish *)\n", + "Admitted." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Example** Using the tactic `destruct` (or `induction`) on a complex\n", + "expression (i.e., one that is not simply a variable) may not leave you\n", + "with enough information for you to finish the proof. The tactic\n", + "`remember` can help in these cases. Its usage is demonstrated below. If\n", + "you are curious, try to finish the proof without `remember` to see what\n", + "goes wrong." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Lemma remember_example : forall v,\n", + " eval_many\n", + " (tm_pred (tm_succ v))\n", + " (match tm_to_nat v with\n", + " | some_nat _ => v\n", + " | no_nat => tm_pred (tm_succ v)\n", + " end).\n", + "Proof.\n", + " intros v. remember (tm_to_nat v) as x. destruct x.\n", + " apply m_one. apply e_predsucc.\n", + " eapply tm_to_nat_dom_only_nvalue.\n", + " rewrite <- Heqx. reflexivity.\n", + " apply m_refl.\n", + "Qed." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "**Exercise** Prove the following lemmas involving the function `interp`\n", + "from a previous exercise:\n", + "\n", + " Lemma interp_reduces : forall t,\n", + " eval_many t (interp t).\n", + "\n", + " Lemma interp_fully_reduces : forall t,\n", + " normal_form (interp t).\n", + "\n", + "Solutions to Exercises\n", + "======================" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Inductive eval_rtc : tm -> tm -> Prop :=\n", + "| r_eval : forall t t',\n", + " eval t t' ->\n", + " eval_rtc t t'\n", + "| r_refl : forall t,\n", + " eval_rtc t t\n", + "| r_trans : forall t u v,\n", + " eval_rtc t u ->\n", + " eval_rtc u v ->\n", + " eval_rtc t v.\n", + "\n", + "Inductive full_eval : tm -> tm -> Prop :=\n", + "| f_value : forall v,\n", + " value v ->\n", + " full_eval v v\n", + "| f_iftrue : forall t1 t2 t3 v,\n", + " full_eval t1 tm_true ->\n", + " full_eval t2 v ->\n", + " full_eval (tm_if t1 t2 t3) v\n", + "| f_iffalse : forall t1 t2 t3 v,\n", + " full_eval t1 tm_false ->\n", + " full_eval t3 v ->\n", + " full_eval (tm_if t1 t2 t3) v\n", + "| f_succ : forall t v,\n", + " nvalue v ->\n", + " full_eval t v ->\n", + " full_eval (tm_succ t) (tm_succ v)\n", + "| f_predzero : forall t,\n", + " full_eval t tm_zero ->\n", + " full_eval (tm_pred t) tm_zero\n", + "| f_predsucc : forall t v,\n", + " nvalue v ->\n", + " full_eval t (tm_succ v) ->\n", + " full_eval (tm_pred t) v\n", + "| f_iszerozero : forall t,\n", + " full_eval t tm_zero ->\n", + " full_eval (tm_iszero t) tm_true\n", + "| f_iszerosucc : forall t v,\n", + " nvalue v ->\n", + " full_eval t (tm_succ v) ->\n", + " full_eval (tm_iszero t) tm_false.\n", + "\n", + "Lemma m_one_sol : forall t t',\n", + " eval t t' ->\n", + " eval_many t t'.\n", + "Proof.\n", + " intros t t' He. apply m_step with (t' := t').\n", + " apply He.\n", + " apply m_refl.\n", + "Qed.\n", + "\n", + "Lemma m_two_sol : forall t t' t'',\n", + " eval t t' ->\n", + " eval t' t'' ->\n", + " eval_many t t''.\n", + "Proof.\n", + " intros t t' t'' He1 He2. apply m_step with (t' := t').\n", + " apply He1.\n", + " apply m_one. apply He2.\n", + "Qed.\n", + "\n", + "Lemma m_iftrue_step_sol : forall t t1 t2 u,\n", + " eval t tm_true ->\n", + " eval_many t1 u ->\n", + " eval_many (tm_if t t1 t2) u.\n", + "Proof.\n", + " intros t t1 t2 u He Hm.\n", + " apply m_step with (t' := tm_if tm_true t1 t2).\n", + " apply e_if. apply He.\n", + " apply m_step with (t' := t1).\n", + " apply e_iftrue.\n", + " apply Hm.\n", + "Qed.\n", + "\n", + "Lemma m_if_iszero_conj_sol : forall v t2 t2' t3 t3',\n", + " nvalue v /\\ eval t2 t2' /\\ eval t3 t3' ->\n", + " eval_many (tm_if (tm_iszero tm_zero) t2 t3) t2' /\\\n", + " eval_many (tm_if (tm_iszero (tm_succ v)) t2 t3) t3'.\n", + "Proof.\n", + " intros v t2 t2' t3 t3' H.\n", + " destruct H as [ Hn [ He1 He2 ] ]. split.\n", + " apply m_three with\n", + " (t' := tm_if tm_true t2 t3) (t'' := t2).\n", + " apply e_if. apply e_iszerozero.\n", + " apply e_iftrue.\n", + " apply He1.\n", + " apply m_three with\n", + " (t' := tm_if tm_false t2 t3) (t'' := t3).\n", + " apply e_if. apply e_iszerosucc. apply Hn.\n", + " apply e_iffalse.\n", + " apply He2.\n", + "Qed.\n", + "\n", + "Lemma two_values_sol : forall t u,\n", + " value t /\\ value u ->\n", + " bvalue t \\/\n", + " bvalue u \\/\n", + " (nvalue t /\\ nvalue u).\n", + "Proof.\n", + " unfold value. intros t u H.\n", + " destruct H as [ [ Hb1 | Hn1 ] H2 ].\n", + " left. apply Hb1.\n", + " destruct H2 as [ Hb2 | Hn2 ].\n", + " right. left. apply Hb2.\n", + " right. right. split.\n", + " apply Hn1.\n", + " apply Hn2.\n", + "Qed.\n", + "\n", + "Lemma m_trans_sol : forall t u v,\n", + " eval_many t u ->\n", + " eval_many u v ->\n", + " eval_many t v.\n", + "Proof.\n", + " intros t u v Hm1 Hm2. induction Hm1.\n", + " apply Hm2.\n", + " apply m_step with (t' := t').\n", + " apply H.\n", + " apply IHHm1. apply Hm2.\n", + "Qed.\n", + "\n", + "Lemma eval_rtc_many_sol : forall t u,\n", + " eval_rtc t u ->\n", + " eval_many t u.\n", + "Proof.\n", + " intros t u Hr. induction Hr.\n", + " apply m_one. apply H.\n", + " apply m_refl.\n", + " apply m_trans with (t' := u).\n", + " apply IHHr1.\n", + " apply IHHr2.\n", + "Qed.\n", + "\n", + "Lemma eval_many_rtc_sol : forall t u,\n", + " eval_many t u ->\n", + " eval_rtc t u.\n", + "Proof.\n", + " intros t u Hm. induction Hm.\n", + " apply r_refl.\n", + " apply r_trans with (u := t').\n", + " apply r_eval. apply H.\n", + " apply IHHm.\n", + "Qed.\n", + "\n", + "Lemma full_eval_to_value_sol : forall t v,\n", + " full_eval t v ->\n", + " value v.\n", + "Proof.\n", + " intros t v Hf. induction Hf.\n", + " apply H.\n", + " apply IHHf2.\n", + " apply IHHf2.\n", + " right. apply n_succ. apply H.\n", + " right. apply n_zero.\n", + " right. apply H.\n", + " left. apply b_true.\n", + " left. apply b_false.\n", + "Qed.\n", + "\n", + "Lemma value_can_expand_sol : forall v,\n", + " value v ->\n", + " exists u, eval u v.\n", + "Proof.\n", + " intros v Hv. exists (tm_if tm_true v v). apply e_iftrue.\n", + "Qed.\n", + "\n", + "Lemma exists_iszero_nvalue_sol : forall t,\n", + " (exists nv, nvalue nv /\\ eval_many t nv) ->\n", + " exists bv, eval_many (tm_iszero t) bv.\n", + "Proof.\n", + " intros t [ nv [ Hnv Hm ]]. destruct Hnv.\n", + " exists tm_true.\n", + " apply m_trans with (t' := tm_iszero tm_zero).\n", + " apply m_iszero. apply Hm.\n", + " apply m_one. apply e_iszerozero.\n", + " exists tm_false.\n", + " apply m_trans with (t' := tm_iszero (tm_succ t0)).\n", + " apply m_iszero. apply Hm.\n", + " apply m_one. apply e_iszerosucc. apply Hnv.\n", + "Qed.\n", + "\n", + "Lemma normal_form_to_forall_sol : forall t,\n", + " normal_form t ->\n", + " forall u, ~ eval t u.\n", + "Proof.\n", + " unfold normal_form, not. intros t H u He.\n", + " apply H. exists u. apply He.\n", + "Qed.\n", + "\n", + "Lemma normal_form_from_forall_sol : forall t,\n", + " (forall u, ~ eval t u) ->\n", + " normal_form t.\n", + "Proof.\n", + " unfold normal_form, not. intros t H [ t' Het' ].\n", + " apply H with (u := t'). apply Het'.\n", + "Qed. \n", + "\n", + "Lemma negation_exercise_sol : forall v1 v2,\n", + " ~ (value v1 \\/ value v2) ->\n", + " ~ (~ bvalue v1 /\\ ~ bvalue v2) ->\n", + " eval tm_true tm_false.\n", + "Proof.\n", + " intros v1 v2 H1 H2. destruct H2.\n", + " split.\n", + " intros Hb. destruct H1. left. left. apply Hb.\n", + " intros Hb. destruct H1. right. left. apply Hb.\n", + "Qed.\n", + "\n", + "Lemma equality_exercise_sol : forall t1 t2 t3 u1 u2 u3 u4,\n", + " tm_if t1 t2 t3 = tm_if u1 u2 u2 ->\n", + " tm_if t1 t2 t3 = tm_if u3 u3 u4 ->\n", + " t1 = u4.\n", + "Proof.\n", + " intros t1 t2 t3 u1 u2 u3 u4 Heq1 Heq2.\n", + " inversion Heq1. subst t1. subst t2. subst t3.\n", + " inversion Heq2. reflexivity.\n", + "Qed.\n", + "\n", + "Lemma succ_not_circular_sol : forall t,\n", + " t <> tm_succ t.\n", + "Proof.\n", + " intros t. induction t.\n", + " intros Heq. inversion Heq.\n", + " intros Heq. inversion Heq.\n", + " intros Heq. inversion Heq.\n", + " intros Heq. inversion Heq.\n", + " intros Heq. inversion Heq. destruct IHt. apply H0.\n", + " intros Heq. inversion Heq.\n", + " intros Heq. inversion Heq.\n", + "Qed.\n", + "\n", + "Lemma inversion_exercise_sol : forall t,\n", + " normal_form t ->\n", + " eval_many (tm_pred t) tm_zero ->\n", + " nvalue t.\n", + "Proof.\n", + " intros t Hnf Hm. inversion Hm. subst. inversion H.\n", + " apply n_zero.\n", + " apply n_succ. apply H2.\n", + " destruct Hnf. exists t'0. apply H2.\n", + "Qed.\n", + "\n", + "Lemma contradictory_equalities_exercise_sol :\n", + " (exists t, exists u, exists v,\n", + " value t /\\\n", + " t = tm_succ u /\\\n", + " u = tm_pred v) ->\n", + " eval tm_true tm_false.\n", + "Proof.\n", + " intros [ t [ u [ v [ [ Hb | Hn ] [ eq1 eq2 ] ] ] ] ].\n", + " destruct Hb.\n", + " inversion eq1.\n", + " inversion eq1.\n", + " destruct Hn.\n", + " inversion eq1.\n", + " inversion eq1. subst t. subst u. inversion Hn.\n", + "Qed.\n", + "\n", + "Lemma eval_fact_exercise_sol : forall t1 t2,\n", + " eval (tm_iszero (tm_pred t1)) t2 ->\n", + " eval t2 tm_false ->\n", + " exists u, t1 = tm_succ u.\n", + "Proof.\n", + " intros t1 t2 He1 He2. inversion He1. subst t2.\n", + " inversion He2. subst t'.\n", + " inversion H0. exists (tm_succ t0). reflexivity.\n", + "Qed.\n", + "\n", + "Lemma normal_form_if_sol : forall t1 t2 t3,\n", + " normal_form (tm_if t1 t2 t3) ->\n", + " t1 <> tm_true /\\ t1 <> tm_false /\\ normal_form t1.\n", + "Proof.\n", + " intros t1 t2 t3 Hnf. destruct t1.\n", + " destruct Hnf. exists t2. apply e_iftrue.\n", + " destruct Hnf. exists t3. apply e_iffalse.\n", + " split.\n", + " intros Heq. inversion Heq.\n", + " split.\n", + " intros Heq. inversion Heq.\n", + " intros [t' He]. destruct Hnf. exists (tm_if t' t2 t3).\n", + " apply e_if. apply He.\n", + " split.\n", + " intros Heq. inversion Heq.\n", + " split.\n", + " intros Heq. inversion Heq.\n", + " intros [t' He]. inversion He.\n", + " split.\n", + " intros Heq. inversion Heq.\n", + " split.\n", + " intros Heq. inversion Heq.\n", + " intros [t' He]. destruct Hnf. exists (tm_if t' t2 t3).\n", + " apply e_if. apply He.\n", + " split.\n", + " intros Heq. inversion Heq.\n", + " split.\n", + " intros Heq. inversion Heq.\n", + " intros [t' He]. destruct Hnf. exists (tm_if t' t2 t3).\n", + " apply e_if. apply He.\n", + " split.\n", + " intros Heq. inversion Heq.\n", + " split.\n", + " intros Heq. inversion Heq.\n", + " intros [t' He]. destruct Hnf. exists (tm_if t' t2 t3).\n", + " apply e_if. apply He.\n", + "Qed.\n", + "\n", + "Lemma full_eval_from_value_sol : forall v w,\n", + " value v ->\n", + " full_eval v w ->\n", + " v = w.\n", + "Proof.\n", + " intros v w Hv Hf. induction Hf.\n", + " reflexivity.\n", + " destruct Hv as [ Hb | Hn ].\n", + " inversion Hb.\n", + " inversion Hn.\n", + " destruct Hv as [ Hb | Hn ].\n", + " inversion Hb.\n", + " inversion Hn.\n", + " rewrite -> IHHf.\n", + " reflexivity.\n", + " right. apply value_succ_nvalue. apply Hv.\n", + " destruct Hv as [ Hb | Hn ].\n", + " inversion Hb.\n", + " inversion Hn.\n", + " destruct Hv as [ Hb | Hn ].\n", + " inversion Hb.\n", + " inversion Hn.\n", + " destruct Hv as [ Hb | Hn ].\n", + " inversion Hb.\n", + " inversion Hn.\n", + " destruct Hv as [ Hb | Hn ].\n", + " inversion Hb.\n", + " inversion Hn.\n", + "Qed.\n", + "\n", + "Lemma value_is_normal_form_sol : forall v,\n", + " value v ->\n", + " normal_form v.\n", + "Proof.\n", + " intros v [ Hb | Hn ] [ t He ].\n", + " destruct Hb; inversion He.\n", + " generalize dependent t.\n", + " induction Hn; intros u He; inversion He; subst.\n", + " destruct (IHHn t'). apply H0.\n", + "Qed.\n", + "\n", + "Theorem eval_deterministic_sol : forall t t' t'',\n", + " eval t t' ->\n", + " eval t t'' ->\n", + " t' = t''.\n", + "Proof.\n", + " intros t t' t'' He1. generalize dependent t''.\n", + " induction He1; intros t'' He2; inversion He2; subst.\n", + " reflexivity.\n", + " inversion H3.\n", + " reflexivity.\n", + " inversion H3.\n", + " inversion He1.\n", + " inversion He1.\n", + " rewrite -> (IHHe1 t1'0).\n", + " reflexivity.\n", + " apply H3.\n", + " rewrite -> (IHHe1 t'0).\n", + " reflexivity.\n", + " apply H0.\n", + " reflexivity.\n", + " inversion H0.\n", + " reflexivity.\n", + " assert (normal_form (tm_succ t)) as Hnf.\n", + " apply nvalue_is_normal_form. apply n_succ. apply H.\n", + " destruct Hnf. exists t'. apply H1.\n", + " inversion He1.\n", + " assert (normal_form (tm_succ t'')) as Hnf.\n", + " apply nvalue_is_normal_form. apply n_succ. apply H0.\n", + " destruct Hnf. exists t'. apply He1.\n", + " rewrite -> (IHHe1 t'0).\n", + " reflexivity.\n", + " apply H0.\n", + " reflexivity.\n", + " inversion H0.\n", + " reflexivity.\n", + " assert (normal_form (tm_succ t)) as Hnf.\n", + " apply nvalue_is_normal_form. apply n_succ. apply H.\n", + " destruct Hnf. exists t'. apply H1.\n", + " inversion He1.\n", + " assert (normal_form (tm_succ t0)) as Hnf.\n", + " apply nvalue_is_normal_form. apply n_succ. apply H0.\n", + " destruct Hnf. exists t'. apply He1.\n", + " rewrite -> (IHHe1 t'0).\n", + " reflexivity.\n", + " apply H0.\n", + "Qed.\n", + "\n", + "Lemma eval_full_eval_sol : forall t t' v,\n", + " eval t t' ->\n", + " full_eval t' v ->\n", + " full_eval t v.\n", + "Proof.\n", + " intros t t' v He. generalize dependent v. induction He.\n", + " intros v Hf. apply f_iftrue.\n", + " apply f_value. left. apply b_true.\n", + " apply Hf.\n", + " intros v Hf. apply f_iffalse.\n", + " apply f_value. left. apply b_false.\n", + " apply Hf.\n", + " intros v Hf. inversion Hf.\n", + " subst. inversion H.\n", + " inversion H0.\n", + " inversion H0.\n", + " subst. apply f_iftrue.\n", + " apply IHHe. apply H3.\n", + " apply H4.\n", + " subst. apply f_iffalse.\n", + " apply IHHe. apply H3.\n", + " apply H4.\n", + " intros v Hf. inversion Hf.\n", + " subst. apply f_succ.\n", + " apply value_succ_nvalue. apply H.\n", + " apply IHHe. apply f_value. right.\n", + " apply value_succ_nvalue. apply H.\n", + " subst. apply f_succ.\n", + " apply H0.\n", + " apply IHHe. apply H1.\n", + " intros v Hf. inversion Hf. apply f_predzero.\n", + " apply f_value. right. apply n_zero.\n", + " intros v Hf. assert (t = v).\n", + " apply full_eval_from_value_sol.\n", + " right. apply H.\n", + " apply Hf.\n", + " subst v. apply f_predsucc.\n", + " apply H.\n", + " apply f_succ.\n", + " apply H.\n", + " apply Hf.\n", + " intros v Hf. inversion Hf.\n", + " subst. destruct H as [ Hb | Hn ].\n", + " inversion Hb.\n", + " inversion Hn.\n", + " subst. apply f_predzero. apply IHHe. apply H0.\n", + " subst. apply f_predsucc.\n", + " apply H0.\n", + " apply IHHe. apply H1.\n", + " intros v Hf. inversion Hf. apply f_iszerozero.\n", + " apply f_value. right. apply n_zero.\n", + " intros v Hf. inversion Hf.\n", + " apply f_iszerosucc with (v := t).\n", + " apply H.\n", + " apply f_value. right. apply n_succ. apply H.\n", + " intros v Hf. inversion Hf.\n", + " subst. destruct H as [ Hb | Hn ].\n", + " inversion Hb.\n", + " inversion Hn.\n", + " subst. apply f_iszerozero. apply IHHe. apply H0.\n", + " subst. apply f_iszerosucc with (v := v0).\n", + " apply H0.\n", + " apply IHHe. apply H1.\n", + "Qed.\n", + "\n", + "Lemma full_eval_complete_sol : forall t v,\n", + " value v ->\n", + " eval_many t v ->\n", + " full_eval t v.\n", + "Proof.\n", + " intros t v Hv Hm. induction Hm.\n", + " apply f_value. apply Hv.\n", + " apply eval_full_eval_sol with (t' := t').\n", + " apply H.\n", + " apply IHHm. apply Hv.\n", + "Qed.\n", + "\n", + "Lemma pred_not_circular_sol : forall t,\n", + " t <> tm_pred t.\n", + "Proof.\n", + " intros t H. induction t; inversion H; auto.\n", + "Qed.\n", + "\n", + "Lemma m_succ_sol : forall t u,\n", + " eval_many t u ->\n", + " eval_many (tm_succ t) (tm_succ u).\n", + "Proof.\n", + " intros t u Hm.\n", + " induction Hm; eauto using m_refl, m_step, e_succ.\n", + "Qed.\n", + "\n", + "Lemma m_pred_sol : forall t u,\n", + " eval_many t u ->\n", + " eval_many (tm_pred t) (tm_pred u).\n", + "Proof.\n", + " intros t u Hm.\n", + " induction Hm; eauto using m_refl, m_step, e_pred.\n", + "Qed.\n", + "\n", + "Fixpoint interp (t : tm) {struct t} : tm :=\n", + " match t with\n", + " | tm_true => tm_true\n", + " | tm_false => tm_false\n", + " | tm_if t1 t2 t3 =>\n", + " match interp t1 with\n", + " | tm_true => interp t2\n", + " | tm_false => interp t3\n", + " | t4 => tm_if t4 t2 t3\n", + " end\n", + " | tm_zero => tm_zero\n", + " | tm_succ t1 => tm_succ (interp t1)\n", + " | tm_pred t1 =>\n", + " match interp t1 with\n", + " | tm_zero => tm_zero\n", + " | tm_succ t2 =>\n", + " match tm_to_nat t2 with\n", + " | some_nat _ => t2\n", + " | no_nat => tm_pred (tm_succ t2)\n", + " end\n", + " | t2 => tm_pred t2\n", + " end\n", + " | tm_iszero t1 =>\n", + " match interp t1 with\n", + " | tm_zero => tm_true\n", + " | tm_succ t2 =>\n", + " match tm_to_nat t2 with\n", + " | some_nat _ => tm_false\n", + " | no_nat => tm_iszero (tm_succ t2)\n", + " end\n", + " | t2 => tm_iszero t2\n", + " end\n", + " end.\n", + "\n", + "Lemma tm_to_bool_dom_includes_bvalue_sol : forall bv,\n", + " bvalue bv -> exists b, tm_to_bool bv = some_bool b.\n", + "Proof.\n", + " intros bv H. destruct H.\n", + " exists true. reflexivity.\n", + " exists false. reflexivity.\n", + "Qed.\n", + "\n", + "Lemma tm_to_bool_dom_only_bvalue_sol : forall bv b,\n", + " tm_to_bool bv = some_bool b -> bvalue bv.\n", + "Proof.\n", + " intros bv b Heq. destruct bv.\n", + " apply b_true.\n", + " apply b_false.\n", + " inversion Heq.\n", + " inversion Heq.\n", + " inversion Heq.\n", + " inversion Heq.\n", + " inversion Heq.\n", + "Qed.\n", + "\n", + "Lemma tm_to_nat_dom_includes_nvalue_sol : forall v,\n", + " nvalue v -> exists n, tm_to_nat v = some_nat n.\n", + "Proof.\n", + " intros v Hnv. induction Hnv.\n", + " exists O. reflexivity.\n", + " destruct IHHnv as [ n Heq ]. exists (S n).\n", + " simpl. rewrite -> Heq. reflexivity.\n", + "Qed.\n", + "\n", + "Lemma tm_to_nat_dom_only_nvalue_sol : forall v n,\n", + " tm_to_nat v = some_nat n -> nvalue v.\n", + "Proof.\n", + " intros v. induction v; intros n Heq.\n", + " inversion Heq.\n", + " inversion Heq.\n", + " inversion Heq.\n", + " apply n_zero.\n", + " apply n_succ.\n", + " simpl in Heq. destruct (tm_to_nat v).\n", + " inversion Heq. eapply IHv. reflexivity.\n", + " inversion Heq.\n", + " inversion Heq.\n", + " inversion Heq.\n", + "Qed.\n", + "\n", + "Lemma interp_reduces_sol : forall t,\n", + " eval_many t (interp t).\n", + "Proof.\n", + " intros t. induction t.\n", + " apply m_refl.\n", + " apply m_refl.\n", + " simpl. destruct (interp t1).\n", + " eapply m_trans.\n", + " apply m_if. apply IHt1.\n", + " eapply m_trans.\n", + " eapply m_one. apply e_iftrue.\n", + " apply IHt2.\n", + " eapply m_trans.\n", + " apply m_if. apply IHt1.\n", + " eapply m_trans.\n", + " eapply m_one. apply e_iffalse.\n", + " apply IHt3.\n", + " apply m_if. apply IHt1.\n", + " apply m_if. apply IHt1.\n", + " apply m_if. apply IHt1.\n", + " apply m_if. apply IHt1.\n", + " apply m_if. apply IHt1.\n", + " apply m_refl.\n", + " simpl. apply m_succ. apply IHt.\n", + " simpl. destruct (interp t).\n", + " apply m_pred. apply IHt.\n", + " apply m_pred. apply IHt.\n", + " apply m_pred. apply IHt.\n", + " eapply m_trans.\n", + " apply m_pred. apply IHt.\n", + " apply m_one. apply e_predzero.\n", + " remember (tm_to_nat t0) as x. destruct x.\n", + " eapply m_trans.\n", + " apply m_pred. apply IHt.\n", + " apply m_one. apply e_predsucc.\n", + " eapply tm_to_nat_dom_only_nvalue.\n", + " rewrite <- Heqx. reflexivity.\n", + " apply m_pred. apply IHt.\n", + " apply m_pred. apply IHt.\n", + " apply m_pred. apply IHt.\n", + " simpl. destruct (interp t).\n", + " apply m_iszero. apply IHt.\n", + " apply m_iszero. apply IHt.\n", + " apply m_iszero. apply IHt.\n", + " eapply m_trans.\n", + " apply m_iszero. apply IHt.\n", + " apply m_one. apply e_iszerozero.\n", + " remember (tm_to_nat t0) as x. destruct x.\n", + " eapply m_trans.\n", + " apply m_iszero. apply IHt.\n", + " apply m_one. apply e_iszerosucc.\n", + " eapply tm_to_nat_dom_only_nvalue.\n", + " rewrite <- Heqx. reflexivity.\n", + " apply m_iszero. apply IHt.\n", + " apply m_iszero. apply IHt.\n", + " apply m_iszero. apply IHt.\n", + "Qed.\n", + "\n", + "Lemma interp_fully_reduces_sol : forall t,\n", + " normal_form (interp t).\n", + "Proof.\n", + " induction t; intros [t' H].\n", + " inversion H.\n", + " inversion H.\n", + " simpl in H. destruct (interp t1).\n", + " destruct IHt2. eauto.\n", + " destruct IHt3. eauto.\n", + " destruct IHt1. inversion H. eauto.\n", + " destruct IHt1. inversion H. eauto.\n", + " destruct IHt1. inversion H. eauto.\n", + " destruct IHt1. inversion H. eauto.\n", + " destruct IHt1. inversion H. eauto.\n", + " inversion H.\n", + " destruct IHt. inversion H. eauto.\n", + " simpl in H. destruct (interp t).\n", + " inversion H. inversion H1.\n", + " inversion H. inversion H1.\n", + " inversion H. destruct IHt. eauto.\n", + " inversion H.\n", + " remember (tm_to_nat t0) as x. destruct x.\n", + " destruct IHt. exists (tm_succ t').\n", + " apply e_succ. apply H.\n", + " inversion H; subst.\n", + " destruct (tm_to_nat_dom_includes_nvalue t')\n", + " as [n Heq].\n", + " apply H1.\n", + " rewrite <- Heqx in Heq. inversion Heq.\n", + " destruct IHt. eauto.\n", + " inversion H. destruct IHt. eauto.\n", + " inversion H. destruct IHt. eauto.\n", + " simpl in H. destruct (interp t).\n", + " inversion H. inversion H1.\n", + " inversion H. inversion H1.\n", + " inversion H. destruct IHt. eauto.\n", + " inversion H.\n", + " remember (tm_to_nat t0) as x. destruct x.\n", + " inversion H.\n", + " inversion H; subst.\n", + " destruct (tm_to_nat_dom_includes_nvalue t0)\n", + " as [n Heq].\n", + " apply H1.\n", + " rewrite <- Heqx in Heq. inversion Heq.\n", + " inversion H. destruct IHt. eauto.\n", + " inversion H. destruct IHt. eauto.\n", + " inversion H. destruct IHt. eauto.\n", + "Qed." + ] + } + ], + "nbformat": 4, + "nbformat_minor": 2, + "metadata": { + "language_info": { + "name": "coq", + "file_extension": ".v", + "mimetype": "text/x-coq", + "version": "8.9.1" + }, + "kernelspec": { + "name": "coq", + "display_name": "Coq", + "language": "coq" + } + } +} diff --git a/advanced.md b/advanced.md new file mode 100644 index 0000000..16a57d6 --- /dev/null +++ b/advanced.md @@ -0,0 +1,2723 @@ +--- +title: My notebook +jupyter: + nbformat: 4 + nbformat_minor: 2 + kernelspec: + display_name: "Coq" + language: "coq" + name: "coq" + language_info: + file_extension: ".v" + mimetype: "text/x-coq" + name: "coq" + version: "8.9.1" +--- + +Adapted from a workshop given at [POPL 2008](https://www.cis.upenn.edu/~plclub/popl08-tutorial/). + +# The NB language, back again + +In this notebook, we will be working with a language very similar to the NB +language from the first assignment. + +## Definitions +### Grammar and terms + +The grammar of our language would be defined as follows: + +``` +t ::= "true" terms + | "false" + | "if" t "then" t "else" t + | 0 + | "succ" t + | "pred" t + | "iszero" t +``` + +To represent the terms of this language in Coq, we will define `tm`, an +`Inductive` data type: + +``` code +Inductive tm : Set := +| tm_true : tm +| tm_false : tm +| tm_if : tm -> tm -> tm -> tm +| tm_zero : tm +| tm_succ : tm -> tm +| tm_pred : tm -> tm +| tm_iszero : tm -> tm. +``` + +Compare the two definitions. For every rule in the grammar, there is a +corresponding _constructor_. Each constructor is a value in Coq that allows us +to obtain values of type `tm`. In contrast to the previous notebook, here we +annotate every constructor with a type. `tm_true` is a constructor corresponding +to the terminal rule `"true"` - it takes no arguments and is therefore annotated +with the simple type `tm`. `tm_succ` is a constructor corresponding to the +`"succ" t` rule - since the rule has a single subterm, the constructor is a +function from `tm` to `tm`. + +Using the above definition, we can create values corresponding to the terms in our language: + +```code +Check (tm_if (tm_iszero tm_zero) tm_false tm_true). +``` + +### Definition of value + +Next, we want to define what it means to be a _value_ in our language. While in +the original NB language we did so through grammar rules, it's equally valid to +define a judgment which tells us which terms are boolean and numeric values +(correspondingly, `bvalue` and `nvalue`): + +``` + --------------- (b_true) + ⊢ bvalue (true) + + ---------------- (b_false) + ⊢ bvalue (false) + + + ---------- (n_zero) + ⊢ nvalue 0 + + ⊢ nvalue t + ----------------- (n_succ) + ⊢ nvalue (succ t) +``` + +Recall that from Curry-Howard correspondence we know that types correspond to +propositions and values correspond to proofs. Therefore, we can represent the +above judgements in Coq by defining a type corresponding to each judgement. +Then, begin able to create a value of type `nvalue` is the same as being able to +construct a proof that a given term is an `nvalue`. + +The definitions are as follows: + +```code +Inductive bvalue : tm -> Prop := +| b_true : bvalue tm_true +| b_false : bvalue tm_false. + +Inductive nvalue : tm -> Prop := +| n_zero : nvalue tm_zero +| n_succ : forall t, + nvalue t -> + nvalue (tm_succ t). +``` + +Those definitions should look similar to the inference rules above, although +they may also look slightly confusing. Before trying to understand their every +part, it may help to see how they are meant to be used. + +The _type_ `nvalue t` represents the _proposition_ that `t` is a numeric value. +For instance, `nvalue (tm_succ tm_zero)` represents the proposition that the +successor of zero (or simply one) is a numeric value. To show that this +proposition is true, we need to construct a value of said type. We can do that +as follows: + +```code +Check (n_succ tm_zero n_zero). +``` + +You should now go back to the definitions and try to understand how they +represent their corresponding inference rules. + +One thing that may still be puzzling are the `Set` and `tm -> Prop` annotation. +If you are suspecting that the second one mentions `tm ->` because the +corresponding type is a _type-level function_ from `tm` to `Prop`, you'd be correct: + +```code +Check nvalue. +Check nvalue tm_zero. +``` + +The difference between `Set` and `Prop` is much more subtle and fundamental. To +put it briefly, types annotated as `Set` are meant to be used as data types, +while those annotated as `Prop` are meant to be used as propositions. Fully +explaining this distinction is beyond the scope of this course, but the above +intuition should serve you well enough. + +As the last thing in this section, we will (finally) define what it means to be +a value. If you recall that `T \/ S` is the data type corresponding to the +proof that either `T` or `S`, the definition is simple enough: + +```code +Definition value (t : tm) : Prop := + bvalue t \/ nvalue t. +``` + +### Operational semantics + +Having defined `tm`s and `value`s, we can define call-by-value operational +semantics for our language. We will define an inductive data type `eval (t : tm) +(t' : tm) : Prop` corresponding to the proposition that `t` evaluates to `t'` in +a single step. The definition is as follows: + +```code +Inductive eval : tm -> tm -> Prop := +| e_iftrue : forall t2 t3, + eval (tm_if tm_true t2 t3) t2 +| e_iffalse : forall t2 t3, + eval (tm_if tm_false t2 t3) t3 +| e_if : forall t1 t1' t2 t3, + eval t1 t1' -> + eval (tm_if t1 t2 t3) (tm_if t1' t2 t3) +| e_succ : forall t t', + eval t t' -> + eval (tm_succ t) (tm_succ t') +| e_predzero : + eval (tm_pred tm_zero) tm_zero +| e_predsucc : forall t, + nvalue t -> + eval (tm_pred (tm_succ t)) t +| e_pred : forall t t', + eval t t' -> + eval (tm_pred t) (tm_pred t') +| e_iszerozero : + eval (tm_iszero tm_zero) tm_true +| e_iszerosucc : forall t, + nvalue t -> + eval (tm_iszero (tm_succ t)) tm_false +| e_iszero : forall t t', + eval t t' -> + eval (tm_iszero t) (tm_iszero t'). +``` + +If you don't feel comfortable with Coq syntax yet, compare the above with the +definition of beta-reduction from our first assignment. + +Next, we define the multi-step evaluation relation `eval_many`: + +```code +Inductive eval_many : tm -> tm -> Prop := +| m_refl : forall t, + eval_many t t +| m_step : forall t t' u, + eval t t' -> + eval_many t' u -> + eval_many t u. +``` + +We say that a term is a `normal_form` if there is no term to which it can step. +We can define this in Coq as follows: + +```code +Definition normal_form (t : tm) : Prop := + ~ exists t', eval t t'. +``` + +### Exercises + +**Exercise** Multi-step evaluation is often defined as the "reflexive, +transitive closure" of single-step evaluation. Write an inductively defined +relation `eval_rtc` that corresponds to that verbal description. + +In case you get stuck or need a hint, you can find solutions to all the +exercises near the bottom of the file. + +**Exercise** Sometimes it is more convenient to use a big-step semantics for a +language. Add the remaining constructors to finish the inductive definition +`full_eval` for the big-step semantics that corresponds to the small-step +semantics defined by `eval`. Build the inference rules so that `full_eval t v` +logically implies both `eval_many t v` and `value v`. In order to do this, you +may need to add the premise `nvalue v` to the appropriate cases. + +Hint: You should end up with a total of 8 cases. + +``` +Inductive full_eval : tm -> tm -> Prop := +| f_value : forall v, + value v -> + full_eval v v +| f_iftrue : forall t1 t2 t3 v, + full_eval t1 tm_true -> + full_eval t2 v -> + full_eval (tm_if t1 t2 t3) v +| f_succ : forall t v, + nvalue v -> + full_eval t v -> + full_eval (tm_succ t) (tm_succ v). +``` + +## Proofs + +So far, we've only seen proofs represented in Coq as manually-constructed +values. For any non-trivial proof value, it's rather inconvenient to manually +construct it. + +Proof values are most easily built interactively, using tactics to manipulate a +proof state. A proof state consists of a set of goals (propositions or types for +which you must produce an inhabitant), each with a context of hypotheses +(inhabitants of propositions or types you are allowed to use). A proof state +begins initially with one goal (the statement of the lemma you are tying to +prove) and no hypotheses. A goal can be solved, and thereby eliminated, when it +exactly matches one of hypotheses in the context. A proof is completed when all +goals are solved. + +Tactics can be used for forward reasoning (which, roughly speaking, means +modifying the hypotheses of a context while leaving the goal unchanged) or +backward reasoning (replacing the current goal with one or more new goals in +simpler contexts). Given the level of detail required in a formal proof, it +would be ridiculously impractical to complete a proof using forward reasoning +alone. However it is usually both possible and practical to complete a proof +using backward reasoning alone. Therefore, we focus almost exclusively on +backward reasoning in this tutorial. Of course, most people naturally a +significant amount of forward reasoning in their thinking process, so it may +take you a while to become accustomed to getting by without it. + +We use the keyword `Lemma` to state a new proposition we wish to prove. +(`Theorem` and `Fact` are exact synonyms for `Lemma`.) The keyword `Proof`, +immediately following the statement of the proposition, indicates the beginning +of a proof script. A proof script is a sequence of tactic expressions, each +concluding with a `.`. Once all of the goals are solved, we use the keyword +`Qed` to record the completed proof. If the proof is incomplete, we may tell Coq +to accept the lemma on faith by using `Admitted` instead of `Qed`. + +We now proceed to introduce the specific proof tactics. + +### Implication and universal quantification + +``` + - [intros] + - [apply] + - [apply with (x := ...)] +``` + +Recall that both implication and universal quantification correspond to function +types and values. Accordingly, we can use the `intros` tactic to move +universally quantified variables and implication antecedents from the goal into +the context as hypotheses. + +If our current goal corresponds to a conclusion of some implication `P`, we can +use the `apply P` tactic to prove our goal by proving the antecedents of `P`. If +you'd suspect from the name of the tactic that this corresponds to applying a +function, you'd be correct. Using `apply` allows building a proof value from the +bottom up. + +#### Example 1 + +In the following example, our proof script will build a value corresponding to +the following proof tree: + +``` + nvalue t + ---------------------------- (e_predsucc) + eval (tm_pred (tm_succ t)) t + ------------------------------------------------ (e_succ) + eval (tm_succ (tm_pred (tm_succ t))) (tm_succ t) +``` + +Step through every cell below to see how this tree is constructed. + +```code +Lemma e_succ_pred_succ : forall t, + nvalue t -> + eval (tm_succ (tm_pred (tm_succ t))) (tm_succ t). +Proof. +``` + +```code + (** Let [t] be a [tm]. *) + intros t. +``` + +```code + (** Assume that [t] is an [nvalue] (and let's call that + assumption [Hn] for future reference). *) + intros Hn. +``` + +```code + (** By [e_succ], in order to prove our conclusion, it suffices + to prove that [eval (tm_pred (tm_succ t)) t]. *) + Check e_succ. + apply e_succ. +``` + +```code + (** That, in turn, can be shown by [e_predsucc], if we are + able to show that [nvalue t]. *) + Check e_predsucc. + apply e_predsucc. +``` + +```code + (** But, in fact, we assumed [nvalue t]. *) + apply Hn. +``` + +``` code +Qed. +``` + +You can see below that there is no magic happening at this point: +`e_succ_pred_succ` is a value that can be used like any other value we have seen +so far. We can ask Coq for its type: + +```code +Check e_succ_pred_succ. +``` + +And we can see the value we have constructed with tactics: + +```code +Print e_succ_pred_succ. +``` + +Compare the value to the proof script above. Observe how function application in +the value corresponds to usages of `apply` tactic. + +#### Example 2 + +Now consider, for a moment, the rule `m_step`: + +``` + eval t t' eval_many t' u + ------------------------- (m_step) + eval_many t u +``` + +If we have a goal such as `eval_many e1 e2`, we should be able to use `apply +m_step` in order to replace it with the goals `eval e1 t'` and `eval_many t' +e2`. But what exactly is `t'` here? When and how is it chosen? It stands to +reason the conclusion is justified if we can come up with any `t'` for which the +premises can be justified. + +Now we note that, in the Coq syntax for the type of `m_step`, all three +variables `t`, `t'`, and `u` are universally quantified. The tactic `apply +m_step` will use pattern matching between our goal and the conclusion of +`m_step` to find the only possible instantiation of `t` and `u`. However, `apply +m_step` will raise an error since it does not know how it should instantiate +`t'`. In this case, the `apply` tactic takes a `with` clause that allows us to +provide this instantiation. This is demonstrated in the proof below. + +Observe how this works in the proof script below. The proof tree here gives a +visual representation of the proof term we are going to construct and the proof +script has again been annotated with the steps in English. + +``` + Letting s = tm_succ + p = tm_pred + lem = e_succ_pred_succ, + + nvalue t + - - - - - - - - - - - - (lem) --------------------- (m_refl) + eval (s (p (s t))) (s t) eval_many (s t) (s t) + ------------------------------------------------------ (m_step) + eval_many (s (p (s t))) (s t) +``` + +``` code +Lemma m_succ_pred_succ : forall t, + nvalue t -> + eval_many (tm_succ (tm_pred (tm_succ t))) (tm_succ t). +Proof. +``` + +```code + (** Let [t] be a [tm], and assume [nvalue t]. *) + intros t Hn. +``` + +```code + (** By [m_step], to show our conclusion, it suffices to find + some [t'] for which + [eval (tm_succ (tm_pred (tm_succ t))) t'] + and + [eval t' (tm_succ t)]. + Let us choose [t'] to be [tm_succ t]. *) + Check m_step. + apply m_step with (t' := tm_succ t). +``` + +```code + (** By the lemma [e_succ_pred_succ], to show + [eval (tm_succ (tm_pred (tm_succ t))) (tm_succ t)], + it suffices to show [nvalue t]. *) + Check e_succ_pred_succ. + apply e_succ_pred_succ. +``` + +```code + (** And, in fact, we assumed [nvalue t]. *) + apply Hn. +``` + +```code + (** Moreover, by the rule [m_refl], we also may conclude + [eval (tm_succ t) (tm_succ t)]. *) + Check m_refl. + apply m_refl. +``` + +```code +Qed. +``` + +#### Example 3 + +Any tactic like `apply` that takes the name of a constructor or lemma as an +argument can just as easily be given a more complicated expression as an +argument. Thus, we may use function application to construct proof objects on +the fly in these cases. Observe how this technique can be used to rewrite the +proof of the previous lemma. + +Although, we have eliminated one use of `apply`, this is not necessarily an +improvement over the previous proof. However, there are cases where this +technique is quite valuable. + +``` code +Lemma m_succ_pred_succ_alt : forall t, + nvalue t -> + eval_many (tm_succ (tm_pred (tm_succ t))) (tm_succ t). +Proof. + intros t Hn. +``` + +```code + Check m_step. + apply (m_step + (tm_succ (tm_pred (tm_succ t))) + (tm_succ t) + (tm_succ t) + ). +``` + +```code + Check e_succ_pred_succ. + apply (e_succ_pred_succ t Hn). +``` + +```code + apply t. +``` + +```code + Check m_refl. + apply (m_refl (tm_succ t)). +``` + +```code +Qed. +``` + +#### Lab 1 + +Write proof scripts for the following lemmas, following the plain language descriptions. + +These lemmas will be useful in later proofs. + +``` code +Lemma m_one : forall t1 t2, + eval t1 t2 -> + eval_many t1 t2. +``` + +```code + (** Let [t1] and [t2] be terms, and assume [eval t1 t2]. We + may conclude [eval_many t1 t2] by [m_step] if we can find + a term [t'] such that [eval t1 t'] and [eval_many t' t2]. + We will choose [t'] to be [t2]. Now we can show + [eval t1 t2] by our assumption, and we can show + [eval_many t2 t2] by [m_refl]. *) +Proof. +``` + +```code + (* to finish *) +Admitted. +``` + +``` code +Lemma m_two : forall t1 t2 t3, + eval t1 t2 -> + eval t2 t3 -> + eval_many t1 t3. +``` + +```code + (** Let [t1], [t2], and [t3] be terms. Assume [eval t1 t2] + and [eval t2 t3]. By [m_step], we may conclude that + [eval_many t1 t3] if we can find a term [t'] such that + [eval t1 t'] and [eval_many t' t3]. Let's choose [t'] to + be [t2]. We know [eval t1 t2] holds by assumption. In + the other case, by the lemma [m_one], to show [eval_many + t2 t3], it suffices to show [eval t2 t3], which is one of + our assumptions. *) +Proof. +``` + +```code + (* to finish *) +Admitted. +``` + +```code +Lemma m_iftrue_step : forall t t1 t2 u, + eval t tm_true -> + eval_many t1 u -> + eval_many (tm_if t t1 t2) u. +``` + +```code + (** Let [t], [t1], [t2], and [u] be terms. Assume that + [eval t tm_true] and [eval_many t1 u]. To show + [eval_many (tm_if t t1 t2) u], by [m_step], it suffices to + find a [t'] for which [eval (tm_if t t1 t2) t'] and + [eval_many t' u]. Let us choose [t'] to be + [tm_if tm_true t1 t2]. Now we can use [e_if] to show that + [eval (tm_if t t1 t2) (tm_if tm_true t1 t2)] if we can + show [eval t tm_true], which is actually one of our + assumptions. Moreover, using [m_step] once more, we can + show [eval_many (tm_if tm_true t1 t2) u] where [t'] is + chosen to be [t1]. Doing so leaves us to show + [eval (tm_if tm_true t1 t2) t1] and [eval_many t1 u]. The + former holds by [e_iftrue] and the latter holds by + assumption. *) +Proof. +``` + +```code + (* to finish *) +Admitted. +``` + +### Working with Definitions + +``` + - [unfold] +``` + + +There is a notion of equivalence on Coq terms that arises from the conversion +rules of the underlying calculus of constructions. It is sometimes useful to be +able to replace one term in a proof with an equivalent one. For instance, we may +want to replace a defined name with its definition. This sort of replacement can +be done the tactic `unfold`. This tactic can be used to manipulate the goal or +the hypotheses. + +``` code +Definition strongly_diverges t := + forall u, eval_many t u -> ~ normal_form u. +``` + +``` code +Lemma unfold_example : forall t t', + strongly_diverges t -> + eval t t' -> + strongly_diverges t'. +Proof. + intros t t' Hd He. + unfold strongly_diverges. intros u Hm. + unfold strongly_diverges in Hd. + apply Hd. apply m_step with (t' := t'). + apply He. + apply Hm. +Qed. +``` + + +**Exercise** In reality, many tactics will perform conversion automatically as necessary. Try +removing the uses of `unfold` from the above proof to check which ones were +necessary. + + +### Working with Conjunction and Disjunction + +``` + - [split] + - [left] + - [right] + - [destruct] (for conjunction and disjunction) +``` + +**Example** If `H` is the name of a conjunctive hypothesis, then `destruct H as p` will +replace the hypothesis `H` with its components using the names in the pattern +`p`. Observe the pattern in the example below. + +``` code +Lemma m_two_conj : forall t t' t'', + eval t t' /\ eval t' t'' -> + eval_many t t''. +Proof. + intros t t' t'' H. + destruct H as [ He1 He2 ]. + apply m_two with (t2 := t'). + apply He1. + apply He2. +Qed. +``` + +**Example** Patterns may be nested to break apart nested structures. Note that +infix conjunction is right-associative, which is significant when trying to +write nested patterns. We will later see how to use `destruct` on many different +sorts of hypotheses. + +``` code +Lemma m_three_conj : forall t t' t'' t''', + eval t t' /\ eval t' t'' /\ eval t'' t''' -> + eval_many t t'''. +Proof. + intros t t' t'' t''' H. + destruct H as [ He1 [ He2 He3 ] ]. + apply m_step with (t' := t'). + apply He1. + apply m_two with (t2 := t''). + apply He2. + apply He3. +Qed. +``` + +**Example** If your goal is a conjunction, use `split` to break it apart into +two separate subgoals. + +``` code +Lemma m_three : forall t t' t'' t''', + eval t t' -> + eval t' t'' -> + eval t'' t''' -> + eval_many t t'''. +Proof. + intros t t' t'' t''' He1 He2 He3. + apply m_three_conj with (t' := t') (t'' := t''). + split. + apply He1. + split. + apply He2. + apply He3. +Qed. +``` + +**Exercise** Hint: You might find lemma `m_three` useful here. + +``` code +Lemma m_if_iszero_conj : forall v t2 t2' t3 t3', + nvalue v /\ eval t2 t2' /\ eval t3 t3' -> + eval_many (tm_if (tm_iszero tm_zero) t2 t3) t2' /\ + eval_many (tm_if (tm_iszero (tm_succ v)) t2 t3) t3'. +Proof. +``` + +```code + (* to finish *) +Admitted. +``` + +**Example** If the goal is a disjunction, we can use the `left` or `right` +tactics to solve it by proving the left or right side of the conclusion. + +``` code +Lemma true_and_succ_zero_values : + value tm_true /\ value (tm_succ tm_zero). +Proof. + unfold value. split. + left. apply b_true. + right. apply n_succ. apply n_zero. +Qed. +``` + +**Example** If we have a disjunction in the context, we can use `destruct` to +reason by cases on the hypothesis. Note the syntax of the associated pattern. + +``` code +Lemma e_if_true_or_false : forall t1 t2, + eval t1 tm_true \/ eval t1 tm_false -> + eval_many (tm_if t1 t2 t2) t2. +Proof. + intros t1 t2 H. destruct H as [ He1 | He2 ]. + apply m_two with (t2 := tm_if tm_true t2 t2). + apply e_if. apply He1. + apply e_iftrue. + apply m_two with (t2 := tm_if tm_false t2 t2). + apply e_if. apply He2. + apply e_iffalse. +Qed. +``` + +#### Lab 2 + +Work on the following exercise. + +**Exercise** + +``` code +Lemma two_values : forall t u, + value t /\ value u -> + bvalue t \/ + bvalue u \/ + (nvalue t /\ nvalue u). +``` + +``` code + (** We know [value t] and [value u], which means either + [bvalue t] or [nvalue t], and either [bvalue u] or + [nvalue u]. Consider the case in which + [bvalue t] holds. Then one of the disjuncts of our + conclusion is proved. Next, consider the case in which + [nvalue t] holds. Now consider the subcase where + [bvalue u] holds. ... *) +Proof. +``` + +``` code + (* to finish *) +Admitted. +``` + +**Example** `destruct` can be used on propositions with implications. This will +have the effect of performing `destruct` on the conclusion of the implication, +while leaving the hypotheses of the implication as additional subgoals. + +``` code +Lemma destruct_example : forall bv t t' t'', + bvalue bv -> + (value bv -> eval t t' /\ eval t' t'') -> + eval_many t t''. +Proof. + intros bv t t' t'' Hbv H. destruct H as [ H1 H2 ]. + Show 2. + unfold value. left. apply Hbv. + apply m_two with (t2 := t'). + apply H1. + apply H2. +Qed. +``` + +**Tip** After applying a tactic that introduces multiple subgoals, it is +sometimes useful to see not only the subgoals themselves but also their +hypotheses. Adding the command `Show n.` to your proof script to cause Coq to +display the nth subgoal in full. + + +## Reasoning by Cases and Induction + +``` code + - [destruct] (for inductively defined propositions) + - [induction] +``` + +**Example** Use `destruct` to reason by cases on an inductively defined datatype +or proposition. + +Note: It is possible to supply `destruct` with a pattern in these instances +also. However, the patterns become increasingly complex for bigger inductive +definitions; so it is often more practical to omit the pattern (thereby letting +Coq choose the names of the terms and hypotheses in each case), in spite of the +fact that this adds an element of fragility to the proof script (since the proof +script will mention names that were system-generated). + +``` code +Lemma e_iszero_nvalue : forall v, + nvalue v -> + eval (tm_iszero v) tm_true \/ + eval (tm_iszero v) tm_false. +Proof. + intros v Hn. +``` + +```code + destruct Hn. +``` + +```code + (* Case [n_zero]. + Note how [v] becomes [tm_zero] in the goal. *) + left. +``` + +```code + apply e_iszerozero. +``` + +```code + (* Case [n_succ]. + Note how [v] becomes [tm_succ v] in the goal. *) + right. +``` + +``` code + apply e_iszerosucc. apply Hn. +Qed. +``` + +**Example** You can use `induction` to reason by induction on an inductively +defined datatype or proposition. This is the same as `destruct`, except that it +also introduces an induction hypothesis in the inductive cases. + +``` code +Lemma m_iszero : forall t u, + eval_many t u -> + eval_many (tm_iszero t) (tm_iszero u). +Proof. + intros t u Hm. induction Hm. + apply m_refl. + apply m_step with (t' := tm_iszero t'). + apply e_iszero. apply H. + apply IHHm. +Qed. +``` + +#### Lab 3 +Work on the following exercise. + +**Exercise** + +``` code +Lemma m_trans : forall t t' u, + eval_many t t' -> + eval_many t' u -> + eval_many t u. +``` + +```code + (** We proceed by induction on the derivation of + [eval_many t t']. + Case [m_refl]: Since [t] and [t'] must be the same, our + conclusion holds by assumption. + Case [m_step]: Now let's rename the [t'] from the lemma + statement to [u0] (as Coq likely will) and observe that + there must be some [t'] (from above the line of the + [m_step] rule) such that [eval t t'] and + [eval_many t' u0]. Our conclusion follows from from + an application of [m_step] with our new [t'] and our + induction hypothesis, which allows us to piece together + [eval_many t' u0] and [eval_many u0 u] to get + [eval_many t' u]. *) +Proof. +``` + +```code + (* to finish *) +Admitted. +``` + +**Example** It is possible to use `destruct` not just on hypotheses but on any +lemma we have proved. If we have a lemma + + +``` + lemma1 : P /\ Q +``` + +then we can use the tactic + +``` + destruct lemma1 as [ H1 H2 ]. +``` + +to continue our proof with `H1 : P` and `H2 : Q` in our context. This works even +if the lemma has antecedents (they become new subgoals); however it fail if the +lemma has a universal quantifier, such as this: + +``` + lemma2 : forall x, P(x) /\ Q(x) +``` + +However, remember that we can build a proof of `P(e) /\ Q(e)` (which can be +destructed) using the Coq expression `lemma2 e`. So we need to phrase our tactic +as + +``` + destruct (lemma2 e) as [ H1 H2 ]. +``` + +An example of this technique is below. + +``` code +Lemma m_iszero_nvalue : forall t v, + nvalue v -> + eval_many t v -> + eval_many (tm_iszero t) tm_true \/ + eval_many (tm_iszero t) tm_false. +Proof. + intros t v Hnv Hm. + destruct (e_iszero_nvalue v) as [ H1 | H2 ]. + apply Hnv. + left. apply m_trans with (t' := tm_iszero v). + apply m_iszero. apply Hm. + apply m_one. apply H1. + right. apply m_trans with (t' := tm_iszero v). + apply m_iszero. apply Hm. + apply m_one. apply H2. +Qed. +``` + +**Exercise** Prove the following lemma. + +Hint: You may be interested in some previously proved lemmas, such as `m_one` +and `m_trans`. + +Note: Even though this lemma is in a comment, its solution is also at the +bottom. (Coq will give an error if we leave it uncommented since it mentions the +`eval_rtc` relation, which was the solution to another exercise.) + +``` +Lemma eval_rtc_many : forall t u, + eval_rtc t u -> + eval_many t u. +``` + +**Exercise** Prove the following lemma. + +``` +Lemma eval_many_rtc : forall t u, + eval_many t u -> + eval_rtc t u. +``` + + +**Exercise** Prove the following lemma. + +``` +Lemma full_eval_to_value : forall t v, + full_eval t v -> + value v. +``` + +## Working with Existential Quantification + +``` code + - [exists] + - [destruct] (for existential propositions) +``` + +**Example** Use `exists` to give the witness for an existential quantifier in +your goal. + +``` code +Lemma if_bvalue : forall t1 t2 t3, + bvalue t1 -> + exists u, eval (tm_if t1 t2 t3) u. +Proof. + intros t1 t2 t3 Hb. destruct Hb. + exists t2. apply e_iftrue. + exists t3. apply e_iffalse. +Qed. +``` + +**Example** You may use `destruct` to break open an existential hypothesis. + +``` code +Lemma m_two_exists : forall t u, + (exists w, eval t w /\ eval w u) -> + eval_many t u. +Proof. + intros t u H. + destruct H as [ w He ]. + destruct He as [ He1 He2 ]. + apply m_two with (t2 := w). + apply He1. + apply He2. +Qed. +``` + +**Example** Tip: We can combine patterns that destruct existentials with +patterns that destruct other logical connectives. + +Here is the same proof with just one use of `destruct`. + +``` code +Lemma m_two_exists' : forall t u, + (exists w, eval t w /\ eval w u) -> + eval_many t u. +Proof. + intros t u H. destruct H as [ w [ He1 He2 ] ]. + apply m_two with (t2 := w). + apply He1. + apply He2. +Qed. +``` + +**Example** Tip: We give patterns to the `intros` tactic to destruct hypotheses +as we introduce them. + +Here is the same proof again without any uses of `destruct`. + +``` code +Lemma m_two_exists'' : forall t u, + (exists w, eval t w /\ eval w u) -> + eval_many t u. +Proof. + intros t u [ w [ He1 He2 ] ]. + apply m_two with (t2 := w). + apply He1. + apply He2. +Qed. +``` + +**Exercise** + +``` code +Lemma value_can_expand : forall v, + value v -> + exists u, eval u v. +Proof. + (* to finish *) +Admitted. +``` + +#### Lab 4 + Work on the following exercise. + +**Exercise** Tip: You should find the lemma `m_iszero` useful. Use `Check +m_iszero.` if you've forgotten its statement. + +``` code +Lemma exists_iszero_nvalue : forall t, + (exists nv, nvalue nv /\ eval_many t nv) -> + exists bv, eval_many (tm_iszero t) bv. +Proof. + (** There exists some [nv] such that [nvalue nv]. Consider + the case where [nv] is [tm_zero]. Then choose [bv] to + be [tm_true]. By [m_trans], we can show that + [eval_many (tm_iszero t) tm_true] by showing + [eval_many (tm_iszero t) (tm_iszero tm_zero)] and + [eval_many (tm_iszero tm_zero) tm_true]. The former + follows from [m_iszero] and our assumption. The latter + follows from [m_one] and the rule [e_iszerozero]. On the + other hand, in the case where [nv] is built from + [tm_succ], we choose [bv] to be [tm_false] and the proof + follows similarly. *) + + (* to finish *) +Admitted. +``` + +## Working with Negation + +``` code + - [unfold not] + - [destruct] (for negation) +``` + +**Example** The standard library defines an uninhabited type `False` and defines +`not P` to stand for `P -> False`. Furthermore, Coq defines the notation `~ P` +to stand for `not P`. (Such notations only affect parsing and printing -- Coq +views `not P` and `~ P` as being syntactically equal.) + +The most basic way to work with negated statements is to unfold `not` and treat +`False` just as any other proposition. + +(Note how multiple definitions can be unfolded with one use of `unfold`. Also, +as noted earlier, many uses of `unfold` are not strictly necessary. You can try +deleting the uses from the proof below to check that the proof script still +works.) + +``` code +Lemma normal_form_succ : forall t, + normal_form (tm_succ t) -> + normal_form t. +Proof. + intros t Hnf. + unfold normal_form. unfold not. + unfold normal_form, not in Hnf. + intros [ t' H' ]. apply Hnf. + exists (tm_succ t'). apply e_succ. apply H'. +Qed. +``` + +**Exercise** + +``` code +Lemma normal_form_to_forall : forall t, + normal_form t -> + forall u, ~ eval t u. +Proof. + (* to finish *) +Admitted. +``` + +**Exercise** + +``` code +Lemma normal_form_from_forall : forall t, + (forall u, ~ eval t u) -> + normal_form t. +Proof. + (* to finish *) +Admitted. +``` + +**Example** If you happen to have `False` as a hypothesis, you may use +`destruct` on that hypothesis to solve your goal. + +``` code +Lemma False_hypothesis : forall v, + False -> + value v. +Proof. + intros v H. destruct H. +Qed. +``` + +**Example** Recalling that `destruct` can be used on propositions with +antecedents and that negation is simply an abbreviation for an implication, +using `destruct` on a negated hypothesis has the derived behavior of replacing +our goal with the proposition that was negated in our context. + +Tip: We actually don't even need to do the unfolding below because `destruct` +would have done it for us. + +``` code +Lemma destruct_negation_example : forall t v, + value v -> + eval t tm_zero -> + (value v -> normal_form t) -> + eval tm_true tm_false. +Proof. + intros t v Hnv He Hnf. + unfold normal_form, not in Hnf. + (* As usual, unfolding was optional here. *) + destruct Hnf. + apply Hnv. + exists tm_zero. apply He. +Qed. +``` + +**Exercise** This one may be a bit tricky. Start by using `destruct` on one of +your hypotheses. + +``` code +Lemma negation_exercise : forall v1 v2, + ~ (value v1 \/ value v2) -> + ~ (~ bvalue v1 /\ ~ bvalue v2) -> + eval tm_true tm_false. +Proof. + (* to finish *) +Admitted. +``` + + +## Working with Equality + +``` code + - [reflexivity] + - [subst] + - [rewrite] + - [inversion] (on equalities) +``` + +**Example** If you have an equality in your context, there are several ways to +substitute one side of the equality for the other in your goal or in other +hypotheses. + +If one side of the equality is a variable `x`, then the tactic `subst x` will +replace all occurrences of `x` in the context and goal with the other side of +the quality and will remove `x` from your context. + +Use `reflexivity` to solve a goal of the form `e = e`. + +``` code +Lemma equality_example_1 : forall t1 t2 t3 u1 u2, + t1 = tm_iszero u1 -> + t2 = tm_succ u2 -> + t3 = tm_succ t2 -> + tm_if t1 t2 t3 = + tm_if (tm_iszero u1) (tm_succ u2) (tm_succ (tm_succ u2)). +Proof. + intros t1 t2 t3 u1 u2 Heq1 Heq2 Heq3. + subst t1. subst t2. subst t3. reflexivity. +Qed. +``` + +**Example** If neither side of the equality in your context is a variable (or if +you don't want to discard the hypothesis), you can use the `rewrite` tactic to +perform a substitution. The arrow after `rewrite` indicates the direction of the +substitution. As demonstrated, you may perform rewriting in the goal or in a +hypothesis. + +``` code +Lemma equality_example_2a : forall t u v, + tm_succ t = tm_succ u -> + eval (tm_succ u) v -> + eval (tm_succ t) v. +Proof. + intros t u v Heq He. rewrite -> Heq. apply He. +Qed. +``` + +``` code +Lemma equality_example_2b : forall t u v, + tm_succ t = tm_succ u -> + eval (tm_succ u) v -> + eval (tm_succ t) v. +Proof. + intros t u v Heq He. rewrite <- Heq in He. apply He. +Qed. +``` + +**Example** We also note that, analogously with `destruct`, we may use `rewrite` +even with a hypothesis (or lemma) that has antecedents. + +``` code +Lemma equality_example_2c : forall t u v, + nvalue v -> + (nvalue v -> tm_succ t = tm_succ u) -> + eval (tm_succ u) v -> + eval (tm_succ t) v. +Proof. + intros t u v Hnv Heq He. rewrite <- Heq in He. + apply He. + apply Hnv. +Qed. +``` + +**Example** If you need to derive additional equalities implied by an equality +in your context (e.g., by the principle of constructor injectivity), you may use +`inversion`. `inversion` is a powerful tactic that uses unification to introduce +more equalities into your context. (You will observe that it also performs some +substitutions in your goal.) + +``` code +Lemma equality_example_3 : forall t u, + tm_succ t = tm_succ u -> + t = u. +Proof. + intros t u Heq. inversion Heq. reflexivity. +Qed. +``` + +**Exercise** + +``` code +Lemma equality_exercise : forall t1 t2 t3 u1 u2 u3 u4, + tm_if t1 t2 t3 = tm_if u1 u2 u2 -> + tm_if t1 t2 t3 = tm_if u3 u3 u4 -> + t1 = u4. +Proof. + (* to finish *) +Admitted. +``` + +**Example** `inversion` will also solve a goal when unification fails on a +hypothesis. (Internally, Coq can construct a proof of `False` from contradictory +equalities.) + +``` code +Lemma equality_example_4 : + tm_zero = tm_true -> + eval tm_true tm_false. +Proof. + intros Heq. inversion Heq. +Qed. +``` + +#### Lab 5 + +Work on `equality_exercise` above and `succ_not_circular` below. + +**Exercise** Note: `e1 <> e2` is a notation for `~ e1 = e2`, i.e., the two are +treated as syntactically equal. + +Note: This is fairly trivial to prove if we have a size function on terms and +some automation. With just the tools we have described so far, it requires just +a little bit of work. + +Hint: The proof requires induction on `t`. (This is the first example of +induction on datatypes, but it is even more straightforward than induction on +propositions.) In each case, unfold the negation, pull the equality into the +context, and use `inversion` to eliminate contradictory equalities. + +``` code +Lemma succ_not_circular : forall t, + t <> tm_succ t. +Proof. + (* to finish *) +Admitted. +``` + +## Reasoning by Inversion + +``` code + - [inversion] (on propositions) +``` + +**Example** The `inversion` tactic also allows you to reason by inversion on an +inductively defined proposition as in paper proofs: we try to match some +proposition with the conclusion of each inference rule and only consider the +cases (possibly none) where there is a successful unification. In those cases, +we may use the premises of the inference rule in our reasoning. + +Since `inversion` may generate many equalities between variables, it is useful +to know that using `subst` without an argument will perform all possible +substitutions for variables. It is a little difficult to predict which variables +will be eliminated and which will be kept by this tactic, but this is a typical +sort of trade-off when using powerful tactics. + +(The use of `subst` in this proof is superfluous, but you can observe that it +simplifies the context.) + +``` code +Lemma value_succ_nvalue : forall t, + value (tm_succ t) -> + nvalue t. +Proof. + intros t H. unfold value in H. destruct H as [ H1 | H2 ]. + (* No unification is possible -- [inversion] solves goal. *) + inversion H1. + (* Just the [n_succ] cases unifies with H2. *) + inversion H2. subst. apply H0. +Qed. +``` + +#### Lab 6 + +Work on the exercise below. + + +**Exercise** + +``` code +Lemma inversion_exercise : forall t, + normal_form t -> + eval_many (tm_pred t) tm_zero -> + nvalue t. +Proof. + (** By inversion on the [eval_many] relation, then conclusion + [eval_many (tm_pred t) tm_zero] must have been derived by + the rule [m_step], which means there is some [t'] for + which [eval (tm_pred t) t'] and [eval_many t' tm_zero]. + Now, by inversion on the [eval] relation, there are only + three ways that [eval (tm_pred t) t'] could have been + derived: + * By [e_predzero], with [t] and [t'] both being equal to + [tm_zero]. Our conclusion follows from [n_zero]. + * By [e_predsucc], with [t] being [tm_succ t0] where we + have [nvalue t0]. In this case, our conclusion is + provable with [n_succ]. + * By [e_pred], with [t] taking an evaluation step. This + contradicts our assumption that [t] is a normal form + (which can be shown by using [destruct] on that + assumption). *) + + (* to finish *) +Admitted. +``` + +**Exercise** Tip: Nested patterns will be useful here. + +``` code +Lemma contradictory_equalities_exercise : + (exists t, exists u, exists v, + value t /\ + t = tm_succ u /\ + u = tm_pred v) -> + eval tm_true tm_false. +Proof. + (* to finish *) +Admitted. +``` + +**Exercise** + +``` code +Lemma eval_fact_exercise : forall t1 t2, + eval (tm_iszero (tm_pred t1)) t2 -> + eval t2 tm_false -> + exists u, t1 = tm_succ u. +Proof. + (* to finish *) +Admitted. +``` + +**Exercise** + +``` code +Lemma normal_form_if : forall t1 t2 t3, + normal_form (tm_if t1 t2 t3) -> + t1 <> tm_true /\ t1 <> tm_false /\ normal_form t1. +Proof. + (* to finish *) +Admitted. +``` + +## Additional Important Tactics + +``` code + - [generalize dependent] + - [assert] + - [;] + - [clear] +``` + +**Example** Sometimes we need to have a tactic that moves hypotheses from our +context back into our goal. Often this is because we want to perform induction +in the middle of a proof and will not get a sufficiently general induction +hypothesis without a goal of the correct form. (To be specific, if we need to +have an induction hypothesis with a `forall` quantifier in front, then we must +make sure our goal has a `forall` quantifier in front at the time we invoke the +`induction` tactic.) Observe how `generalize dependent` achieves this in the +proof below, moving the variable `t` and all dependent hypotheses back into the +goal. You may want to remove the use of `generalize dependent` to convince +yourself that it is performing an essential role here. + +``` code +Lemma value_is_normal_form : forall v, + value v -> + normal_form v. +Proof. + intros v [ Hb | Hn ] [ t He ]. + destruct Hb. + inversion He. + inversion He. + generalize dependent t. induction Hn. + intros t He. inversion He. + intros u He. inversion He. subst. destruct (IHHn t'). + apply H0. +Qed. +``` + +**Exercise** Coq has many operations (called "tacticals") to combine smaller +tactics into larger ones. + +If `t1` and `t2` are tactics, then `t1; t2` is a tactic that executes `t1`, and +then executes `t2` on subgoals left by or newly generated by `t1`. This can help +to eliminate repetitious use of tactics. Two idiomatic uses are performing +`subst` after `inversion` and performing `intros` after `induction`. More +opportunities to use this tactical can usually be discovered after writing a +proof. (It is worth noting that some uses of this tactical can make proofs less +readable or more difficult to maintain. Alternatively, some uses can make proofs +more readable or easier to maintain. It is always good to think about your +priorities when writing a proof script.) + +Revise the proof for `value_is_normal_form` to include uses of the `;` tactical. + + +**Example** Sometimes it is helpful to be able to use forward reasoning in a +proof. One form of forward reasoning can be done with the tactic `assert`. +`assert` adds a new hypothesis to the context but asks us to first justify it. + +``` code +Lemma nvalue_is_normal_form : forall v, + nvalue v -> + normal_form v. +Proof. + intros v Hnv. + assert (value v) as Hv. right. apply Hnv. + apply value_is_normal_form. apply Hv. +Qed. +``` + +**Example** `assert` can also be supplied with a tactic that proves the +assertion. We rewrite the above proof using this form. + +``` code +Lemma nvalue_is_normal_form' : forall v, + nvalue v -> + normal_form v. +Proof. + intros v Hnv. + assert (value v) as Hv by (right; apply Hnv). + apply value_is_normal_form. apply Hv. +Qed. +``` + +**Example** The proof below introduces two new, simple tactics. First, the +tactic `replace e1 with e2` performs a substitution in the goal and then +requires that you prove `e2 = e1` as a new subgoal. This often allows us to +avoid more cumbersome forms of forward reasoning. Second, the `clear` tactic +discards a hypothesis from the context. Of course, this tactic is never needed, +but it can be nice to use when there are complicated, irrelevant hypotheses in +the context. + +``` code +Lemma single_step_to_multi_step_determinacy : + (forall t u1 u2, eval t u1 -> eval t u2 -> u1 = u2) -> + forall t v1 v2, + eval_many t v1 -> normal_form v1 -> + eval_many t v2 -> normal_form v2 -> + v1 = v2. +Proof. + intros H t v1 v2 Hm1 Hnf1 Hm2 Hnf2. induction Hm1. + clear H. destruct Hm2. + reflexivity. + destruct Hnf1. exists t'. apply H. + destruct Hm2. + destruct Hnf2. exists t'. apply H0. + apply IHHm1; clear IHHm1. + apply Hnf1. + replace t' with t'0. + apply Hm2. + apply H with (t := t). + apply H1. + apply H0. +Qed. +``` + +**Exercise** This proof is lengthy and thus somewhat challenging. All of the +techniques from this section will be useful; some will be essential. In +particular, you will need to use `generalize dependent` at the beginning of the +proof. You will find `assert` helpful in the cases where your assumptions are +contradictory but none of them are in a negative form. In that situation, you +can assert a negative statement that follows from your hypotheses (recall that +`normal_form` is a negative statement). Finally, you will want to use the above +lemma `nvalue_is_normal_form`. Good luck! + +``` code +Theorem eval_deterministic : forall t t' t'', + eval t t' -> + eval t t'' -> + t' = t''. +Proof. + (* to finish *) +Admitted. +``` + +**Exercise** Prove the following lemmas. The last is quite long, and you may +wish to wait until you know more about automation. + +``` +Lemma full_eval_from_value : forall v w, + value v -> + full_eval v w -> + v = w. + +Lemma eval_full_eval : forall t t' v, + eval t t' -> + full_eval t' v -> + full_eval t v. + +Lemma full_eval_complete : forall t v, + value v -> + eval_many t v -> + full_eval t v. +``` + +## Basic Automation + +``` code + - [eapply], [esplit] + - [auto], [eauto] +``` + +**Example** You can use `eapply e` instead of `apply e with (x := e1)`. This +will generate subgoals containing unification variables that will get unified +during subsequent uses of `apply`. + +``` code +Lemma m_if : forall t1 u1 t2 t3, + eval_many t1 u1 -> + eval_many (tm_if t1 t2 t3) (tm_if u1 t2 t3). +Proof. + intros t1 u1 t2 t3 Hm. induction Hm. + apply m_refl. + eapply m_step. + apply e_if. apply H. + apply IHHm. +Qed. +``` + +**Example** You can use `esplit` to turn an existentially quantified variable in +your goal into a unification variable. + +``` code +Lemma exists_pred_zero : + exists u, eval (tm_pred tm_zero) u. +Proof. + esplit. apply e_predzero. +Qed. +``` + +**Example** The `auto` tactic solves goals that are solvable by any combination +of + +- `intros` +- `apply` (used on some local hypothesis) +- `split`, `left`, `right` +- `reflexivity` + +If `auto` cannot solve the goal, it will leave the proof state completely +unchanged (without generating any errors). + +The lemma below is a proposition that has been contrived for the sake of +demonstrating the scope of the `auto` tactic and does not say anything of +practical interest. So instead of thinking about what it means, you should think +about the operations that `auto` had to perform to solve the goal. + +Note: It is important to remember that `auto` does not destruct hypotheses! +There are more advanced forms of automation available that do destruct +hypotheses in some specific ways. + +``` code +Lemma auto_example : forall t t' t'', + eval t t' -> + eval t' t'' -> + (forall u, eval t t' -> eval t' u -> eval_many t u) -> + eval t' t \/ t = t /\ eval_many t t''. +Proof. + auto. +Qed. +``` + +**Example** The `eauto` tactic solves goals that are solvable by some +combination of + +- `intros` +- `eapply` (used on some local hypothesis) +- `split`, `left`, `right` +- `esplit` +- `reflexivity` + +lemma has two significantly differences from the previous one, both of which +render `auto` useless. + +``` code +Lemma eauto_example : forall t t' t'', + eval t t' -> + eval t' t'' -> + (forall u, eval t u -> eval u t'' -> eval_many t t'') -> + eval t' t \/ (exists u, t = u) /\ eval_many t t''. +Proof. + eauto. +Qed. +``` + +**Example** You can enhance `auto` (or `eauto`) by appending `using x_1, ..., +x_n`, where each `x_i` is the name of some constructor or lemma. Then `auto` +will attempt to apply those constructors or lemmas in addition to the +assumptions in the local context. + +``` code +Lemma eauto_using_example : forall t t' t'', + eval t t' -> + eval t' t'' -> + eval t' t \/ t = t /\ eval_many t t''. +Proof. + eauto using m_step, m_one. +Qed. +``` + +#### Lab 7 + +**Exercise** Go back and rewrite your proofs for `m_one`, `m_two`, and +`m_iftrue_step`. You should be able to make them very succinct given what you +know now. + + +**Exercise** See how short you can make these proofs. + +Note: This is an exercise. We are not making the claim that shorter proofs are +necessarily better! + +Hint: Remember that we can connect tactics in sequence with `;`. However, as you +can imagine, figuring out the best thing to write after a `;` usually involves +some trial and error. + +``` code +Lemma pred_not_circular : forall t, + t <> tm_pred t. +Proof. + (* to finish *) +Admitted. +``` + +``` code +Lemma m_succ : forall t u, + eval_many t u -> + eval_many (tm_succ t) (tm_succ u). +Proof. + (* to finish *) +Admitted. +``` + +``` code +Lemma m_pred : forall t u, + eval_many t u -> + eval_many (tm_pred t) (tm_pred u). +Proof. + (* to finish *) +Admitted. +``` + +**Exercise** Go back and rewrite your proofs for `m_trans` and `two_values`. +Pulling together several tricks you've learned, you should be able to prove +`two_values` in one (short) line. Since this is a notebook, the easiest way for +you to do that may be to copy the cells here. + + +**Note** Sometimes there are lemmas or constructors that are so frequently +needed by `auto` that we don't want to have to add them to our `using` clause +each time. Coq allows us to request that certain propositions that always be +considered by `auto` and `eauto`. + +The following command adds four lemmas to the default search procedure of +`auto`. + +``` code +Hint Resolve m_if m_succ m_pred m_iszero. +``` + +Constructors of inductively defined propositions are some of the most frequently +needed by `auto`. Instead of writing + +``` + Hint Resolve b_true b_false. +``` + +we may simply write + +``` + Hint Constructors bvalue. +``` + +Let's add all our constructors to `auto`. + +``` code +Hint Constructors bvalue nvalue eval eval_many. +``` + +By default `auto` will never try to unfold definitions to see if a lemma or +constructor can be applied. With the `Hint Unfold` command, we can instruct +`auto` to try unfold definitions in the goal as it is working. + +``` code +Hint Unfold value normal_form. +``` + +There are a few more variants on the `Hint` command that can be used to further +customize `auto`. You can learn about them in the Coq reference manual. + +## Functions and Conversion + +``` code + - [Fixpoint/struct] + - [match ... end] + - [if ... then ... else ...] + - [simpl] + - [remember] +``` + +In this section we start to use Coq as a programming language and learn how to +reason about programs defined within Coq. + +**Example** Coq defines many datatypes in its standard libraries. Have a quick +look now through the library `Datatypes` to see some of the basic ones, in +particular `bool` and `nat`. (Note that constructors of the datatype `nat` are +the letter `O` and the letter `S`. However, Coq will parse and print `nat`s +using a standard decimal representation.) + +We define two more datatypes here that will be useful later. + +``` code +Inductive bool_option : Set := +| some_bool : bool -> bool_option +| no_bool : bool_option. +``` + +``` code +Inductive nat_option : Set := +| some_nat : nat -> nat_option +| no_nat : nat_option. +``` + +**Example** We can define simple (non-recursive) functions from one datatype to +another using the `Definition` keyword. The `match` construct allows us to do +case analysis on a datatype. The `match` expression has a first-match semantics +and allows nested patterns; however, Coq's type checker demands that +pattern-matching be exhaustive. + +We define functions below for converting between Coq `bool`s and boolean values +in our object language. + +``` code +Definition tm_to_bool (t : tm) : bool_option := + match t with + | tm_true => some_bool true + | tm_false => some_bool false + | _ => no_bool + end. +``` + +``` code +Definition bool_to_tm (b : bool) : tm := + match b with + | true => tm_true + | false => tm_false + end. +``` + +**Example** Coq also has an `if/then/else` expression. It can be used, not just +with the type `bool` but, in fact, with any datatype having exactly two +constructors (the first constructor corresponding to the `then` branch and the +second to the `else` branch). Thus, we can define a function `is_bool` as below. + +``` code +Definition is_bool (t : tm) : bool := + if tm_to_bool t then true else false. +``` + +**Example** To define a recursive function, use `Fixpoint` instead of +`Definition`. + +The type system will only allow us to write functions that terminate. The +annotation `{struct t}` here informs the type-checker that termination is +guaranteed because the function is being defined by structural recursion on `t`. + +``` code +Fixpoint tm_to_nat (t : tm) {struct t} : nat_option := + match t with + | tm_zero => some_nat O + | tm_succ t1 => + match tm_to_nat t1 with + | some_nat n => some_nat (S n) + | no_nat => no_nat + end + | _ => no_nat + end. + +Fixpoint nat_to_tm (n : nat) {struct n} : tm := + match n with + | O => tm_zero + | S m => tm_succ (nat_to_tm m) + end. +``` + +**Exercise** Write a function `interp : tm -> tm` that returns the normal form +of its argument according to the small-step semantics given by `eval`. + +Hint: You will want to use `tm_to_nat` (or another auxiliary function) to +prevent stuck terms from stepping in the cases `e_predsucc` and `e_iszerosucc`. + + +**Example** The tactic `simpl` (recursively) reduces the application of a +function defined by pattern-matching to an argument with a constructor at its +head. You can supply `simpl` with a particular expression if you want to prevent +it from simplifying elsewhere. + +``` code +Lemma bool_tm_bool : forall b, + tm_to_bool (bool_to_tm b) = some_bool b. +Proof. + intros b. destruct b. + simpl (bool_to_tm true). simpl. reflexivity. + (* It turns out that [simpl] is unnecessary above, since + [reflexivity] can automatically check that two terms are + convertible. *) + reflexivity. +Qed. +``` + +**Example** We can also apply the tactic `simpl` in our hypotheses. + +``` code +Lemma tm_bool_tm :forall t b, + tm_to_bool t = some_bool b -> + bool_to_tm b = t. +Proof. + intros t b Heq. destruct t. + simpl in Heq. inversion Heq. + simpl. reflexivity. + (* As with [reflexivity], [inversion] can automatically + perform reduction on terms as necessary, so the above use + of [simpl] was optional. *) + inversion Heq. reflexivity. + simpl in Heq. inversion Heq. + (* Again, the above use of [simpl] was optional. *) + inversion Heq. + inversion Heq. + inversion Heq. + inversion Heq. +Qed. +``` + +**Exercise** + +``` code +Lemma tm_to_bool_dom_includes_bvalue : forall bv, + bvalue bv -> exists b, tm_to_bool bv = some_bool b. +Proof. + (* to finish *) +Admitted. +``` + +**Exercise** + +``` code +Lemma tm_to_bool_dom_only_bvalue : forall bv b, + tm_to_bool bv = some_bool b -> bvalue bv. +Proof. + (* to finish *) +Admitted. +``` + +**Example** Not all uses of `simpl` are optional. Sometimes they are necessary +so that we can use the `rewrite` tactic. Observe, also, how using `rewrite` can +automatically trigger a reduction if it creates a redex. + +``` code +Lemma nat_tm_nat : forall n, + tm_to_nat (nat_to_tm n) = some_nat n. +Proof. + intros n. induction n. + reflexivity. + simpl. rewrite -> IHn. reflexivity. +Qed. +``` + +**Example** Here's an example where it is necessary to use `simpl` on a +hypothesis. To trigger a reduction of a `match` expression in a hypothesis, we +use the `destruct` tactic on the expression being matched. + +``` code +Lemma tm_nat_tm : forall t n, + tm_to_nat t = some_nat n -> + nat_to_tm n = t. +Proof. + intros t. induction t; intros n Heq. + inversion Heq. + inversion Heq. + inversion Heq. + inversion Heq. reflexivity. + simpl in Heq. destruct (tm_to_nat t). + inversion Heq. simpl. rewrite -> IHt. + (* Note how we may use [rewrite] even on an equation + that is preceded by some other hypotheses. *) + reflexivity. + reflexivity. + inversion Heq. + inversion Heq. + inversion Heq. +Qed. +``` + +**Exercise** + +``` code +Lemma tm_to_nat_dom_includes_nvalue : forall v, + nvalue v -> exists n, tm_to_nat v = some_nat n. +Proof. + (* to finish *) +Admitted. +``` + +**Exercise** + +``` code +Lemma tm_to_nat_dom_only_nvalue : forall v n, + tm_to_nat v = some_nat n -> nvalue v. +Proof. + (* to finish *) +Admitted. +``` + +**Example** Using the tactic `destruct` (or `induction`) on a complex expression +(i.e., one that is not simply a variable) may not leave you with enough +information for you to finish the proof. The tactic `remember` can help in these +cases. Its usage is demonstrated below. If you are curious, try to finish the +proof without `remember` to see what goes wrong. + +``` code +Lemma remember_example : forall v, + eval_many + (tm_pred (tm_succ v)) + (match tm_to_nat v with + | some_nat _ => v + | no_nat => tm_pred (tm_succ v) + end). +Proof. + intros v. remember (tm_to_nat v) as x. destruct x. + apply m_one. apply e_predsucc. + eapply tm_to_nat_dom_only_nvalue. + rewrite <- Heqx. reflexivity. + apply m_refl. +Qed. +``` + +**Exercise** Prove the following lemmas involving the function `interp` from a +previous exercise: + +``` +Lemma interp_reduces : forall t, + eval_many t (interp t). + +Lemma interp_fully_reduces : forall t, + normal_form (interp t). +``` + + +# Solutions to Exercises + +``` code +Inductive eval_rtc : tm -> tm -> Prop := +| r_eval : forall t t', + eval t t' -> + eval_rtc t t' +| r_refl : forall t, + eval_rtc t t +| r_trans : forall t u v, + eval_rtc t u -> + eval_rtc u v -> + eval_rtc t v. + +Inductive full_eval : tm -> tm -> Prop := +| f_value : forall v, + value v -> + full_eval v v +| f_iftrue : forall t1 t2 t3 v, + full_eval t1 tm_true -> + full_eval t2 v -> + full_eval (tm_if t1 t2 t3) v +| f_iffalse : forall t1 t2 t3 v, + full_eval t1 tm_false -> + full_eval t3 v -> + full_eval (tm_if t1 t2 t3) v +| f_succ : forall t v, + nvalue v -> + full_eval t v -> + full_eval (tm_succ t) (tm_succ v) +| f_predzero : forall t, + full_eval t tm_zero -> + full_eval (tm_pred t) tm_zero +| f_predsucc : forall t v, + nvalue v -> + full_eval t (tm_succ v) -> + full_eval (tm_pred t) v +| f_iszerozero : forall t, + full_eval t tm_zero -> + full_eval (tm_iszero t) tm_true +| f_iszerosucc : forall t v, + nvalue v -> + full_eval t (tm_succ v) -> + full_eval (tm_iszero t) tm_false. + +Lemma m_one_sol : forall t t', + eval t t' -> + eval_many t t'. +Proof. + intros t t' He. apply m_step with (t' := t'). + apply He. + apply m_refl. +Qed. + +Lemma m_two_sol : forall t t' t'', + eval t t' -> + eval t' t'' -> + eval_many t t''. +Proof. + intros t t' t'' He1 He2. apply m_step with (t' := t'). + apply He1. + apply m_one. apply He2. +Qed. + +Lemma m_iftrue_step_sol : forall t t1 t2 u, + eval t tm_true -> + eval_many t1 u -> + eval_many (tm_if t t1 t2) u. +Proof. + intros t t1 t2 u He Hm. + apply m_step with (t' := tm_if tm_true t1 t2). + apply e_if. apply He. + apply m_step with (t' := t1). + apply e_iftrue. + apply Hm. +Qed. + +Lemma m_if_iszero_conj_sol : forall v t2 t2' t3 t3', + nvalue v /\ eval t2 t2' /\ eval t3 t3' -> + eval_many (tm_if (tm_iszero tm_zero) t2 t3) t2' /\ + eval_many (tm_if (tm_iszero (tm_succ v)) t2 t3) t3'. +Proof. + intros v t2 t2' t3 t3' H. + destruct H as [ Hn [ He1 He2 ] ]. split. + apply m_three with + (t' := tm_if tm_true t2 t3) (t'' := t2). + apply e_if. apply e_iszerozero. + apply e_iftrue. + apply He1. + apply m_three with + (t' := tm_if tm_false t2 t3) (t'' := t3). + apply e_if. apply e_iszerosucc. apply Hn. + apply e_iffalse. + apply He2. +Qed. + +Lemma two_values_sol : forall t u, + value t /\ value u -> + bvalue t \/ + bvalue u \/ + (nvalue t /\ nvalue u). +Proof. + unfold value. intros t u H. + destruct H as [ [ Hb1 | Hn1 ] H2 ]. + left. apply Hb1. + destruct H2 as [ Hb2 | Hn2 ]. + right. left. apply Hb2. + right. right. split. + apply Hn1. + apply Hn2. +Qed. + +Lemma m_trans_sol : forall t u v, + eval_many t u -> + eval_many u v -> + eval_many t v. +Proof. + intros t u v Hm1 Hm2. induction Hm1. + apply Hm2. + apply m_step with (t' := t'). + apply H. + apply IHHm1. apply Hm2. +Qed. + +Lemma eval_rtc_many_sol : forall t u, + eval_rtc t u -> + eval_many t u. +Proof. + intros t u Hr. induction Hr. + apply m_one. apply H. + apply m_refl. + apply m_trans with (t' := u). + apply IHHr1. + apply IHHr2. +Qed. + +Lemma eval_many_rtc_sol : forall t u, + eval_many t u -> + eval_rtc t u. +Proof. + intros t u Hm. induction Hm. + apply r_refl. + apply r_trans with (u := t'). + apply r_eval. apply H. + apply IHHm. +Qed. + +Lemma full_eval_to_value_sol : forall t v, + full_eval t v -> + value v. +Proof. + intros t v Hf. induction Hf. + apply H. + apply IHHf2. + apply IHHf2. + right. apply n_succ. apply H. + right. apply n_zero. + right. apply H. + left. apply b_true. + left. apply b_false. +Qed. + +Lemma value_can_expand_sol : forall v, + value v -> + exists u, eval u v. +Proof. + intros v Hv. exists (tm_if tm_true v v). apply e_iftrue. +Qed. + +Lemma exists_iszero_nvalue_sol : forall t, + (exists nv, nvalue nv /\ eval_many t nv) -> + exists bv, eval_many (tm_iszero t) bv. +Proof. + intros t [ nv [ Hnv Hm ]]. destruct Hnv. + exists tm_true. + apply m_trans with (t' := tm_iszero tm_zero). + apply m_iszero. apply Hm. + apply m_one. apply e_iszerozero. + exists tm_false. + apply m_trans with (t' := tm_iszero (tm_succ t0)). + apply m_iszero. apply Hm. + apply m_one. apply e_iszerosucc. apply Hnv. +Qed. + +Lemma normal_form_to_forall_sol : forall t, + normal_form t -> + forall u, ~ eval t u. +Proof. + unfold normal_form, not. intros t H u He. + apply H. exists u. apply He. +Qed. + +Lemma normal_form_from_forall_sol : forall t, + (forall u, ~ eval t u) -> + normal_form t. +Proof. + unfold normal_form, not. intros t H [ t' Het' ]. + apply H with (u := t'). apply Het'. +Qed. + +Lemma negation_exercise_sol : forall v1 v2, + ~ (value v1 \/ value v2) -> + ~ (~ bvalue v1 /\ ~ bvalue v2) -> + eval tm_true tm_false. +Proof. + intros v1 v2 H1 H2. destruct H2. + split. + intros Hb. destruct H1. left. left. apply Hb. + intros Hb. destruct H1. right. left. apply Hb. +Qed. + +Lemma equality_exercise_sol : forall t1 t2 t3 u1 u2 u3 u4, + tm_if t1 t2 t3 = tm_if u1 u2 u2 -> + tm_if t1 t2 t3 = tm_if u3 u3 u4 -> + t1 = u4. +Proof. + intros t1 t2 t3 u1 u2 u3 u4 Heq1 Heq2. + inversion Heq1. subst t1. subst t2. subst t3. + inversion Heq2. reflexivity. +Qed. + +Lemma succ_not_circular_sol : forall t, + t <> tm_succ t. +Proof. + intros t. induction t. + intros Heq. inversion Heq. + intros Heq. inversion Heq. + intros Heq. inversion Heq. + intros Heq. inversion Heq. + intros Heq. inversion Heq. destruct IHt. apply H0. + intros Heq. inversion Heq. + intros Heq. inversion Heq. +Qed. + +Lemma inversion_exercise_sol : forall t, + normal_form t -> + eval_many (tm_pred t) tm_zero -> + nvalue t. +Proof. + intros t Hnf Hm. inversion Hm. subst. inversion H. + apply n_zero. + apply n_succ. apply H2. + destruct Hnf. exists t'0. apply H2. +Qed. + +Lemma contradictory_equalities_exercise_sol : + (exists t, exists u, exists v, + value t /\ + t = tm_succ u /\ + u = tm_pred v) -> + eval tm_true tm_false. +Proof. + intros [ t [ u [ v [ [ Hb | Hn ] [ eq1 eq2 ] ] ] ] ]. + destruct Hb. + inversion eq1. + inversion eq1. + destruct Hn. + inversion eq1. + inversion eq1. subst t. subst u. inversion Hn. +Qed. + +Lemma eval_fact_exercise_sol : forall t1 t2, + eval (tm_iszero (tm_pred t1)) t2 -> + eval t2 tm_false -> + exists u, t1 = tm_succ u. +Proof. + intros t1 t2 He1 He2. inversion He1. subst t2. + inversion He2. subst t'. + inversion H0. exists (tm_succ t0). reflexivity. +Qed. + +Lemma normal_form_if_sol : forall t1 t2 t3, + normal_form (tm_if t1 t2 t3) -> + t1 <> tm_true /\ t1 <> tm_false /\ normal_form t1. +Proof. + intros t1 t2 t3 Hnf. destruct t1. + destruct Hnf. exists t2. apply e_iftrue. + destruct Hnf. exists t3. apply e_iffalse. + split. + intros Heq. inversion Heq. + split. + intros Heq. inversion Heq. + intros [t' He]. destruct Hnf. exists (tm_if t' t2 t3). + apply e_if. apply He. + split. + intros Heq. inversion Heq. + split. + intros Heq. inversion Heq. + intros [t' He]. inversion He. + split. + intros Heq. inversion Heq. + split. + intros Heq. inversion Heq. + intros [t' He]. destruct Hnf. exists (tm_if t' t2 t3). + apply e_if. apply He. + split. + intros Heq. inversion Heq. + split. + intros Heq. inversion Heq. + intros [t' He]. destruct Hnf. exists (tm_if t' t2 t3). + apply e_if. apply He. + split. + intros Heq. inversion Heq. + split. + intros Heq. inversion Heq. + intros [t' He]. destruct Hnf. exists (tm_if t' t2 t3). + apply e_if. apply He. +Qed. + +Lemma full_eval_from_value_sol : forall v w, + value v -> + full_eval v w -> + v = w. +Proof. + intros v w Hv Hf. induction Hf. + reflexivity. + destruct Hv as [ Hb | Hn ]. + inversion Hb. + inversion Hn. + destruct Hv as [ Hb | Hn ]. + inversion Hb. + inversion Hn. + rewrite -> IHHf. + reflexivity. + right. apply value_succ_nvalue. apply Hv. + destruct Hv as [ Hb | Hn ]. + inversion Hb. + inversion Hn. + destruct Hv as [ Hb | Hn ]. + inversion Hb. + inversion Hn. + destruct Hv as [ Hb | Hn ]. + inversion Hb. + inversion Hn. + destruct Hv as [ Hb | Hn ]. + inversion Hb. + inversion Hn. +Qed. + +Lemma value_is_normal_form_sol : forall v, + value v -> + normal_form v. +Proof. + intros v [ Hb | Hn ] [ t He ]. + destruct Hb; inversion He. + generalize dependent t. + induction Hn; intros u He; inversion He; subst. + destruct (IHHn t'). apply H0. +Qed. + +Theorem eval_deterministic_sol : forall t t' t'', + eval t t' -> + eval t t'' -> + t' = t''. +Proof. + intros t t' t'' He1. generalize dependent t''. + induction He1; intros t'' He2; inversion He2; subst. + reflexivity. + inversion H3. + reflexivity. + inversion H3. + inversion He1. + inversion He1. + rewrite -> (IHHe1 t1'0). + reflexivity. + apply H3. + rewrite -> (IHHe1 t'0). + reflexivity. + apply H0. + reflexivity. + inversion H0. + reflexivity. + assert (normal_form (tm_succ t)) as Hnf. + apply nvalue_is_normal_form. apply n_succ. apply H. + destruct Hnf. exists t'. apply H1. + inversion He1. + assert (normal_form (tm_succ t'')) as Hnf. + apply nvalue_is_normal_form. apply n_succ. apply H0. + destruct Hnf. exists t'. apply He1. + rewrite -> (IHHe1 t'0). + reflexivity. + apply H0. + reflexivity. + inversion H0. + reflexivity. + assert (normal_form (tm_succ t)) as Hnf. + apply nvalue_is_normal_form. apply n_succ. apply H. + destruct Hnf. exists t'. apply H1. + inversion He1. + assert (normal_form (tm_succ t0)) as Hnf. + apply nvalue_is_normal_form. apply n_succ. apply H0. + destruct Hnf. exists t'. apply He1. + rewrite -> (IHHe1 t'0). + reflexivity. + apply H0. +Qed. + +Lemma eval_full_eval_sol : forall t t' v, + eval t t' -> + full_eval t' v -> + full_eval t v. +Proof. + intros t t' v He. generalize dependent v. induction He. + intros v Hf. apply f_iftrue. + apply f_value. left. apply b_true. + apply Hf. + intros v Hf. apply f_iffalse. + apply f_value. left. apply b_false. + apply Hf. + intros v Hf. inversion Hf. + subst. inversion H. + inversion H0. + inversion H0. + subst. apply f_iftrue. + apply IHHe. apply H3. + apply H4. + subst. apply f_iffalse. + apply IHHe. apply H3. + apply H4. + intros v Hf. inversion Hf. + subst. apply f_succ. + apply value_succ_nvalue. apply H. + apply IHHe. apply f_value. right. + apply value_succ_nvalue. apply H. + subst. apply f_succ. + apply H0. + apply IHHe. apply H1. + intros v Hf. inversion Hf. apply f_predzero. + apply f_value. right. apply n_zero. + intros v Hf. assert (t = v). + apply full_eval_from_value_sol. + right. apply H. + apply Hf. + subst v. apply f_predsucc. + apply H. + apply f_succ. + apply H. + apply Hf. + intros v Hf. inversion Hf. + subst. destruct H as [ Hb | Hn ]. + inversion Hb. + inversion Hn. + subst. apply f_predzero. apply IHHe. apply H0. + subst. apply f_predsucc. + apply H0. + apply IHHe. apply H1. + intros v Hf. inversion Hf. apply f_iszerozero. + apply f_value. right. apply n_zero. + intros v Hf. inversion Hf. + apply f_iszerosucc with (v := t). + apply H. + apply f_value. right. apply n_succ. apply H. + intros v Hf. inversion Hf. + subst. destruct H as [ Hb | Hn ]. + inversion Hb. + inversion Hn. + subst. apply f_iszerozero. apply IHHe. apply H0. + subst. apply f_iszerosucc with (v := v0). + apply H0. + apply IHHe. apply H1. +Qed. + +Lemma full_eval_complete_sol : forall t v, + value v -> + eval_many t v -> + full_eval t v. +Proof. + intros t v Hv Hm. induction Hm. + apply f_value. apply Hv. + apply eval_full_eval_sol with (t' := t'). + apply H. + apply IHHm. apply Hv. +Qed. + +Lemma pred_not_circular_sol : forall t, + t <> tm_pred t. +Proof. + intros t H. induction t; inversion H; auto. +Qed. + +Lemma m_succ_sol : forall t u, + eval_many t u -> + eval_many (tm_succ t) (tm_succ u). +Proof. + intros t u Hm. + induction Hm; eauto using m_refl, m_step, e_succ. +Qed. + +Lemma m_pred_sol : forall t u, + eval_many t u -> + eval_many (tm_pred t) (tm_pred u). +Proof. + intros t u Hm. + induction Hm; eauto using m_refl, m_step, e_pred. +Qed. + +Fixpoint interp (t : tm) {struct t} : tm := + match t with + | tm_true => tm_true + | tm_false => tm_false + | tm_if t1 t2 t3 => + match interp t1 with + | tm_true => interp t2 + | tm_false => interp t3 + | t4 => tm_if t4 t2 t3 + end + | tm_zero => tm_zero + | tm_succ t1 => tm_succ (interp t1) + | tm_pred t1 => + match interp t1 with + | tm_zero => tm_zero + | tm_succ t2 => + match tm_to_nat t2 with + | some_nat _ => t2 + | no_nat => tm_pred (tm_succ t2) + end + | t2 => tm_pred t2 + end + | tm_iszero t1 => + match interp t1 with + | tm_zero => tm_true + | tm_succ t2 => + match tm_to_nat t2 with + | some_nat _ => tm_false + | no_nat => tm_iszero (tm_succ t2) + end + | t2 => tm_iszero t2 + end + end. + +Lemma tm_to_bool_dom_includes_bvalue_sol : forall bv, + bvalue bv -> exists b, tm_to_bool bv = some_bool b. +Proof. + intros bv H. destruct H. + exists true. reflexivity. + exists false. reflexivity. +Qed. + +Lemma tm_to_bool_dom_only_bvalue_sol : forall bv b, + tm_to_bool bv = some_bool b -> bvalue bv. +Proof. + intros bv b Heq. destruct bv. + apply b_true. + apply b_false. + inversion Heq. + inversion Heq. + inversion Heq. + inversion Heq. + inversion Heq. +Qed. + +Lemma tm_to_nat_dom_includes_nvalue_sol : forall v, + nvalue v -> exists n, tm_to_nat v = some_nat n. +Proof. + intros v Hnv. induction Hnv. + exists O. reflexivity. + destruct IHHnv as [ n Heq ]. exists (S n). + simpl. rewrite -> Heq. reflexivity. +Qed. + +Lemma tm_to_nat_dom_only_nvalue_sol : forall v n, + tm_to_nat v = some_nat n -> nvalue v. +Proof. + intros v. induction v; intros n Heq. + inversion Heq. + inversion Heq. + inversion Heq. + apply n_zero. + apply n_succ. + simpl in Heq. destruct (tm_to_nat v). + inversion Heq. eapply IHv. reflexivity. + inversion Heq. + inversion Heq. + inversion Heq. +Qed. + +Lemma interp_reduces_sol : forall t, + eval_many t (interp t). +Proof. + intros t. induction t. + apply m_refl. + apply m_refl. + simpl. destruct (interp t1). + eapply m_trans. + apply m_if. apply IHt1. + eapply m_trans. + eapply m_one. apply e_iftrue. + apply IHt2. + eapply m_trans. + apply m_if. apply IHt1. + eapply m_trans. + eapply m_one. apply e_iffalse. + apply IHt3. + apply m_if. apply IHt1. + apply m_if. apply IHt1. + apply m_if. apply IHt1. + apply m_if. apply IHt1. + apply m_if. apply IHt1. + apply m_refl. + simpl. apply m_succ. apply IHt. + simpl. destruct (interp t). + apply m_pred. apply IHt. + apply m_pred. apply IHt. + apply m_pred. apply IHt. + eapply m_trans. + apply m_pred. apply IHt. + apply m_one. apply e_predzero. + remember (tm_to_nat t0) as x. destruct x. + eapply m_trans. + apply m_pred. apply IHt. + apply m_one. apply e_predsucc. + eapply tm_to_nat_dom_only_nvalue. + rewrite <- Heqx. reflexivity. + apply m_pred. apply IHt. + apply m_pred. apply IHt. + apply m_pred. apply IHt. + simpl. destruct (interp t). + apply m_iszero. apply IHt. + apply m_iszero. apply IHt. + apply m_iszero. apply IHt. + eapply m_trans. + apply m_iszero. apply IHt. + apply m_one. apply e_iszerozero. + remember (tm_to_nat t0) as x. destruct x. + eapply m_trans. + apply m_iszero. apply IHt. + apply m_one. apply e_iszerosucc. + eapply tm_to_nat_dom_only_nvalue. + rewrite <- Heqx. reflexivity. + apply m_iszero. apply IHt. + apply m_iszero. apply IHt. + apply m_iszero. apply IHt. +Qed. + +Lemma interp_fully_reduces_sol : forall t, + normal_form (interp t). +Proof. + induction t; intros [t' H]. + inversion H. + inversion H. + simpl in H. destruct (interp t1). + destruct IHt2. eauto. + destruct IHt3. eauto. + destruct IHt1. inversion H. eauto. + destruct IHt1. inversion H. eauto. + destruct IHt1. inversion H. eauto. + destruct IHt1. inversion H. eauto. + destruct IHt1. inversion H. eauto. + inversion H. + destruct IHt. inversion H. eauto. + simpl in H. destruct (interp t). + inversion H. inversion H1. + inversion H. inversion H1. + inversion H. destruct IHt. eauto. + inversion H. + remember (tm_to_nat t0) as x. destruct x. + destruct IHt. exists (tm_succ t'). + apply e_succ. apply H. + inversion H; subst. + destruct (tm_to_nat_dom_includes_nvalue t') + as [n Heq]. + apply H1. + rewrite <- Heqx in Heq. inversion Heq. + destruct IHt. eauto. + inversion H. destruct IHt. eauto. + inversion H. destruct IHt. eauto. + simpl in H. destruct (interp t). + inversion H. inversion H1. + inversion H. inversion H1. + inversion H. destruct IHt. eauto. + inversion H. + remember (tm_to_nat t0) as x. destruct x. + inversion H. + inversion H; subst. + destruct (tm_to_nat_dom_includes_nvalue t0) + as [n Heq]. + apply H1. + rewrite <- Heqx in Heq. inversion Heq. + inversion H. destruct IHt. eauto. + inversion H. destruct IHt. eauto. + inversion H. destruct IHt. eauto. +Qed. +``` diff --git a/build-advanced.sh b/build-advanced.sh new file mode 100755 index 0000000..eb36a08 --- /dev/null +++ b/build-advanced.sh @@ -0,0 +1,3 @@ +#!/usr/bin/env bash + +pandoc advanced.md -o advanced.ipynb