Details

First a few definitions.

• An arithmetic type  is either the type ( int) or one of the standard subtypes of defined in the int_1 theory. Specifically: ( nat), ( nat_plus), ( int_nzero), i...} ( int_upper), i...j } ( int_seg), or i...j} ( int_iseg).

• An arithmetic literal  is one of
  • the relations a = b T and a b T where T is an arithmetic type,
  • the relation a = b T where T is an arithmetic type,
  • Any of the inequalities < , > , , or ,
  • Either of the above inside one or more negations ( ).

SupInf recognizes the arithmetic literals that occur in a sequent either at the top level of a clause or buried under

mwedge and mvee connectives.

There are two variants on the SupInf tactic: SupInf and SupInf'  . Only SupInf' tries inferring additional arithmetic information about the non-linear terms in arithmetic expressions.

The information on a non-linear term is gathered in two ways:

1. The standard type-inference function get_type   is run on the term, and if it returns one of the standard arithmetic subtypes of Z , then the predicate information from the subtype is used.
2. Arithmetic property lemmas are examined.

where C is constructed from 's, 's and arithmetic literals. match handles  are selected from C. A match handle is a non-linear arithmetic term that occurs as an argument to an arithmetic literal in C such that all the free variables contained in C and the are also contained in the non-linear term. An arithmetic lemma  is considered as providing information about each of its match handles.

Currently, an arithmetic property lemma  is only used if after matching the match handle in C with the non-linear term that information is desired on, all the instantiated are equal to hypotheses of the sequent. This is perhaps an overly strict condition.

Arithmetic property lemmas are identified by invoking the ML function

SupInf' is currently under development and should be used with caution. Hopefully all changes to it will only be enhancements, so if it is successful now, it will be successful in the future. One problem with it is that the process of type-checking subgoals created by instantiating arithmetic property lemmas can cause the creation of subgoals that require arithmetic reasoning to solve. When SupInf' is used as part of a type-checking tactic (as it is in Auto'), there are sometimes cases when SupInf' unendingly gets invoked on subgoals derived from ones that it itself created. Further work is needed on SupInf' to avoid this happening.

SupInf identifies counter-examples if it fails. These can be viewed by looking at value of the ML variable supinf_info. The value gives a list of bindings of variables in the goal for the counter-example. There are two kinds of counter-examples; integer and rational. If SupInf finds an integer counterexample, then you know that the goal is definitely unprovable. If a rational counter-example, then SupInf is unsure whether the goal is true or not. These latter cases should be rare in practice.

A couple of examples of uses of the SupInf tactic are as follows. It is able to prove the goal

but on

finds the counterexample x = 1 and y= 2. Examples of arithmetic property lemmas are:

where rem is the remainder function and:

where nth_tl(n;as) takes the nth tail of list as, | is the list length function and |as|. is an abbreviation for the integer segment {0...|as|-1}. The latter lemma is invoked when SupInf proves the goal: