Skip to main content
PRL Project



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

Tactics

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.

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

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

expon_unrollC
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:

lt_q_expand
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:

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

SAuto
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:

rat_to_intC
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.

int_to_ratC
Rewrites integer expressions to rational ones.

RAuto
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:

PosHD
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:

PosCD
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:

rnw_evalC
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.

real_apply_evalC
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:

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

rat_to_realC
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.

rat_to_real_witnessC
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