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:
- $n<m$. Let $q=0$ and $r=n$, Then clearly $n=qm+r$ and $r<m$.
- $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.
