Zulip Chat Archive

Stream: new members

Topic: getting from 2 = 1 to false


view this post on Zulip Matt Diamond (Jan 14 2021 at 21:40):

I was working on a simple proof by contradiction and got to the point where I was able to generate the hypothesis h : 2 = 1. On a whim I tried cases h and it closed out the goal (which was false). So I have two questions:
1) why did cases work here?
2) is there a better or more "correct" way to get from 2 = 1 to false? I figure I'm probably missing something embarrassingly obvious...

view this post on Zulip Marcus Rossel (Jan 14 2021 at 21:43):

(deleted)

view this post on Zulip Alex J. Best (Jan 14 2021 at 21:45):

cases seems fine in this situation, if the numbers were bigger using tactic#norm_num would be better.

view this post on Zulip Alex J. Best (Jan 14 2021 at 21:45):

For example:

example (h : 200000 = 1000000) : false :=
begin
  norm_num at h,
end

works, but

example (h : 200000 = 1000000) : false :=
begin
  cases h,
end

gives
deep recursion was detected at 'expression equality test' (potential solution: increase stack space in your system), not so fun

view this post on Zulip Riccardo Brasca (Jan 14 2021 at 22:01):

If your question is why Lean can prove this "by cases", this is because N is an inductive type: a natural number is 0 or of the form succ n for some n : N. cases is smart enough to write 1 as succ 0 and 2 as succ 1 = succ (succ 0) and it also knows that succ is injective (this is quite subtle point I think, related to no_confusion).

view this post on Zulip Riccardo Brasca (Jan 14 2021 at 22:09):

This is analogous to having a finite set S={a,b}S = \{a, b\} and saying that, given xSx \in S, we have x=ax=a or x=bx=b. Even if for a human being (at least, for me) these two situations are rather different, for Lean they are very similar, a finite type is an inductive type where you can enumerate all elements.

view this post on Zulip Riccardo Brasca (Jan 14 2021 at 22:09):

See for example https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html

view this post on Zulip Matt Diamond (Jan 14 2021 at 22:12):

that makes sense

view this post on Zulip Matt Diamond (Jan 14 2021 at 22:13):

thank you both for the helpful answers!


Last updated: May 10 2021 at 00:31 UTC