# Prove antisymmetry of leq from scratch

This question is based on an assignment for one of my university modules that used Coq. The module is now over, so I now feel free to extend the given code for my own pursuits.

I want to prove some theorems within Peano arithmetic from scratch. To that end, I am not importing any libraries. Rather I define the following:

``````Inductive nat : Set :=
| O : nat
| S : nat -> nat.

Inductive leq: nat -> nat -> Prop :=
| leq_eq: forall n, leq n n
| leq_succ: forall n m, leq n m -> leq n (S m).

Fixpoint plus (n m: nat) : nat :=
match m with | O => n | S p => S (plus n p) end.
``````

I’ve hit a snag when trying to prove the following theorem:

``````Theorem leq_antisymmetric2: forall m n, leq m n /\ leq n m -> m = n.
Proof. intros. destruct H. induction H. reflexivity.
assert (leq (S m) m). apply (leq_transitive (S m) n m). auto.
...
``````

After running the commands shown my current context looks like this:

``````1 subgoal
n, m : nat
H : leq n m
H0 : leq (S m) n
IHleq : leq m n -> n = m
H1 : leq (S m) m
______________________________________(1/1)
n = S m
``````

I know `leq (S m) m` should be false but I can’t formalise it in Coq. How can I do this? Or is there a simpler way to prove `leq_antisymmetric2`?

I already have the following theorems proven:

• basic laws related to the successor function
• transitivity of `leq` (as `leq_transitive`)
• `leq n O -> n = O` and `leq O n`
• `leq n (plus n p)`, called `leq_plus` – I think I can use this, but how do I instantiate an existential quantification within `H1`?

You can certainly prove a lemma of the form:

``````Lemma leq_S_neg : forall n, (S n) n -> False.
``````

Then, you can apply that lemma to `H1` to obtain `False` as a hypothesis, at which point you can easily discharge the contradiction.

I certainly can prove `leq_S_neg`. However, right now I need to use this other theorem relating the order to addition:

``````Theorem leq_addition: forall m n, leq m n -> exists p, plus m p = n.
Proof. intros. induction n as [| n H0].
inversion H. exists O. apply left_identity_plus.
inversion H. exists O. apply right_identity_plus.
destruct H0. apply H3. exists (S x). simpl. rewrite H0.
reflexivity. Qed.
``````

This looks rather ugly, and I want to avoid its use. Is it possible and if so how?

In particular, if I could use `leq_plus` to turn `leq (S m) m` into something like

``````x: nat
H2: plus (S m) x = m
``````

then my task would become easier.

Turning an hypothesis `leq (S m) m` into `plus (S m) x = m` requires `leq_addition` (you need `A -> B` to turn hypothesis `A` into `B`).

Concerning your proof of antisymmetry. One possibility (probably not the best) is the following:

1. prove `forall n m, leq (S n) (S m) -> leq n m`
2. prove antisymmetry by `induction m; destruct n`

Tell me if you need more details.

Well, I eventually decided that it was fine to leave `leq_addition` and its converse `addition_leq` in the code, because it made proving certain other facts much easier (reasoning on equality, not propositions). I proved `addition_leq` using `leq_plus` in a simple way.

So I proved `leq_succ_neg`:

``````Lemma leq_succ_neg: forall n, leq (S n) n -> False.
Proof. intros. apply leq_addition in H. destruct H.
rewrite <- successor_shift in H. rewrite <- right_identity_plus in H.
apply (plus_cancellative n (S x) O) in H. inversion H. Qed.
``````

and then just completed `leq_antisymmetric2` by adding `apply leq_succ_neg in H1. contradiction. Qed.` to what I wrote in the thread opener.

Another, larger problem I had been facing was how to prove the cancellation law for multiplication. I eventually completed it with even more help from the Gitter chat:

``````Theorem mul_cancellative: forall m n p, mul m (S p) = mul n (S p) -> m = n.
Proof. induction m; destruct n; intro p. auto.
rewrite left_annihilator_mul. intro.
symmetry in H. apply mul_zero_zero in H. destruct H. auto. inversion H.
rewrite left_annihilator_mul. intro.
apply mul_zero_zero in H. destruct H. auto. inversion H.
simpl. intro. apply succ_eq_succ in H.
rewrite mul_commutative in H. simpl in H.
rewrite (plus_commutative (mul p m) p) in H. rewrite plus_associative in H.
rewrite (mul_commutative (S n) p) in H. simpl in H.
rewrite (plus_commutative (mul p n) p) in H. rewrite plus_associative in H.
apply plus_cancellative in H.
rewrite mul_commutative in H. rewrite (mul_commutative p n) in H.
simpl in IHm. apply IHm in H.
rewrite H. reflexivity. Qed.
``````

Here is a gist with all the theorems I’ve proven in Peano arithmetic, using Coq, from scratch – including all the theorems discussed above.