# Zulip Chat Archive

## Stream: general

### Topic: lemma surprisingly not proved by rfl

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

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

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

#### Mario Carneiro (Jul 02 2018 at 20:56):

I will add a lemma for it

#### Mario Carneiro (Jul 02 2018 at 20:57):

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

#### Kevin Buzzard (Jul 02 2018 at 21:06):

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

-- am I missing an import?

#### Mario Carneiro (Jul 02 2018 at 21:11):

`algebra.ordered_group`

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

#### Mario Carneiro (Jul 02 2018 at 21:24):

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

also fails

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

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

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

#### Mario Carneiro (Jul 02 2018 at 21:49):

Not really, I mean that is the point

#### Sebastian Ullrich (Jul 02 2018 at 21:49):

Sorry, I meant making it irreducible or a newtype.

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

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

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

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

#### Mario Carneiro (Jul 02 2018 at 22:56):

fixed

Last updated: May 07 2021 at 00:30 UTC