Library CoqIntro
A streamlined interactive tutorial on fundamentals of Coq,
focusing on a minimal set of features needed for developing
programming language metatheory.
Mostly developed by Aaron Bohannon, with help from Benjamin Pierce, Dimitrios Vytiniotis, and Steve Zdancewic.
Mostly developed by Aaron Bohannon, with help from Benjamin Pierce, Dimitrios Vytiniotis, and Steve Zdancewic.
Contents
- Getting Started
- Definitions
- Proofs
- Working with Implication and Universal Quantification
- Working with Definitions
- Working with Conjunction and Disjunction
- Reasoning by Cases and Induction
- Working with Existential Quantification
- Working with Negation
- Working with Equality
- Reasoning by Inversion
- Additional Important Tactics
- Basic Automation
- Functions and Conversion
- Solutions to Exercises
To get started...
- Install Coq (from the Download page of the main Coq web site)
- Install an IDE: either CoqIDE (from the same page) or Proof General (use Google to find it).
- Which should you choose? Their command sets are similar,
so basically the trade-offs are simple:
- Proof General is an extension of Emacs (or XEmacs, if you prefer), while CoqIDE uses a simpler point-and-click model of editing.
- PG is pretty easy to install; CoqIDE is very easy to install if you can find a pre-built version for the OS you are running on but can be a little tricky to build from scratch because it has lots of dependencies.
- Familiarize yourself with the most important commands
-
- If you are using PG, try this:
- Open this file and check that the mode line says something like "coq Holes Scripting"
- Go down a few pages and do C-C C-return. Notice that the part of the file above the cursor changes color (and becomes read-only), indicating that it has been sent to Coq.
- Come back here and do C-C C-return again
- You now know all you really need to navigate in this file and send parts of it to Coq, but there are some other navigation commands that are sometimes more convenient. To see a couple more, do C-C C-n several times and observe the result; then do C-C C-u a couple of times and observe the result.
- If you are using PG, try this:
-
- If you are using CoqIDE, try this:
- Open this file.
- Scroll down a few pages.
- Hover the mouse over each the buttons at the top of the window; this will make the "tool tips" appear so you can see which is which.
- Press the "Go to cursor" button. Observe what happens.
- Press the forward and backward buttons a few times. Observe.
- Scroll back to here again and start reading.
- If you are using CoqIDE, try this:
- Open the Coq reference manual (from the Documentation page of the Coq web site) in a web browser. Spend 30 seconds looking over the table of contents to get an idea what's there. (There is no need to actually read anything now.)
In this file, we will be working with a very simple language
of expressions over natural numbers and booleans. First we
need to define the datatype of terms.
The Inductive keyword defines a new inductive type. We name our new type tm and declare that tm lives in the sort Set. Types in Set are datatypes, which can be used just like those in standard programming languages. After the inductive definition, the global environment contains the name of the newly defined type, along with the names of all of the constructors. Coq also automatically defines a few operators for eliminating values of the new type (tm_rec, tm_ind, etc.); we can ignore these for the time being, since we will not need to use them directly.
The Inductive keyword defines a new inductive type. We name our new type tm and declare that tm lives in the sort Set. Types in Set are datatypes, which can be used just like those in standard programming languages. After the inductive definition, the global environment contains the name of the newly defined type, along with the names of all of the constructors. Coq also automatically defines a few operators for eliminating values of the new type (tm_rec, tm_ind, etc.); we can ignore these for the time being, since we will not need to use them directly.
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.
Next, we want to designate some of our tm expressions as
"values" in our object language. Mathematically, the
property of being a value is a unary relation over tms.
The definition of the unary relation value will be built
from the definition of two auxiliary relations: bvalue for
the set of boolean values and nvalue for the set of
numerical values.
We define n-ary relations in Coq much as we do on paper -- by giving a set of inference rules that can be used to justify the membership of a tuple in the relation. The definition of such an inference system also uses the keyword Inductive. Although this is exactly the same device we used to build the set tm, in this case we want to do something slightly different: we will be using it to inductively defining the structures (derivation trees) that justify the membership of a tuple in a relation, rather than directly defining a set inductively. These derivation trees will need to be given a dependent type in order to ensure that only correct derivation trees can be built. It is possible to view their type as a datatype such as tm; however, it is more natural to interpret it as a proposition, so it will be declared to live in Prop instead of Set. Prop is parallel to Set in the sort hierarchy, but types in Prop can be thought of as logical propositions rather than datatypes. The inhabitants of types in Prop can be thought of as proofs rather than programs.
The unary relations bvalue and nvalue are defined by very simple inference systems, each having just two rules. After defining these inference systems, bvalue and nvalue will each be a family of types indexed by elements of tm. We can build inhabitants of some (but not all) of the types in these families with the constructors from our inductive definition. Semantically, we consider the proposition bvalue t to be true if it is inhabited and false if it is not. (It is worth noting at this point that, by default, Coq's logic is constructive and P ∨ not P is provable for some P but not for others. However, it is sound to add the law of the excluded middle as an axiom, if desired.)
We define n-ary relations in Coq much as we do on paper -- by giving a set of inference rules that can be used to justify the membership of a tuple in the relation. The definition of such an inference system also uses the keyword Inductive. Although this is exactly the same device we used to build the set tm, in this case we want to do something slightly different: we will be using it to inductively defining the structures (derivation trees) that justify the membership of a tuple in a relation, rather than directly defining a set inductively. These derivation trees will need to be given a dependent type in order to ensure that only correct derivation trees can be built. It is possible to view their type as a datatype such as tm; however, it is more natural to interpret it as a proposition, so it will be declared to live in Prop instead of Set. Prop is parallel to Set in the sort hierarchy, but types in Prop can be thought of as logical propositions rather than datatypes. The inhabitants of types in Prop can be thought of as proofs rather than programs.
The unary relations bvalue and nvalue are defined by very simple inference systems, each having just two rules. After defining these inference systems, bvalue and nvalue will each be a family of types indexed by elements of tm. We can build inhabitants of some (but not all) of the types in these families with the constructors from our inductive definition. Semantically, we consider the proposition bvalue t to be true if it is inhabited and false if it is not. (It is worth noting at this point that, by default, Coq's logic is constructive and P ∨ not P is provable for some P but not for others. However, it is sound to add the law of the excluded middle as an axiom, if desired.)
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 : ∀ t,
nvalue t →
nvalue (tm_succ t).
The Definition keyword is used for defining non-recursive
functions (including 0-ary functions, i.e., constants).
Here we define the unary predicate value using disjunction
on propositions (written ∨).
Note: It is not actually necessary to provide the types of the arguments nor the return type when they can easily be inferred; for example, the annotations : tm and : Prop are optional here.
Note: It is not actually necessary to provide the types of the arguments nor the return type when they can easily be inferred; for example, the annotations : tm and : Prop are optional here.
Having defined tms and values, we can define a
call-by-value operational semantics of our language by
giving a definition of the single-step evaluation of one
term to another. We give this as an inductively defined
binary relation.
Inductive eval : tm → tm → Prop :=
| e_iftrue : ∀ t2 t3,
eval (tm_if tm_true t2 t3) t2
| e_iffalse : ∀ t2 t3,
eval (tm_if tm_false t2 t3) t3
| e_if : ∀ t1 t1' t2 t3,
eval t1 t1' →
eval (tm_if t1 t2 t3) (tm_if t1' t2 t3)
| e_succ : ∀ t t',
eval t t' →
eval (tm_succ t) (tm_succ t')
| e_predzero :
eval (tm_pred tm_zero) tm_zero
| e_predsucc : ∀ t,
nvalue t →
eval (tm_pred (tm_succ t)) t
| e_pred : ∀ t t',
eval t t' →
eval (tm_pred t) (tm_pred t')
| e_iszerozero :
eval (tm_iszero tm_zero) tm_true
| e_iszerosucc : ∀ t,
nvalue t →
eval (tm_iszero (tm_succ t)) tm_false
| e_iszero : ∀ t t',
eval t t' →
eval (tm_iszero t) (tm_iszero t').
We define multi-step evaluation with the relation
eval_many. This relation includes all of the pairs of
terms that are connected by sequences of evaluation steps.
Inductive eval_many : tm → tm → Prop :=
| m_refl : ∀ t,
eval_many t t
| m_step : ∀ t t' u,
eval t t' →
eval_many t' u →
eval_many t u.
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.
A term is a normal_form if there is no term to which it
can step. Note the concrete syntax for negation and
existential quantification in the definition below.
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).
Tip
If you want to see the type of an identifier x, you can use the command Check x. If you want to see the definition of an identifier x, you can use the command Print x.
A proposition and its proof are both represented as terms in
the calculus of inductive constructions, which is
syntactically very small.
Proof terms 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 use 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.
Proof terms 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 use 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.
Example
The tactic intros x1 ... xn moves antecedents and universally quantified variables from the goal into the context as hypotheses. The tactic apply is complementary to intros. If the conclusion (the part following the rightmost arrow) of a constructor, hypothesis, or lemma e matches our current goal, then apply e will replace the goal with a new goal for each premise/antecedent of e. If e has no premises, then the current goal is solved. Using apply allows us to build a proof tree from the bottom up. In the following example, our proof script will effectively build 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 the proof to see how this tree is constructed. For each tactic, we give the corresponding statement in a written proof. (The uses of Check are inessential.)
Let t be a tm.
Assume that t is an nvalue (and let's call that
assumption Hn for future reference).
By e_succ, in order to prove our conclusion, it suffices
to prove that eval (tm_pred (tm_succ t)) t.
That, in turn, can be shown by e_predsucc, if we are
able to show that nvalue t.
But, in fact, we assumed nvalue t.
Qed.
Hint for PG users
If you place the cursor after Proof. and do C-c C-return, you'll notice that the window displaying Coq's responses is (annoyingly) empty, instead of showing what is to be proved. The reason for this is that, actually, a different buffer is being displayed! (To see this, do C-c C-n and C-c C-u a few times and notice that the buffer name in the mode line changes.) You can use C-c C-p to switch the display back from the *response* buffer to the *goals* buffer.Example
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. (Note that the use of this feature means that our proof scripts are not invariant under alpha-equivalence on the types of our constructors and lemmas. If this is a concern, there are other means of achieving the same result in a way that is compatible with alpha-conversion. See the next example.)
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)
Let t be a tm, and assume nvalue t.
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.
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.
And, in fact, we assumed nvalue t.
Moreover, by the rule m_refl, we also may conclude
eval (tm_succ t) (tm_succ t).
Example
Coq is built around the Curry-Howard correspondence. Proofs of universally quantified propositions are functions that take the witness of the quantifier as an argument. Similarly, proofs of implications are functions that take one proof as an argument and return another proof. Observe the types of the following terms.Check (e_succ_pred_succ).
Check (e_succ_pred_succ tm_zero).
Check (n_zero).
Check (e_succ_pred_succ tm_zero n_zero).
Example
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.
Lemma m_succ_pred_succ_alt : ∀ t,
nvalue t →
eval_many (tm_succ (tm_pred (tm_succ t))) (tm_succ t).
Check m_step.
Check e_succ_pred_succ.
Check m_refl.
Qed.
Hint for PG users
By default, the "." key is "electric" -- it inserts a period _and_ causes the material up to the cursor to be sent to Coq. If you find this behavior annoying, it can be toggled by doing "C-c .".Exercise
Write a proof script to prove the following lemma, based upon the proof given in English.Note: The lemma and the next should be useful in later proofs.
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.
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.
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.
Example
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.Definition strongly_diverges t :=
∀ u, eval_many t u → ~ normal_form u.
Lemma unfold_example : ∀ t t',
strongly_diverges t →
eval t t' →
strongly_diverges t'.
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.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.
Lemma m_if_iszero_conj : ∀ 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'.
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'.
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.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.
Lemma e_if_true_or_false : ∀ t1 t2,
eval t1 tm_true ∨ eval t1 tm_false →
eval_many (tm_if t1 t2 t2) t2.
eval t1 tm_true ∨ eval t1 tm_false →
eval_many (tm_if t1 t2 t2) t2.
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. ...
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.
Lemma destruct_example : ∀ bv t t' t'',
bvalue bv →
(value bv → eval t t' ∧ eval t' t'') →
eval_many t t''.
bvalue bv →
(value bv → eval t t' ∧ eval t' t'') →
eval_many t t''.
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.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).
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.
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.
Exercise
It is possible to use destruct not just on hypotheses but on any lemma we have proved. If we have a lemmalemma1 : 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.
Lemma m_iszero_nvalue : ∀ t v,
nvalue v →
eval_many t v →
eval_many (tm_iszero t) tm_true ∨
eval_many (tm_iszero t) tm_false.
nvalue v →
eval_many t v →
eval_many (tm_iszero t) tm_true ∨
eval_many (tm_iszero t) tm_false.
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.
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.
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.
Exercise
Tip: You should find the lemma m_iszero useful. Use Check m_iszero. if you've forgotten its statement.
Lemma exists_iszero_nvalue : ∀ t,
(∃ nv, nvalue nv ∧ eval_many t nv) →
∃ bv, eval_many (tm_iszero t) bv.
(∃ nv, nvalue nv ∧ eval_many t nv) →
∃ bv, eval_many (tm_iszero t) bv.
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.
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.)
Example
If you happen to have False as a hypothesis, you may use destruct on that hypothesis to solve your goal.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.
Lemma destruct_negation_example : ∀ t v,
value v →
eval t tm_zero →
(value v → normal_form t) →
eval tm_true tm_false.
value v →
eval t tm_zero →
(value v → normal_form t) →
eval tm_true tm_false.
Lemma negation_exercise : ∀ v1 v2,
~ (value v1 ∨ value v2) →
~ (~ bvalue v1 ∧ ~ bvalue v2) →
eval tm_true tm_false.
~ (value v1 ∨ value v2) →
~ (~ bvalue v1 ∧ ~ bvalue v2) →
eval tm_true tm_false.
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.
Lemma equality_example_1 : ∀ 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)).
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)).
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.
Lemma equality_example_2a : ∀ t u v,
tm_succ t = tm_succ u →
eval (tm_succ u) v →
eval (tm_succ t) v.
Lemma equality_example_2b : ∀ t u v,
tm_succ t = tm_succ u →
eval (tm_succ u) v →
eval (tm_succ t) v.
tm_succ t = tm_succ u →
eval (tm_succ u) v →
eval (tm_succ t) v.
Lemma equality_example_2b : ∀ t u v,
tm_succ t = tm_succ u →
eval (tm_succ u) v →
eval (tm_succ t) v.
Example
We also note that, analogously with destruct, we may use rewrite even with a hypothesis (or lemma) that has antecedents.
Lemma equality_example_2c : ∀ t u v,
nvalue v →
(nvalue v → tm_succ t = tm_succ u) →
eval (tm_succ u) v →
eval (tm_succ t) v.
nvalue v →
(nvalue v → tm_succ t = tm_succ u) →
eval (tm_succ u) v →
eval (tm_succ t) v.
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.)
Lemma equality_exercise : ∀ 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.
tm_if t1 t2 t3 = tm_if u1 u2 u2 →
tm_if t1 t2 t3 = tm_if u3 u3 u4 →
t1 = u4.
Example
inversion will also solve a goal when unification fails on a hypothesis. (Internally, Coq can construct a proof of False from contradictory equalities.)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.
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.)
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).
Lemma contradictory_equalities_exercise :
(∃ t, ∃ u, ∃ v,
value t ∧
t = tm_succ u ∧
u = tm_pred v) →
eval tm_true tm_false.
(∃ t, ∃ u, ∃ v,
value t ∧
t = tm_succ u ∧
u = tm_pred v) →
eval tm_true tm_false.
Lemma eval_fact_exercise : ∀ t1 t2,
eval (tm_iszero (tm_pred t1)) t2 →
eval t2 tm_false →
∃ u, t1 = tm_succ u.
eval (tm_iszero (tm_pred t1)) t2 →
eval t2 tm_false →
∃ u, t1 = tm_succ u.
Lemma normal_form_if : ∀ t1 t2 t3,
normal_form (tm_if t1 t2 t3) →
t1 ≠ tm_true ∧ t1 ≠ tm_false ∧ normal_form t1.
normal_form (tm_if t1 t2 t3) →
t1 ≠ tm_true ∧ t1 ≠ tm_false ∧ normal_form t1.
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 ∀ quantifier in front, then we must make sure our goal has a ∀ 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.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.Example
assert can also be supplied with a tactic that proves the assertion. We rewrite the above proof using this form.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.
Lemma single_step_to_multi_step_determinacy :
(∀ t u1 u2, eval t u1 → eval t u2 → u1 = u2) →
∀ t v1 v2,
eval_many t v1 → normal_form v1 →
eval_many t v2 → normal_form v2 →
v1 = v2.
(∀ t u1 u2, eval t u1 → eval t u2 → u1 = u2) →
∀ t v1 v2,
eval_many t v1 → normal_form v1 →
eval_many t v2 → normal_form v2 →
v1 = v2.
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!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.
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.Example
You can use esplit to turn an existentially quantified variable in your goal into a unification variable.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.
Lemma auto_example : ∀ t t' t'',
eval t t' →
eval t' t'' →
(∀ u, eval t t' → eval t' u → eval_many t u) →
eval t' t ∨ t = t ∧ eval_many t t''.
eval t t' →
eval t' t'' →
(∀ u, eval t t' → eval t' u → eval_many t u) →
eval t' t ∨ t = t ∧ eval_many t t''.
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
This lemma has two significantly differences from the previous one, both of which render auto useless.
Lemma eauto_example : ∀ t t' t'',
eval t t' →
eval t' t'' →
(∀ u, eval t u → eval u t'' → eval_many t t'') →
eval t' t ∨ (∃ u, t = u) ∧ eval_many t t''.
eval t t' →
eval t' t'' →
(∀ u, eval t u → eval u t'' → eval_many t t'') →
eval t' t ∨ (∃ u, t = u) ∧ eval_many t t''.
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.
Lemma eauto_using_example : ∀ t t' t'',
eval t t' →
eval t' t'' →
eval t' t ∨ t = t ∧ eval_many t t''.
eval t t' →
eval t' t'' →
eval t' t ∨ t = t ∧ eval_many t t''.
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.
Lemma pred_not_circular : ∀ t,
t ≠ tm_pred t.
Lemma m_succ : ∀ t u,
eval_many t u →
eval_many (tm_succ t) (tm_succ u).
Lemma m_pred : ∀ t u,
eval_many t u →
eval_many (tm_pred t) (tm_pred u).
t ≠ tm_pred t.
Lemma m_succ : ∀ t u,
eval_many t u →
eval_many (tm_succ t) (tm_succ u).
Lemma m_pred : ∀ t u,
eval_many t u →
eval_many (tm_pred t) (tm_pred u).
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.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.
Constructors of inductively defined propositions are some of
the most frequently needed by auto. Instead of writing
we may simply write
Let's add all our constructors to auto.
Hint Resolve b_true b_false.
we may simply write
Hint Constructors bvalue.
Let's add all our constructors to auto.
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.
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
- 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 nats using a standard decimal representation.)We define two more datatypes here that will be useful later.
Inductive bool_option : Set :=
| some_bool : bool → bool_option
| no_bool : bool_option.
Inductive nat_option : Set :=
| some_nat : nat → nat_option
| no_nat : nat_option.
| some_bool : bool → bool_option
| no_bool : bool_option.
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 bools and boolean values in our object language.
Definition tm_to_bool (t : tm) : bool_option :=
match t with
| tm_true ⇒ some_bool true
| tm_false ⇒ some_bool false
| _ ⇒ no_bool
end.
Definition bool_to_tm (b : bool) : tm :=
match b with
| true ⇒ tm_true
| false ⇒ tm_false
end.
match t with
| tm_true ⇒ some_bool true
| tm_false ⇒ some_bool false
| _ ⇒ no_bool
end.
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.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.
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.
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.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.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.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.
Lemma remember_example : ∀ 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).
eval_many
(tm_pred (tm_succ v))
(match tm_to_nat v with
| some_nat _ ⇒ v
| no_nat ⇒ tm_pred (tm_succ v)
end).
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).
Inductive eval_rtc : tm → tm → Prop :=
| r_eval : ∀ t t',
eval t t' →
eval_rtc t t'
| r_refl : ∀ t,
eval_rtc t t
| r_trans : ∀ t u v,
eval_rtc t u →
eval_rtc u v →
eval_rtc t v.
Inductive full_eval : tm → tm → Prop :=
| f_value : ∀ v,
value v →
full_eval v v
| f_iftrue : ∀ t1 t2 t3 v,
full_eval t1 tm_true →
full_eval t2 v →
full_eval (tm_if t1 t2 t3) v
| f_iffalse : ∀ t1 t2 t3 v,
full_eval t1 tm_false →
full_eval t3 v →
full_eval (tm_if t1 t2 t3) v
| f_succ : ∀ t v,
nvalue v →
full_eval t v →
full_eval (tm_succ t) (tm_succ v)
| f_predzero : ∀ t,
full_eval t tm_zero →
full_eval (tm_pred t) tm_zero
| f_predsucc : ∀ t v,
nvalue v →
full_eval t (tm_succ v) →
full_eval (tm_pred t) v
| f_iszerozero : ∀ t,
full_eval t tm_zero →
full_eval (tm_iszero t) tm_true
| f_iszerosucc : ∀ t v,
nvalue v →
full_eval t (tm_succ v) →
full_eval (tm_iszero t) tm_false.
Lemma m_one_sol : ∀ t t',
eval t t' →
eval_many t t'.
Lemma m_two_sol : ∀ t t' t'',
eval t t' →
eval t' t'' →
eval_many t t''.
Lemma m_iftrue_step_sol : ∀ t t1 t2 u,
eval t tm_true →
eval_many t1 u →
eval_many (tm_if t t1 t2) u.
Lemma m_if_iszero_conj_sol : ∀ 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'.
Lemma two_values_sol : ∀ t u,
value t ∧ value u →
bvalue t ∨
bvalue u ∨
(nvalue t ∧ nvalue u).
Lemma m_trans_sol : ∀ t u v,
eval_many t u →
eval_many u v →
eval_many t v.
Lemma eval_rtc_many_sol : ∀ t u,
eval_rtc t u →
eval_many t u.
Lemma eval_many_rtc_sol : ∀ t u,
eval_many t u →
eval_rtc t u.
Lemma full_eval_to_value_sol : ∀ t v,
full_eval t v →
value v.
Lemma value_can_expand_sol : ∀ v,
value v →
∃ u, eval u v.
Lemma exists_iszero_nvalue_sol : ∀ t,
(∃ nv, nvalue nv ∧ eval_many t nv) →
∃ bv, eval_many (tm_iszero t) bv.
Lemma normal_form_to_forall_sol : ∀ t,
normal_form t →
∀ u, ~ eval t u.
Lemma normal_form_from_forall_sol : ∀ t,
(∀ u, ~ eval t u) →
normal_form t.
Lemma negation_exercise_sol : ∀ v1 v2,
~ (value v1 ∨ value v2) →
~ (~ bvalue v1 ∧ ~ bvalue v2) →
eval tm_true tm_false.
Lemma equality_exercise_sol : ∀ 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.
Lemma succ_not_circular_sol : ∀ t,
t ≠ tm_succ t.
Lemma inversion_exercise_sol : ∀ t,
normal_form t →
eval_many (tm_pred t) tm_zero →
nvalue t.
Lemma contradictory_equalities_exercise_sol :
(∃ t, ∃ u, ∃ v,
value t ∧
t = tm_succ u ∧
u = tm_pred v) →
eval tm_true tm_false.
Lemma eval_fact_exercise_sol : ∀ t1 t2,
eval (tm_iszero (tm_pred t1)) t2 →
eval t2 tm_false →
∃ u, t1 = tm_succ u.
Lemma normal_form_if_sol : ∀ t1 t2 t3,
normal_form (tm_if t1 t2 t3) →
t1 ≠ tm_true ∧ t1 ≠ tm_false ∧ normal_form t1.
Lemma full_eval_from_value_sol : ∀ v w,
value v →
full_eval v w →
v = w.
Lemma value_is_normal_form_sol : ∀ v,
value v →
normal_form v.
Theorem eval_deterministic_sol : ∀ t t' t'',
eval t t' →
eval t t'' →
t' = t''.
Lemma eval_full_eval_sol : ∀ t t' v,
eval t t' →
full_eval t' v →
full_eval t v.
Lemma full_eval_complete_sol : ∀ t v,
value v →
eval_many t v →
full_eval t v.
Lemma pred_not_circular_sol : ∀ t,
t ≠ tm_pred t.
Lemma m_succ_sol : ∀ t u,
eval_many t u →
eval_many (tm_succ t) (tm_succ u).
Lemma m_pred_sol : ∀ t u,
eval_many t u →
eval_many (tm_pred t) (tm_pred u).
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 : ∀ bv,
bvalue bv → ∃ b, tm_to_bool bv = some_bool b.
Lemma tm_to_bool_dom_only_bvalue_sol : ∀ bv b,
tm_to_bool bv = some_bool b → bvalue bv.
Lemma tm_to_nat_dom_includes_nvalue_sol : ∀ v,
nvalue v → ∃ n, tm_to_nat v = some_nat n.
Lemma tm_to_nat_dom_only_nvalue_sol : ∀ v n,
tm_to_nat v = some_nat n → nvalue v.
Lemma interp_reduces_sol : ∀ t,
eval_many t (interp t).
Lemma interp_fully_reduces_sol : ∀ t,
normal_form (interp t).
This page has been generated by coqdoc