Theorem Proofs in Coq

Background

I am learning assistance, Coq, on my own. So far, I have completed reading Yves Bertot's Coq in a Hurry. Now, my goal is to prove some basic results concerning the natural numbers, culminating with the so-called division algorithm. However, I have encountered some setbacks on my way towards that goal. In particular, the two following results have proved (pun intended) to be more difficult to prove in Coq than I initially imagined. In fact, I have, after many fruitless attempts, resorted to prove them by hand (as shown below). This is clearly not helping me become more proficient in handling Coq; which is why I turn to this forum. My hope is that someone on this site is able and willing to help me translate my proofs below into a proof that Coq accepts. All help is sincerely appreciated!

Theorem A

For all $x,y \in N$ \begin{equation} x y$ then $\neg \text{I}(N,x,y)$ also by definition. If $x>y$ and $y>x$ then by transitivity and reflexivity, we have $\text{I}(N,x,y)$, which is a contradiction. Consequently, no more than one of the statements is true.

We keep $y$ fixed and induct on $x$. When $\text{I}(N,0,y)$ we have $0 y$. If $x>y$, then clearly $S(x) >y$. If $\text{I}(N,x,y)$, then $S(x) >y$ (as $S(x) >x$ for all $x\in \mathbb{N}$). Finally, suppose $x or (less x y) (I N x y).


Theorem Ntrichotomy: (forall x y:N,
or (less x y) (or (I N x y) (less y x))).

Useful results

Here, I have gathered some of the results that I have defined, and proved up to this point. These are the ones that I refer to above. This is the code that I have managed to write so far, note that most consists of definitions.

```
( Sigma types )

Inductive Sigma (A:Set)(B:A -> Set) :Set :=
Spair: forall a:A, forall b : B a,Sigma A B.

Definition E (A:Set)(B:A -> Set)
(C: Sigma A B -> Set)
(c: Sigma A B)
(d: (forall x:A, forall y:B x,
C (Spair A B x y))): C c :=

match c as c0 return (C c0) with
| Spair a b => d a b
end.

( Binary sum type )

Induct

Coq is a bit more cruel than paper proofs: when you write "and we are done" or "clearly" in a paper proof, there is often much more to do to convince Coq.

Now I did a little clean up of your code, while trying to keep it in the same spirit. You can find it here.

Several remarks:

-
I used built in datatypes and definitions where I thought it wouldn't hurt your intent. Note that if I had used built-in equality instead of identity and the built in "less-than" relation, proofs would have been much easier, as many of your lemmas are in the database of known theorems, which are checked at each call of

auto with arith.

-
I used some tactics you're probably not aware of, but a "real" Coq super-user would have much more powerful tactics at hand and written her own tactics to simplify the job. I always recommend CPDT as the place to learn about using tactics in a powerful manner.

-
I used notations and tabbing to improve readability and built-in constructs like matching and the induction tactic to make things easier to prove and re-factor. In particular, your definition of less was hard to work with, you can see how I slightly modified it from
$$ \exists x,\ m + (x+1) = n $$
to the equivalent (but easier to use)
$$ \exists x,\ (x + m)+1 = n$$
this kind of "definition tweaking" happens a lot in formal proofs.

-
While you may get answers to these kinds of questions here, I highly recommend you submit your work to Coq-Club which was created with the express purpose of answering these kinds of questions.

StackExchange Computer Science Q#18765, answer score: 7