Stream: Coq users

Topic: `Variant`

view this post on Zulip Quinn (Nov 09 2021 at 00:08):

I was reading ITrees and came across Variant, which I understand is an alternative to Inductive when you don't need the induction principle. What are some use cases for this?

view this post on Zulip Li-yao (Nov 09 2021 at 01:10):

You can't accidentally write a Fixpoint on a Variant, apart from that it's just a minimalistic preference.

view this post on Zulip Li-yao (Nov 09 2021 at 01:14):

It's the number 1 FAQ from people who read the itree source code, I almost regret the distraction it causes :)

view this post on Zulip Quinn (Nov 09 2021 at 02:14):

so without induction principle I can't write Fixpoint?

view this post on Zulip Li-yao (Nov 09 2021 at 02:56):

You can write an induction principle but it's boring because it just does destruct/match.

view this post on Zulip Guillaume Melquiond (Nov 09 2021 at 04:41):

There seems to be some misconceptions.

  1. Variant forbids recursive types, which makes it an extremely restrictive form of Inductive.
  2. By default (Unset Nonrecursive Elimination Schemes), Variant does not produce an induction principle, because induction principles on non-recursive types are pointless.
  3. The ability to write Fixpoint is completely unrelated to the existence of an induction principle. You can write the exact same Fixpoint functions, whether or not there is an induction principle for a given recursive type.
  4. By default (Set Elimination Schemes), Coq generates an induction principle for recursive types. In some cases, it is completely pointless. But since this principle has zero impact on Fixpoint, one can always use the latter to define the correct induction principle.

view this post on Zulip Gaëtan Gilbert (Nov 09 2021 at 08:09):

fixpoints are forbidden on variants since (as a side effect of forbidding fixpoints on records with eta)

Last updated: May 24 2024 at 21:01 UTC