Mercurial > cpdt > repo
comparison src/Predicates.v @ 61:b581446229fd
Make exercises display properly in HTML
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 30 Sep 2008 14:02:40 -0400 |
| parents | 41ee8f8c9d17 |
| children | 55199444e5e7 |
comparison
equal
deleted
inserted
replaced
| 60:41ee8f8c9d17 | 61:b581446229fd |
|---|---|
| 864 %\item%#<li># Prove these tautologies of propositional logic, using only the tactics [apply], [assumption], [constructor], [destruct], [intro], [intros], [left], [right], [split], and [unfold]. | 864 %\item%#<li># Prove these tautologies of propositional logic, using only the tactics [apply], [assumption], [constructor], [destruct], [intro], [intros], [left], [right], [split], and [unfold]. |
| 865 %\begin{enumerate}%#<ol># | 865 %\begin{enumerate}%#<ol># |
| 866 %\item%#<li># [(True \/ False) /\ (False \/ True)]#</li># | 866 %\item%#<li># [(True \/ False) /\ (False \/ True)]#</li># |
| 867 %\item%#<li># [P -> ~ ~P]#</li># | 867 %\item%#<li># [P -> ~ ~P]#</li># |
| 868 %\item%#<li># [P /\ (Q \/ R) -> (P /\ Q) \/ (P /\ R)]#</li># | 868 %\item%#<li># [P /\ (Q \/ R) -> (P /\ Q) \/ (P /\ R)]#</li># |
| 869 #</ol> </li>#%\end{enumerate}% *) | 869 #</ol> </li>#%\end{enumerate}% |
| 870 | 870 |
| 871 (** remove printing exists*) | 871 %\item%#<li># Prove the following tautology of first-order logic, using only the tactics [apply], [assert], [assumption], [destruct], [eapply], [eassumption], and %\textit{%#<tt>#exists#</tt>#%}%. You will probably find [assert] useful for stating and proving an intermediate lemma, enabling a kind of "forward reasoning," in contrast to the "backward reasoning" that is the default for Coq tactics. [eassumption] is a version of [assumption] that will do matching of unification variables. Let some variable [T] of type [Set] be the set of individuals. [x] is a constant symbol, [p] is a unary predicate symbol, [q] is a binary predicate symbol, and [f] is a unary function symbol. |
| 872 (** %\item%#<li># Prove the following tautology of first-order logic, using only the tactics [apply], [assert], [assumption], [destruct], [eapply], [eassumption], and [exists]. You will probably find [assert] useful for stating and proving an intermediate lemma, enabling a kind of "forward reasoning," in contrast to the "backward reasoning" that is the default for Coq tactics. [eassumption] is a version of [assumption] that will do matching of unification variables. Let some variable [T] of type [Set] be the set of individuals. [x] is a constant symbol, [p] is a unary predicate symbol, [q] is a binary predicate symbol, and [f] is a unary function symbol. **) | 872 %\begin{enumerate}%#<ol># |
| 873 (** printing exists $\exists$ *) | |
| 874 (** %\begin{enumerate}%#<ol># | |
| 875 %\item%#<li># [p x -> (forall x, p x -> exists y, q x y) -> (forall x y, q x y -> q y (f y)) -> exists z, q z (f z)]#</li># | 873 %\item%#<li># [p x -> (forall x, p x -> exists y, q x y) -> (forall x y, q x y -> q y (f y)) -> exists z, q z (f z)]#</li># |
| 876 #</ol> </li>#%\end{enumerate}% | 874 #</ol> </li>#%\end{enumerate}% |
| 877 | 875 |
| 878 %\item%#<li># Define an inductive predicate capturing when a natural number is an integer multiple of either 6 or 10. Prove that 13 does not satisfy your predicate, and prove that any number satisfying the predicate is not odd. It is probably easiest to prove the second theorem by indicating "odd-ness" as equality to [2 * n + 1] for some [n].#</li># | 876 %\item%#<li># Define an inductive predicate capturing when a natural number is an integer multiple of either 6 or 10. Prove that 13 does not satisfy your predicate, and prove that any number satisfying the predicate is not odd. It is probably easiest to prove the second theorem by indicating "odd-ness" as equality to [2 * n + 1] for some [n].#</li># |
| 879 | 877 |
| 890 %\item%#<li># Define typing judgments for expressions, values, and commands. The expression and command cases will be in terms of a typing assignment.#</li># | 888 %\item%#<li># Define typing judgments for expressions, values, and commands. The expression and command cases will be in terms of a typing assignment.#</li># |
| 891 %\item%#<li># Define a predicate [varsType] to express when a variable assignment and a variable typing agree on the types of variables.#</li># | 889 %\item%#<li># Define a predicate [varsType] to express when a variable assignment and a variable typing agree on the types of variables.#</li># |
| 892 %\item%#<li># Prove that any expression that has type [t] under variable typing [vt] evaluates under variable assignment [va] to some value that also has type [t] in [vt], as long as [va] and [vt] agree.#</li># | 890 %\item%#<li># Prove that any expression that has type [t] under variable typing [vt] evaluates under variable assignment [va] to some value that also has type [t] in [vt], as long as [va] and [vt] agree.#</li># |
| 893 %\item%#<li># Prove that any command that has type [t] under variable typing [vt] evaluates under variable assignment [va] to some value that also has type [t] in [vt], as long as [va] and [vt] agree.#</li># | 891 %\item%#<li># Prove that any command that has type [t] under variable typing [vt] evaluates under variable assignment [va] to some value that also has type [t] in [vt], as long as [va] and [vt] agree.#</li># |
| 894 #</ol> </li>#%\end{enumerate}% | 892 #</ol> </li>#%\end{enumerate}% |
| 895 | |
| 896 A few hints that may be helpful: | 893 A few hints that may be helpful: |
| 897 %\begin{enumerate}%#<ol># | 894 %\begin{enumerate}%#<ol># |
| 898 %\item%#<li># One easy way of defining variable assignments and typings is to define both as instances of a polymorphic map type. The map type at parameter [T] can be defined to be the type of arbitrary functions from variables to [T]. A helpful function for implementing insertion into such a functional map is [eq_nat_dec], which you can make available with [Require Import Arith.]. [eq_nat_dec] has a dependent type that tells you that it makes accurate decisions on whether two natural numbers are equal, but you can use it as if it returned a boolean, e.g., [if eq_nat_dec n m then E1 else E2].#</li># | 895 %\item%#<li># One easy way of defining variable assignments and typings is to define both as instances of a polymorphic map type. The map type at parameter [T] can be defined to be the type of arbitrary functions from variables to [T]. A helpful function for implementing insertion into such a functional map is [eq_nat_dec], which you can make available with [Require Import Arith.]. [eq_nat_dec] has a dependent type that tells you that it makes accurate decisions on whether two natural numbers are equal, but you can use it as if it returned a boolean, e.g., [if eq_nat_dec n m then E1 else E2].#</li># |
| 899 %\item%#<li># If you follow the last hint, you may find yourself writing a proof that involves an expression with [eq_nat_dec] that you would like to simplify. Running [destruct] on the particular call to [eq_nat_dec] should do the trick. You can automate this advice with a piece of Ltac: [[ | 896 %\item%#<li># If you follow the last hint, you may find yourself writing a proof that involves an expression with [eq_nat_dec] that you would like to simplify. Running [destruct] on the particular call to [eq_nat_dec] should do the trick. You can automate this advice with a piece of Ltac: [[ |
| 900 | 897 |