This does mean that both reduction and equivalence need to have a bunch of compatibility rules, but in Coq "reduction" as in running a program is entirely separate from how it checks equivalence anyway, the former being either CBV or CBN and the latter being a mutually recursive process of reducing to WHNF then congruent equivalence checking then further WHNFing
I wrote them in substitution form instead of explicitly for each form for reduction in my rules and surprisingly it works for my proofs
It's just not very algorithmic if you're implementing it
I mean it's pretty much the same structure as the definition of substitution (which... I haven't written out in full either) so it's obvious enough that they're the same
iauto is basically the mathematician's "Trivial."
A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.