Extra defeq rules

Stream: general

[Chris Hughes]

I'm quoting a discussion from another topic because I think Gabriel raised an interesting point.
Gabriel Ebner said:

At the risk of completely derailing this discussion, it would also be cool to have eta for decidable instances. That is, make it so that example (a b : Decidable p) : a = b := rfl. We have quite a bit of ugly library design in mathlib to work around decidability diamonds (i.e., if you have a theorem about classical.decidable you can't use it prove something about a computable instance). See e.g. the noncomputable polynomials issue.

There are other examples of equalities that we would like to add to the kernel that are basically theorems and not true by definition or easily automatically provable. I made a list of a bunch of type class diamonds recently by searching Zulip for "diamond" and there are a few diamonds that arise because one piece of data in a type class is uniquely determined by the rest, e.g. sups are unique given a partial order, or inverses in a group are unique given the monoid structure. Adding custom rules like this would be cool. Also, making module Z _ and fintype _ a subsingleton definitionally would be cool. Another more ambitious but very useful set of rules to add would be things like eval_X, eval_C and the following eta rule for polynomials eval₂ (f.comp C) (f X) = f, which is kind of analogous to eta for products, making use of the UMP for polys. That way our current ext; simp method for proving mundane equalities of morphisms could be definitional.

In my opinion it's a fundamental design flaw of both Lean and Coq that we rely on a method (defeq) to prove things that doesn't let us add any user proved theorems and we end up having to change the definition of a group to add stuff in the middle of the hierarchy.

Will we ever be able to add stuff like that?

[Gabriel Ebner]

Also, making [...] fintype _ a subsingleton definitionally would be cool.

Do you remember some concrete examples where it would have helped, or that were ugly because of fintype-diamonds?

[Gabriel Ebner]

we rely on a method (defeq) to prove things that doesn't let us add any user proved theorems

For practical reasons we need some restrictions here, definitional equality needs to stay reasonably decidable. We also want a form of conservativity, adding definitions to the environment should also not make earlier definitions type-incorrect.

[Gabriel Ebner]

Another consideration for defeq reductions is that they should interact well with unification. If a and b unify, then whnf(a) and whnf(b) should also unify.

[Rob Lewis]

It's not exactly what you're proposing, but some keywords here are "extensional type theory" and "equality reflection." If every provable equality becomes definitional, type checking is undecidable. There are proof assistants built around this (https://arxiv.org/pdf/1802.06217.pdf, and I think PVS?) but they come with tradeoffs.

[Reid Barton]

I think fintype _ being definitionally subsingleton would let you derive a equality reflection rule.

[Reid Barton]

Using also the computation rule for quotients.

[Reid Barton]

For example if y z : X and h : y = z then fintype { x : X // x = z } is inhabited by both [[ [<z, rfl>] ]] and [[ [<y, h>] ]] and we should be able to extract the elements z and y from these respectively.

[Mario Carneiro]

I think this is all idle speculation, but I would take the tradeoffs associated with extensional type theory any day. It really just means we need a better mechanism for being able to provide defeq proofs when needed; currently we have the worst of both worlds because type checking is undecidable anyway, and there isn't anything we can do when the kernel fails to deduce a certain defeq

[Jannis Limperg]

Jesper Cockx and collaborators are working on rewrite rules in Agda and Coq. These allow you to turn propositional equalities into definitional equalities, subject to a confluence check to keep type checking decidable. (You can also disable the checker for more fun/breakage.) Latest paper: https://hal.archives-ouvertes.fr/hal-02901011

[Reid Barton]

In any case if we want to make fintype definitionally a subsingleton then we can just do that--the tradeoff is somewhere else.
At present, I think the best compromise within Lean as it exists today is:

1. Get rid of any classically irrelevant data such as decidable_eq or data-carrying fintype in the assumptions of the primary definitions, making them noncomputable
2. Add "realizers" that are secondary, computable versions of the definitions that take these computational assumptions, plus lemmas that say they are equal to the primary ones for any choice of the computational data.

One way to do 1+2 is to give the computable definition first, and then make the main definition invoke it with instances provided by classical/choice.

[Reid Barton]

There are at least 3 kinds of reasons we like having definitional equalities:

1. We want to prove a propositional equality A = B and we can prove it by rfl. This is the least important reason--we're just proving a proposition so the stakes are low (it doesn't matter how we do it), and we have a lot of other good tools for proving propositions (e.g. simp, congr).

2. We don't want to distinguish between two expressions f x and f y where x and y are something like decidability hypotheses (typically implicit arguments). This is sort of a special case of 1, but it is a bit different because we might not even realize that we are in a situation where both f x and f y are involved. Again we can get out of it using congr, but a simpler solution is to just not make definitions that depend on decidability hypotheses in the first place.
   A variant is that x and y are something like topological_space instances that are propositionally but not definitionally equal--then we can't simply not take the topological_space instance, but I'm also not clear on what the proposed rules for adding definitional equalities would look like.

3. We need the definitional equality for the conversion rule: a : P x so a : P y. In this case you're in a really bad spot if you don't have the definitional equality, since you need to use eq.rec and nobody wants to do that.

The motivation for opposite to be a structure with definitional eta in the other thread was to deal with 3 for the morphisms of the opposite category.