Paolo Giarrusso (Jul 02 2022 at 22:02): 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).
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.
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?
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 :-)
Paolo Giarrusso (Jul 03 2022 at 02:00):TIL
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?
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: Apr 19 2024 at 17:02 UTC