# Zulip Chat Archive

## Stream: general

### Topic: simp lemmas with hypotheses

#### Scott Morrison (Feb 08 2019 at 05:01):

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 (Feb 08 2019 at 05:01):

Is there are way to have `simp`

use it? If not, why are lemmas like this marked with `simp`

?

#### Simon Hudon (Feb 08 2019 at 22:50):

Yes, you just need `simp *`

#### Scott Morrison (Feb 08 2019 at 23:23):

@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 (Feb 08 2019 at 23:23):

I don't understand how to convince `simp`

to use `degree_C`

, without holding its hand.

#### Simon Hudon (Feb 08 2019 at 23:29):

Can you show the error message?

#### Scott Morrison (Feb 08 2019 at 23:32):

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 (Feb 08 2019 at 23:33):

what if you write `by simp * ; refl`

?

#### Mario Carneiro (Feb 08 2019 at 23:42):

where did `some 0`

come from?

#### Scott Morrison (Feb 08 2019 at 23:45):

@Simon Hudon, `by simp *; refl`

seems to do it.

#### Scott Morrison (Feb 08 2019 at 23:45):

I think I don't understand what `simp *`

does. I always thought that just included all the local hypotheses as simp lemmas.

#### Scott Morrison (Feb 08 2019 at 23:47):

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 (Feb 08 2019 at 23:48):

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

instead of `option nat`

#### Mario Carneiro (Feb 08 2019 at 23:48):

with `some n`

a lot of simp lemmas won't trigger for it

#### Scott Morrison (Feb 08 2019 at 23:55):

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

#### Scott Morrison (Feb 08 2019 at 23:55):

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

#### Scott Morrison (Feb 08 2019 at 23:56):

In particular, that `some 0`

was entirely my doing.

Last updated: May 16 2021 at 21:11 UTC