1
$\begingroup$

When one is busy writing a proof in Lean, one sometimes encounters symbols, like + or <=, but one does not know what the underlying function name and instance function name is. How does one go about unfolding a symbol. This is useful if you want to do simp or rw on that function.

Is there a way to use tactics to get the underlying function, for example to know that + is, I had to guess to do rw [HAdd.hAdd], I did not find it, I just remembered that H is sometimes prefixed.

Now I can write:

theorem nat_add_succ_is_succ_add (n m: Nat):
  succ n + m = succ (n + m) := by
  rw [HAdd.hAdd]
  unfold instHAdd
  simp
  rw [Add.add]
  unfold instAddNat

My Tactic state is then

nm: Nat
⊢ { add := Nat.add }.1 (succ n) m = succ ({ add := Nat.add }.1 n m)

This seems like a long way to go and also I didn't know how to find HAdd.hAdd. Is there a more efficient way and how does one go about finding HAdd.hAdd or can we skip this altogether using some other command or tactic?

I would also like to unfold my Tactic state to the point that I get:

Nat.add (succ n) m = succ (Nat.add n m)

But simp takes me back to +.

Is there a way to bring my Tactic state to this state?

$\endgroup$
3
  • 1
    $\begingroup$ simp only to answer your specific question at the end. $\endgroup$ Mar 10, 2023 at 15:51
  • 1
    $\begingroup$ And usually clicking on things in the tactic state (using widgets) is the quick way to identify what the head symbol actually is. $\endgroup$ Mar 10, 2023 at 15:52
  • $\begingroup$ related: proofassistants.stackexchange.com/questions/1672/… $\endgroup$
    – Jason Rute
    Mar 10, 2023 at 17:24

1 Answer 1

4
$\begingroup$

You don't need to know what + is short for if you use simp.

  simp only [(· + ·), Add.add]
  -- new goal: ⊢ Nat.add (succ n) m = succ (Nat.add n m)

Here I simply typed out the functions I saw in the info view. I used simp only to avoid the global simp lemma Nat.add_eq, which as you said would bring us back to +.

Now, why does that simp lemma exist? Because we want to make sure that we don't end up with goals using a mixture of abstract + and concrete functions like Nat.add, which could complicate applying further lemmas to them, i.e. + is considered the "canonical form" of Nat.add. Nat.add_succ is an example of such a lemma stated in terms of +, and so we can do the proof without ever unfolding +.

theorem nat_add_succ_is_succ_add2 (n m : Nat) :
    succ n + m = succ (n + m) := by
  induction m <;> simp_all [Nat.add_succ]

This theorem already exists as Nat.succ_add by the way.

$\endgroup$
3
  • $\begingroup$ simp only [(· + ·), Add.add] is pretty great, but how would one do a rw [(· + ·)] ? $\endgroup$ Mar 12, 2023 at 13:51
  • $\begingroup$ rw doesn't know about that syntax. It is essentially a dumber simp, so it's expected to do less, though whether this particular feature should be supported is a good question. $\endgroup$ Mar 12, 2023 at 17:27
  • $\begingroup$ I was assuming that the syntax for (· + ·) was a general syntax that could be used with rewrite, unfold or anywhere where you would want to reference the + function in a tactic. $\endgroup$ Mar 13, 2023 at 10:34

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.