Stream: Coq users

Topic: ✔ how to prove trivial theorem with ssreflect

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.

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.

Andrey Klaus (Aug 19 2021 at 12:19):

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

Notification Bot (Aug 19 2021 at 12:19):

Andrey Klaus has marked this topic as resolved.

Notification Bot (Aug 19 2021 at 12:20):

Andrey Klaus has marked this topic as unresolved.

Notification Bot (Aug 19 2021 at 12:20):

Andrey Klaus has marked this topic as resolved.

Last updated: Apr 18 2024 at 09:02 UTC