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 @ohad @totbwf @AndrasKovacs Right!
(You can do it via layers of encoding, but it gets awful really, really quickly.)
@JacquesC2 writes "You can do it via layers of encoding, but it gets awful really, really quickly."
I agree with the "but".
But I disagree with the "You can do it via layers".
Yes, you can in principle, if you take the object-language of your proof assistant as the meta-language, and then encode the object-language within it.
But what if I have already proved something, using the object-language of the proof assistant, and I want to draw a meta-theoretical conclusion?
This happens all the time. In e.g. TypeTopology we have about 260k lines of code (including comments and blank lines).
Do I need to translate this to the encoded language if I want to meta-reason about it? Of course this is a ludicrous requirement.
(Which we often do in papers. I can give explicit examples on demand.)
@MartinEscardo @ohad @totbwf @AndrasKovacs I agree, having both reflection and reification would be extremely useful. Not a la Lisp (or worse) but in a more principled way.
Conor Titania Mc Bride@JacquesC2 @MartinEscardo @ohad @totbwf @AndrasKovacs We are clearly banging our heads off an abstraction ceiling in a dimension wherein we are currently stuck. That provokes.
@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.
@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.
Zanzi @ Monoidal Cafe@ohad @JacquesC2 @totbwf @AndrasKovacs Implementing a well-typed by construction type theory with type variables inevitably involves a lot of green slime due to needing to do type-substitution in terms. This makes it impractical to build any serious compiler machinery on top of this.
So, personally, I'd like to work in a dependent type theory which has built-in support for equational solving of substitution theories to avoid dealing with this kind of green slime.
Reed Mullanix@ohad @JacquesC2 @AndrasKovacs Because those same grad students who are tired of doing the same bazillion-many cases are *even more* tired of doing those bazillion cases with the mechanical pedant watching