Unfolding type class definitions in order to rewrite

Stream: lean4

[Daniel Patterson]

If I write a lemma as, say,

theorem nat_0_plus : forall (x : Nat), Nat.add 0 x  = x

Then I can rewrite with Nat.add (good!). If I write it instead as:

theorem nat_0_plus : forall (x : Nat), 0 + x  = x

I _assume_ that the type class resolution is finding the same addition definition, but I'm wondering how I can, for lack of a better term, unfold the type class indirection so that I can rewrite with the actual definition.

[Jannis Limperg]

The whole tactic framework assumes that the normal form of Nat.add 0 x is 0 + x, i.e. @HAdd.hAdd ... 0 x. So instead of unfolding the notation and reducing Nat.add, you should write lemmas like 0 + x = 0 and then simp with them. (Btw, unlike Coq and Agda, Lean's addition recurses on the right, so you can't rewrite with Nat.add in your example anyway.)

[Andrés Goens]

@Daniel Patterson if really want to unfold it for some reason though, one thing you can do is use set_option pp.raw true which will show you what the instance actually is, and unfold it:

set_option pp.raw true
variable (x : Nat)
#check 0 + x -- HAdd.hAdd.{0 0 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) _uniq.23954 : Nat

theorem nat_0_plus : forall (x : Nat), 0 + x  = x := by
  intros x
  unfold HAdd.hAdd
  unfold instHAdd
  unfold Add.add
  unfold instAddNat
  unfold Nat.add

you see there's a couple of layers there of typeclasses but it indeed ends up at the same definition, which is why it's much better to just use these normal forms and avoid explicitly unfolding, unless you really need to, like @Jannis Limperg says.

[Sebastian Ullrich]

dsimp only [(· + ·), Add.add] is a bit shorter and doesn't need pp options to find out

[Daniel Patterson]

Sebastian Ullrich said:

dsimp only [(· + ·), Add.add] is a bit shorter and doesn't need pp options to find out

This is great -- any pointers as to what it's doing? :)

(motivation for this is _teaching_ -- probably I'll just try to avoid typeclass syntax wholesale, but still experimenting).

[Andrés Goens]

Daniel Patterson said:

This is great -- any pointers as to what it's doing? :)

(motivation for this is _teaching_ -- probably I'll just try to avoid typeclass syntax wholesale, but still experimenting).

If you set up your editor properly (I imagine the Lean4 plugin for vs code does this directly) you can just hover over something and get a pop-up explanation, for this example: Screen-Shot-2022-11-23-at-10.37.55.png

It tells us how dsimp will only use the definitions and then by passing the (· + ·) function Lean will use that function as a definition to simplify. (The only I imagine makes dsimp only use the definitions passed in square brackets to it, and not from a database (like simp), but I'm guessing there)

[Sebastian Ullrich]

I suppose it would be nice if rw and perhaps even unfold accepted (· + ·) as well

[Daniel Patterson]

Yeah, it was the use of (· + ·) that somewhat surprised me. That is syntax sugar for fun x y => x + y (as I understand it). I was trying to understand what it meant to do definitional simplification with that. I would have _thought_ some amount of notation unfolding would be needed, which is why I was asking for clarification!