Zulip Chat Archive

Stream: general

Topic: lemma surprisingly not proved by rfl


view this post on Zulip Chris Hughes (Jul 02 2018 at 15:13):

Is there a shorter way to prove this and why isn't rfl working? Is it because the type of the lhs is with_bot ℕ and the rhs is option ℕ? (The types are defeq)

import algebra.ordered_group

example : (0 : with_bot ) = some 0 := rfl -- doesn't work

example : (0 : with_bot ) = some 0 :=
by unfold has_zero.zero add_monoid.zero has_one.one monoid.one
  add_comm_monoid.zero semiring.zero ordered_semiring.zero linear_ordered_semiring.zero
  decidable_linear_ordered_semiring.zero comm_semiring.zero

view this post on Zulip Chris Hughes (Jul 02 2018 at 15:32):

Looked a little deeper and it seems (0 : with_bot ℕ) is defeq to some (1 : multplicative ℕ). I feel like perhaps the fact that this lemma is not rfl means the definition ought to be changed.

view this post on Zulip Mario Carneiro (Jul 02 2018 at 20:56):

Oh, this is weird! It is in fact the case that (0 : with_bot ℕ) = some 0, but the tactics are very confused about it. Here's simp proving that they are different, and then the kernel says it's a wrong proof:

example : (0 : with_bot ℕ) ≠ (some 0 : option ℕ) :=
show some _ ≠ some 0, begin
  simp [multiplicative.monoid],
end

view this post on Zulip Mario Carneiro (Jul 02 2018 at 20:56):

I will add a lemma for it

view this post on Zulip Mario Carneiro (Jul 02 2018 at 20:57):

as a slight hack, you can instead prove it by dec_trivial

view this post on Zulip Kevin Buzzard (Jul 02 2018 at 21:06):

failed to synthesize type class instance for
⊢ has_zero (with_bot ℕ)

-- am I missing an import?

view this post on Zulip Mario Carneiro (Jul 02 2018 at 21:11):

algebra.ordered_group

view this post on Zulip Mario Carneiro (Jul 02 2018 at 21:23):

@Sebastian Ullrich Minimized:

def nat2 := nat
instance : has_one nat2 := ⟨(0 : ℕ)⟩
example : (0 : ℕ) ≠ (1 : nat2) := by simp

view this post on Zulip Mario Carneiro (Jul 02 2018 at 21:24):

In this example example : (0 : ℕ) = (1 : nat2) := rfl also fails

view this post on Zulip Sebastian Ullrich (Jul 02 2018 at 21:36):

@Mario Carneiro Thanks, this seems to be an imprecise term pattern match at https://github.com/leanprover/lean/blob/master/src/library/type_context.cpp#L2906-L2907

view this post on Zulip Mario Carneiro (Jul 02 2018 at 21:37):

Ooh, that's a tricky one. I'd hate for you to have to do defeq checks constantly there out of paranoia for tricks like I showed...

view this post on Zulip Sebastian Ullrich (Jul 02 2018 at 21:49):

Yeah. It's probably not a good idea in general to declare instances on semireducible defs like multiplicative. Is it feasible to change that?

view this post on Zulip Mario Carneiro (Jul 02 2018 at 21:49):

Not really, I mean that is the point

view this post on Zulip Sebastian Ullrich (Jul 02 2018 at 21:49):

Sorry, I meant making it irreducible or a newtype.

view this post on Zulip Mario Carneiro (Jul 02 2018 at 21:50):

Probably not. An important aspect of the semireducible part is that you can prove multiplicative versions of additive theorems by defeq

view this post on Zulip Mario Carneiro (Jul 02 2018 at 21:51):

It's fine as long as it gives way to a sufficiently forceful "unfold", but I'm not sure irreducible will

view this post on Zulip Mario Carneiro (Jul 02 2018 at 21:52):

I would say that users should avoid having things of type multiplicative A in their goal at all

view this post on Zulip Mario Carneiro (Jul 02 2018 at 21:54):

so I think I will change the definition of the with_bot instance so that it unfolds directly rather than showing the multiplicative stuff

view this post on Zulip Mario Carneiro (Jul 02 2018 at 22:56):

fixed


Last updated: May 07 2021 at 00:30 UTC