# Simple Coq help

**URL:** <https://discourse.rocq-prover.org/t/simple-coq-help/2509>\
**Category:** Using Rocq\
**Created:** [January 14, 2025, 8:37pm UTC](https://discourse.rocq-prover.org/t/simple-coq-help/2509 "2025-01-14T20:37:24Z")\
**Posts on this page:** 7\
**Page:** 1

<div class="post-metadata">

**Author:** ![Lilipop](https://avatars.discourse-cdn.com/v4/letter/l/8491ac/32.png) [@Lilipop](https://discourse.rocq-prover.org/u/Lilipop)\
**Post date:** [January 14, 2025, 8:37pm UTC](https://discourse.rocq-prover.org/t/simple-coq-help/2509/1 "2025-01-14T20:37:24Z")

</div>

Hi all,

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

These first three should be proved using the given definition:

```coq
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:

```coq
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:

```coq
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!

---

<div class="post-metadata">

**Author:** ![thomas-lamiaux](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/thomas-lamiaux/32/982_2.png) [@thomas-lamiaux](https://discourse.rocq-prover.org/u/thomas-lamiaux)\
**Post date:** [January 14, 2025, 8:56pm UTC](https://discourse.rocq-prover.org/t/simple-coq-help/2509/2 "2025-01-14T20:56:21Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![Lilipop](https://avatars.discourse-cdn.com/v4/letter/l/8491ac/32.png) [@Lilipop](https://discourse.rocq-prover.org/u/Lilipop)\
**Post date:** [January 14, 2025, 9:57pm UTC](https://discourse.rocq-prover.org/t/simple-coq-help/2509/3 "2025-01-14T21:57:03Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![davidjao](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/davidjao/32/866_2.png) [@davidjao](https://discourse.rocq-prover.org/u/davidjao)\
**Post date:** [January 15, 2025, 3:13am UTC](https://discourse.rocq-prover.org/t/simple-coq-help/2509/4 "2025-01-15T03:13:38Z")

</div>

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

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

---

<div class="post-metadata">

**Author:** ![ybertot](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ybertot/32/61_2.png) [@ybertot](https://discourse.rocq-prover.org/u/ybertot)\
**Post date:** [January 15, 2025, 8:02am UTC](https://discourse.rocq-prover.org/t/simple-coq-help/2509/5 "2025-01-15T08:02:52Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![thomas-lamiaux](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/thomas-lamiaux/32/982_2.png) [@thomas-lamiaux](https://discourse.rocq-prover.org/u/thomas-lamiaux)\
**Post date:** [January 15, 2025, 8:42am UTC](https://discourse.rocq-prover.org/t/simple-coq-help/2509/6 "2025-01-15T08:42:44Z")

</div>

> [@Lilipop](#):
>
> could you give more details please.

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 `k`does 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

---

<div class="post-metadata">

**Author:** ![Lilipop](https://avatars.discourse-cdn.com/v4/letter/l/8491ac/32.png) [@Lilipop](https://discourse.rocq-prover.org/u/Lilipop)\
**Post date:** [January 16, 2025, 8:36am UTC](https://discourse.rocq-prover.org/t/simple-coq-help/2509/7 "2025-01-16T08:36:41Z")

</div>

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