Euclidean Algorithm in Coq

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},0$, if $m>0$ then there are natural numbers $q$ and $r$ such that $n=qm+r$ and $r

• $n \geq m$ Let $l=n-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):=

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:

• 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).

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

• 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

• Try to procure or borrow Coq'Art which is the (very) extended version of Coq In a Hurry.

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

StackExchange Computer Science Q#18908, answer score: 2