Stream: Coq users

Topic: contradiction ?


view this post on Zulip zohaze (Jun 18 2023 at 13:16):

H: (In n l ->
f1 a c = true->
 true = false\/ false=true).

while a c n:nat. What is the meaning of H . Secondly, i can write it as below

H: (In n l ->
f1 a c=true->
 true = false)->False.

view this post on Zulip bubble sort now (Jun 18 2023 at 16:10):

thanks for writing in. could you post the whole file you're working on

view this post on Zulip Pierre Castéran (Jun 18 2023 at 18:12):

You can't replace the hypothesis H with your second proposition, which is equivalent to the negation of the first H.

view this post on Zulip zohaze (Jun 19 2023 at 14:44):

If i cannot replace H ,then how it could be useful? Under what conditions it happens? Now i have In n l & f1 a c = true in hypothesis.
There is no way to close sub lemma on the basis of H?

view this post on Zulip Pierre Castéran (Jun 19 2023 at 15:19):

If you post the whole Coq script (as we asked a lot of times), we could try to answer.
Otherwise, we cannot comment on the context, initial goal, etc., which we are not supposed to guess (for multiple reasons: it takes useless time, and we cannot be sure of guessing the "right" information).
If this subgoal really appears in a Coq session, please post the script which generated it.

view this post on Zulip Paolo Giarrusso (Jun 19 2023 at 18:04):

also you've never explained why you don't post the real code, even if we've probably been asking for years

view this post on Zulip Paolo Giarrusso (Jun 19 2023 at 18:05):

That conclusion isn't created by magic, Coq just executes your tactics — maybe some definition is more complex than needed, maybe those are fine and they just simplify to this thing, we can't tell.

view this post on Zulip Paolo Giarrusso (Jun 19 2023 at 18:06):

All we can say is that false = true <-> False etc


Last updated: Jun 13 2024 at 19:02 UTC