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.