Extending judgmental equality by hand

Stream: Type theory

[Roman Bars]

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]

Nope, this is all hardcoded in the kernel and external verifiers

[Mario Carneiro]

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]

The problem with manually adding rules to turn rfl into 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]

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]

@Jannis Limperg thank you the paper "The Taming of the Rew" seems to be roughly in the right direction

[Jannis Limperg]

Yeah I think that's the latest one.

[Kevin Buzzard]

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]

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