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 Qed
ed? 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).
If you use fix
directly (that includes Lemma ... with
), you do need a lot of things to be transparent.
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
?
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
:-)
TIL
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?
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: Oct 13 2024 at 01:02 UTC