Why won't dsimp reduce 'plus a (succ b)'?

Stream: new members

[Adam Dingle]

Let's define natural numbers plus an addition function:

inductive MyNat
  | zero
  | succ (n : MyNat)

def plus (a : MyNat) : MyNat → MyNat
  | .zero => a
  | .succ b => .succ (plus a b)

Now I'd like to prove that addition cancels on the right. Here we go:

example : plus a c = plus b c → a = b := by
  induction c
  case zero => exact id
  case succ n ih =>
    ...

The proof state now looks like this:

a b n: MyNat
ih: plus a n = plus b n → a = b
⊢ plus a (MyNat.succ n) = plus b (MyNat.succ n) → a = b

I'd like to simplify the goal to

⊢ MyNat.succ (plus a n) = MyNat.succ (plus b n) → a = b

which looks more like ih. However I can't seem to make that step. I tried dsimp, but it has no effect on the goal. That surprises me, since this is just a beta-reduction to a term that is definitionally equal. Why won't dsimp do what I want? Is there another tactic that will?

[Eric Rodriguez]

Are you saying dsimp [plus]?

[Adam Dingle]

Aha! OK, dsimp [plus] did the trick. Thanks.

However, now suppose that I want to make the same proof using the built-in Nat type, rather than my own MyNat type. Here we go:

variable (a b c : Nat)

example : a + c = b + c → a = b := by
  induction c
  case zero => exact id
  case succ n ih =>
    ...

The proof state now looks like this:

abcn: ℕ
ih: a + n = b + n → a = b
⊢ a + Nat.succ n = b + Nat.succ n → a = b

Once again, I'd like to reduce the goal to

Nat.succ (a + n) = Nat.succ (b + n) → a = b

If + becomes Nat.add in the process, that's OK. Still, I don't see how to do this. I tried

dsimp [Add.add]
dsimp [Nat.add]
dsimp [· + ·]

but none of them were willing to reduce the + function. Any ideas?

[Eric Rodriguez]

hmm, I'm not sure; you can write your own lemma and use that (and if the proof is literally rfl then dsimp will be happy with it) but it does seem hard to pierce through the veil of HAdd and Add.

[Adam Dingle]

Thanks. Actually I realized there's a built-in lemma that is exactly that:

theorem Nat.add_succ (n m : Nat) : n + succ m = succ (n + m) :=
  rfl

So dsimp [Nat.add_succ] does exactly what I want.

Still, it seems like it would be nice if dsimp could pierce through HAdd and Add without a helper lemma. If that's somehow possible, I'd be interested to hear about it.

[Mauricio Collares]

dsimp only [Add.add, Nat.add, (· + ·)] worked here (the order shouldn't matter)

[Adam Dingle]

Fascinating. That's a bit of a mouthful, but it's good to know that it is actually possible. :)

[Kyle Miller]

dsimp! unfolds definitions automatically

[Adam Dingle]

That sounds promising, however it doesn't seem to help in the example I just gave. As Mauricio pointed out, dsimp only [Add.add, Nat.add, (· + ·)] will reduce a + succ n to succ (Nat.add a n), but dsimp! doesn't affect it at all.