Unfold and non-refl equational lemmas.

[leodemoura]

The unfold tactic is implemented using the automatically generated equational lemmas.
unfold is currently just an alternative name for dunfold.
So, it doesn't work, for example, for functions defined using well founded recursion.

open nat well_founded

def gcd : ℕ → ℕ → ℕ | y := λ x,
if h : y = 0 then
    x
else
    have x % y < y, by { apply mod_lt, cases y, contradiction, apply succ_pos },
    gcd (x % y) y

lemma gcd_zero_right (x : nat) : gcd 0 x = x := 
by unfold gcd; simp

We need an unfold tactic that uses non-refl equational lemmas.

There is a problem. The current dunfold f is "multi-pass". In the following example unfold f will reduce f (succ (succ a)) into f (succ a) + 2 and then it will unfold again the new f (succ a).

open nat

def f : nat → nat
| 0        := 1
| (succ a) := f a + 2

example (a : nat) : f (succ (succ a)) = f a + 2 + 2 :=
by unfold f; refl

We cannot do this for functions such as gcd since it will produce non-termination.
I'm assuming it would be confusing to have a different behavior for non-refl lemmas.
One option is to rename the current unfold/dunfold to reduce, and add a new unfold tactic which performs a single pass. That is, in the example above, unfold f would produce the goal

f (succ a) + 2 = f a + 2 + 2

[digama0]

Is it possible to make the syntax unfold* f acceptable? Obviously the meaning is to unfold repeatedly. Otherwise, unfold f g h will unfold each identifier at most once.

[leodemoura]

Is it possible to make the syntax unfold* f acceptable? Obviously the meaning is to unfold repeatedly.

I suggested reduce f for reducing the goal while unfolding f.
Note that, at #1646, @JasonGross uses unfold denote_let_inM to reduce the goal while unfolding denote_let_inM.
Another motivation is that reduce f will not allow us to specify which occurrences (first, second, etc). are unfolded while unfold f will. This is somewhat broken in the current implementation. unfold with and without occurrences are two different tactics with very different behavior.

[digama0]

I've mentioned before that I am baffled by the number of definitional reduction tactics that currently exist, so I am reticent to have yet another one with a somewhat different name. Perhaps we should have an issue on restructuring them and/or providing clear documentation on the purpose and use cases for each tactic.

[Kha]

Is the semantic and performance difference of repeat { unfold f } impractical? I would certainly prefer that over a new tactic.

[leodemoura]

Is the semantic and performance difference of repeat { unfold f } impractical? I would certainly prefer that over a new tactic.

@Kha We already have performance problem with unfold f. See issue #1646.
repeat {unfold f} would make it even slower.
Moreover, unfold and reduce are two different operations with different options.

[gebner]

I agree with @digama0, there are too many non-discoverable different reduction tactics. My vote would go for unfold1 and unfold--then at least auto-completion would help you.

[leodemoura]

@gebner We need an efficient reduce tactic. This is unavoidable. Eventually, we will need to implement an efficient reduce f based on an efficient reduction engine (e.g., Krivine machine with support for open terms). We can try to merge dsimp and reduce, but this is also hard. dsimp needs to be extensible. reduce should be fast. Note that, unfold was once implemented on top of dsimp, but it was too inefficient. That being said, it is feasible to implement the new unfold tactic (what you call unfold1) on top of the extensible dsimp.

[gebner]

@leodemoura I'm just arguing about naming. I agree, the actual implementation should be different.

[digama0]

My concern is also not about performance, but about semantics and user-discoverability. Under the hood, you can implement each combination of options whatever way you think will make it fastest, but the porcelain commands should have a memorable and consistent notation. The fact that unfold f g h does not take brackets and dsimp [f, g, h] does always gets me.

Performance aside, how many tactics do you need to get all of the current semantics? I really don't understand how dsimp is different from unfold, so I will leave that aside for now. Then I see only one two:

• unfold1 f
• delta f

using gebner's notation so it is clear which I am referring to. In terms of this,

• unfold1 f g h = unfold1 f, unfold1 g, unfold1 h
• unfold f g h = repeat { unfold1 f <|> unfold1 g <|> unfold1 h }
• dsimp [f, g, h] =?= unfold f g h

