9
$\begingroup$

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))).
$\endgroup$
  • 3
    $\begingroup$ To understand how far you've got, it would help if you'd post your Coq code so far, so that we could load it and check that what we propose works for your definitions. $\endgroup$ – Gilles Dec 9 '13 at 0:09
  • 1
    $\begingroup$ A couple of comments and clarifying questions:- Would it be sufficient for your purposes to just use syntactic equality ("=" in Coq) instead of I(N,x,y)? Is there a reason for using 'or' the way you've defined it? Coq (well, the basic libraries for Coq) have a way of expression logical disjunction that facilitates certain nice aspects of proofs. Similarly there's a way to define 'less' that may be more workable for you. To this end you might want to have a look at the early chapters of Software Foundations. While the end of the book... $\endgroup$ – Luke Mathieson Dec 9 '13 at 2:00
  • $\begingroup$ ... is about verifying programs etc., the start is quite a good introduction to Coq, and has theorems like the ones you've got as exercises and examples. It's free, and it's actually all written as Coq scripts, so you can do the exercises and compile them as you're reading through. For what you're doing here, there's interesting bits and pieces in the chapters Basics, Induction, Prop and Logic - and probably some dependencies from the bits inbetween. $\endgroup$ – Luke Mathieson Dec 9 '13 at 2:03
  • 1
    $\begingroup$ Another note, Thm P5 (inductive principle) is built in to Coq in a stronger form (structural induction), so you don't need to explicitly take that as an axiom. $\endgroup$ – Luke Mathieson Dec 9 '13 at 5:03
  • $\begingroup$ I have posted the Coq code that I have written so far. $\endgroup$ – user11942 Dec 9 '13 at 9:53
6
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ Great answer Cody! It is wonderful to learn that there are generous people like you out there, who are willing to help others in need. I sincerely appreciate it! I will most definitely take a look at CPDT and Coq-Club; both of which I will most probably need in the near future as I continue to work towards proving the division algorithm in Coq. $\endgroup$ – user11942 Dec 10 '13 at 0:59
  • $\begingroup$ Thanks! Note that this is often called "Euclidian division" and is already present in some libraries (over the integers though) $\endgroup$ – cody Dec 10 '13 at 16:41
  • $\begingroup$ It does not surprise me, the Coq libraries I have looked at have been remarkably well stocked with definitions, lemmas and theorems. I will seek to post my approach to the Euclidian division algorithm as a question by tomorrow at the latest. $\endgroup$ – user11942 Dec 10 '13 at 17:32
4
$\begingroup$

Cody's answer is excellent, and fulfils your question about translating your proof to Coq. As a complement to that, I wanted to add the same results, but proven using a different route, mainly as an illustration of some bits of Coq and to demonstrate what you can prove syntactically with very little additional work. This is not a claim however that this is the shortest route - just a different one. The proofs only include one additional helper lemma, and rely only on basic definitions, I don't introduce addition, multiplication or any of their properties, or functional extensionality, and the only Peano axioms are a simple form of a <= b -> a+c <= b+c in the helper lemma (just for c=1) and structural induction, which comes with inductive types for free anyway.

Like Cody, where I thought it made no difference, I used predefined types etc., so before the proof, I'll describe those:

  • I used the built in nat type for natural numbers, which has (up to precise naming) the same definition as yours:

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

  • I used the built in le and lt for less than or equal and less than respectively, which have notational shorthands "<=" and "<" for readability. They are defined:

Inductive le : nat -> nat -> Prop :=
| le_n : forall n, le n n
| le_S : forall n m, (le n m) -> (le n (S m)).

and

Definition lt (n m:nat) := le (S n) m.

  • The built in eq (shorthand "=") is syntactic equality and works the same as your "I", with one constructor that just says anything is equal to itself. The symmetric and transitive properties are easy proofs from there, but we won't need them in this case. The definition for eq below has the notation built into it.

Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x

  • Lastly, I've used the propositional or (shorthand "\/" - which is backslash forwardslash), which has two constructors, basically that either you have evidence for the left argument, or the right argument. Coq also has some shorthand tactics, left and right, which just mean "apply or_introl" and "apply or_intror" respectively.

