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
 identity/commutativity/associativity/cancellation of addition
 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:
 prove
forall n m, leq (S n) (S m) > leq n m
 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.