Unfolding during unification

Stream: lean4

[Leni Aniva]

Consider this example:

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

If I replace congrArg with rewrite, the proof cannot proceed.

Looking into the type of this congrArg application, it seems like there is unfolding of the definition of + taking place during Meta.isDefEq. Is there a way to trigger this unfolding? unfold Nat.add or rw [←Nat.add.eq_def] do not work either.

[Leni Aniva]

e.g.

example (x n : Nat) (h : x.succ + n = (x + n).succ)
  : x.succ + n.succ = (x + n.succ).succ := by
  have := congrArg Nat.succ h
  exact this

shows

x n : Nat
h : x.succ + n = (x + n).succ
this : (x.succ + n).succ = (x + n).succ.succ
⊢ x.succ + n.succ = (x + n.succ).succ

What I want is a process to transform the target from x.succ + n.succ = (x + n.succ).succ to (x.succ + n).succ = (x + n).succ.succ. Without using Nat.succ_add since I need to generalize this to other inductives.

[Aaron Liu]

change? Not sure what exactly you want here.

[Leni Aniva]

Aaron Liu said:

change? Not sure what exactly you want here.

A tactic which replaces the target x.succ + n.succ = (x + n.succ).succ by (x.succ + n).succ = (x + n).succ.succ via some definition unfolding process.

[Aaron Liu]

By the way before you get to Nat.add you need to peel off docs#instHAdd and docs#instAddNat and you have to reduce docs#HAdd.hAdd and docs#Add.add.

[Aaron Liu]

Leni Aniva said:

Aaron Liu said:

change? Not sure what exactly you want here.

A tactic which replaces the target x.succ + n.succ = (x + n.succ).succ by (x.succ + n).succ = (x + n).succ.succ via some definition unfolding process.

These are not definitionally equal.

[Aaron Liu]

How does the tactic tell how much to unfold? reduce can unfold a lot but you probably don't want that much. change will try to change the goal to something definitionally equal but you have to tell it what to change to.

[Aaron Liu]

import Mathlib.Tactic.DefEqTransformations

example (x n : Nat) (h : x.succ + n = (x + n).succ)
  : x.succ + n.succ = (x + n.succ).succ := by
  have := congrArg Nat.succ h
  -- unfold everything (turn on smart unfolding for something more controlled)
  -- sometimes it doesn't work because it unfolds too much
  set_option smartUnfolding false in reduce at this ⊢
  exact this

[Ruben Van de Velde]

You don't really want to do this in general - you can rewrite with a theorem that says that (x+y.succ) = (x+y).succ

[Leni Aniva]

Ruben Van de Velde said:

You don't really want to do this in general - you can rewrite with a theorem that says that (x+y.succ) = (x+y).succ

I know. I chose this example to specifically ask for the case when this kind of theorem does not exist.

[Leni Aniva]

Aaron Liu said:

Leni Aniva said:

Aaron Liu said:

change? Not sure what exactly you want here.

A tactic which replaces the target x.succ + n.succ = (x + n.succ).succ by (x.succ + n).succ = (x + n).succ.succ via some definition unfolding process.

These are not definitionally equal.

Then how did congrArg finish the proof in this case?

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

[Ruben Van de Velde]

Yeah, the left- and right-hand sides are definitionally equal after applying succ -

example (x n : Nat) : (x.succ + n).succ = x.succ + n.succ := rfl
example (x n : Nat) : (x + n).succ.succ = (x + n.succ).succ := rfl

[Leni Aniva]

Ruben Van de Velde said:

Yeah, the left- and right-hand sides are definitionally equal after applying succ -

example (x n : Nat) : (x.succ + n).succ = x.succ + n.succ := rfl
example (x n : Nat) : (x + n).succ.succ = (x + n.succ).succ := rfl

Is there a way to apply this succ as a tactic that transforms one into the other?

[Leni Aniva]

Seems like the only way to do it is change, but it is a bit of a trial and error process?

[Ruben Van de Velde]

I don't follow your question

[Leni Aniva]

Ruben Van de Velde said:

I don't follow your question

Since the two types are definitionally equivalent, if the current target is the first one, is there a way to modify it to become the second one via some unfolding/delta-reduction tactic?

[Ruben Van de Velde]

Ruben Van de Velde said:

You don't really want to do this in general - you can rewrite with a theorem that says that (x+y.succ) = (x+y).succ

Still this ^

[Leni Aniva]

Ruben Van de Velde said:

Ruben Van de Velde said:

You don't really want to do this in general - you can rewrite with a theorem that says that (x+y.succ) = (x+y).succ

Still this ^

What if such a theorem doesn't exist for the types I'm working on? The example I have shown above has been extracted from the proof of this particular statement, and if it were to show up on its own I want to be able to prove it.

[Ruben Van de Velde]

You can write the theorem yourself

[Leni Aniva]

again, this particular case shows up during the proof of this exact theorem. it would be circular to prove the theorem using itself

[Aaron Liu]

