Noob: 50 = 40 -> false

Stream: new members

[Kevin Sullivan]

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]

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]

1) have you tried norm_num from tactic.norm_num?
2) have you tried simp?

[Kevin Buzzard]

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

[Kenny Lau]

but that isn't the fastest way

[Kevin Buzzard]

no but it is the canonical way

[Kevin Buzzard]

and it scores highly for clean as well

[Kevin Buzzard]

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]

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]

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]

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]

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

you should unfold set_of too

[Kevin Buzzard]

I should have switched pp.notation false back on one last time!

[Kevin Buzzard]

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

also you can make that shorter by making one big unfold

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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