Search code examples
coqcoq-tactic

What is the idiomatic way to get `auto` to perform case analysis?

Inductive Foo : nat -> Type :=
  | a : Foo 1.

(* ... *)

Goal forall m, Foo m -> m = 1.
Proof.
  auto.
Fail Qed.

Is there a straightforward approach to do this?

Solution

  • You can use Hint Extern together with a tactic script that executes the case analysis. For example, this one will use destruct if the argument is a variable, and use inversion_clear otherwise:

    Inductive Foo : nat -> Type :=
| a : Foo 1.

Hint Extern 1 => match goal with
                 | [ H : Foo ?m |- _ ]
                   => first [ is_var m; destruct H | inversion_clear H ]
                 end.

Goal forall m, Foo m -> m = 1.
Proof.
  auto.
Qed.