## 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