Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Just a note: you can convert raw url text to a link, like this: <https://example.com>
, giving https://example.com, as long as the Markdown+Itex option is chosen.
Theorem 44:
Proof. May be next time.
? :-)
Formalized the proof using Coq
https://www.mediafire.com/file/kxhk8yo50yq6amo/99.v/file
No one understands it yet. Even great Andrej Bauer (the founder of 21st century mathematics) can’t understand.
great Andrej Bauer (the founder of 21st century mathematics)
I think that is going too far… :-)
Summary of the first 200 lines
Definitions of lambda-terms and de Bruijn terms;
Standard definition of the ’transfer’ function
transfer (Gamma, M)
this function takes a list of variables (context) Gamma, a lambda-term M and produces a de Bruijn term;
Definitions of simultaneous substitution
M [N0/x0,…,Nk/xk]
and similar de Bruijn substitution
M’ [N’0,…,N’k]
(the last definition may be my own, but not very strange) ;
Statement of the main theorem
forall context Gamma, lambda-term M and substitution [N0/x0,…,Nk/xk]
if the list x0,…,xk does not contain repetitions then
transfer (Gamma, M [N0/x0,…,Nk/xk]) = M’[N’0,…,N’k]
where
M’ = transfer ([x0,…,xk]++Gamma, M)
N’0 = transfer (Gamma, N0)
…
N’k = transfer (Gamma, Nk)
I have looked at the link in the first post above, and I can see why the arXiv might have suggested it be rewritten. As it stands, it’s not an academic article, more like a personal record of a proof. I can only say I am not an expert in any of this, so I can’t give any substantial feedback. But write a proper introduction, include a bit of a literature review, describe the Coq proof at a high level with snippets of the interesting or tricky parts, and any readers might be more inclined to look at it. Also, put the Coq proof in a GitHub repo and also put the pdf of the human-readable article in there too. Leaving the .v file in a file-sharing website is not standard practice.
1 to 9 of 9