CODEWITHSUNDEEP
coqproofcoq-tactic
Rakeeb Hossain
Rakeeb Hossain

Reputation: 363

Coq: Proving relation between < and ≤

I am learning Coq right now and in a larger proof I have become stumped by the following sub-proof:

  Theorem sub : ∀ n m : nat, n ≤ m → n ≠ m → n < m.

Or, once unfolded:

  Theorem sub : ∀ n m : nat, n ≤ m → n ≠ m → S n ≤ m.

Here, "n ≤ m" is inductively defined as follows:

  Inductive le : nat → nat → Prop :=
  | le_n : ∀ n : nat, le n n
  | le_S : ∀ n m : nat, (le n m) → (le n (S m)).

I have not gotten very far, but my attempt looks like this:

  Theorem sub : ∀ n m : nat, n ≤ m → n ≠ m → n < m.
  Proof.
    unfold lt.
    intro n.
    induction n.
    - induction m.
      + intros. exfalso. contradiction.
      + admit.
    - admit.
  Admitted.

In the first inductive step (marked by the first admit), the inductive hypothesis shows the following :

1 subgoal
m : nat
IHm : 0 ≤ m → 0 ≠ m → 1 ≤ m
______________________________________(1/1)
0 ≤ S m → 0 ≠ S m → 1 ≤ S m

I am not sure how I can leverage this hypothesis to prove the subgoal. I would appreciate any guidance in the right direction.

Upvotes: 2

Views: 745

Answers (1)

SCappella
SCappella

Reputation: 10414

Since le is defined as an inductive predicate, it makes more sense to do the induction on that, rather than n. le doesn't make any references to 0 or even S n (it does have S m), so induction on n is probably not the way to go. Induction on m might work, but it's probably harder than necessary.

Before starting a formal proof, it can often be helpful to think about how you would prove this informally (still using the same definitions, though). If you assume that n ≤ m, then by the inductive definition of lt, this means that either n and m are the same, or m is the successor of some number m' and n is less than or equal to m' (can you see why the definition of lt implies this?). In the first case, we'll have to use the additional hypothesis that n ≠ m to derive a contradiction. In the second case, we won't even need that. n ≤ m' implies that S n ≤ S m', so since m = S m', S n ≤ m, i.e., n < m.

For the formalization, we'll have to prove that assumption on the last line that n ≤ m implies S n ≤ S m. You should try a similar informal analysis to prove it. Other than that, the informal proof should be straightforward to formalize. Case analysis on H: n ≤ m is just destruct H..

One more thing. This isn't essential, but can often help in the long run. When defining an inductive type (or predicate), if you can factor out a parameter that's used the same way in each constructor, it can make the induction principle more powerful. The way you have it with le, n is universally quantified and used the same way for both constructors. Every instance of le starts with le n.

  Inductive le : nat → nat → Prop :=
  | le_n : ∀ n : nat, le n n
  | le_S : ∀ n m : nat, (le n m) → (le n (S m)).

That means that we can factor out that index into a parameter.

  Inductive le' (n: nat) : nat → Prop :=
  | le_n' : le' n n
  | le_S' : ∀ m : nat, (le' n m) → (le' n (S m)).

This gives you a slightly simpler/better induction principle.

le'_ind
     : forall (n : nat) (P : nat -> Prop),
       P n ->
       (forall m : nat, le' n m -> P m -> P (S m)) ->
       forall n0 : nat, le' n n0 -> P n0

Compare this to le_ind.

le_ind
     : forall P : nat -> nat -> Prop,
       (forall n : nat, P n n) ->
       (forall n m : nat, le n m -> P n m -> P n (S m)) ->
       forall n n0 : nat, le n n0 -> P n n0

Basically what's happening here is that with le_ind, you have to prove everything for every n. With le'_ind, you only need to prove it for the particular n that you're using. This can sometimes simplify proofs, though it's not necessary for the proof of your theorem. It's a good exercise to prove that these two predicates are equivalent.

Upvotes: 3

Related Questions