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.
Martin Escardo@ohad @JacquesC2 @totbwf @AndrasKovacs
This discussion is going on several tangents, but if you read any serious mathematical paper, you will see that there is both object-level and meta-level discussion.
At the moment proof assistants are good at object-level discussions, and, although they do support meta-level programming (in a crappy way in my view), they don't support meta-level reasoning (at all).
@MartinEscardo @JacquesC2 @totbwf @AndrasKovacs another tangent: I'm finding 'meta' confusing in these settings, so decided to adopt the antonym 'mesa'. You fix the language, and then it's 'mesa^n-languages' all the way down.