simp lemmas with hypotheses

Stream: general

[Scott Morrison]

The lemma

@[simp] lemma degree_C (ha : a ≠ 0) : degree (C a) = (0 : with_bot ℕ) := ...

in polynomial.lean is marked as simp. However it doesn't get applied by simp, even when there's an explicit hypothesis ha : a ≠ 0 available.

[Scott Morrison]

Is there are way to have simp use it? If not, why are lemmas like this marked with simp?

[Simon Hudon]

Yes, you just need simp *

[Scott Morrison]

@Simon Hudon, sorry, I don't understand. Here's my example:

import data.polynomial

open polynomial

variables {α : Type} [integral_domain α] [decidable_eq α]

lemma test (a : α) (ha : a ≠ 0) : degree (C a) = (0 : with_bot ℕ) :=
by simp [degree_C ha]

lemma test' (a : α) (ha : a ≠ 0) : degree (C a) = (0 : with_bot ℕ) :=
by simp * -- fails

[Scott Morrison]

I don't understand how to convince simp to use degree_C, without holding its hand.

[Simon Hudon]

Can you show the error message?

[Scott Morrison]

tactic failed, there are unsolved goals
state:
α : Type,
_inst_1 : integral_domain α,
_inst_2 : decidable_eq α,
a : α,
ha : a ≠ 0
⊢ some 0 = 0

[Simon Hudon]

what if you write by simp * ; refl?

[Mario Carneiro]

where did some 0 come from?

[Scott Morrison]

@Simon Hudon, by simp *; refl seems to do it.

[Scott Morrison]

I think I don't understand what simp * does. I always thought that just included all the local hypotheses as simp lemmas.

[Scott Morrison]

I'm not really sure how we got a some 0 here, @Mario Carneiro. This seems to be closely related to the question @Aditya Agarwal had: there are many ways to get something in with_bot nat...

[Mario Carneiro]

The preferred way is the coercion, which has the advantage that it actually has type with_bot nat instead of option nat

[Mario Carneiro]

with some n a lot of simp lemmas won't trigger for it

[Scott Morrison]

Shoot... I've been working with a copy of mathlib with a dumb stray simp lemma I introduced earlier.

[Scott Morrison]

My "minimal working examples" are just wrong...

[Scott Morrison]

In particular, that some 0 was entirely my doing.