RFC: consistent (fine-grained?) equational lemmas

nomeata commented 6 months ago

In this issue I’d like to flesh out and describe our plans for how Lean should generate equational lemmas.

Status quo

The status quo is unsatisfactory in a few ways, at least according to my current understanding:

The logic for creating the equational lemmas (in Lean.Elab.Eqns.mkEqnTypes) is basically “split until it holds by rfl, and only near recursive calls”. This is somewhat hard to predict for users, and may (potentially, not sure) lead to different results depending on how the recursion is implemented.
Because it splits as little as possible, we may get equational lemmas that have “big” case expressions on the right. When they are used by the simplifier to reduce applications to constructors, the term will become large, only to be made smaller again because of the case-of-constructor. More fine-grained equational lemmas would simplify more efficiently.
The equational lemmas do not necessarily correspond to the cases of the functional induction theorem, violating the principle of least surprise.
Equational lemmas do not really exist for non-recursive functions (they are always just the unfolding lemma), but would sometimes be useful there as well. Especially now that we have “lazyily defined theorems” by way of reserved names,
Sometimes the equational lemmas are suitable for dsimp, sometimes they are not.
Right now, for structural recursion, first the equational lemmas are generated, and then the unfolding lemma, while for well-founded recursion, first the unfolding lemma is derived from fix_eq, and then the equational lemmas follow.

Proposal (variant A)

Splitting heuristics

We want uniform equational lemams, so the same heuristics is used for non-recursive, structurally recursive and well-founded recursive lemmas. In particular

We don’t use rfl to stop early.
We split matches even if there is no recursive call on the right hand side.

This should split more than before, which should imply that where previously an equational lemma was by rfl, it will still be by rfl, and where possible, we do use rfl in the proof to make them dsimp lemmas. (TODO: not quite true: there are some matches where splitting them introduces assumptions, and breaks the rfl-property. Should we not split those?)

This splitting does not necessarily yield consistency with the foo.induct lemma. This should be fine as long as the induction cases are more specialized than the equations, i.e. in each induction case there is one equational lemma that will apply.

Simp API

What does it mean to write simp [f]?

Ideally, the user can understand the semantics of simp [f] as if f was expanded to a list of “normal” theorems, and nothing else behaves differently.

This points to a design where simp [f] is equivalent to simp [f.eq_1, f.eq_2,…]. If the user wants to unfold f more aggressively, revealing the matches on the RHS, they can write simp [f.eq_def].

DSimp interaction

A wrinkle here is that simp also calls dsimp: How should dsimp behave?

Note that right now, simp [some_lemma] will use some_lemma also in dsimp if it happens to be by rfl. We can use the same rule her as well: simp [f] is simp [f.eq_1, f.eq_2,…] and will allow dsimp to use those f.eq_n that are by rfl.

We may want to special case the use of simp [f.eq_def]: Here the user is really asking to unfold f aggressively, so it seems reasonable to try do that in dsimp as much as possible. So even if f.eq_def isn’t a rfl-theorem (e.g. due to structural recursion), this should enable the use of “smart unfolding”, so that dsimp unfolds f whenever it can.

Variants

Also splitting `if-then-else`

The above is less bold about making the equational theorems fine-grained and consistent with the induction principle, by not splitting if-expressions.

One could go further and do that. This would bring equational theorems into one-to-one correspondance with the induction principle cases, but it has costs:

Right now simp [foo] will use local facts to discharge the side-conditoins of equational lemmas, without using [*]. By splitting if expressions, the shape of these side-conditions will not be restricted to those generated by the match compiler due to overlaps, but could be arbitrary conditions. We’d need a way to recognize them reliably (not using the shape) and discharge them.
It might break even more code if that code relies on foo.eq_<n> being more coarse-grained. In particular if a function has an if-expression on the rhs the equational theorms may be harder to apply.
What I am most worried about: Will the users expect that? And if they have foo x, how can they make progress, without manually writing cases_on (copy of condition in definition of foo)? Note that simp [foo.eq_def] will make progress, but will likely loop. Would we need a functional split tactic that looks for foo x and then splits x as needed?

Impact

Add :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.

Kha commented 6 months ago

And if they have foo x, how can they make progress

delta foo would still work I assume?

Or should we not split equational lemmas on if, so that one can always make simp [foo] make progress just by matching on inductive data types

I haven't though very hard about it yet but that sounds like the least surprising solution to me. induct behavior could also be adjusted by an attribute.

digama0 commented 6 months ago

Or should we not split equational lemmas on if, so that one can always make simp [foo] make progress just by matching on inductive data types

I haven't though very hard about it yet but that sounds like the least surprising solution to me. induct behavior could also be adjusted by an attribute.

I agree, I think only match should create equation lemma splits, not if. Splitting if means that arbitrary propositions end up as conditions in a conditional rewrite rule, and simp is sometimes too smart about this and will simplify those propositions in the wrong way, meaning that you can't just do unfold; split <;> simp anymore.

nomeata commented 6 months ago

Thanks for confirming my worries. I have now split the proposal into two, variant A would split the equational lemma only along match expressions that take parameters (or subterms thereof) apart, and variant B describes the bolder plan. It may make sense to do A and later think about B.

