feat(meta/environment): the equations that lead to a given definition are now accessible in Lean code

[cipher1024]

Co-authored-by: Daniel Fabian daniel.fabian@integral-it.ch

[cipher1024]

Written together with @DanielFabian

[cipher1024]

e <- get_defn_spec n

gives us a pre-term parsed from the equations typed in by the user. Those are distinct from the equations proved by the equation compiler as their can be fewer equations when multiple cases can be described by the same equation

[gebner]

There are two issues here:

1. The expression that is stored is not the equations, but the pre-expression of the definition (even if this is not an equation). Nothing is stored for auxiliary definitions for matches. Storing pre-expressions in general might be useful, but then please rename the API to reflect this (i.e., rename everything to defn_spec and update the doc string).
2. If you want the equations before the equation compiler duplicates them, then you can store the elaborated equations here (or maybe in the equation compiler):

   lean/src/frontends/lean/elaborator.cpp

   Line 2683 in 572b494

   ensure_no_unassigned_metavars(new_e);

   (the new_e variable contains the elaborated equations)

[DanielFabian]

@gebner What we are after here are the equations you see in the pattern match. So if your pattern match contains 5 lines in the source code, we need a sorted list of 5 equations. And sorted, because at this point, the left hand sides are not yet disjoint. Rather, the equations need to be applied in order and the first match wins.

The whole point of this is so that we get a target for something we would like to automatically prove. E.g.:

def foo : nat -> nat :=
| 0 := 1
| n := 2

in this case, we want an easy way to get two goals, in order: foo 0 = 1, forall n, foo n = 2.

You'll notice, that the second theorem is false. But it becomes true, if you modify it slightly:
forall n, n != 0 -> foo n = 2.

The idea is that you get this ever-growing list of premises as you go through the pattern match cases where at every point, the universally quantified theorem is true, but only because you also know that any of the previous patterns were already handled and therefore are now known to be impossible.

If this is our goal, are the elaborated equations the ones we need?

[gebner]

If this is our goal, are the elaborated equations the ones we need?

Yes, I'd strongly suggest that.