7.6 Introductions
Introduction tactics address goals which are inductive constants. They are used when one guesses that the goal can be obtained with one of its constructors' type.7.6.1 Constructor num
This tactic applies to a goal such that the head of its conclusion is an inductive constant (say I). The argument num must be less or equal to the numbers of constructor(s) of I. Let ci be the i-th constructor of I, then Constructor i is equivalent to Intros; Apply ci.Error messages:
- Not an inductive product
- Not enough Constructors
Variants:
- Constructor This tries Constructor 1 then Constructor 2, ..., then Constructor n where n if the number of constructors of the head of the goal.
- Constructor num with bindings_list
Let ci be the i-th constructor of I, then Constructor i with bindings_list is equivalent to Intros; Apply ci with bindings_list.
Warning: the terms in the bindings_list are checked in the context where Constructor is executed and not in the context where Apply is executed (the introductions are not taken into account). - Split
Applies if I has only one constructor, typically in the case of conjunction AÙ B. It is equivalent to Constructor 1. - Exists bindings_list
Applies if I has only one constructor, for instance in the case of existential quantification $ x× P(x). It is equivalent to Intros; Constructor 1 with bindings_list. - Left, Right
Apply if I has two constructors, for instance in the case of disjunction AÚ B. They are respectively equivalent to Constructor 1 and Constructor 2. - Left bindings_list, Right bindings_list,
Split bindings_list
Are equivalent to the corresponding Constructor i with bindings_list.