Rewrite not sufficiently aggressive

Stream: lean4

[Leni Aniva]

There is a clause in the code for rewrite such that it will skip over possible sites if the head index doesn't match. For example:

example (m : Nat) :  Nat.add 0 m = m := by
  rewrite [Nat.zero_add]

does not work, while replacing rewrite by apply does.

In this simple example, we can replace rewrite by apply. What if the rewrite occurs inside a larger expression? In which case the insufficiently aggressive rewrite could not make progress. Is there a general way to handle this type of issue?

[Ruben Van de Velde]

Best approach: make sure you don't end up with Nat.add in your state from the start

Second best: use the library theorem that probably exists that Nat.add a b = a + b

Worst: use the erw tactic instead

[Jovan Gerbscheid]

Note that rewrite uses the reducible transparency setting, meaning that the rewrite wouldn't go through anyways. Similarly with_reducible apply also doesn't work here.

The erw tactic bumps up the transparency to default. But its use is discouraged in mathlib.

[Kyle Miller]

erw also uses head index matching, so it doesn't work here either

[Leni Aniva]

Kyle Miller said:

erw also uses head index matching, so it doesn't work here either

Is there a reason other than performance about why rewrite uses index matching?

[Leni Aniva]

Ruben Van de Velde said:

Best approach: make sure you don't end up with Nat.add in your state from the start

Second best: use the library theorem that probably exists that Nat.add a b = a + b

Worst: use the erw tactic instead

Not generating .add seems difficult. Even conv with whnf creates .adds from the normal + for natural numbers.

[Jovan Gerbscheid]

Why would you use conv with whnf?

[Aaron Liu]

I only use whnf as an "exploring" tactic and it never makes it into my final proof

[Kyle Miller]

I have to #xy: why are you using whnf? As you see, it puts expressions into a form that basic tactic do not support.

There are comments inside the Lean source code about normal forms it expects. One of them is using functions like HAdd.hAdd instead of the underlying instance definitions. That also includes OfNat.ofNat, which similarly is denormalized by whnf.

[Aaron Liu]

instead of whnf you can usually just change to the type you want

[Kyle Miller]

(@Aaron Liu This is likely for something programmatic, sochange is unlikely to be helpful)

[Leni Aniva]

Jovan Gerbscheid said:

Why would you use conv with whnf?

Sometimes a rewrite cannot proceed because it could not find the rewriting pattern in the target, and this could only be rectified with whnf. I've asked this question before. e.g.

example (x n : Nat) (h : x.succ + n = (x + n).succ)
  : x.succ + n.succ = (x + n.succ).succ := by
  rewrite [h]
  rfl

I just want to explain that entirely avoiding Nat.add is unlikely

[Kyle Miller]

example comment: https://github.com/leanprover/lean4/blob/655a39ceb8c7123dc14a064e0d4e4ae292a3b436/src/Lean/Meta/Tactic/Simp/Main.lean#L105

[Leni Aniva]

Kyle Miller said:

(Aaron Liu This is likely for something programmatic, sochange is unlikely to be helpful)

I'll use change as a last resort

[Aaron Liu]

You could call whnf on the lhs of the rewriting theorem too

[Kyle Miller]

Leni Aniva said:

I've asked this question before.

I asked about a spec for what you're actually trying to do, and I didn't get any understanding of how you are in this situation that you need to rewrite using terms that are not in the right form to rewrite. Using whnf/unfold_projs seems like a hack papering over something missing to the story.

[Floris van Doorn]

I agree with the others that whnf is not the way to go. In your last example, you should just perform rewrites with multiple lemmas (some of which are definitional reductions)

[Leni Aniva]

Kyle Miller said:

Leni Aniva said:

I've asked this question before.

I asked about a spec for what you're actually trying to do, and I didn't get any understanding of how you are in this situation that you need to rewrite using terms that are not in the right form to rewrite. Using whnf/unfold_projs seems like a hack papering over something missing to the story.

