Specifying a Rule

In the context of a particular goal a rule is specified by giving a name and, possibly, certain parameters. As there are a large number of rules it would be unfortunate to have to remember a unique name for each one. Instead, there are small number of generic names, and the proof  editor infers the specific rule desired from the form of the goal. In fact, for the rules dealing with specific types or objects of specific types, there are only the names intro, elim and reduce. The intro  rules are those which break down the conclusion of the goal, and the elim  rules are those which use a hypothesis. Accordingly, the first parameter of any elim rule is the declared variable or number of the hypothesis to be used. The reduce  rules are the computation rules. The first parameter of a reduce rule is a number that specifies which term of the equality is to be reduced. Among the parameters  of some rules are keyword parameters which have the following form:

• new 
  This parameter is used to give new  names for hypotheses in the subgoals. In most cases the defaults, which are derived from subterms of the conclusion of the goal, suffice. For technical reasons the same variable can be declared at most once in a hypothesis list, so if a default name is already declared a new name will have to be given. Whenever this parameter is used it must be the case that the names given are all distinct and do not occur in the hypothesis list of the goal.
• using T , over  
  These parameters are used when judging the equality of noncanonical  forms in types dependent on the principal argument of the noncanonical form. The using parameter specifies the type of the principal argument of the noncanonical form. The value should be a canonical type which is appropriate for the particular noncanonical form. The over  parameter specifies the dependence of the type over which the equality is being judged on the principal argument of the form. Each occurrence of z in T indicates such a dependency. The proof editor always checks that the term obtained by substituting the principal argument for z in T is --convertible  to the type of the equality judgement.
• at
  The value of this parameter is the universe level at which any type judgements in the subgoals are to be made. The default is .