Julin S (Mar 16 2023 at 13:42): 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?
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.
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.
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?
Théo Winterhalter (Mar 16 2023 at 19:30):Ah indeed. Does destruct not use the elimination provided?
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.
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.
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.
Pierre-Marie Pédrot (Mar 17 2023 at 10:16):Internally some tactics also use the scheme, like rewrite and other equality-related tactics.
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
Pierre-Marie Pédrot (Mar 17 2023 at 11:26):rewrite uses eq_rect internally.
Pierre-Marie Pédrot (Mar 17 2023 at 11:26):(or whatever your equality is)
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 ... *)
not sure when it uses a predeclared scheme (just defining equal_rew_r doesn't work)
Last updated: Apr 19 2024 at 02:02 UTC