I'm developing a tactic or function that normalizes the current goal into a form, where no more subterms can be reduced, and where rewrites are not blocked because of differing head elements. For example, in the x.succ + n.succ = (x + n.succ).succ example, the (x + n.succ).succ part should be normalized into (x + n).succ.succ. Currently I'm using whnf to achieve this, but whnf keeps generating Nat.add so I'm asking how to deal with this problem.

[Leni Aniva]

Floris van Doorn said:

I agree with the others that whnf is not the way to go. In your last example, you should just perform rewrites with multiple lemmas (some of which are definitional reductions)

Which lemmas are those? Nat.add.eq_def?

[Jovan Gerbscheid]

In this case, you need the lemma Nat.add_succ : n + m.succ = (n + m).succ

[Leni Aniva]

Jovan Gerbscheid said:

In this case, you need the lemma Nat.add_succ : n + m.succ = (n + m).succ

I have explained in the original question that the use case is general and such lemmas may not be available. The x.succ + n.succ example was extracted from the proof of Nat.add_succ and using Nat.add_succ to prove it would be circular reasoning.

[Aaron Liu]

Leni Aniva said:

I'm developing a tactic or function that normalizes the current goal into a form, where no more subterms can be reduced, and where rewrites are not blocked because of differing head elements.

What does "reduced" mean?

[Jovan Gerbscheid]

Nat.add_succ will always exist when working with Lean. So maybe give an example that is "general"?

[Leni Aniva]

Aaron Liu said:

Leni Aniva said:

I'm developing a tactic or function that normalizes the current goal into a form, where no more subterms can be reduced, and where rewrites are not blocked because of differing head elements.

What does "reduced" mean?

Where no more computation can happen even when you unfold definitions. For example, [].length should be reduced to 0.

[Leni Aniva]

Jovan Gerbscheid said:

Nat.add_succ will always exist when working with Lean. So maybe give an example that is "general"?

Suppose I created a new Nat type that has the same add_succ lemma as Nat.

[Aaron Liu]

How do you determine what to reduce? Should it reduce List.length l to

List.brecOn l fun x f =>
  (match (motive := (x : List α) → List.below x → Nat) x with
    | [] => fun x => 0
    | head :: as => fun x => x.1 + 1)
    f

?

[Leni Aniva]

Aaron Liu said:

How do you determine what to reduce? Should it reduce List.length l to

List.brecOn l fun x f =>
    (match (motive := (x : List α) → List.below x → Nat) x with
      | [] => fun x => 0
      | head :: as => fun x => x.1 + 1)
      f

?

Currently it just reduces everything possible. Eventually, I want the tactic to accept rewrite lemmas, and reduce the target/lctx to the point where these lemmas can execute, so the question about whether List.length l should be reduced is dependent on the forms of these lemmas.

For example, in this case

example (x n : Nat) (h : x.succ + n = (x + n).succ)
  : x.succ + n.succ = (x + n.succ).succ := by

the only way I know to make the rewrite h executable on the target is via whnf

[Kyle Miller]

Leni Aniva said:

I have explained in the original question that the use case is general and such lemmas may not be available.

I read that, but I think you might be underestimating the amount of context that I'd need to understand that. I am sure there are specific constraints to your general problem, given that you do not like the general advice we're giving that you need to develop the theory around each type's definitions. It's solid advice, and it needs strong motivation for why that is unacceptable. Using whnf is known to be an antipattern for normal proofs.

You've mentioned the idea "what if we make our own Nat type": if it's the same as Nat, why are you not using Nat, which has all the lemmas already available?

Where is this example coming from in the first place?

example (x n : Nat) (h : x.succ + n = (x + n).succ)
  : x.succ + n.succ = (x + n.succ).succ := by

You may have answered this, but I'm not certain yet that taking a step back then forward again would put you into a better position.

[Kyle Miller]

You're free to reduce everything in sight of course, but then you need to be on your own and develop a fully-reduced set of lemmas and follow the design patterns of keeping normal forms in mind. The rw tactic is not going to help you avoid thinking about normal forms. The head-index key matching is both for performance and for normal form considerations.

[Leni Aniva]

Kyle Miller said:

Leni Aniva said:

I have explained in the original question that the use case is general and such lemmas may not be available.

