Skip to main content
PRL Project

next up previous
Next: Tactic Code Up: Formalizing Constructive Real Analysis Previous: The Intermediate Value


The following is a listing of the user defined tactics in the rational and real libraries together with illustrations of their use. Some do a fair amount of computation or rewriting while others are basically macros for various sequences of tactics that show up repeatedly in the libraries. ``Direct computation'' tactics perform only term reduction and unfolding and folding of definitions.

This tactic decomposes an ifthenelse term and rewrites the Boolean condition to a proposition. From qabsval_le_q:

This is a direct computation tactic that reduces a/b.num to a and a/b.den to b. From eq_q_refl:

This unrolls the definition of expon using direct computation.

The effect is to replace a^n with if n =z 1 then a else (a * a^(n - 1)). From expon_preserves_pos:

Converts a < b to a.num * b.den < b.num * a.den. le_q_expand and eq_q_expand are similar. From lt_q_qmax:

This tactic rewrites absolute values of rational arithmetic expressions to expressions with absolute values in the numerators. From rat_triangle:

This is a version of the autotactic that tries calling AbSetMemEqTypeCD. It is useful for handling membership goals of the form a = b T where T is a set type. From real_pos_inc:

Rewrites expressions of rational integers (rationals of the form a/1) to integer expressions. In the example, from canon_bound_property, the conclusion is an equality between rationals.

Rewrites integer expressions to rational ones.

Like SAuto except that if it gets stuck on a membership goal it will try to unfold the type subterm. It is useful for goals like a = b where the type needs unfolding. From rat_nzero_to_real_nzero:

Decomposes a hypothesis of the form a > 0 and obtains a witness, although it sometimes must be used with the tactic Unhide. From real_pos_lemma:

This takes a term as an argument to be used as a witness for a goal of the form a > 0. From rneg_functionality_wrt_lt_r:

This tactic is similar to qnd_evalC except that it takes pairs which are nonzero reals. In this example from pos_quasi_decidable the term in the conclusion is actually a display for rnum( ), which becomes rnum(< 1,n>) after (D 2) is applied.

This direct computation tactic takes a real expression applied to a natural number, and ``distributes'' the application inside the expression according to the definitions of the operations involved. The operations it knows about are radd, rneg, rsub, real_rat, rmul_gen, rmax and rabsval. From radd_preserves_pos:

Rewrites expressions of reals which are constant sequences to rational expressions.

Rewrites rational expressions to real expressions, but does not recognize qinv or qdiv. The reason for this is that rinv and rdiv must be given nonzero reals, requiring witnesses. In this example from halving_to_zero the conclusion is a rational expression. It gets converted to a real expression and then is decomposed so that it matches hypothesis 7.

Same as rat_to_realC except that it handles qinv and qdiv. It takes a natural number to be used as a witness for all instances of rinv and rdiv. This tactic does not get used in the library so we have a cooked up example:

next up previous
Next: Tactic Code Up: Formalizing Constructive Real Analysis Previous: The Intermediate Value