Simple Coq help

Using Coq
1

Hi all,

I am having some hard time with the following lemmas, any help would be appreciated :frowning:

These first three should be proved using the given definition:

Module OrderNat.
Definition le (n m : nat) := exists p, n + p = m.
Infix "<=" := le.

Lemma le_succ_r : forall n m : nat, n <= S m <-> n <= m \/ n = S m.
Proof.
intros.
split.
  + intros. unfold le in H. destruct H as [p Hp]. destruct p.
    - rewrite -> add_0_r in Hp. right. exact Hp.
    - left. 
Admitted.

Lemma nle_succ_diag_l : forall n : nat, ~ S n <= n.
Proof.
intros.
  unfold not.
  unfold le. intros. destruct H as [p Hp]. simpl in Hp. 
  rewrite <- add_succ_r in Hp.
  induction n.
  + simpl in Hp. discriminate.
  + apply IHn.
Admitted

Lemma le_antisymm : forall n m, n <= m -> m <= n -> n = m.
Proof.
intros n m.
  unfold le. intros.
  destruct H as [p1 H1].
  destruct H0 as [p2 H2].
Admitted.

And these should be done using this:

Module NatOrderDef.

Inductive le (n : nat) : nat -> Prop :=
  | le_n : le n n
  | le_S : forall m, le n m -> le n (S m).

End NatOrderDef.

Lemma le_add_l : forall n m, n <= m + n.
Proof.
intros.
  induction n.
  + rewrite -> add_0_r.
    apply le_0_l.
  + rewrite -> add_succ_r.
    destruct m.
    * simpl. apply le_n.
    * apply le_S. 
Admitted.

Lemma le_trans : forall n m p, n <= m -> m <= p -> n <= p.
Proof.
intros.
  induction n.
  + induction p.
    - apply le_n.
    - apply le_S. apply le_0_l.
Admitted.

And finally, the trick in these is to use the tactic ā€œinversionā€, but I think I am doing it wrong:

Lemma le_succ_l : forall n m, S n <= m -> n <= m.
Proof.
  intros.
  inversion H. 
  - apply le_S. apply le_n.
  - rewrite -> H1. inversion H. 
    * apply le_S.
Admitted.

Lemma succ_le_mono : forall n m, n <= m <-> S n <= S m.
Proof.
  split. 
  + intros. inversion H.
    * apply le_n.
    * apply le_S. apply le_succ_r.
Admitted.

Lemma le_antisymm : forall n m, n <= m -> m <= n -> n = m.
Proof.
  intros. 
  inversion H H0. 
  + reflexivity.
Admitted.

Thanks for the precious help!

2

Hi, for the first proof you will need either the tactic injection that simplifies equalities, or to rewrite by the lemma S n = S m -> n = m. For the converse direction, you will need the tactic exists n. It should work similarly for the rest of the proofs. Donā€™t hesitate to check out zulip for short questions and more interactive discussions.

3

It is a bit unclear to me how an exists n can solve all the proofs? could you give more details please.
PS: thanks for the zulip information, I did not know that.

4

Hereā€™s the first proof (and only the first proof), in case you need an example to get started.

From Coq Require Import PeanoNat.
Import Nat.

Module OrderNat.
Definition le (n m : nat) := exists p, n + p = m.
Infix "<=" := le.

Lemma le_succ_r : forall n m : nat, n <= S m <-> n <= m \/ n = S m.
Proof.
intros.
split.
  - intros. unfold le in H. destruct H as [p Hp]. destruct p.
    + rewrite -> add_0_r in Hp. right. exact Hp.
    + left.
      exists p.
      rewrite add_succ_r in Hp.
      injection Hp.
      trivial.
  - intros [H | H].
    + destruct H as [p Hp].
      exists (S p).
      subst.
      rewrite add_succ_r.
      reflexivity.
    + exists 0.
      subst.
      rewrite add_0_r.
      reflexivity.
Qed.
1 Like
5

I believe you should first try to come up with a convincing proof in English, and then see I you would translate that English proof into a the Coq language.

So for the first proof. Letā€™s look at the left-to-right direction first. n <= S m means S m = n + p for some p. There are two cases for p, either p = 0 or p = S q for some q. If p = 0, then S m = n + 0, which is the same as S m = n, and thus the right-hand side of your disjunction. If p = S q, then S m = n + S q, and thus S m = S (n + q), so we can deduce m = n + q because S is injective. Now, letā€™s try to collect the important facts:

  • n + 0 = n, how do you know that?
  • n + S q = S (n + q), how do you know that?
  • S a = S b -> a = b, how do you know that?

You already found out that you needed a theorem called Nat.add_0_r (you probably imported the Nat module). You should normally be able to find the other two theorems by using Search. Here are the directive I suggest.

Require Import Arith.
Search (_ + S _).
Search (S _ = S _).

It seems you got stuck at the step of finding and using this injection lemma.

In the end you will need to prove n <= m by exhibiting the difference between these two numbers. If S m = n + S q, then the difference between the two numbers is q, so you will need exists p.

Advanced users often avoid relying on lemmas such as eq_add_S or Nat.succ_inj, because the tactic injection has the same effect, and you do not need to know or find the name of a specific theorem. I suggest that you lookup the documentation for that tactic.

6

If you want to prove exist p, n = p + m, then exists k basically says there is such a p and it is k, it will then ask to prove that indeed n + k = m. Note, that kdoes not have to be a variable, it could be S (S m) or sth

PS: sorry I did not mean it was going to solve it all automatically, just that you will need this two tactics among the others that you probably already know

1 Like
7

Thanks a lot for all the help, I managed to do most of the lemmas. I was missing the injection tactic for sure!