comparison src/Reflection.v @ 149:e70fbfc56c46

Reflection exercise
author Adam Chlipala <adamc@hcoop.net>
date Wed, 29 Oct 2008 14:39:00 -0400
parents 0952c4ba209b
children eee4fd311f64
comparison
equal deleted inserted replaced
148:0952c4ba209b 149:e70fbfc56c46
618 and_ind (fun (_ : True) (H11 : False) => False_ind False H11) 618 and_ind (fun (_ : True) (H11 : False) => False_ind False H11)
619 H9) H7) H5) H3) H1) H 619 H9) H7) H5) H3) H1) H
620 : True /\ True /\ True /\ True /\ True /\ True /\ False -> False 620 : True /\ True /\ True /\ True /\ True /\ True /\ False -> False
621 ]] *) 621 ]] *)
622 622
623
624 (** * Exercises *)
625
626 (** %\begin{enumerate}%#<ol>#
627
628 %\item%#<li># Implement a reflective procedure for normalizing systems of linear equations over rational numbers. In particular, the tactic should identify all hypotheses that are linear equations over rationals where the equation righthand sides are constants. It should normalize each hypothesis to have a lefthand side that is a sum of products of constants and variables, with no variable appearing multiple times. Then, your tactic should add together all of these equations to form a single new equation, possibly clearing the original equations. Some coefficients may cancel in the addition, reducing the number of variables that appear.
629
630 To work with rational numbers, import module [QArith] and use [Open Local Scope Q_scope]. All of the usual arithmetic operator notations will then work with rationals, and there are shorthands for constants 0 and 1. Other rationals must be written as [num # den] for numerator [num] and denominator [den]. Use the infix operator [==] in place of [=], to deal with different ways of expressing the same number as a fraction. For instance, a theorem and proof like this one should work with your tactic:
631
632 [[
633 Theorem t2 : forall x y z, (2 # 1) * (x - (3 # 2) * y) == 15 # 1
634 -> z + (8 # 1) * x == 20 # 1
635 -> (-6 # 2) * y + (10 # 1) * x + z == 35 # 1.
636 [[
637
638 intros; reflectContext; assumption.
639 [[
640 Qed.
641
642 Your solution can work in any way that involves reflecting syntax and doing most calculation with a Gallina function. These hints outline a particular possible solution. Throughout, the [ring] tactic will be helpful for proving many simple facts about rationals, and tactics like [rewrite] are correctly overloaded to work with rational equality [==].
643
644 %\begin{enumerate}%#<ol>#
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>#
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>#
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>#
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>#
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>#
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>#
656 %\item%#<li># Write a tactic [reflect] to reflect a [Q] expression into [exp], with respect to a given list of variable values.#</li>#
657 %\item%#<li># Write a tactic [reflectEqs] to reflect a formula that begins with a sequence of implications from linear equalities whose lefthand sides are expressed with [expDenote]. This tactic should build a [list (exp * Q)] representing the equations. Remember to give an explicit type annotation when returning a nil list, as in [constr:(@nil (exp * Q))].#</li>#
658 %\item%#<li># Now this final tactic should do the job:
659 [[
660 Ltac reflectContext :=
661 let ls := findVarsHyps in
662 repeat match goal with
663 | [ H : ?e == ?num # ?den |- _ ] =>
664 let r := reflect ls e in
665 change (expDenote ls r == num # den) in H;
666 generalize H
667 end;
668 match goal with
669 | [ |- ?g ] => let re := reflectEqs g in
670 intros;
671 let H := fresh "H" in
672 assert (H : eqsDenote ls re); [ simpl in *; tauto
673 | repeat match goal with
674 | [ H : expDenote _ _ == _ |- _ ] => clear H
675 end;
676 generalize (linearizeEqsCorrect ls re H); clear H; simpl;
677 match goal with
678 | [ |- ?X == ?Y -> _ ] =>
679 ring_simplify X Y; intro
680 end ]
681 end.
682
683 #</ol>#%\end{enumerate}%
684 #</li>#
685
686 #</ol>#%\end{enumerate}% *)