delta is separate since it does not use equational lemmas and instead directly unfolds an identifier to its internals.

If the behavior of these commands matches what I have written here, then I think that we could get away with just one tactic unfold' = unfold1 with a * option to make it act like unfold as I mentioned at the start.

I assume the reason dsimp uses brackets is because it accepts terms instead of just identifiers. What is the purpose of these terms? If it is simply inlining additional equational lemmas, then I don't see why we can't have unfold also take them and thus uniformize the notation.

(Again, I am talking only about the behavior of these tactics, not performance. If the underlying unfold1 f tactic does not accept custom equations, then it can call dsimp instead if it is passed a non-constant.)

[leodemoura]

@digama0 There are other dimensions (e.g., definitional vs propositional equality).
The current unfold only supports refl equational lemmas. As I described above, unfold gcd does not work since its equational lemma is not a refl-lemma.
When using propostional equality, we have different strategies for rewriting an expression and how to handle the at modifier. We have different possibilities, and there is no clear winner (i.e., best approach). There is also the issue whether the tactic supports occurrences (1st, 2nd, etc) or not.

Under the hood, you can implement each combination of options whatever way you think will make it fastest

It is not always clear what is the most efficient.
I think it is also important to distinguish different operations that have different behavior.
Reduction and unfolding are two different operations.

If the behavior of these commands matches what I have written here

You ignored many cases: occurrences, at modifier, definitional vs propositional.
For example: dsimp [f, g, h] =?= unfold f g h is not true.
I want to be able to say unfold gcd, but dsimp [gcd] should produce an error (it doesn't in the current version, it just doesn't do anything).

What is the purpose of these terms?

The motivation is to allow users to fix parameters of a refl-lemma.

[digama0]

There are other dimensions (e.g., definitional vs propositional equality).

Very true. We can uniformize the initial d so that dtac means "a restricted version of tac that only performs simplification/reduction/unfolding when the rewriting is a definitional equality", which applies at least to simp/dsimp and unfold/dunfold. Again, the key here is that the addition is uniform and communicated to the user. Of course this also implies that the format for input to dtac is the same as tac.

There is also the issue whether the tactic supports occurrences (1st, 2nd, etc) or not.

AFAIK there is no support for occurrences anywhere in the tactic framework. We should implement support for them, but again, it should be done in a consistent and uniform way and deserves its own issue for nailing down the syntax.

I think it is also important to distinguish different operations that have different behavior.
Reduction and unfolding are two different operations.

I 100% agree on the first sentence, but I am confused by the second because my operational definition for these synonymizes the two. I think I know what reduction is (consistent replacement of expressions matching a certain form, hopefully associated with some kind of termination pathway), but this is what I get from the unfold tactic. For me "unfold" is a vaguer notion, but I suppose it does not have the same association to a termination pathway. Anyway that's just my interpretation of the words - what do you want them to mean in this context?

For example: dsimp [f, g, h] =?= unfold f g h is not true.
I want to be able to say unfold gcd, but dsimp [gcd] should produce an error (it doesn't in the current version, it just doesn't do anything).

I put the ? there because I know it's not true, but I don't know why. Following the initial d convention I mention above, it should do exactly what simp does, but without using non-definitional equalities; since gcd has no definitional equations associated with it, it does nothing (and I guess it should produce an error since it did not change the goal?).

How then do you feel about the equality dsimp [f, g, h] =?= dunfold f g h? Again I assume it's not true, but I don't know why.

[leodemoura]

AFAIK there is no support for occurrences anywhere in the tactic framework. We should implement support for them, but again, it should be done in a consistent and uniform way and deserves its own issue for nailing down the syntax.

https://github.com/leanprover/lean/blob/master/library/init/meta/occurrences.lean
https://github.com/leanprover/lean/blob/master/library/init/meta/rewrite_tactic.lean#L11-L12

I 100% agree on the first sentence, but I am confused by the second because my operational definition for these synonymizes the two.

For me, reduce f applies arbitrary reductions (beta/zeta etc), not only delta. The other reductions can be disabled (like in simp where we can disable zeta, projection reduction, etc). The goal is to build reduce on top of a reduction engine, and support different reduction strategies. For reduce, occurrences should not be supported since the order we visit nodes depends on the reduction strategy.
Finally, reduce only produces definitionally equal terms.

