Mercurial > cpdt > repo

comparison src/Subset.v @ 339:aaeba4cfd075

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Work around coqdoc bug
author Adam Chlipala <adam@chlipala.net>
date Mon, 10 Oct 2011 16:12:04 -0400
parents c7faf3551c5d
children e76aced46eb1
comparison
equal deleted inserted replaced
338:c7faf3551c5d 339:aaeba4cfd075
928 (** * Exercises *) 928 (** * Exercises *)
929 929
930 (** All of the notations defined in this chapter, plus some extras, are available for import from the module [MoreSpecif] of the book source. 930 (** All of the notations defined in this chapter, plus some extras, are available for import from the module [MoreSpecif] of the book source.
931 931
932 %\begin{enumerate}%#<ol># 932 %\begin{enumerate}%#<ol>#
933 %\item%#<li># Write a function of type [forall n m : nat, {n <= m} + {n > m}]. That is, this function decides whether one natural is less than another, and its dependent type guarantees that its results are accurate.#</li># 933 %\item%#<li># Write a function of type [forall n m : nat, {][n <= m} + {][n > m}]. That is, this function decides whether one natural is less than another, and its dependent type guarantees that its results are accurate.#</li>#
934 934
935 %\item%#<li># %\begin{enumerate}%#<ol># 935 %\item%#<li># %\begin{enumerate}%#<ol>#
936 %\item%#<li># Define [var], a type of propositional variables, as a synonym for [nat].#</li># 936 %\item%#<li># Define [var], a type of propositional variables, as a synonym for [nat].#</li>#
937 %\item%#<li># Define an inductive type [prop] of propositional logic formulas, consisting of variables, negation, and binary conjunction and disjunction.#</li># 937 %\item%#<li># Define an inductive type [prop] of propositional logic formulas, consisting of variables, negation, and binary conjunction and disjunction.#</li>#
938 %\item%#<li># Define a function [propDenote] from variable truth assignments and [prop]s to [Prop], based on the usual meanings of the connectives. Represent truth assignments as functions from [var] to [bool].#</li># 938 %\item%#<li># Define a function [propDenote] from variable truth assignments and [prop]s to [Prop], based on the usual meanings of the connectives. Represent truth assignments as functions from [var] to [bool].#</li>#
939 %\item%#<li># Define a function [bool_true_dec] that checks whether a boolean is true, with a maximally expressive dependent type. That is, the function should have type [forall b, {b = true} + {b = true -> False}]. #</li># 939 %\item%#<li># Define a function [bool_true_dec] that checks whether a boolean is true, with a maximally expressive dependent type. That is, the function should have type [forall b, {b = true} + {b = true -> False}]. #</li>#
940 %\item%#<li># Define a function [decide] that determines whether a particular [prop] is true under a particular truth assignment. That is, the function should have type [forall (truth : var -> bool) (p : prop), {propDenote truth p} + {~ propDenote truth p}]. This function is probably easiest to write in the usual tactical style, instead of programming with [refine]. The function [bool_true_dec] may come in handy as a hint.#</li># 940 %\item%#<li># Define a function [decide] that determines whether a particular [prop] is true under a particular truth assignment. That is, the function should have type [forall (truth : var -> bool) (p : prop), {propDenote truth p} + {~ propDenote truth p}]. This function is probably easiest to write in the usual tactical style, instead of programming with [refine]. The function [bool_true_dec] may come in handy as a hint.#</li>#
941 %\item%#<li># Define a function [negate] that returns a simplified version of the negation of a [prop]. That is, the function should have type [forall p : prop, {p' : prop | forall truth, propDenote truth p <-> ~ propDenote truth p'}]. To simplify a variable, just negate it. Simplify a negation by returning its argument. Simplify conjunctions and disjunctions using De Morgan's laws, negating the arguments recursively and switching the kind of connective. Your [decide] function may be useful in some of the proof obligations, even if you do not use it in the computational part of [negate]'s definition. Lemmas like [decide] allow us to compensate for the lack of a general Law of the Excluded Middle in CIC.#</li># 941 %\item%#<li># Define a function [negate] that returns a simplified version of the negation of a [prop]. That is, the function should have type [forall p : prop, {p' : prop | forall truth, propDenote truth p <-> ~ propDenote truth p'}]. To simplify a variable, just negate it. Simplify a negation by returning its argument. Simplify conjunctions and disjunctions using De Morgan's laws, negating the arguments recursively and switching the kind of connective. Your [decide] function may be useful in some of the proof obligations, even if you do not use it in the computational part of [negate]'s definition. Lemmas like [decide] allow us to compensate for the lack of a general Law of the Excluded Middle in CIC.#</li>#
942 #</ol>#%\end{enumerate}% #</li># 942 #</ol>#%\end{enumerate}% #</li>#
943 943
944 %\item%#<li># Implement the DPLL satisfiability decision procedure for boolean formulas in conjunctive normal form, with a dependent type that guarantees its correctness. An example of a reasonable type for this function would be [forall f : formula, {truth : tvals | formulaTrue truth f} + {forall truth, ~ formulaTrue truth f}]. Implement at least %``%#"#the basic backtracking algorithm#"#%''% as defined here: 944 %\item%#<li># Implement the DPLL satisfiability decision procedure for boolean formulas in conjunctive normal form, with a dependent type that guarantees its correctness. An example of a reasonable type for this function would be [forall f : formula, {truth : tvals | formulaTrue truth f} + {][forall truth, ~ formulaTrue truth f}]. Implement at least %``%#"#the basic backtracking algorithm#"#%''% as defined here:
945 %\begin{center}\url{http://en.wikipedia.org/wiki/DPLL_algorithm}\end{center}% 945 %\begin{center}\url{http://en.wikipedia.org/wiki/DPLL_algorithm}\end{center}%
946 #<blockquote><a href="http://en.wikipedia.org/wiki/DPLL_algorithm">http://en.wikipedia.org/wiki/DPLL_algorithm</a></blockquote># 946 #<blockquote><a href="http://en.wikipedia.org/wiki/DPLL_algorithm">http://en.wikipedia.org/wiki/DPLL_algorithm</a></blockquote>#
947 It might also be instructive to implement the unit propagation and pure literal elimination optimizations described there or some other optimizations that have been used in modern SAT solvers.#</li># 947 It might also be instructive to implement the unit propagation and pure literal elimination optimizations described there or some other optimizations that have been used in modern SAT solvers.#</li>#
948 948
949 #</ol>#%\end{enumerate}% *) 949 #</ol>#%\end{enumerate}% *)