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