# Zulip Chat Archive

## Stream: new members

### Topic: Noob: 50 = 40 -> false

#### Kevin Sullivan (Oct 30 2018 at 03:16):

What would be the cleanest / canonical way to prove this in a tactic script? nat.no_confusion only works when the left side is zero.

#### Kevin Sullivan (Oct 30 2018 at 03:20):

Also, when I'm proving a set membership proposition, such as x \in S, what can I do to have the goal rewritten as the underlying proposition, e.g., x = 1 \/ x = 2 \/ false, for the claim that x \in {1, 2}?

#### Simon Hudon (Oct 30 2018 at 03:32):

1) have you tried `norm_num`

from `tactic.norm_num`

?

2) have you tried `simp`

?

#### Kevin Buzzard (Oct 30 2018 at 07:53):

If 50 and 40 are nats then because equality is decidable on nat you can do `example : 50 = 40 → false := dec_trivial`

`

#### Kenny Lau (Oct 30 2018 at 07:54):

but that isn't the fastest way

#### Kevin Buzzard (Oct 30 2018 at 07:54):

no but it is the canonical way

#### Kevin Buzzard (Oct 30 2018 at 07:54):

and it scores highly for clean as well

#### Kevin Buzzard (Oct 30 2018 at 07:57):

As for the other question, `x ∈ ({1, 2} : set ℕ)`

is *definitionally equal* to `x = 2 ∨ x = 1 ∨ false`

and you can just treat the goal like it said this, e.g.

example (x : ℕ) (H : x = 1) : x ∈ ({1, 2} : set ℕ) := begin right, left, assumption end

#### Kevin Buzzard (Oct 30 2018 at 07:58):

The pretty printer assumes you'd rather see `x ∈ {1, 2}`

so leaves it like that. If you want to explicitly change it then you can use `change`

, a tactic which will change the goal to a definitionally equal goal.

example (x : ℕ) (H : x = 2) : x ∈ ({1, 2} : set ℕ) := begin change x = 2 ∨ x = 1 ∨ false, left, assumption end

#### Kevin Sullivan (Oct 30 2018 at 17:00):

Thank you. Up until now I've avoided using anything that my (mostly) young undergraduates won't understand from first principles. But now, it's time for black box tactics. I won't be able to explain dec_trivial to them, but it is clean and is supported in the standard libraries. As for "change," thanks for that. I was trying unfold, but it didn't get me all the way to the disjunction that defines a set.

#### Mario Carneiro (Oct 30 2018 at 17:23):

I think `dec_trivial`

has a clean explanation in the type theory. Roughly, there is a term of type `nat -> nat -> bool`

that says whether two natural numbers are equal or not, and we assert that this is `tt`

by refl, so in order for the `dec_trivial`

term to typecheck it forces computation of this function. The function itself is easy to define by recursion on the natural numbers.

#### Kevin Buzzard (Oct 30 2018 at 19:50):

--set_option pp.notation false example (x : ℕ) (H : x = 2) : x ∈ ({1, 2} : set ℕ) := begin unfold has_mem.mem, unfold set.mem, unfold has_insert.insert, unfold set.insert, unfold has_mem.mem, unfold set.mem, unfold singleton, unfold has_insert.insert, unfold set.insert, unfold has_mem.mem, unfold set.mem, unfold has_emptyc.emptyc, left, assumption end

We don't quite land at where you want though, the goal ultimately is

{b : ℕ | b = 2 ∨ {b : ℕ | b = 1 ∨ false} b} x

When I knew less about Lean, I used to write code which looked like this a lot, and then when I'd finished doing all the unfolding I'd just replace it all with a `change`

(or `show`

-- they're the same I think, although `change ... at h`

works with hypotheses too).

#### Mario Carneiro (Oct 30 2018 at 20:08):

you should unfold `set_of`

too

#### Kevin Buzzard (Oct 30 2018 at 20:10):

I should have switched `pp.notation false`

back on one last time!

#### Kevin Buzzard (Oct 30 2018 at 20:10):

--set_option pp.notation false example (x : ℕ) (H : x = 2) : x ∈ ({1, 2} : set ℕ) := begin unfold has_mem.mem, unfold set.mem, unfold has_insert.insert, unfold set.insert, unfold has_mem.mem, unfold set.mem, unfold singleton, unfold has_insert.insert, unfold set.insert, unfold has_mem.mem, unfold set.mem, unfold has_emptyc.emptyc, unfold set_of, -- ⊢ x = 2 ∨ x = 1 ∨ false left, assumption end

#### Mario Carneiro (Oct 30 2018 at 20:13):

also you can make that shorter by making one big `unfold`

#### Mario Carneiro (Oct 30 2018 at 20:13):

since you won't have to cycle back through the same things

#### Kevin Buzzard (Oct 30 2018 at 20:16):

example (x : ℕ) (H : x = 2) : x ∈ ({1, 2} : set ℕ) := begin unfold has_mem.mem set.mem has_insert.insert set.insert singleton set_of has_emptyc.emptyc, -- ⊢ x = 2 ∨ x = 1 ∨ false left, assumption end

I never knew that. I knew I could put them all in one line but I hadn't appreciated that `unfold x y z`

behaved differently to `unfold x, unfold y, unfold z`

#### Chris Hughes (Oct 30 2018 at 20:28):

example (x : ℕ) : x = 2 -> x ∈ ({1, 2} : set ℕ) := or.inl

Last updated: May 16 2021 at 21:11 UTC