Next question: Should it split only tail-recursive match (like the induction principle) or any eligible match (like they do now). Example:

def drop (n : Nat) (xs : List α) : List α  :=
  if n = 0 then xs else
  match xs with
  | [] => []
  | _ :: xs => drop (n-1) xs

/--
info: drop.eq_2.{u_1} {α : Type u_1} (n : Nat) (head : α) (xs_2 : List α) :
  drop n (head :: xs_2) = if n = 0 then head :: xs_2 else drop (n - 1) xs_2
-/
#guard_msgs in
#check drop.eq_2

The existing equational theorems in a way lift the match outside the if. That’s probably convenient in many cases, and here prevents simp [drop] from looping, but it also means that the case n=0 has to be handled “twice”, or at least that a proof would not follow the structure of the function drop, but rather that of

def drop (n : Nat) (xs : List α) : List α  :=
  match xs with
  | [] =>        if n = 0 then xs else []
  | _ :: ys =>   if n = 0 then xs else drop (n-1) ys

in the sense that I have to split xs before I can make progress with simp [drop], and then the n = 0 case has to be handled twice.

nomeata commented 6 months ago

Another question: Which match expressions should be split?

Clearly those that match on the functions’s parameters, or on variables introduced by such matches. But judging from the existing code, it will also try to split matches that match on other, possibly complicated, expressions, which would lead to similarly conditional equations as splitting on if.

I think I have seen this in the wild recently, although I can't quite reproduce it now. I tried to make it split such a match in

import Lean

def foo (n : Nat) : Nat :=
  match n % 42 with
  | 0 => 0
  | m => 
    match n with
    | 0 => 0
    | n+1 => foo n
-- structural or wf, both lead to the same behavior in this case    
-- termination_by n    

open Lean Meta
def tst (declName : Name) : MetaM Unit := do
  IO.println (← getEqnsFor? declName)

#eval tst `foo
#check foo._eq_1

but that merely shows the match-duplication behavior discussed in the previous comment. (And, incidentially, getUnfoldEqnFor fails for this function).

nomeata commented 5 months ago

Just now on Zulip:

Possibly (depending how we treat @[simp]) this change would cause

@[simp, inline] protected def elim : Option α → β → (α → β) → β
  | some x, _, f => f x
  | none, y, _ => y

to add only the fine-grained equations to the default simp set (those that match on the constructor).

nomeata commented 5 months ago

After a discussion with Leo, in particular about the semantics of simp [f], I revised the RFC. Changes:

no separate f.deq_n lemmas. There is one set of equational lemmas, some of them may be rfl-theorems.
The equational lemmas are derived uniformly for non-recursive, structuraly recursive and wf recursive functions.
simp [f] is equivalent to simp [f.eq_1, f.eq_2…]. No smart unfolding, dsimp uses the equational theorems when they are by rfl.
simp [f.eq_def] unfolds f more aggressively. For dsimp, this is also recognized as “use the smart unfolding”.

nomeata commented 5 months ago

@leodemoura pointed me to https://github.com/david-christiansen/ssft24/blob/281c8c3d2c154bcc7f842972d691bfa60031b220/Imp/Expr/Eval.lean#L48 which is a non-recursive function that would likely benefit from fine grained equational lemmas, for example in the proof at https://github.com/david-christiansen/ssft24/blob/281c8c3d2c154bcc7f842972d691bfa60031b220/Imp.lean#L51

Using mathlib’s count_heartbeats command, and using #4154, it seems that

count_heartbeats in
theorem popCount_correctBig :
    ∃ σ, (run (Env.init x) popcount 8) = some σ ∧ σ "x" = pop_spec x := by
  simp [run, popcount, Expr.eval, Expr.BinOp.apply.eq_def, Env.set, Value, pop_spec, pop_spec.go]
  sorry -- bv_decide

(corresponding to the status quo) takes 3166 heartbeats, and

  simp [run, popcount, Expr.eval, Expr.BinOp.apply, Env.set, Value, pop_spec, pop_spec.go]

takes 3152 heartbeats.

I did include run

def foo1 := @Expr.BinOp.apply.eq_2
def foo2 := @Expr.BinOp.apply.eq_def

before so that the lemma generation does not play a role here.

It goes in the right direction but doesn’t look like a gamechanger just yet.

Incidentially, I had to update leansat for my PR. Changes at https://github.com/leanprover/leansat/compare/main...nomeata:leansat:ssft24. Noteworthy observations:

The developer seems to expect that rw [foo] uses .eq_def, i.e. can rewrite any application, not just one to constructors.
For the function mkFullAdderCarry just looking at mkFullAdderCarry.eq_1 causes a heartbeat timeout. This means we have to worry about large complicated fuction blowing up the lemma generation code. It is also an argument in favor of more careful splitting, e.g. don’t split matches that are nested, maybe not even nested under a let.
Some proofs broke in ways that I did not fully investigate.

nomeata commented 2 months ago

These three PRs implement the core of this proposal, and provide uniform equational theorems across all three kinds of functions (non-rec, wf, structural), so closing this as completed.

I did not change the logic of deciding how to split the equations; if we get more evidence that we need to change something here that’ll be a new RFC.

leanprover / lean4