2
$\begingroup$

Suppose that I have a hypothesis H1 : a > y and another hypothesis H2 : a <= y in Coq. I want to use the fact that combining these hypothesis is an instance of False so that I get to prove my goal automatically. How should I do it ? (btw, assume that both a and y are nat).

$\endgroup$

4 Answers 4

3
$\begingroup$

If you choose to use gt_not_le_stt, you don't need to destruct a nor y.

  Goal forall a y, a > y -> a <= y -> False.
Proof.
 intros a y H H0.
 apply Arith_prebase.gt_not_le_stt in H. 
 exact (H H0).
Qed.

Of course, there are a lot of other solutions, depending on the libraries, tactics and lemmas you choose to use (including the magic lia).

$\endgroup$
2
$\begingroup$

There are several quicker solutions.

Require Import PeanoNat.
Lemma helper : forall a y, a > y -> a <= y -> False.
Proof.
  intros a y H.
  apply Nat.nle_gt. (* Coq guesses the direction of <-> to use *)
  exact H. (* conversion between > and < *)
Qed.

For these simple linear inequalities, there is lia.

Require Import Lia.
Lemma helper' : forall a y, a > y -> a <= y -> False.
Proof. lia. Qed.
$\endgroup$
2
$\begingroup$

As mentioned by @Pierre Casteran, there are multiple possible versions. For the record, here is a simple mathcomp-based one.

From mathcomp Require Import all_ssreflect. 

Lemma helper : forall a y, a > y -> a <= y -> False.
Proof. by  move=> a y ay; rewrite leqNgt ay. Qed.
$\endgroup$
1
$\begingroup$

whatever .. here's a long-cut...

Lemma helper : forall a y, a > y -> a <= y -> False.
Proof.
    intros. destruct y.
    - destruct a.
        + apply Arith_prebase.gt_irrefl_stt in H. destruct H.
        + apply Arith_prebase.le_n_0_eq_stt in H0.
            rewrite H0 in H. apply Arith_prebase.gt_irrefl_stt in H. destruct H.
    - destruct a.
        + apply Arith_prebase.gt_not_le_stt in H. unfold not in H.
            apply H in H0. destruct H0.
        + apply Arith_prebase.gt_not_le_stt in H. unfold not in H.
            apply H in H0. destruct H0.
Qed.
$\endgroup$

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.