5
$\begingroup$

Question

How do I write more intuitive proofs of the two following results in Coq?

Theorem Course_of_values_ind: 
        InductiveRel N less

  Theorem DivRem: (forall d n:N, 
      (Sigma N (fun q => (Sigma N (fun s =>
         and  (I N n (add (mul (succ d) q) s)) (less s (succ d))))))).

Background

I recognize all of these results are already built into Coq, and so it is possible to provide much easier proofs than what I am asking for. This is something I have managed to do on my own; simply using the Coq library for this particular task. Even though this is much more concise (and thus arguably more elegant), I find don't find it very instructive.Luke Mathieson provided a good example of this when he gave an alternative proof in Coq of trichonomy for natural numbers:

(*
  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

Notice that the actual proof of the theorem in Coq does not reveal how the proof would look like informally. Thus, my hope is that someone may be kind enough to give a more, shall we say "intuitive", proof of the Euclidean division algorithm in Coq. The proof I have in mind will uses structural induction, which rests on the validity of the following lemma:

Lemma: $(\mathbb{N},<)$ is well founded. (Course_of_values_ind)

As this is so critical to the proof of the Euclidean division algorithm I decided to prove it.

Proof:

Suppose that $P(x)$ set $(x:N$) is a progressive predicate (definition is given below the proof of the Euclidean division algorithm) on $N$. Define \begin{equation} Q(x)=_{def}(\forall y:N)(y<x \subset P(y)) \tag{*}\end{equation}

It is enough to prove $(\forall x:N)Q(x)$, as then for any $x:N$ we have $x<S(x)$ and so $P(x)$. $Q(0)$ follows by Peano's forth axiom. The inductive step $(\forall x N)(Q(x) \subset Q(S(x)))$ follows by theorem A (see Theorem Proofs in Coq) combined with Peano 1a and 1b (see Code-file).

For all natural numbers $n$ and $m$ if $n>0$, if $m>0$ then there are natural numbers $q$ and $r$ such that $n=qm+r$ and $r<m$.

One may formalize this as:

\begin{equation}(\forall n:\mathbb{N})(\forall k:\mathbb{N})(\exists q:\mathbb{N})(\exists r:\mathbb{N})(n=_{\mathbb{N}}q\cdot S(k)+r \land r<S(k) \end{equation}

where $m:=S(k)$. Now, an informal proof of the so-called Eucliean theorem can be given as:

Proof:

Let $k$ be an arbitrary natural number, define $m:=S(k)$ and then proceed by strong induction on $n$ (this is justified by lemma). Suppose $n$ is a natural number and for every $l <n$ there are natural numbers $q$ and $r$ such that $l=mq+r$ and $r <m$. We now have two cases:

  1. $n<m$. Let $q=0$ and $r=n$, Then clearly $n=qm+r$ and $r<m$.
  2. $n \geq m$ Let $l=n-m<n$ and observe that since $n \geq m$, $l$ is a natural number. By the inductive hypothesis one may now choose $q'$ and $r'$ such that $l=q'm+r'$ and $r'<m$. But, this means we have $n-m=q'm+r'$, so $n=q'm+r'+m=m(q'+1)+r'$. So, if we let $q=q'+1$ and $r=r'$, then we have $n=qm+r$ and $r<m$.

Definitions of the terms I use in my informal proofs

      Definition Progressive 
           (A:Set)(R: A -> A -> Set)(P:A -> Set):=
        (forall x:A, 
         (forall y:A, R y x -> P y) -> P x).

        Definition InductiveRel 
        (A:Set)(R: A -> A -> Set):=
        (forall P:A->Set, Progressive A R P -> 
        forall x:A, P x). 

        Theorem Course_of_values_ind: 
        InductiveRel N less
    Definition Decidable (A B:Set)(R: A -> B -> Set):Set :=
    forall x:A, forall y:B, or (R x y) (not (R x y)).


    Definition and (A B:Set) := prod A B.
    Definition and_el_left (A B: Set)(p: and A B) 
    := fst p.
    Definition and_el_right (A B: Set)(p: and A B) 
    := snd p.
(* Euclidean Division *)

Theorem DivRem: (forall d n:N, 
  (Sigma N (fun q => (Sigma N (fun s =>
     and  (I N n (add (mul (succ d) q) s)) (less s (succ d))))))).

Code-file

This code was generously provided by cody (again see Theorem Proofs in Coq). It is my intent to add the results presented above to this code as soon as they are all complete.

(* 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. *)

Print sigT.

(* 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. *)

Print sum.

(* 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. *)

Print False.


(* 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. *)

Print unit.


(* 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. *)

Print bool.

(* 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. *)

Print nat.

(* 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. *)

Definition Tr (b : bool) : Type := if b then unit else False.

(* Identity type *)

(* Inductive I {A: Type}(x: A) : A -> Type :=  *)
(*   r : I x x. *)

(* Print I_rect. *)

(* Hint Resolve r.  *)

Print identity.

Notation "x ~ y" := (identity x y)(at level 60).

Notation "#":=(identity_refl)(at level 10).

Definition J 
  (A : Type)
  (C: (forall x y : A, forall e : x ~ y, Type)) 
  (d: (forall x:A, C x x (# x))) :
  (forall (a : A)(b : A)(e : a ~ b),  C a b e) :=
    fun a b e =>
      match e in _ ~ b with
        | # => d a
      end.

Check J.

(* functions are extensional wrt identity types *)

Definition id_ext {A B: Type} {x y : A} (f: A -> B): 
  (x ~ y -> (f x) ~ (f y))
  := fun p =>
    match p with
      # => # (f x)
    end.

(* addition *)

(* Definition add (m n:N) : N := R (fun z=> N) m (fun x y => succ y) n. *)

Print plus.

(* multiplication *)

(* Definition mul (m n:N) : N := R (fun z=> N) zero (fun x y => add y m) n. *)

Print mult.

(* Axioms of Peano verified *)

Require Import Arith.

Theorem P1a: (forall x: nat, (0 + x) ~ x).
Proof.
  simpl; auto.
Defined.


Theorem P1b: forall x y: nat, ((S x) + y) ~ (S (x + y)).
Proof.
  simpl; auto.
Defined.

Theorem P2a: (forall x: nat, (0 * x) ~ 0).
Proof.
  simpl; auto.
Defined.

Theorem P2b: forall x y: nat, ((S x) * y) ~ (y + (x * y)).
Proof.
  simpl; auto.
Defined.

(* Definition pd (n: N): N := R (fun _=> N) zero (fun x y=> x) n. *)

Print pred.

Theorem P3: (forall x y: nat, (S x) ~ (S y) -> x ~ y).
Proof.
 intros x y p.
 apply (id_ext pred p).
Defined.

(* Definition not (A:Set): Set:= (A -> N_0). *)

Print notT.

Definition isnonzero (n: nat): bool:= if n then false else true.

Eval compute in isnonzero 1.
Eval compute in isnonzero 0.

Notation "x !~ y":= (notT (x ~ y))(at level 60).

Definition false_if_succ (n : nat) : Type := if n then unit else False.

Hint Resolve tt.

Theorem P4 : (forall x: nat, (S x) !~ 0).
Proof.
  intro x.
  intro.
  assert (false_if_succ (S x)).
  rewrite H.
  simpl; auto.
  simpl in X; auto.
Qed.


Theorem P5 (P:nat -> Type): P 0 -> (forall x:nat, P x -> P (S x)) -> (forall x:nat, P x).
Proof.
  intros; induction x; auto.
Defined.

(* I(A,-,-) is an equivalence relation *)

(*All these are in the std library *)

Lemma Ireflexive (A:Set): (forall x:A, x ~ x).
Proof.
  auto.
Defined.

Lemma Isymmetric (A:Set): (forall x y:A, x ~ y -> y ~ x).
Proof.
  auto.
Defined.

Lemma Itransitive (A:Set): (forall x y z:A, x ~ y -> y ~ z -> x ~ z).
Proof.
  intros x y z e1 e2.
  rewrite e1; auto.
Defined.

Lemma S_cong : (forall m n:nat, m ~ n -> (S m) ~ (S n)).
Proof.
  intros m n e; rewrite e; auto.
Defined.

Lemma zeroadd: (forall n:nat, (n + 0) ~ n).
Proof.
  induction n; simpl; auto.
  rewrite IHn; auto.
Defined.

Hint Rewrite zeroadd.

Lemma Sadd: (forall m n:nat, (m + (S n)) ~ (S (m + n))).
Proof.
  induction m; intro n; auto.
  simpl; rewrite IHm; auto.
Defined.

Hint Rewrite Sadd.

Lemma commutative_add: (forall m n:nat, (m + n) ~ (n + m)).
Proof.
  induction m; intro n.
  rewrite zeroadd; auto.
  simpl; rewrite IHm.
  rewrite Sadd; auto.
Defined.

Lemma associative_add: (forall m n k:nat, ((m + n) + k) ~ (m + (n + k))).
Proof.
  induction m; auto.
  intros n k; simpl.
  rewrite IHm; auto.
Defined.

Print sum.

Open Scope type_scope.

(* Definition or (A B : Set):= (A + B). *)

Definition less (m n: nat) := { z : nat & S (z + m) ~ n}.

Notation "m < n" := (less m n)(at level 70).

Lemma less_lem : forall n m : nat, n < (S m) -> (n < m) + (n ~ m).
Proof.
  intros n m leq.
  elim leq.
  induction x; simpl; intro e.
  right.
  apply P3; auto.
  left.
  exists x.
  apply P3; auto.
Defined.


Theorem nattrichotomy: forall n m:nat, (n < m) + (n ~ m) + (m < n).
Proof.
  induction n; induction m; simpl.
  left; right; auto.
  left; left.
  exists m; rewrite zeroadd; auto.
  right; exists n; rewrite zeroadd; auto.
  destruct IHm as [ leq | gt ].
  destruct leq as [lt | eq].
  left; left; destruct lt.
  exists (S x).
  simpl; rewrite i; auto.
  left; left; exists 0.
  rewrite eq; simpl; auto.
  generalize (less_lem _ _ gt); intro less_eq.
  destruct less_eq as [less| eq].
  right.
  destruct less.
  exists x.
  rewrite Sadd; rewrite<- i; auto.
  left;right; rewrite eq; auto.
Defined.
$\endgroup$
  • 1
    $\begingroup$ So, what's your question? I scanned through what you wrote and couldn't find a clear question. Did I miss it? There's background, a claim of a lemma, an asserted proof, some definition, a bunch of code... but I don't see a question. I assume you're familiar with the StackExchange concept and you know that this is a question-and-answer site, not a discussion forum? (See the 'help center' link at the upper-right of the page.) $\endgroup$ – D.W. Dec 12 '13 at 5:50
  • $\begingroup$ Oh, sorry @D.W. I seem to have forgot to add the actual question at the beginning. Is this better? $\endgroup$ – user11942 Dec 12 '13 at 9:51
  • $\begingroup$ @user11942 Thanks for adding a question. However, I don't feel this is a good match for Stack Exchange. It feels a lot like a programming question -- I know it's not exactly that but it's very close. It seems that what you want most is a tutorial, but this is a question-and-answer site, which isn't really the place for tutorials. And "Writing Intuitive Proofs in Coq" sounds like it would make a good title for a book: good answers are likely to be very, very long. For this reason, I'd now vote to close as "Too broad" but the system doesn't let people change the reason for their close vote. $\endgroup$ – David Richerby Dec 12 '13 at 18:44
2
$\begingroup$

I have a few suggestions. Here is the updated version. As you can see I run out of steam at the end (I'll finish up when I get the time).

Again several suggestions:

  1. cs.stackexchange usually doesn't answer specific questions about coq developments which, by definition, usually aren't a huge help to others. You'd be much more welcome on the coq-club mailing list (and the answers would be by people more expert than I).
  2. Use the built-in equality! The equality you are using is excruciatingly hard to work with as many tactics (replace, auto with arith, ring, omega) won't do anything with it.
  3. I suggest you start with a less ambitious project. While simple on paper, proving Euclidian division from scratch isn't feasible in Coq if you're still struggling with elementary things about < or addition. Here even with the omega tactic, things are far from trivial for a beginner. It's a slow road at first...
  4. Try to procure or borrow Coq'Art which is the (very) extended version of Coq In a Hurry.
  5. My code is terrible. I should have developed high-level tactics and hint databases to make the proofs simpler (mimicking auto with arith). I'll do it if I find the time.
$\endgroup$
  • $\begingroup$ Thanks @cody! I will most certainly take your advice and subscribe to the mailing list $\textbf{and}$ do less ambitious projects. As you said, it is far more challenging (at least for a beginner like myself) to prove Euclidean division in Coq then on paper. $\endgroup$ – user11942 Dec 12 '13 at 23:41
  • $\begingroup$ @user11942 I just want to (explicitly) second the advice in Cody's answer. Particularly point 2, and the logical extension of it. A lot of the pieces you're putting together have already been done, in largely or exactly the same way, but have the advantage that they're properly integrated with the tactic library. $\endgroup$ – Luke Mathieson Dec 12 '13 at 23:41
  • 2
    $\begingroup$ @user11942 In addition to Coq'Art, I also strongly recommend the starting chapters of Software Foundations. It takes you through a lot of this stuff, with inline examples and exercises - it's really aimed at teaching Coq from absolute basics. It also has the advantage of being free! $\endgroup$ – Luke Mathieson Dec 12 '13 at 23:42

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.