Do you know which definitional equality you want to rewrite by?

[Leni Aniva]

Aaron Liu said:

Do you know which definitional equality you want to rewrite by?

The definition of Nat.add, but when I tried to rewrite by Nat.add.eq_def it doesn't work. See above.

[Robin Arnez]

We have theorems for that stuff:

example (x n : Nat) (h : x.succ + n = (x + n).succ) :
    x.succ + n.succ = (x + n.succ).succ := by
  rw [Nat.add_succ, Nat.add_succ, h]

[Kyle Miller]

@Leni Aniva I think you'll find more success getting help here if you have a clearer spec for what you're wanting and why. I haven't been able to make sense of what you're looking for exactly.

Maybe it's "how do I unfold notation"? Or "how do I fully reduce a term"? Or ...?

[Aaron Liu]

Leni Aniva said:

Aaron Liu said:

Do you know which definitional equality you want to rewrite by?

The definition of Nat.add, but when I tried to rewrite by Nat.add.eq_def it doesn't work. See above.

It works

import Mathlib.Tactic.DefEqTransformations

example (x n : Nat) (h : x.succ + n = (x + n).succ) :
    x.succ + n.succ = (x + n.succ).succ := by
  unfold_projs
  rw [Nat.add.eq_def]

[Leni Aniva]

Robin Arnez said:

We have theorems for that stuff:

example (x n : Nat) (h : x.succ + n = (x + n).succ) :
    x.succ + n.succ = (x + n.succ).succ := by
  rw [Nat.add_succ, Nat.add_succ, h]

I know there is a theorem for this, but in this case I am trying to prove these elementary theorems about addition without using the theorems themselves

[Aaron Liu]

Can you write a #mwe?

[Leni Aniva]

Aaron Liu said:

Can you write a #mwe?

I have

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

and I want to transform the target from x.succ + n.succ = (x + n.succ).succ to (x.succ + n).succ = (x + n).succ.succ using tactics.

[Ruben Van de Velde]

But why

[Aaron Liu]

/--
trace: x n : Nat
h : x.succ + n = (x + n).succ
⊢ (x.succ + n).succ = (x + n).succ.succ
---
warning: declaration uses 'sorry'
-/
#guard_msgs in
example (x n : Nat) (h : x.succ + n = (x + n).succ) : x.succ + n.succ = (x + n.succ).succ := by
  change (x.succ + n).succ = (x + n).succ.succ
  trace_state
  sorry

[Aaron Liu]

The goal has been changed.

[Leni Aniva]

Ruben Van de Velde said:

But why

If I have some other data structure (analogous toNat) and some other addition function (analogous to Nat.add), I might want to prove properties about this custom addition, in which case I would not have access to already proven theorems. I want to know how I can substitute in the definition of this addition function so I can prove properties about it.

[Leni Aniva]

Aaron Liu said:

/--
trace: x n : Nat
h : x.succ + n = (x + n).succ
⊢ (x.succ + n).succ = (x + n).succ.succ
---
warning: declaration uses 'sorry'
-/
#guard_msgs in
example (x n : Nat) (h : x.succ + n = (x + n).succ) : x.succ + n.succ = (x + n.succ).succ := by
  change (x.succ + n).succ = (x + n).succ.succ
  trace_state
  sorry

but this requires the writer to be able to see that the two targets are the same. Is there a way to execute this change by substituting in the definition of Nat.add? I see that there is unfold_projs which can do it.

[Aaron Liu]

Leni Aniva said:

I want to know how I can substitute in the definition of this addition function so I can prove properties about it.

The way you're supposed to do this is to follow your definition with a battery of theorems that together cover every possible case for the inputs, and then you rewrite using those theorems instead of unfolding.

[Aaron Liu]

Leni Aniva said:

but this requires the writer to be able to see that the two targets are the same. Is there a way to execute this change by substituting in the definition of Nat.add? I see that there is unfold_projs which can do it.

You will have to provide an algorithm for determining what to rewrite to in order for me to be able to implement it.

[Leni Aniva]

Aaron Liu said:

Leni Aniva said:

but this requires the writer to be able to see that the two targets are the same. Is there a way to execute this change by substituting in the definition of Nat.add? I see that there is unfold_projs which can do it.

You will have to provide an algorithm for determining what to rewrite to in order for me to be able to implement it.

1. Turn + into Nat.add
2. Substitute in the definition of Nat.add

I think unfold_projs can do this perfectly, as you answered above.

[Leni Aniva]

Aaron Liu said:

Leni Aniva said:

Aaron Liu said:

Do you know which definitional equality you want to rewrite by?

The definition of Nat.add, but when I tried to rewrite by Nat.add.eq_def it doesn't work. See above.

It works

import Mathlib.Tactic.DefEqTransformations

example (x n : Nat) (h : x.succ + n = (x + n).succ) :
    x.succ + n.succ = (x + n.succ).succ := by
  unfold_projs
  rw [Nat.add.eq_def]

This seems to be the best way to do it