pianke (Mar 28 2023 at 02:42): 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?
Laurent Théry (Mar 28 2023 at 10:23):There are two tactics exfalso and contradiction that can help you.
pianke (Mar 28 2023 at 16:55):Thanks. It works. But when i applied inversion H then why it is not working?
Laurent Théry (Mar 28 2023 at 17:05):What is H?
pianke (Mar 28 2023 at 17:09):Above false statements.(eq1's statement -> eq2's statement->False)
Laurent Théry (Mar 28 2023 at 17:26):exfalso; apply H does not work?
Last updated: Apr 19 2024 at 10:02 UTC