Stream: Coq users

Topic: ✔ how to prove trivial theorem with ssreflect


view this post on Zulip Andrey Klaus (Aug 19 2021 at 11:13):

Hello everyone.
What is simple way to prove a theorem below using ssreflect?

Inductive isZero : nat -> Prop := IsZero : isZero 0.
Theorem isZero_contra : isZero 1 -> False.

view this post on Zulip YAMAMOTO Mitsuharu (Aug 19 2021 at 11:45):

I would do the following:

by case E: _ /.

Probably https://sympa.inria.fr/sympa/arc/ssreflect/2014-10/msg00006.html is helpful for dealing with more complicated cases.

view this post on Zulip Andrey Klaus (Aug 19 2021 at 12:19):

Thank you very much for the example and for the link.

view this post on Zulip Notification Bot (Aug 19 2021 at 12:19):

Andrey Klaus has marked this topic as resolved.

view this post on Zulip Notification Bot (Aug 19 2021 at 12:20):

Andrey Klaus has marked this topic as unresolved.

view this post on Zulip Notification Bot (Aug 19 2021 at 12:20):

Andrey Klaus has marked this topic as resolved.


Last updated: Jan 31 2023 at 14:03 UTC