## 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):

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: Jun 20 2024 at 13:02 UTC