my stance on definitional equality is my stance on genders, either there should be no defeq at all, or anything you want can be defeq

@LunaDragofelis definitional equality, defeq for short, is a concept in type theory. basically, you have propositional equality that you have to supply a proof for, and definitional equality that follows from the rules of the system and any definitions that you make.

for example in Lean, if a is a natural number, "a + 0 = a" is a definitional equality but "0 + a = a" does not hold definitionally, only propositionally.

@LunaDragofelis the reason you would want definitional equality is that you can use it automatically. so if you prove something about all numbers smaller than `a + b`, and want to apply it to the numbers smaller than `a`, then you are immediately done by setting `b = 0`.

but the drawback is that it does not work if instead you want to apply it to the numbers smaller than `b` by setting `a = 0`


@LunaDragofelis so you have this tight coupling between definitions and all proofs you want to write about them. it would be much easier if you had no way of distinguishing `a + 0 = a` from `0 + a = a`, either by making neither definitional (and moreover having no defeq at all) or making both definitional (and moreover allowing anything to be defeq if you want it (and supply the appropriate proof)

· · Web · 0 · 0 · 2
Sign in to participate in the conversation

Mastodon is a server for a federated social network: everyone can run a server if they want to, including me. So this is a Mastodon server for me (Vierkantor) and my friends.