coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: frank maltman <frank.maltman AT googlemail.com>
- To: <coq-club AT inria.fr>
- Subject: [Coq-Club] Contradicting Zneg p >= 2
- Date: Wed, 8 Jun 2011 11:33:09 +0000
- Domainkey-signature: a=rsa-sha1; c=nofws; d=googlemail.com; s=gamma; h=date:from:to:subject:message-id:x-mailer:mime-version:content-type :content-transfer-encoding; b=kZqztzTqE2D8REzUdI7j6217/Zb6RWPDGzQciEB3FfnoZ6Om2HO3hvcnpMk23ZCozS OR7qKADrkc7nIw4PKEQf6Ke/uHDZAW8oM+EIX2KxtFRIwQ6eAd3xmHWh8kixGgCUG0aS 5DqOZiWbqoUqhEuS44j4UWUMBHdN4X5TFiDBM=
Hello.
Given:
p : positive
HM : Zneg p >= 2
============================
0 < 0
I have a proof of Zneg p < 2:
> Check (Zlt_le_trans (Zneg p) 0 2 (Zlt_neg_0 p) (Zlt_le_weak 0 2 (Zgt_lt 2 0
> (Zgt_pos_0 2)))).
Zlt_le_trans (Zneg p) 0 2 (Zlt_neg_0 p)
(Zlt_le_weak 0 2 (Zgt_lt 2 0 (Zgt_pos_0 2)))
: Zneg p < 2
According to the manual, I use the 'contradict' tactic to show that
the context contains an inconsistent hypothesis:
p : positive
============================
~ Zneg p >= 2
How do I get from a proof of 'Zneg p < 2' to a proof of '~ Zneg p >= 2'?
There seem to be various lemmas in Coq.ZArith.Zorder but I'm looking for
something matching:
forall m n : Z, m < n -> ~ m >= n.
... and can't find it (seems to have just about every other combination
but that one).
- [Coq-Club] Contradicting Zneg p >= 2, frank maltman
- Re: [Coq-Club] Contradicting Zneg p >= 2,
Evgeny Makarov
- Re: [Coq-Club] Contradicting Zneg p >= 2, frank maltman
- Re: [Coq-Club] Contradicting Zneg p >= 2,
Evgeny Makarov
Archive powered by MhonArc 2.6.16.