CODEWITHSUNDEEP
numberscoqproof
ewokonfire
ewokonfire

Reputation: 13

Coq: How do I prove that forall n m : nat, (n > m) -> (S n > S m)?

So I've been learning to use Coq and until now I've been using a natural type that I defined myself, and so I'm not 100% clear on what can be done with the default natural type. Program Fixpoint requires it, though, and I've ended up needing to make use of the (obvious to humans) fact that (n > m) -> (S n > S m). I can't seem to prove that though - I run something like

Theorem gt_triv : forall n m : nat, n > m -> (S n) > (S m).
intros.

and then I have a hypothesis n > m and a target proof (S n) > (S m), but I can't seem to do anything with it (other than unfold it to S (S m) <= S n, which doesn't seem much more useful) - I have no idea what commands I'd even run for that.

Thanks for any advice.

Upvotes: 0

Views: 790

Answers (3)

larsr
larsr

Reputation: 5811

Theorem gt_triv : forall n m : nat, n > m -> (S n) > (S m).
  induction 1.
  - apply le_n.
  - apply le_S, IHle.
Qed.

Upvotes: 0

Yves
Yves

Reputation: 4236

The fastest way to prove this statement is to use libraries or automated tactics that are specialized in linear integer arithmetic.

First example.

Require Import Arith.

Search (S _ > S _).  (* This is not needed, *)
  (* but this is how you can find the relevant theorem. *)

Theorem gt_triv : forall n m: nat, n > m -> S n > S m.
Proof.
exact gt_n_S.
Qed.

Another solution is to observe that the statement of gt_triv contains comparisons between affine formulas in the variables. This is covered by an existing automated tactic called lia. So another solution would have the following complete script.

Require Import Lia. 
Theorem gt_triv : forall n m: nat, n > m -> S n > S m.
Proof.
lia.
Qed.

Upvotes: 2

Tiago Campos
Tiago Campos

Reputation: 538

If you notice your theorem is a corollary of n <= m -> S n <= S m, once as you said the definition of x > y unfolds to S y <= x. So, to prove the lemma above, you just need to do induction on m.

Theorem gt_triv : forall n m : nat, n <= m -> S n <= S m.
  intros.
  (* By definition of leb in the relation n <= m, m is the only one which is 
      inductively defined, we should stick n and do induction on m *)
  generalize dependent n.
  induction m.
  intros.
  destruct n.
  apply le_n.
  (* there is no x + 1 <= 0 *)
  inversion H.
  intros.
  (* notice we need a n <= m to solve our goal, but we only have a n <= S m, therefore
      by our definition H is constructed by n <= m (by construction of le_S) or n = m (by construction of le_n)*)
  inversion H.
  (*trivially both are equal*)
  apply le_n.
  (* our induction hypothesis give us S n <= S m, so S n <= S (S m) is trivial by constructor le_S*)
  apply (le_S _ _ (IHm _ H1)).
Qed.

Now your theorem that you're trying to prove becomes very easy :

Theorem gt_really_triv : forall n m : nat, n > m -> (S n) > (S m).
intros.
apply gt_triv.
trivial.
Qed.

There are a lot of ways to prove that theorem, you don't need to use my definition. I recommend you to try one more time to prove that theorem using other approaches, for example, you can use a double induction principle on naturals.

Upvotes: 1

Related Questions