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: