advanced.ipynb

{
 "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",
    "Before we begin\n",
    "===============\n",
    "\n",
    "The point of this workshop is to give you a feel for what is it like to\n",
    "do proofs in Coq, and also to illustrate what the Curry-Howard\n",
    "isomorphism really is and what are its applications. This workshop is\n",
    "not graded, and you will not see Coq during the exam (though there’s a\n",
    "big chance you’ll see Curry-Howard, and you may see a fragment of CoC).\n",
    "\n",
    "However, we cannot actually properly teach you how to do proofs in Coq\n",
    "or to explain everything we will do in details, because we simply don’t\n",
    "have enough time for that. In case you are interested in knowing more,\n",
    "you can go through this notebook (or its full version, check the README\n",
    "[here](https://c4science.ch/diffusion/9452/)) in detail yourself, you\n",
    "could read the [Software\n",
    "Foundations](https://softwarefoundations.cis.upenn.edu/) book, and you\n",
    "could take a look at the [Certified Programming with Dependent\n",
    "Types](http://adam.chlipala.net/cpdt/) book.\n",
    "\n",
    "Coq vs CoC\n",
    "==========\n",
    "\n",
    "During the lecture, you have already seen how we can formulate CoC on\n",
    "paper. In this notebook, we will be working with Coq, an interactive\n",
    "theorem assistant with a type system based on an extension of CoC. The\n",
    "differences are slight, but they are there, so let’s start by inspecting\n",
    "them.\n",
    "\n",
    "First things first: you can use the `Check` command to inspect types of\n",
    "terms."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Check 0."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Naturally, we type `0` as `nat`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Check nat."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "If we think in terms of set theory, then all `nat`s form a `Set`. More\n",
    "to the point, `Set` in Coq is a kind of types that represent *data*\n",
    "(more on this in a second).\n",
    "\n",
    "We can define our own types with the `Inductive` command:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Inductive nat' : Set :=\n",
    "| zero'\n",
    "| succ' (n : nat')\n",
    "."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The `Inductive` command introduces an *inductive* data type, inductive\n",
    "in this case meaning being defined inductively. The above definition is\n",
    "basically the same as the following Scala definition:\n",
    "\n",
    "``` scala\n",
    "sealed trait Nat\n",
    "final case object Zero extends Nat\n",
    "final case class Succ(n: Nat) extends Nat\n",
    "```\n",
    "\n",
    "We say that `zero'` and `succ'` are *constructors* for the `nat'` type,\n",
    "since they are the fundamental/primitive way of constructing values of\n",
    "type `nat'`. They are themselves values or functions:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Check zero'.\n",
    "Check succ'."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "And they can also be used to destruct/pattern match on values of type\n",
    "`nat'`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Fixpoint add (n : nat') (m : nat') : nat' :=\n",
    "  match n with\n",
    "  | zero'   => m\n",
    "  | succ' n => add n (succ' m)\n",
    "  end."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Coq is an interactive theorem assistant, so we’d like to use it to do\n",
    "some proofs. Recall that by the Curry-Howard isomorphism, types are\n",
    "propositions and terms that inhabit them are proofs that those\n",
    "propositions are true. Then, if we want to do proofs about whether a\n",
    "number is even or not, we first thing need to define a type for this\n",
    "proposition. Specifically, if `n` is even, we would like to be able to\n",
    "construct a value of type `is_even' n` (note that `is_even'` will need\n",
    "to be a type operator). We can define `is_even'` as follows:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Inductive is_even' : nat' -> Prop :=\n",
    "| zero_even' : is_even' zero'\n",
    "| double_succ_even' (n : nat') (p : is_even' n) : is_even' (succ' (succ' n))\n",
    "."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "As expected, we needed to annotate `is_even'` with `nat' -> Prop` as its\n",
    "type, meaning it’s a type operator from `nat'`s to a propositions (more\n",
    "on `Prop` in a second). We have two constructors for this proposition,\n",
    "and both of them now have annotations for their result types.\n",
    "\n",
    "The first one, `zero_even'`, is a proof that 0 is even, and accordingly\n",
    "its type is `is_even' zero'`. The other one is more complicated. We can\n",
    "understand it as follows: if we want to prove that `n+2` is even, we\n",
    "need to have `n` (naturally) and we need a proof that `n` is even – a\n",
    "value of type `is_even' n`.\n",
    "\n",
    "We can also type function literals with dependent function types. For\n",
    "instance, say that we want to take a value of type `is_even' n` and we\n",
    "want to apply `double_succ_even'` to this value twice – in this case, we\n",
    "want to take a value `n` and use it in a type, so we need a\n",
    "term-dependent function type. Here’s a definition of this function in\n",
    "Coq:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Check fun n : nat' => \n",
    "      fun p : is_even' n =>\n",
    "      double_succ_even' _ (double_succ_even' _ p)."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "(Ignore the underscores for now, they are for boring arguments.) The\n",
    "type of this value has the form `forall n : nat', t`. That’s the Coq\n",
    "equivalent of `(n : nat') -> t` (or `Π(n : nat')t`) from CoC. Believe it\n",
    "or not, the above value is a proof of a trivial statement – namely, that\n",
    "if `n` is even, then so is `n + 4`. You can read out loud this value’s\n",
    "type as follows: “for all n, n being even implies that n+4 is even”.\n",
    "\n",
    "Why the underscores? Because `double_succ_even'` actually needs *two*\n",
    "arguments, an `n : nat'` and a `p : is_even' n`. The value for the first\n",
    "one can be figured out based on the type of the second one, so with an\n",
    "underscore we can tell Coq exactly that – to figure out for us what\n",
    "value should be passed there. Neat.\n",
    "\n",
    "Sets and Props\n",
    "--------------\n",
    "\n",
    "Now, let’s come back to `Set`. You may have noticed that for `is_even'`,\n",
    "we’ve used `Prop` instead. What are those things? Well, here’s what Coq\n",
    "can tell us:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Check Set.\n",
    "Check Prop."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Both `Set` and `Prop` are universes of “proper” types, in the sense of\n",
    "the `*` sort you’ve seen in CoC, whereas `Type` is the equivalent of the\n",
    "“box” sort. How come we have two variants of `*`? The short answer is:\n",
    "`Set` is the universe of *data*, while `Prop` is the universe of\n",
    "*propositions*. That’s honestly as much as you need to understand in\n",
    "order to work with Coq.\n",
    "\n",
    "The longer answer is that there’s multiple small differences between\n",
    "them, all aligned with the above intuition. Values from `Set` can be\n",
    "“extracted” to create OCaml programs, while values from `Prop` cannot\n",
    "(and will in fact be ignored when extracting values from `Set`). `Set`\n",
    "is predicative (meaning universal types can’t quantify over other\n",
    "universal types, like in Hindley-Milner), while `Prop` is impredicative\n",
    "(meaning universal types are as powerful as in System F). On the basis\n",
    "of the proof irrelevance principle, we assume that any two values of the\n",
    "same type from `Prop` are equal. We do not do the same for types in\n",
    "`Set`, which allows us the nice property that `0` is different from `1`\n",
    "and, more generally, allows distinguishing any two values via, for\n",
    "instance, pattern matching. There’s other differences as well, but\n",
    "again: you don’t actually need to know any of them 99% of the time.\n",
    "\n",
    "Alternative form of Inductive\n",
    "-----------------------------\n",
    "\n",
    "Recall the types of `zero'` and `succ'`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Check zero'.\n",
    "Check succ'."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We could also define `nat'` by annotating each constructor with its\n",
    "type, as follows:\n",
    "\n",
    "``` coq\n",
    "Inductive nat' : Set :=\n",
    "| zero' : nat'\n",
    "| succ' : nat' -> nat'\n",
    ".\n",
    "```\n",
    "\n",
    "This is more convenient for more complex definitions, so we will be\n",
    "using this form from now on.\n",
    "\n",
    "Now, let’s start the actual workshop!\n",
    "\n",
    "The NB language, back again\n",
    "===========================\n",
    "\n",
    "During your first project, you worked with the NB language, a trivial\n",
    "system that had natural numbers, booleans and some basic operations for\n",
    "them. In this notebook, we will be working with a very similar language.\n",
    "We will use Coq to encode terms from the NB language, as well as basic\n",
    "judgments and some simple proofs.\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",
    "We will represent these terms in Coq with `tm`, an 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": [
    "This definition is mostly straightforward – for every rule in the\n",
    "grammar, there’s a corresponding constructor. Using the above\n",
    "definition, we can create values corresponding to the terms in our\n",
    "language:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "(* Represents the term \"if (iszero 0) then false else true\" *)\n",
    "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 judgments which tells us which terms are boolean\n",
    "and numeric values. The judgments will have the form `⊢ bvalue t` and\n",
    "`⊢ nvalue t` (for reasons which will become clear in a second). They are\n",
    "defined as follows:\n",
    "\n",
    "       ⊢ bvalue true       (b_true)\n",
    "       ⊢ bvalue false      (b_false)\n",
    "\n",
    "         ⊢ nvalue 0        (n_zero)\n",
    "      \n",
    "         ⊢ nvalue t\n",
    "      -----------------    (n_succ)\n",
    "      ⊢ nvalue (succ t)\n",
    "\n",
    "How do we represent these judgments in Coq? Both `bvalue` and `nvalue`\n",
    "will need to be type operators, like `is_even'`. A judgment is clearly a\n",
    "proposition, so they will both be `Prop`s. The actual definitions are as\n",
    "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": [
    "We have one constructor per each axiom and inference rule – observe that\n",
    "the constructor types are actually quite similar to the rules they\n",
    "represent. We had to assign `n_succ` a dependent function type, since\n",
    "the corresponding inference rule is implicitly quantified with a `t`.\n",
    "\n",
    "Let’s emphasize again what we have. The *type* `nvalue t` represents the\n",
    "*proposition* that `t` is a numeric value. For instance,\n",
    "`nvalue (tm_succ tm_zero)` represents the proposition that the successor\n",
    "of zero (or simply one) is a numeric value. To show that this\n",
    "proposition is true, we need to construct a value of said type. We can\n",
    "do that as follows:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "(** Note: n_succ needs two arguments, a `t : tm` and an `nvalue t`. *)\n",
    "Check (n_succ tm_zero n_zero). "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "As the last thing in this section, we will (finally) define what it\n",
    "means to be a value. In Coq, `T \\/ S` is the data type corresponding to\n",
    "the proof that either `T` or `S` is true. If we use it, the definition\n",
    "is 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. Formally, reduction was a\n",
    "relation between terms. In Coq, we will define an inductive data type\n",
    "`eval (t : tm) (t' : tm) : Prop` corresponding to the proposition that\n",
    "`t` evaluates to `t'` in a single step. The definition is as 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`,\n",
    "corresponding to multi-step beta-reduction.\n",
    "\n",
    "Its inference rules are:\n",
    "\n",
    "     -------------  (m_refl)\n",
    "     eval_many t t \n",
    "     \n",
    "     eval t t'    eval_many t' u\n",
    "     ---------------------------  (m_step)\n",
    "           eval_many t u\n",
    "\n",
    "And its definition is:"
   ]
  },
  {
   "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": [
    "<!--\n",
    "### Aside\n",
    "\n",
    "You may be surprised that we defined data types for propositions that a term is\n",
    "a value and that a term evaluates to another term. We could also define a function\n",
    "that checks if a term is a value and returns a boolean, and a function that takes\n",
    "a term and returns the term its argument reduces to. How come we didn't do that?\n",
    "\n",
    "Here we could discuss decidability vs. undecidability and the fact that it's\n",
    "difficult to do induction on fixpoints.\n",
    "-->\n",
    "\n",
    "### Exercises\n",
    "\n",
    "**Note** The exercises below may be hard. If you find yourself stuck\n",
    "when doing them, copy the definitions from solutions here - they will be\n",
    "useful later on.\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."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "(** Write your solution here *)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**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."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "(**\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",
    "*)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "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 trying to prove) and no hypotheses. A\n",
    "goal can be solved, and thereby eliminated, when it exactly matches one\n",
    "of 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 use 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, we will create a value corresponding to a\n",
    "(still) simple proposition. Step through every cell below to see how\n",
    "this value 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": [
    "At this point, we have successfully concluded our proof;\n",
    "`e_succ_pred_succ` is a value that can be used like any other value we\n",
    "have seen so far. It corresponds 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",
    "We can see the value we have constructed with the following command:"
   ]
  },
  {
   "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": [
    "#### 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 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 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": [
    "Reasoning by Cases and Induction\n",
    "--------------------------------\n",
    "\n",
    "        - [destruct] (for inductively defined propositions)\n",
    "        - [induction]\n",
    "\n",
    "**Example** Use `destruct` to reason by cases on an inductively defined\n",
    "datatype or proposition."
   ]
  },
  {
   "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": [
    "**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.)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "(**\n",
    "Lemma eval_rtc_many : forall t u,\n",
    "  eval_rtc t u ->\n",
    "  eval_many t u.\n",
    "*)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Exercise** Prove the following lemma."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "(**\n",
    "Lemma eval_many_rtc : forall t u,\n",
    "  eval_many t u ->\n",
    "  eval_rtc t u.\n",
    "*)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Exercise** Prove the following lemma."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "(**\n",
    "Lemma full_eval_to_value : forall t v,\n",
    "  full_eval t v ->\n",
    "  value v.\n",
    "*)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "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."
   ]
  }
 ],
 "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"
  }
 }
}