Stream: Coq users

Topic: contra conditions


view this post on Zulip pianke (Mar 28 2023 at 02:42):

I have function with two arguments. Its output may be true or false. I have destruct it as (f a b) eqn:eq1 and another condition like eq2.
Now in hypothesis i have 2 conditions
eq1:statement
eq2:statement
In the presence of (eq1 ) eq2 can't exist. Therefore i have written it as
eq1's statement ->
eq2's statement->False.
But when i apply it, i get message" it is not an inductive type ". What is the meaning of this. We can extract any thing from False?

view this post on Zulip Laurent Théry (Mar 28 2023 at 10:23):

There are two tactics exfalso and contradiction that can help you.

view this post on Zulip pianke (Mar 28 2023 at 16:55):

Thanks. It works. But when i applied inversion H then why it is not working?

view this post on Zulip Laurent Théry (Mar 28 2023 at 17:05):

What is H?

view this post on Zulip pianke (Mar 28 2023 at 17:09):

Above false statements.(eq1's statement -> eq2's statement->False)

view this post on Zulip Laurent Théry (Mar 28 2023 at 17:26):

exfalso; apply H does not work?


Last updated: Jun 16 2024 at 01:42 UTC