Mercurial > cpdt > repo
comparison src/Reflection.v @ 150:eee4fd311f64
Reflection exercise
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Wed, 29 Oct 2008 17:41:38 -0400 |
| parents | e70fbfc56c46 |
| children | e71904f61e69 |
comparison
equal
deleted
inserted
replaced
| 149:e70fbfc56c46 | 150:eee4fd311f64 |
|---|---|
| 645 %\item%#<li># Define an inductive type [exp] of expressions over rationals (which inhabit the Coq type [Q]). Include variables (represented as natural numbers), constants, addition, substraction, and multiplication.#</li># | 645 %\item%#<li># Define an inductive type [exp] of expressions over rationals (which inhabit the Coq type [Q]). Include variables (represented as natural numbers), constants, addition, substraction, and multiplication.#</li># |
| 646 %\item%#<li># Define a function [lookup] for reading an element out of a list of rationals, by its position in the list.#</li># | 646 %\item%#<li># Define a function [lookup] for reading an element out of a list of rationals, by its position in the list.#</li># |
| 647 %\item%#<li># Define a function [expDenote] that translates [exp]s, along with lists of rationals representing variable values, to [Q].#</li># | 647 %\item%#<li># Define a function [expDenote] that translates [exp]s, along with lists of rationals representing variable values, to [Q].#</li># |
| 648 %\item%#<li># Define a recursive function [eqsDenote] over [list (exp * Q)], characterizing when all of the equations are true.#</li># | 648 %\item%#<li># Define a recursive function [eqsDenote] over [list (exp * Q)], characterizing when all of the equations are true.#</li># |
| 649 %\item%#<li># Fix a representation [lhs] of flattened expressions. Where [len] is the number of variables, represent a flattened equation as [ilist Q len]. Each position of the list gives the coefficient of the corresponding variable.#</li># | 649 %\item%#<li># Fix a representation [lhs] of flattened expressions. Where [len] is the number of variables, represent a flattened equation as [ilist Q len]. Each position of the list gives the coefficient of the corresponding variable.#</li># |
| 650 %\item%#<li># Write a recursive function [linearize] that takes a constant [k] and an expression [e] and optionally returns a [lhs] equivalent to [k * e]. This function returns [None] when it discovers that the input expression is not linear. The parameter [len] of the [lhs] should be a parameter of [linearize], too. The functions [singleton], [everywhere], and [map2] from [DepList] will probably be helpful. It is also helpful to know that [Qplus] is the identifier for rational addition.#</li># | 650 %\item%#<li># Write a recursive function [linearize] that takes a constant [k] and an expression [e] and optionally returns a [lhs] equivalent to [k * e]. This function returns [None] when it discovers that the input expression is not linear. The parameter [len] of [lhs] should be a parameter of [linearize], too. The functions [singleton], [everywhere], and [map2] from [DepList] will probably be helpful. It is also helpful to know that [Qplus] is the identifier for rational addition.#</li># |
| 651 %\item%#<li># Write a recursive function [linearizeEqs : list (exp * Q) -> option (lhs * Q)]. This function linearizes all of the equations in the list in turn, building up the sum of the equations. It returns [None] if the linearization of any constituent equation fails.#</li># | 651 %\item%#<li># Write a recursive function [linearizeEqs : list (exp * Q) -> option (lhs * Q)]. This function linearizes all of the equations in the list in turn, building up the sum of the equations. It returns [None] if the linearization of any constituent equation fails.#</li># |
| 652 %\item%#<li># Define a denotation function for [lhs].#</li># | 652 %\item%#<li># Define a denotation function for [lhs].#</li># |
| 653 %\item%#<li># Prove that, when [exp] linearization succeeds on constant [k] and expression [e], the linearized version has the same meaning as [k * e].#</li># | 653 %\item%#<li># Prove that, when [exp] linearization succeeds on constant [k] and expression [e], the linearized version has the same meaning as [k * e].#</li># |
| 654 %\item%#<li># Prove that, when [linearizeEqs] succeeds on an equation list [eqs], then the final summed-up equation is true whenever the original equation list is true.#</li># | 654 %\item%#<li># Prove that, when [linearizeEqs] succeeds on an equation list [eqs], then the final summed-up equation is true whenever the original equation list is true.#</li># |
| 655 %\item%#<li># Write a tactic [findVarsHyps] to search through all equalities on rationals in the context, recursing through addition, subtraction, and multiplication to find the list of expressions that should be treated as variables. This list should be suitable as an argument to [expDenote] and [eqsDenote], associating a [Q] value to each natural number that stands for a variable.#</li># | 655 %\item%#<li># Write a tactic [findVarsHyps] to search through all equalities on rationals in the context, recursing through addition, subtraction, and multiplication to find the list of expressions that should be treated as variables. This list should be suitable as an argument to [expDenote] and [eqsDenote], associating a [Q] value to each natural number that stands for a variable.#</li># |