Stream: Type theory
Roman Bars (Mar 12 2021 at 05:59):
Apparently there is an issue with the formalization of CDGAs (and I guess graded objects in general) because (n-1)+1 is not judgmentally equal to n.
We could go full extensional but then judgmental equality would no longer be decidable (actually it isn't decidable currently either as pointed out by Carneiro in his thesis but for different reasons).
But the specific case of (n-1)+1=n certainly can be checked decidably right? Could Lean allow for manual addition of things to judgmental equality? Would that make formalizers' lives simpler?
Mario Carneiro (Mar 12 2021 at 13:57):
Nope, this is all hardcoded in the kernel and external verifiers
Mario Carneiro (Mar 12 2021 at 14:01):
Personally, I would much prefer if lean admitted full equality reflection, making the type theory extensional. This would solve a lot of DTT hell issues, making it approximately equivalent to how ZFC and HOL formalizations go. However, I think lean would need to compensate with better support for kicking back undecidable defeq problems to the user, because it's likely that it will lose track of why some term typechecks and we will need a mechanism to remind it; currently this happens in obscure enough locations that it's okay that the UI around it is terrible but with equality reflection it would become much more common.
Mario Carneiro (Mar 12 2021 at 14:05):
The problem with manually adding rules to turn
simp besides the fact that everything gets slower, is that those added rules can cause normalization to loop and other bad things like lack of confluence. Maybe more interesting, it can cause true defeqs to fail to check, because they were normalized the wrong way to something that is not defeq in the strict sense anymore and there is no confluence to fix the situation
Jannis Limperg (Mar 12 2021 at 15:27):
The Agda people, specifically Jesper Cockx, have been working on rewrite rules as a mechanism for extending defeq for some time; might wanna look up their papers. It's interesting to me that Agda is moving towards more powerful and pervasive defeq while Lean/mathlib actively discourages it.
Roman Bars (Mar 12 2021 at 16:14):
@Jannis Limperg thank you the paper "The Taming of the Rew" seems to be roughly in the right direction
Jannis Limperg (Mar 12 2021 at 16:14):
Yeah I think that's the latest one.
Kevin Buzzard (Mar 12 2021 at 16:45):
We saw in category theory that there were
refl proofs which were taking a long time, and it was much easier just to do a couple of rewrites. I would say that in mathematics we do a lot of equational reasoning and things are unlikely to be defeq; this is not really a concept known to mathematicians anyway.
Roman Bars (Mar 22 2021 at 11:27):
Apparently this paper describes how to extend Coq's equality while keeping decidable type checking: https://link.springer.com/chapter/10.1007/978-3-642-15205-4_40
Last updated: May 08 2021 at 21:09 UTC