Stream: Coq users

Topic: Should (custom) induction principles be transparent?


view this post on Zulip Paolo Giarrusso (Jul 02 2022 at 22:02):

I just realized list_ind is transparent. And that seems crucial in some proofs — say I'm proving lemma bar by induction over a datatype foo that contains a list foo, and I call list_ind and then I recursively call bar; the termination checker would fail if list_ind were Qeded? Somehow (a) I had never realized this (b) Software Foundations doesn't seem to say (at least in https://softwarefoundations.cis.upenn.edu/lf-current/IndPrinciples.html) (c) I've often written Qeded principles and gotten away with it — and I suspect they're even faster to termination-check, since they never need to be inlined.

(I think https://github.com/Blaisorblade/dot-iris/blob/d1cc6b96d5acf342561e23522378c5deb89988c6/theories/Dot/syn/syn.v#L330-L345 is an example).

view this post on Zulip Li-yao (Jul 02 2022 at 22:26):

If you use fix directly (that includes Lemma ... with), you do need a lot of things to be transparent.

view this post on Zulip Paolo Giarrusso (Jul 03 2022 at 01:59):

do you know another way? on #coq the suggestion was a mutual induction on foo and list foo — but I guess that's basically inlining list_ind foo?

view this post on Zulip Paolo Giarrusso (Jul 03 2022 at 02:00):

and yes, dealing with a 5-way mutual inductive let me see quite a bit of fun other stuff, somehow I hadn't noticed list_ind :-)

view this post on Zulip Paolo Giarrusso (Jul 03 2022 at 02:00):

TIL

view this post on Zulip Li-yao (Jul 03 2022 at 08:57):

I was thinking of a mutual induction principle but that would still need a transparent list_ind.
Maybe induction on depth, even though it's its own can of worms?

view this post on Zulip Paolo Giarrusso (Jul 03 2022 at 11:04):

Transparent principles sounds much less painful than depth — in fact, you probably can't see the pain at all.
But luckily, this argument seems to only apply to type constructors


Last updated: Feb 04 2023 at 21:02 UTC