Zulip Chat Archive

Stream: new members

Topic: Single `.` in place of proof


view this post on Zulip Eric Wieser (Jul 27 2020 at 13:21):

I just found this in mathlib (modulo notation which I removed to make a #mwe)

theorem cons_ne_nil (a : ) (l : list ) : list.cons a l  list.nil.

What does . mean?

view this post on Zulip Mario Carneiro (Jul 27 2020 at 13:27):

it means nothing, it just ends the definition. The actual proof is an empty pattern match

view this post on Zulip Eric Wieser (Jul 27 2020 at 13:31):

An empty pattern match in that there are zero instances of false to match against?

view this post on Zulip Eric Wieser (Jul 27 2020 at 13:41):

I'm puzzled because it seems there is something to match against:

example (a : ) (l : list ) : list.cons a l  list.nil
| h := begin
  sorry
end

view this post on Zulip Mario Carneiro (Jul 27 2020 at 13:47):

It's matching on the equality, and the only constructor for equality, rfl, is not type correct, so no match arms are needed

view this post on Zulip Mario Carneiro (Jul 27 2020 at 13:47):

example (a : ) (l : list ) : list.cons a l  list.nil
| h := by cases h

view this post on Zulip Utensil Song (Jul 27 2020 at 13:53):

@Eric Wieser Check out https://leanprover.zulipchat.com/#narrow/stream/240192-Berkeley-Lean.20Seminar/topic/Periods.20at.20the.20end.20of.20statements


Last updated: May 07 2021 at 00:30 UTC