ohadProve dozens of syntactic substitution lemmata in one fell swoop with an induction principle with only two cases? Check.
Compositionality needs three cases though. :(
There are grad students younger than this proof that are cursing and cussing because they need to deal with bazillion-many cases for every SIGPLAN submission.
Jacques Carette@ohad Now you need to teach this to proof assistants, i.e. they should internalize this.
@JacquesC2 I already taught the computational content of this proof to a dependently-typed compiler. This means I can already manipulate families of well-scoped, well-typed AST representations without metaprogramming the AST traversals for substitution and splicing.
Happy to help a proof assistant teacher of a proof assistant with a reasonable theory and meta-theory and a reasonable development team. I suspect I'm already doing it vacuously. I'd be even happier to discover I'm not doing it vacuously anymore.
@ohad Work on convincing @totbwf . That won't help with any current proof assistant, but... it'll likely help.
Then I'd say convince @AndrasKovacs .
@JacquesC2 @totbwf @AndrasKovacs The starting point must be different than 'why can't you do it with the existing ones?'. After twenty years the question is: why didn't **you** do it with the existing ones, or built ones that could do it?
@ohad @totbwf @AndrasKovacs Because I don't know how to build a proof assistant (beyond a toy one). Formalizing this in one is pointless. It's integrating it into its very functioning that is the only remaining, interesting part.
I build stuff akin to this. They worked. But I used the wrong method (meta-programming). Others are still using the wrong method.
This needs programming, not meta-programming.
@JacquesC2 @totbwf @AndrasKovacs sorry, but why do you *need* the proofs to integrate this into the implementation of a proof assistant? With very few exceptions, we don't prove these correct, and even if we do, it's not the canon implementation.
@ohad @totbwf @AndrasKovacs Discussion evolved and veered.
Proofs are only needed to convince oneself that implementing "free substitution machinery" isn't a pile of hacks. Piles of hacks have been done - we know this can work. You've shown there's a strong reason for that. Great.
Now there's no reason not to implement this as a feature.