Zulip Chat Archive

Stream: general

Topic: simp lemmas with hypotheses


view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Simon Hudon (Feb 08 2019 at 22:50):

Yes, you just need simp *

view this post on Zulip 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

view this post on Zulip Scott Morrison (Feb 08 2019 at 23:23):

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

view this post on Zulip Simon Hudon (Feb 08 2019 at 23:29):

Can you show the error message?

view this post on Zulip 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

view this post on Zulip Simon Hudon (Feb 08 2019 at 23:33):

what if you write by simp * ; refl?

view this post on Zulip Mario Carneiro (Feb 08 2019 at 23:42):

where did some 0 come from?

view this post on Zulip Scott Morrison (Feb 08 2019 at 23:45):

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

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 08 2019 at 23:48):

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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Feb 08 2019 at 23:55):

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

view this post on Zulip 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