0
$\begingroup$

According to the documentation, there should be a Lemma le_not_gt_iff in Coq.Structures.OrdersFacts, but I haven't succeeded in referencing it.

I am trying to prove 2 < 1 → False as part of a proof. I tried Nat.order tactic but it didn't work.

So now I am looking into Coq.Structures.OrdersFacts to find another Lemma that can help, and found le_not_gt_iff.

The problem I have is that the import

Require Import Coq.Structures.OrdersFacts.

doesn't seem to be enough to have access to the Lemma. I see it seems to be encapsulated in a module definition OrderedTypeFullFacts, but I don't know how to import that.

$\endgroup$

1 Answer 1

1
$\begingroup$

Unless there are educational reasons for not using it, I would use the lia tactic:

Require Import Lia.
Goal  2 < 1 -> False.
lia.
$\endgroup$
2
  • $\begingroup$ Perfect, that worked. There is no educational reason, I am just a beginner that didn't know lia existed. $\endgroup$
    – kutschkem
    Commented Jul 3 at 8:41
  • $\begingroup$ You will like lia - as long as you don't multiply variables (lia is for "linear integer arithmetic" - multiplication with constants is fine) it can solve most complicated networks of equalities, inequalities and a bit of logic. $\endgroup$
    – M Soegtrop
    Commented Jul 3 at 8:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.