Stream: Coq users

Topic: Variant vs Inductive


view this post on Zulip Julin S (Mar 16 2023 at 13:42):

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?

view this post on Zulip Pierre Roux (Mar 16 2023 at 13:46):

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.

view this post on Zulip Théo Winterhalter (Mar 16 2023 at 14:32):

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.

view this post on Zulip Meven Lennon-Bertrand (Mar 16 2023 at 18:41):

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?

view this post on Zulip Théo Winterhalter (Mar 16 2023 at 19:30):

Ah indeed. Does destruct not use the elimination provided?

view this post on Zulip Dominique Larchey-Wendling (Mar 17 2023 at 08:15):

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.

view this post on Zulip Meven Lennon-Bertrand (Mar 17 2023 at 09:41):

As far as I know indeed destruct (and similar tactics like case and inversion) are all defined directly using pattern-matching, and only inductionuses the elimination scheme.

view this post on Zulip Pierre-Marie Pédrot (Mar 17 2023 at 10:14):

This. There is also the somewhat legacy elim tactic, which is like case but using the elimination scheme.

view this post on Zulip Pierre-Marie Pédrot (Mar 17 2023 at 10:16):

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

view this post on Zulip Paolo Giarrusso (Mar 17 2023 at 11:15):

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

view this post on Zulip Pierre-Marie Pédrot (Mar 17 2023 at 11:26):

rewrite uses eq_rect internally.

view this post on Zulip Pierre-Marie Pédrot (Mar 17 2023 at 11:26):

(or whatever your equality is)

view this post on Zulip Gaëtan Gilbert (Mar 17 2023 at 11:28):

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 ... *)

view this post on Zulip Gaëtan Gilbert (Mar 17 2023 at 11:29):

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