Are there scenarios where using `Variant`

instead of `Inductive`

have benefits?

The manual page says:

The Variant command is similar to the Inductive command, except that it disallows recursive definition of types (for instance, lists cannot be defined using Variant). No induction scheme is generated for this variant, unless the Nonrecursive Elimination Schemes flag is on.

So I suppose the only difference is that inductions schemes don't get generated.

In what kind of situations would that be helpful?

It has two points: (i) avoid generating the (useless) induction schemes: `my_inductive_{rect,ind,rec,sind}`

, thus avoiding namespace pollution (ii) check that you didn't accidentally made your declaration recursive. But I agree it's more a nice small feature than a killer feature.

It's also very handy when you want to define `my_inductive_rect`

yourself, so it's the one that's picked by *default* by the induction tactic.

I see the point of `Unset Elimination Scheme.`

for general inductive types where you'd want to use your own custom induction principle. But for (non-recursive) variants, is the `induction`

tactic really useful, rather than a simple `case`

/`destruct`

?

Ah indeed. Does `destruct`

not use the elimination provided?

`destruct x using X_rect`

uses the `X_rect`

elimination schemes but w/o the `using`

, I think `destruct`

is implemented as a pattern matching, possibly reverting the dependent hypotheses in the conclusion. Possibly also the implementation of `destruct`

has changed over the Coq revisions.

As far as I know indeed `destruct`

(and similar tactics like `case`

and `inversion`

) are all defined directly using pattern-matching, and only `induction`

uses the elimination scheme.

This. There is also the somewhat legacy `elim`

tactic, which is like case but using the elimination scheme.

Internally some tactics also use the scheme, like rewrite and other equality-related tactics.

... rewrite? I can understand the scheme for equality, but rewrite using my_inductive_rect (or friends) would be surprising

rewrite uses eq_rect internally.

(or whatever your equality is)

`rewrite`

auto declares a rewrite scheme using `match`

```
Variant equal {A} a : A -> Prop := eqrefl : equal a a.
Goal equal 1 0 -> 0 = 1.
intros H. rewrite H.
Show Proof.
(* (fun H : equal 1 0 => internal_equal_rew_r nat 1 0 (fun n : nat => 0 = n) ?Goal H) *)
Print internal_equal_rew_r.
(* ... match in equal ... *)
```

not sure when it uses a predeclared scheme (just defining `equal_rew_r`

doesn't work)

Last updated: Jun 15 2024 at 08:01 UTC