constructor

When faced with a goal consisting of an inductive proposition with multiple constructors (such as le or NoDup), the constructor tactic iteratively attempts to apply each inductive constructor until one makes progress.

This tactic can succeed in multiple ways. Consider the following scenario:

Inductive example : nat -> Prop :=
| EOdd (n : nat) :
    even n = false ->
    example n
| EEven (n : nat) :
    even n = true ->
    example n.

Goal forall n, even n = true -> example n.
Proof.
    intros.
    constructor;
    (* This will print out:
        even n = false
        even n = true
       as `constructor` first tries to prove
       the goal via EOdd, `assumption` fails,
       and then we backtrack and try EEven *)
    match goal with 
    | [|- ?G] => idtac G; assumption
    end.

Binding values to specific names is supported, as with apply.

Furthermore, a specific constructor’s index can be supplied to specifically apply that one.

Syntax

(* Simple usage *)
constructor.

(* Bind to variables in the applied constructor *)
constructor with (n := S x) (m := 5).

(* Apply the 5th constructor in the type's constructor list *)
constructor 5.

Examples

Before

n: nat
=========================
n = 0 \/ 1 <= n

constructor.

After (or_introl applied)

n: nat
=========================
n = 0

Resources

Reference Documentation

---