[Solved]: Theorem Proofs in Coq

Problem Detail: 

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 < S(y) \subset x < y \lor \text{I}(N,x,y) \end{equation} Proof:

Suppose $x < S(y)$. Hence there is a $z \in N$ with \begin{equation} \text{I}(N,x+S(z),S(y)) \tag{*}\end{equation} Hence by (Peano 1b and 3) \begin{equation} \text{I}(N,x+z,y) \end{equation}

Define a predicate \begin{equation} Q(u):=(\text{I}(N,x+u,y) \subset x<y \lor \text{I}(N,x,y) \end{equation}

It is sufficient to show $Q(z)$. We prove this by induction on $z$. To see $Q(0)$, not ethat if $\text{I}(N,x+0,y)$ holds then $\text{I}(N,x,y)$ is true by Peano 1a. Thus, $x<y \lor \text{I}(n,x,y)$. Now, we prove $Q(S(v))$: Suppose $\text{I}(N,x+S(v),y)$. From this definition we have $x<y$ and thus $x<y \lor \text{I}(N,x,y)$ also in this case. Finally, Peano's fifth axiom gives $Q(z)$ and by $(*)$ we get $x < y \lor \text{I}(N,x,y)$. \begin{equation} \tag{$\square$} \end{equation}

Theorem B

For all $x,y \in N$ \begin{equation} x <y \lor \text{I}(N,x,y) \lor y<x \end{equation} Proof:

If $x<y$ then $\neg \text{I}(N,x,y)$ by definition, and if $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 \lor \text{I}(N,0,y)$ for all $y$, which proves the base case. Next, suppose the theorem holds for $x$; now we want to prove the theorem for $S(x)$. From the trichotomy for $x$, there are three cases: $x<y,\text{I}(N,x,y)$, and $x>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 <y$ Then, by theorem A we have $S(x) < y$ or $\text{I}(N,S(x),y)$, and in either case we are done. \begin{equation} \tag{$\square$} \end{equation}

The theorems that I wish to prove, can be expressed as follows in Coq.

Lemma less_lem (x y:N) : less x (succ y) -> 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 *)  Inductive sum' (A B:Set):Set :=  inl': A -> sum' A B | inr': B -> sum' A B.  Print sum'_rect.  Definition D (A B : Set)(C: sum' A B -> Set) (c: sum' A B) (d: (forall x:A, C (inl' A B x))) (e: (forall y:B, C (inr' A B y))): C c :=  match c as c0 return C c0 with | inl' x => d x | inr' y => e y end.  (* Three useful finite sets *)  Inductive N_0: Set :=.  Definition R_0   (C:N_0 -> Set)   (c: N_0): C c := match c as c0 return (C c0) with end.  Inductive N_1: Set := zero_1:N_1.  Definition R_1    (C:N_1 -> Set)   (c: N_1)   (d_zero: C zero_1): C c := match c as c0 return (C c0) with   | zero_1 => d_zero end.  Inductive N_2: Set := zero_2:N_2 | one_2:N_2.  Definition R_2    (C:N_2 -> Set)   (c: N_2)   (d_zero: C zero_2)   (d_one: C one_2): C c := match c as c0 return (C c0) with   | zero_2 => d_zero   | one_2  => d_one end.   (* Natural numbers *)  Inductive N:Set := zero: N | succ : N -> N.  Print N.   Print N_rect.  Definition R    (C:N -> Set)   (d: C zero)   (e: (forall x:N, C x -> C (succ x))):   (forall n:N, C n) := fix F (n: N): C n :=   match n as n0 return (C n0) with   | zero => d   | succ n0 => e n0 (F n0)   end.  (* Boolean to truth-value converter *)  Definition Tr (c:N_2) : Set := match c as c0 with   | zero_2 => N_0   | one_2 => N_1 end.  (* Identity type *)  Inductive I (A: Set)(x: A) : A -> Set := r :  I A x x.  Print I_rect.  Theorem J    (A:Set)   (C: (forall x y:A,                forall z: I A x y, Set))   (d: (forall x:A, C x x (r A x)))   (a:A)(b:A)(c:I A a b): C a b c. induction c. apply d. Defined.  (* functions are extensional wrt   identity types *)  Theorem I_I_extensionality (A B: Set)(f: A -> B): (forall x y:A, I A x y -> I B (f x) (f y)). Proof. intros x y P. induction P. apply r. Defined.   (* addition *)  Definition add (m n:N) : N   := R (fun z=> N) m (fun x y => succ y) n.  (* multiplication *)  Definition mul (m n:N) : N   := R (fun z=> N) zero (fun x y => add y m) n.   (* Axioms of Peano verified *)  Theorem P1a: (forall x: N, I N (add x zero) x). intro x. (* force use of definitional equality   by applying reflexivity *) apply r. Defined.   Theorem P1b: (forall x y: N,  I N (add x (succ y)) (succ (add x y))). intros. apply r. Defined.   Theorem P2a: (forall x: N, I N (mul x zero) zero). intros. apply r. Defined.   Theorem P2b: (forall x y: N,  I N (mul x (succ y)) (add (mul x y) x)). intros. apply r. Defined.  Definition pd (n: N): N := R (fun _=> N) zero (fun x y=> x) n.  (* alternatively Definition pd (x: N): N := match x as x0 with   | zero => zero   | succ n0 => n0 end. *)  Theorem P3: (forall x y:N,  I N (succ x) (succ y) -> I N x y). intros x y p. apply (I_I_extensionality N N pd (succ x) (succ y)). apply p. Defined.  Definition not (A:Set): Set:= (A -> N_0).  Definition isnonzero (n: N): N_2:= R (fun _ => N_2) zero_2 (fun x y => one_2) n.   Theorem P4 : (forall x:N,  not (I N (succ x) zero)). intro x. intro p.  apply (J N (fun x y z =>      Tr (isnonzero x) -> Tr (isnonzero y))     (fun x => (fun t => t)) (succ x) zero) . apply p. simpl. apply zero_1. Defined.  Theorem P5 (P:N -> Set): P zero -> (forall x:N, P x -> P (succ x))    -> (forall x:N, P x). intros base step n. apply R. apply base. apply step. Defined.  (* I(A,-,-) is an equivalence relation *)  Lemma Ireflexive (A:Set): (forall x:A, I A x x). intro x. apply r. Defined.  Lemma Isymmetric (A:Set): (forall x y:A, I A x y -> I A y x). intros x y P. induction P. apply r. Defined.  Lemma Itransitive (A:Set):  (forall x y z:A, I A x y -> I A y z -> I A x z). intros x y z P Q. induction P. assumption. Defined.   Lemma succ_cong : (forall m n:N, I N m n -> I N (succ m) (succ n)). intros m n H. induction H. apply r. Defined.  Lemma zeroadd: (forall n:N, I N (add zero n) n). intro n. induction n. simpl. apply r. apply succ_cong. auto.  Defined.  Lemma succadd: (forall m n:N, I N (add (succ m) n) (succ (add m n))). intros. induction n. simpl. apply r. simpl. apply succ_cong. auto.  Defined.  Lemma commutative_add: (forall m n:N, I N (add m n) (add n m)). intros n m; elim n. apply zeroadd. intros y H; elim (succadd m y). simpl. rewrite succadd. apply succ_cong. assumption.   Defined.  Lemma associative_add: (forall m n k:N,  I N (add (add m n) k) (add m (add n k))). intros m n k. induction k. simpl. apply Ireflexive. simpl. apply succ_cong. assumption. Defined.  Definition or (A B : Set):= sum' A B.   Definition less (m n: N) :=  Sigma N (fun z => I N (add m (succ z)) n).    Lemma less_lem (x y:N) :  less x (succ y) -> or (less x y) (I N x y). intro. destruct H. right.  (* Here is where I'm working right now *)  Defined.   Theorem Ntrichotomy: (forall x y:N,  or (less x y) (or (I N x y) (less y x))). 

Asked By : user11942

Answered By : cody

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:

1. 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. 

2. 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.

3. 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.

4. 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.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/18765