Inductive or (A B : Prop) : Prop :=
or_introl : A -> A / B | or_intror : B -> A / B

What now follows are my proofs, in principle, if markup doesn't get in the way, you should be able to just cut and past this into a Coq .v file and it will work. I've included comments to note interesting bits, but they are in (* *) delimiters, so you shouldn't have to remove them.

Theorem lt_or_eq: forall (n m : nat),
  n < S m -> n < m \/ n = m.
Proof.
(*
  This proof is just a case analysis on n and m, whether they're zero or
  a successor of something.
*)
destruct n as [|n']; destruct m as [|m']. 

(*n = 0, m = 0*)
intros.
  right. reflexivity.

(*n = 0, m = S m'*)
intros H.
  inversion H.
  inversion H1.
  left. unfold lt. constructor.
  (*The constructor tactic tries to match the goal to a constructor
    that's in the environment.*) 
  left. unfold lt. constructor. assumption.
  (*Assumption tries to match the goal to something that's in the
    current context*)

(*n = S n', m = 0
  This case is false, so we can invert our way out of it.*)
intros.
  inversion H. inversion H1.

(*n = S n', m = S m'*)
intros.
  inversion H.
    right. reflexivity.
    left. unfold lt. assumption.
Qed.


(*
  The following lemma with be useful in the proof of the trichotomy theorem,
  it's pretty obviously true, and easy to prove. The interesting part for
  anyone relatively new to Coq is that the induction is done on the
  hypothesis "a <= b", rather than on either a or b.
*)
Lemma a_le_b_implies_Sa_le_Sb: forall a b, a <= b -> S a <= S b.
Proof.
  intros a b Hyp.
  induction Hyp.
  constructor.
  constructor.
  apply IHHyp.
Qed.

(*
  The proof of the trichotomy theorem is a little more involved than the
  last one but again we don't use anything particularly tricky. 
  Other than the helper lemma above, we don't use anything other than the
  definitions.

  The proof proceeds by induction on n, then induction on m.  My personal
  feeling is that this can probably be shortened.  
*)
Theorem trich: forall (n m : nat),
  n < m \/ n = m \/ m < n.
Proof.
  induction n.
    induction m.
      right. left. reflexivity.
        inversion IHm.
          left. unfold lt. constructor. unfold lt in H. assumption.
          inversion H.
          left. unfold lt. subst. constructor.
          inversion H0.     
    induction m.
      assert (n < 0 \/ n = 0 \/ 0 < n).
      apply IHn.
      inversion H.
      inversion H0.
      inversion H0.
      right. right. subst. unfold lt. constructor.
      right. right. unfold lt. constructor. assumption.
      inversion IHm. unfold lt in H.
      left. unfold lt. constructor. assumption.
      inversion H; subst.
      left. unfold lt. constructor.
      inversion H0.
      right. left. reflexivity.
      right. right. apply lt_or_eq in H0.

      inversion H0.
      apply a_le_b_implies_Sa_le_Sb. assumption.
      subst. unfold lt. apply a_le_b_implies_Sa_le_Sb. assumption.
Qed.

(*
  The following is just to show what can be done with some of the tactics
  The omega tactic implements a Pressburger arithmetic solver, so anything
  with natural numbers, plus, multiplication by constants, and basic logic
  can just be solved. Not very interesting for practicing Coq, but cool to
  know.
*)

Require Import Omega.

Example trich' : forall (n m : nat),
  n < m \/ n = m \/ m < n.
Proof.
  intros.
  omega.
Qed.
$\endgroup$
  • $\begingroup$ Another wonderful answer! I am truly grateful to you for the time and effort you have put into answering my question. $\endgroup$ – user11942 Dec 10 '13 at 17:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.