Stream: Coq users

Topic: wrong statement

zohaze (Dec 09 2022 at 15:52):

IH1 : false = true -> false = true
goal: false = true
Above IH1 may helpful in solving goal statement?

Patrick Nicodemus (Dec 09 2022 at 18:08):

No, it is not possible to prove the given goal from the assumption.

Patrick Nicodemus (Dec 09 2022 at 18:10):

You cannot prove something which is contradictory (false = true) unless your assumptions are themselves contradictory.

However, it is not a contradiction that (false = true -> false = true). This is perfectly sound, it is a tautology of propositional logic

zohaze (Dec 10 2022 at 17:32):

when we have false=true in hypothesis, then we can prove any thing from it. Then why i am unable to prove false=true here?
Is there any difference between false=true & false=true->false=true?

Pierre Castéran (Dec 10 2022 at 17:57):

Your sentence "we have false=true in hypothesis" is quite ambiguous. The contradiction holds when your hypothesis is just false=true. But, as Patrick mentionned, a proposition which may contain false=true, like false=true -> false= true, may be non-contradictory.

Goal false = true -> 2 = 3.
intro; discriminate.
Qed.
Goal (false = true -> false = true) -> 2= 3.
intro H;  discriminate H. (* stuck *)
Abort.

Last updated: Oct 13 2024 at 01:02 UTC