I read that, but I think you might be underestimating the amount of context that I'd need to understand that. I am sure there are specific constraints to your general problem, given that you do not like the general advice we're giving that you need to develop the theory around each type's definitions. It's solid advice, and it needs strong motivation for why that is unacceptable. Using whnf is known to be an antipattern for normal proofs.

You've mentioned the idea "what if we make our own Nat type": if it's the same as Nat, why are you not using Nat, which has all the lemmas already available?

Where is this example coming from in the first place?

example (x n : Nat) (h : x.succ + n = (x + n).succ)
  : x.succ + n.succ = (x + n.succ).succ := by

You may have answered this, but I'm not certain yet that taking a step back then forward again would put you into a better position.

Suppose we create a new data type, equipped with its own set of arithmetic operations (i.e. implementing Add or Mul, etc.). Then we need to prove properties about these operations without built-in add_comm and other lemmas. I want to develop a tactic that can help with this use case.

Another way of thinking about this is I want to make a tactic version of the proof of Nat.add_comm and other lemmas in Lean's Init library.

[Kyle Miller]

Leni Aniva said:

I want to develop a tactic that can help with this use case.

Ok, what I am hearing is that you want to take the equation lemmas for the operations and automatically rephrase them in terms of the HAdd/HMul, etc. classes.

Then, maybe, there's an automated theorem prover angle after this, to prove properties like add_comm.

The important thing is defining the right lemmas first. That example doesn't look like any of the lemmas you'd want to generate. You want Nat.add_zero and Nat.add_succ, which require unfolding definitions, and follow the structure of the equation lemmas. That's it, and everything else about addition follows from those.

[Leni Aniva]

Kyle Miller said:

Leni Aniva said:

I want to develop a tactic that can help with this use case.

Ok, what I am hearing is that you want to take the equation lemmas for the operations and automatically rephrase them in terms of the HAdd/HMul, etc. classes.

Then, maybe, there's an automated theorem prover angle after this, to prove properties like add_comm.

The important thing is defining the right lemmas first. That example doesn't look like any of the lemmas you'd want to generate. You want Nat.add_zero and Nat.add_succ, which require unfolding definitions. That's it, and everything else about addition follows from those.

The example is the last congrArg operation from Nat.add_succ, structured in tactic form

[Kyle Miller]

I don't understand: Nat.add_succ is proved with rfl. Both of the basic lemmas are definitional equalities. The special thing about Nat.add_succ is purely that it's written in terms of + instead of Nat.add.

[Leni Aniva]

Kyle Miller said:

I don't understand: Nat.add_succ is proved with rfl. Both of the basic lemmas are definitional equalities. The special thing about Nat.add_succ is purely that it's written in terms of + instead of Nat.add.

sorry, I meant succ_add, not add_succ:

theorem succ_add : ∀ (n m : Nat), (succ n) + m = succ (n + m)
  | _, 0   => rfl
  | n, m+1 => congrArg succ (succ_add n m)

[Kyle Miller]

Right, and so succ_add should be proved using your generated "add_succ"

[Leni Aniva]

Kyle Miller said:

Right, and so succ_add should be proved using your generated "add_succ"

but succ_add is not proven using add_succ in `Init.Data.Nat.Basic?

[Leni Aniva]

In any case, thanks for the explanation. I think I've a way to handle this.

[Kyle Miller]

Sorry, had to step away for a bit. The Init proof is proving it from scratch for some reason, possibly because it's more convenient when no tactics are available yet.

Here's a model using the Nat.add_zero/Nat.add_succ restatements of the equation lemmas, and using rewrite instead of rw to verify that the lemmas do the job:

theorem Nat.succ_add' {m n : Nat} : m.succ + n = (m + n).succ := by
  induction n using Nat.rec with
  | zero => rewrite [Nat.add_zero, Nat.add_succ]; rfl
  | succ n' ih => rewrite [Nat.add_succ, ih, Nat.add_succ]; rfl

I use using Nat.rec to avoid using the custom induction principle that Nat uses, whose purpose is to put things in terms of notation. There's also a small complexity here that Lean sometimes normalizes Nat literals to use OfNat, so you can see a 1 instead of Nat.zero.succ in one of the goal states.