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.
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.