For me, unfold f should be a surgical operation, and it should support the occurrences parameter.
There is no reduction strategy, or support for other reduction rules, we should just search for f-applications, and reduce the appropriate ones. unfold may also produce provably equal terms. There are also issues such as dunfold f vs. unfold f when f only has refl-lemmas. The behavior may be different depending on how we implement unfold.

How then do you feel about the equality dsimp [f, g, h] =?= dunfold f g h? Again I assume it's not true, but I don't know why.

This is not true in the current implementation since dsimp applies several reductions other than delta.
For me, dsimp is a variant of reduce. In interactive mode, we should probably support only reduce.
The extensible dsimp (https://github.com/leanprover/lean/blob/master/library/init/meta/simp_tactic.lean#L77)
should be available for users that want to implement their own reduction tactics.

[digama0]

Finally, reduce only produces definitionally equal terms.

I don't know about this. If you are creating a general reduction engine, you will probably want to have special reduction rules which are not associated to the standard reduction pathway of DTT, and thus are not definitional equalities (for example, it would be great if reduce supported coinductive types after the appropriate reduction rules have been marked). The initial d convention can be used here to separate out those rules that hold definitionally, so that we also get a dreduce tactic.

This is not true in the current implementation since dsimp applies several reductions other than delta.
For me, dsimp is a variant of reduce. In interactive mode, we should probably support only reduce.
The extensible dsimp (https://github.com/leanprover/lean/blob/master/library/init/meta/simp_tactic.lean#L77)
should be available for users that want to implement their own reduction tactics.

Okay, now I think we are converging. If reduce is extended with additional reduction rules, then we get simp. Put another way, reduce is a special case of simp (and dreduce a special case of dsimp) which uses a restricted collection of simp rules which are marked as "reductions". So really all that is needed is a new @[reduce] annotation which goes on e.g. coinductive reduction rules (and also contains different admissibility criteria, i.e. perm rules are not allowed).

Regarding the choice of unfold vs dunfold to users, I would say always use the non-d version if possible, and the d version if you need to avoid the underlying eq.rec for some reason. If f contains only rfl-lemmas, then of course dunfold should work on it, and even if f contains some rfl-lemmas and some provable equalities it should reduce along any equations that it can.

[leodemoura]

@digama0 I'm not sure I like a reduce that is not definitional. First, the whole story about an efficient reduction engine would quickly disappear since we would need to produce proofs. There are a bunch of technical issues that had to be addressed when implementing simp. I don't want to do it again.
For me, the reduce that accepts non-refl lemmas and/or extra reduction rules is our simp.

Perhaps, you want a symbolic evaluator that can be extended, is efficient (and does not produce proofs).
This is useful for debugging and testing, but we would not be able to use it in proofs.

In interactive tactic mode, I agree we can survive with:

• unfold and dunfold, where unfold is the preferred one as you suggested (they support occurrences, definitions to unfold, and flag to specify whether equational lemmas or raw definitions are used for unfolding). The last flag allows us to get rid of delta. unfold is based on the simp primitives, and dunfold on the dsimp primitives. It performs a single pass (to make sure the occurrences parameter has a consistent behavior).
• reduce (definitions to unfold apply delta, flag to specify whether equational lemmas or raw definitions are used for unfolding, disable/enable other reduction rules).
• simp (definitional and propositional equalities, flags for disabling reduction rules, support for equational lemmas).
• rw (supports occurrences, at modifier, definitional and propositional equalities), it creates an eq.rec proof.

They all support the at modifier.

We can still provide the dsimp primitives for users that want to implement their own tactics.
https://github.com/leanprover/lean/blob/master/library/init/meta/simp_tactic.lean#L77

[gebner]

For me, the reduce that accepts non-refl lemmas and/or extra reduction rules is our simp.

From an implementation point of view, I agree. But from a UX point of view this is confusing as hell, since simp does much, much more than just reducing using non-refl lemmas. For example, by default it rewrites using associativity, commutativity, etc.--and I definitely want simp to do that. How about the following for the user-facing tactics?

• dunfold performs a single reduction step using equational rfl-lemmas or delta, depending on the argument (implemented using dsimp)
• unfold performs the same operation but can also use non-rfl lemmas (implemented using the simplifier)
• dreduce is the efficient reduction engine (what you call reduce)
• reduce performs the same operation, but also uses non-rfl lemmas (and hence needs to produce proofs, implemented using the simplifier; I guess we should also use norm_num here?)
• simp applies all lemmas tagged with [simp] (and whatever simproc, algebraic normalizer, etc. extensions will be there in the future)
• optionally dsimp, but I'm not sure if this should be different than dreduce

The rationale for the naming scheme is the following: we already use the d prefix to indicate definitional operations, so we should use it consistently whenever possible. Each of the dunfold/unfold, dreduce/reduce, dsimp/simp pairs only differs in whether they return definitionally equal terms, but are otherwise identical and take the same arguments. The unfold/reduce/simp suffix indicates how much rewriting/simplification happens.

We need to have a non-definitional reduction tactic. Functions on nested inductives are implemented using well-founded recursion and hence don't reduce definitionally, even if they're structurally recursive. Not being able to reduce them is inconvenient. (I'm aware of the obvious non-termination issue, maybe we should require the user to explicitly mark these definitions as reductions.)

[gebner]

I just wanted to point out that gcd_zero_right in the motivating example is actually a definitional reduction:

lemma gcd_zero_right (x : nat) : gcd 0 x = x := rfl

Having gcd 0 x definitionally reduce to x was the motivation for #1680. My suggestion there was to add gcd_zero_right as a reduction rule for dunfold so that the type_context will use it for unification (in the future).

[leodemoura]

@gebner I used gcd_zero_right to demonstrate that unfold doesn't work for functions defined by well founded recursion. This is a big issue. I added rw [gcd] as a workaround. Here is another example.

lemma gcd_ne_zero (x y : nat) (h : x ≠ 0) : gcd x y = gcd (y % x) x := 
by rw [gcd]; simph

[leodemoura]

• dreduce is the efficient reduction engine (what you call reduce)
• reduce performs the same operation, but also uses non-rfl lemmas (and hence needs to produce proofs, implemented using the simplifier; I guess we should also use norm_num here?)

@gebner "Confusing as hell" is in the eye of the beholder. I also think dreduce and reduce is "confusing as hell". (your) reduce will not do what the user expects since it is based on simp. Thus, it cannot reduce arbitrary (reducible) terms in our goals. In practice, most of the time, we only need simp, unfold and reduce (your dreduce).

We need to have a non-definitional reduction tactic. Functions on nested inductives are implemented using well-founded recursion and hence don't reduce definitionally, even if they're structurally recursive. Not being able to reduce them is inconvenient. (I'm aware of the obvious non-termination issue, maybe we should require the user to explicitly mark these definitions as reductions.)

I disagree. Most users will use simp for that. In systems without dependent types (e.g., Isabelle), users use simp for doing this, and it looks very natural. simp is not a full solution for system with dependent types because we cannot reduce/simplify arbitrary subterms using it.

I usually reduce (your dreduce) when we are making heavy use of dependent types, and we have cleanup our goal using definitional equalities. Definitional equalities can be used in any subterm.

I agree that is sad that a function application f a b cannot be reduced definitionally (using the equational lemmas) if f was defined by well founded recursion. The best we can do in this case is to expose the internal implementation based on well_founded.fix (which is rarely useful).
BTW, there is a possible solution for this issue. We can implement a K-like reduction for acc.rec.
I describe this approach at issue #654. The problem is that type checking may loop.

[semorrison]

While all these tactics are being discussed together, could I bring up an incidental point: could we aim to have consistent failure behaviour across all these reduction tactics? Ideally I would prefer that all of these tactics fail if they can't find anything to do.

(I know that this sometimes costs extra uses of try, but I'd far prefer to be able to use failure as flow control in writing automation. Even in interactive mode, I'd prefer to see a tactic failing when it doesn't do anything.)

[leodemoura]

Ideally I would prefer that all of these tactics fail if they can't find anything to do.

Ok. We will use this approach.

[leodemoura]

The commits above address the original issue and the @semorrison's suggestion.