Zulip Chat Archive

Stream: new members

Topic: Noob: 50 = 40 -> false


view this post on Zulip 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.

view this post on Zulip 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}?

view this post on Zulip Simon Hudon (Oct 30 2018 at 03:32):

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

view this post on Zulip 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
`

view this post on Zulip Kenny Lau (Oct 30 2018 at 07:54):

but that isn't the fastest way

view this post on Zulip Kevin Buzzard (Oct 30 2018 at 07:54):

no but it is the canonical way

view this post on Zulip Kevin Buzzard (Oct 30 2018 at 07:54):

and it scores highly for clean as well

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Mario Carneiro (Oct 30 2018 at 20:08):

you should unfold set_of too

view this post on Zulip Kevin Buzzard (Oct 30 2018 at 20:10):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 30 2018 at 20:13):

also you can make that shorter by making one big unfold

view this post on Zulip Mario Carneiro (Oct 30 2018 at 20:13):

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

view this post on Zulip 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

view this post on Zulip 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