Hi Russell, At some point in time I thought about making a hint database for inequalities. As it turned out, it would not be very helpful since most of the lemmas you can use require instantiating lots of other variables. As such, we thought it might be more interesting to make some kind of automated tactic, but we never got around to implementing it...
The idea would be: reduce (a < b) to 0 < (b-a), simplify the righthandside using Rational, then somehow get that down to 0 < 1. It is not so trivial as it sounds, though :) Simply adding those lemmas to algebra does not sound (to me) like a good idea... Luís On Tue, Sep 23, 2008 at 8:21 PM, <[EMAIL PROTECTED]> wrote: > I'd like to add pos_one and less_leEq (and probably more) to some hintDb. > Should I add it to algebra, or is some other database more appropriate? > > -- > Russell O'Connor <http://r6.ca/> > ``All talk about `theft,''' the general counsel of the American Graphophone > Company wrote, ``is the merest claptrap, for there exists no property in > ideas musical, literary or artistic, except as defined by statute.'' > _______________________________________________ > C-CoRN mailing list > [email protected] > http://mailman.science.ru.nl/mailman/listinfo/c-corn > _______________________________________________ C-CoRN mailing list [email protected] http://mailman.science.ru.nl/mailman/listinfo/c-corn
