Date: Tue, 3 Jan 2017 18:07:49 -0500
Subject: [PATCH] books/bookvolbib COQ Program Construction papers
Goal: Proving Axiom Correct
\index{Coquand, Thierry}
\index{Huet, G\'erard}
\index{Paulin, Christine}
\begin{chunk}{axiom.bib}
@misc{COQx16,
author = {Coquand, Thierry and Huet, G\'erard and Paulin, Christine},
title = "The COQ Proof Assistant",
year = "2016",
url = "https://coq.inria.fr"
}
\index{Coquand, Thierry}
\index{Huet, G\'erard}
\index{Paulin, Christine}
\begin{chunk}{axiom.bib}
@misc{COQx16a,
author = {Coquand, Thierry and Huet, G\'erard and Paulin, Christine},
title = "COQ Proof Assistant Library Coq.ZArith.Znumtheory",
year = "2016",
url = "https://coq.inria.fr/library/Coq.ZArith.Znumtheory.html"
}
\index{Parent, Catherine}
\begin{chunk}{axiom.bib}
@techreport{Pare94,
author = "Parent, Catherine",
title = "Synthesizing proofs from programs in the Calculus of Inductive
Constructions",
year = "1994",
institution = {Ecole Normale Sup\'erieure de Lyon},
abstract =
"In type theory, a proof can be represented as a typed $\lambda$-term.
There exist methods to mark logical parts in proofs and extract their
algorithmic contents. The result is a correct program with respect to
a specification. This paper focuses on the inverse problem: how to
generate a proof from its specification. The framework is the Calculus
of Inductive Constructions. A notion of coherence is introduced between
a specification and a program containing types but no logical proofs.
This notion is based on the definition of an extraction function called
the weak extraction. Such a program can give a method to reconstruct a
set of logical properties needed to have a proof of the initial
specification. This can be seen either as a method of proving programs
or as a method of synthetically describing proofs.",
paper = "Pare94.pdf"
}
\end{chunk}
\index{Parent-Vigouroux, Catherine}
\begin{chunk}{axiom.bib}
@article{Pare97,
author = "Parent-Vigouroux, Catherine",
title = "Verifying programs in the Calculus of Inductive Constructions",
year = "1997",
journal = "Formal Aspects of Computing",
volume = "9",
number = "5",
pages = "484-517",
abstract =
"This paper deals with a particular approach to the verification of
functional programs. A specification of a program can be represented
by a logical formula. In a constructive framework, developing a program
then corresponds to proving this formula. Given a specification and a
program, we focus on reconstructing a proof of the specification whose
algorithmic contents corresponds to the given program. The best we can
hope is to generate proof obligations on atomic parts of the program
corresponding to logical properties to be verified. First, this paper
studies a weak extraction of a program from a proof that keeps track
of intermediate specifications. From such a program, we prove the
determinism of retrieving proof obligations. Then, heuristic methods
are proposed for retrieving the proof from a natural program containing
only partial annotations. Finally, the implementation of this methos as
a tactic of the {\sl Coq} proof assistant is presented.",
paper = "Pare97.pdf"
}
\end{chunk}
\index{Parent-Vigouroux, Catherine}
\begin{chunk}{axiom.bib}
@misc{Pare96,
author = "Parent-Vigouroux, Catherine",
title = "Natural proofs versus programs optimization in the
Calculus of Inductive Constructions",
year = "1996",
abstract =
"This paper presents how to automatically prove that an 'optimized'
program is correct with respect to a set of given properties that is a
specification. Proofs of specifications contain logical and
computational parts. Programs can be seen as computational parts of
proofs. They can thus be extracted from proofs and be certified to be
correct. The inverse problem can be solved: it is possible to
reconstruct proof obligations from a program and its specification.
The framework is a type theory where a proof can be represented as a
typed $\lambda$-term and, particularly, the Calculus of Inductive
Constructions. This paper shows how programs can be simplified in
order to be written in a much closer way to the ML one's. Indeed,
proofs structures are often much more heavy than program structures.
The problem is consequently to consider natural programs (in a ML sense)
and see how to retrieve natural structures of proofs from them.",
paper = "Pare96.pdf"
}
\end{chunk}
\index{Parent, Catherine}
\begin{chunk}{axiom.bib}
@inproceedings{Pare93,
author = "Parent, Catherine",
title = "Developing Certified Programs in the System Coq: The Program
Tactic",
booktitle = "Proc. Int. Workshop on Types for Proofs and Programs",
publisher = "Springer-Verlag",
isbn = "3-540-58085-9",
pages = "291-312",
year = "1993",
abstract =
"The system {\sl Coq} is an environment for proof development based on
the Calculus of Constructions extended by inductive definitions. The
specification of a program can be represented by a logical formula and
the program itself can be extracted from the constructive proof of the
specification. In this paper, we look at the possibility of inverting
the specification and a program, builds the logical condition to be
verified in order to obtain a correctness proof of the program. We
build a proof of the specification from the program from which the
program can be extracted. Since some information cannot automatically
be inferred, we show how to annotate the program by specifying some of
its parts in order to guide the search for the proof.",
paper = "Pare93.ps"
}
\end{chunk}
\index{Coquand, Thierry}
\index{Huet, G\'erard}
\begin{chunk}{axiom.bib}
@techreport{Coqu86,
author = {Coquand, Thierry and Huet, G\'erard},
title = "The Calculus of Constructions",
year = "1986",
institution = "INRIA Centre de Rocquencourt",
number = "530",
url = "https://hal.inria.fr/inria-00076024/document",
abstract =
"The Calculus of Constructions is a higher-order formalism for
constructive proofs in natural deduction style. Every proof is a
$\lambda$-expression, typed with propositions of the underlying
logic. By removing types we get a pure $\lambda$-expression,
expressing its associated algorithm. Computing this
$\lambda$-expression corresponds roughly to cut-elimination. It is our
thesis that (as already advocated by Martin-Lof) the Curry-Howard
correspondence between propositions and types is a powerful paradigm
for Computer Science. In the case of Constructions, we obtain the
notion of a very high-level functional programming language, with
complex polymorphism well-suited for modules specification. The notion
of type encompasses the usual notioin of data type, but allows as well
arbitrarily complex algorithmic specifications. We develop the basic
theory of a Calculus of Constructions, and prove a strong
normalization theorem showing that all computations terminate.
Finally, we suggest various extensions to stronger calculi.",
paper = "Coqu86.pdf"
}
\end{chunk}
---
books/bookvol13.pamphlet | 359 ++++++++++++++++++++++++++++++++++++++++
books/bookvolbib.pamphlet | 165 ++++++++++++++++++
changelog | 3 +
patch | 171 +++++++++++++++++--
src/axiom-website/patches.html | 2 +
5 files changed, 685 insertions(+), 15 deletions(-)
diff --git a/books/bookvol13.pamphlet b/books/bookvol13.pamphlet
index 10ef1ad..0ee912f 100644
--- a/books/bookvol13.pamphlet
+++ b/books/bookvol13.pamphlet
@@ -746,6 +746,365 @@ proof: \[ a | b \implies |a| \le |b|; b | a \implies |b| \le |a|;
{\rm \ therefore\ } |a|=|b| \implies a = \pm b\]
\[ a | 1 \iff a = \pm 1\]
+\chapter{COQ proof of GCD}
+This is the proof of GCD\cite{COQx16a} in the COQ\cite{COQx16} sources:
+\begin{verbatim}
+Library Coq.ZArith.Znumtheory
+
+Require Import ZArith_base.
+Require Import ZArithRing.
+Require Import Zcomplements.
+Require Import Zdiv.
+Require Import Wf_nat.
+
+For compatibility reasons, this Open Scope isn't local as it should
+
+Open Scope Z_scope.
+
+This file contains some notions of number theory upon Z numbers:
+
+ a divisibility predicate Z.divide
+ a gcd predicate gcd
+ Euclid algorithm euclid
+ a relatively prime predicate rel_prime
+ a prime predicate prime
+ properties of the efficient Z.gcd function
+
+
+Notation Zgcd := Z.gcd (compat "8.3").
+Notation Zggcd := Z.ggcd (compat "8.3").
+Notation Zggcd_gcd := Z.ggcd_gcd (compat "8.3").
+Notation Zggcd_correct_divisors := Z.ggcd_correct_divisors (compat "8.3").
+Notation Zgcd_divide_l := Z.gcd_divide_l (compat "8.3").
+Notation Zgcd_divide_r := Z.gcd_divide_r (compat "8.3").
+Notation Zgcd_greatest := Z.gcd_greatest (compat "8.3").
+Notation Zgcd_nonneg := Z.gcd_nonneg (compat "8.3").
+Notation Zggcd_opp := Z.ggcd_opp (compat "8.3").
+
+The former specialized inductive predicate Z.divide is now a generic existential predicate.
+
+Notation Zdivide := Z.divide (compat "8.3").
+
+Its former constructor is now a pseudo-constructor.
+
+Definition Zdivide_intro a b q (H:b=q*a) : Z.divide a b := ex_intro _ q H.
+
+Results concerning divisibility
+
+Notation Zdivide_refl := Z.divide_refl (compat "8.3").
+Notation Zone_divide := Z.divide_1_l (compat "8.3").
+Notation Zdivide_0 := Z.divide_0_r (compat "8.3").
+Notation Zmult_divide_compat_l := Z.mul_divide_mono_l (compat "8.3").
+Notation Zmult_divide_compat_r := Z.mul_divide_mono_r (compat "8.3").
+Notation Zdivide_plus_r := Z.divide_add_r (compat "8.3").
+Notation Zdivide_minus_l := Z.divide_sub_r (compat "8.3").
+Notation Zdivide_mult_l := Z.divide_mul_l (compat "8.3").
+Notation Zdivide_mult_r := Z.divide_mul_r (compat "8.3").
+Notation Zdivide_factor_r := Z.divide_factor_l (compat "8.3").
+Notation Zdivide_factor_l := Z.divide_factor_r (compat "8.3").
+
+Lemma Zdivide_opp_r a b : (a | b) -> (a | - b).
+
+Lemma Zdivide_opp_r_rev a b : (a | - b) -> (a | b).
+
+Lemma Zdivide_opp_l a b : (a | b) -> (- a | b).
+
+Lemma Zdivide_opp_l_rev a b : (- a | b) -> (a | b).
+
+Theorem Zdivide_Zabs_l a b : (Z.abs a | b) -> (a | b).
+
+Theorem Zdivide_Zabs_inv_l a b : (a | b) -> (Z.abs a | b).
+
+Hint Resolve Z.divide_refl Z.divide_1_l Z.divide_0_r: zarith.
+Hint Resolve Z.mul_divide_mono_l Z.mul_divide_mono_r: zarith.
+Hint Resolve Z.divide_add_r Zdivide_opp_r Zdivide_opp_r_rev Zdivide_opp_l
+ Zdivide_opp_l_rev Z.divide_sub_r Z.divide_mul_l Z.divide_mul_r
+ Z.divide_factor_l Z.divide_factor_r: zarith.
+
+Auxiliary result.
+
+Lemma Zmult_one x y : x >= 0 -> x * y = 1 -> x = 1.
+
+Only 1 and -1 divide 1.
+
+Notation Zdivide_1 := Z.divide_1_r (compat "8.3").
+
+If a divides b and b divides a then a is b or -b.
+
+Notation Zdivide_antisym := Z.divide_antisym (compat "8.3").
+Notation Zdivide_trans := Z.divide_trans (compat "8.3").
+
+If a divides b and b<>0 then |a| <= |b|.
+
+Lemma Zdivide_bounds a b : (a | b) -> b <> 0 -> Z.abs a <= Z.abs b.
+
+Z.divide can be expressed using Z.modulo.
+
+Lemma Zmod_divide : forall a b, b<>0 -> a mod b = 0 -> (b | a).
+
+Lemma Zdivide_mod : forall a b, (b | a) -> a mod b = 0.
+
+Z.divide is hence decidable
+
+Lemma Zdivide_dec a b : {(a | b)} + {~ (a | b)}.
+
+Theorem Zdivide_Zdiv_eq a b : 0 < a -> (a | b) -> b = a * (b / a).
+
+Theorem Zdivide_Zdiv_eq_2 a b c :
+ 0 < a -> (a | b) -> (c * b) / a = c * (b / a).
+
+Theorem Zdivide_le: forall a b : Z,
+ 0 <= a -> 0 < b -> (a | b) -> a <= b.
+
+Theorem Zdivide_Zdiv_lt_pos a b :
+ 1 < a -> 0 < b -> (a | b) -> 0 < b / a < b .
+
+Lemma Zmod_div_mod n m a:
+ 0 < n -> 0 < m -> (n | m) -> a mod n = (a mod m) mod n.
+
+Lemma Zmod_divide_minus a b c:
+ 0 < b -> a mod b = c -> (b | a - c).
+
+Lemma Zdivide_mod_minus a b c:
+ 0 <= c < b -> (b | a - c) -> a mod b = c.
+
+Greatest common divisor (gcd).
+There is no unicity of the gcd; hence we define the predicate Zis_gcd a b g expressing that g is a gcd of a and b. (We show later that the gcd is actually unique if we discard its sign.)
+
+Inductive Zis_gcd (a b g:Z) : Prop :=
+ Zis_gcd_intro :
+ (g | a) ->
+ (g | b) ->
+ (forall x, (x | a) -> (x | b) -> (x | g)) ->
+ Zis_gcd a b g.
+
+Trivial properties of gcd
+
+Lemma Zis_gcd_sym : forall a b d, Zis_gcd a b d -> Zis_gcd b a d.
+
+Lemma Zis_gcd_0 : forall a, Zis_gcd a 0 a.
+
+Lemma Zis_gcd_1 : forall a, Zis_gcd a 1 1.
+
+Lemma Zis_gcd_refl : forall a, Zis_gcd a a a.
+
+Lemma Zis_gcd_minus : forall a b d, Zis_gcd a (- b) d -> Zis_gcd b a d.
+
+Lemma Zis_gcd_opp : forall a b d, Zis_gcd a b d -> Zis_gcd b a (- d).
+
+Lemma Zis_gcd_0_abs a : Zis_gcd 0 a (Z.abs a).
+
+Hint Resolve Zis_gcd_sym Zis_gcd_0 Zis_gcd_minus Zis_gcd_opp: zarith.
+
+Theorem Zis_gcd_unique: forall a b c d : Z,
+ Zis_gcd a b c -> Zis_gcd a b d -> c = d \/ c = (- d).
+
+Extended Euclid algorithm.
+Euclid's algorithm to compute the gcd mainly relies on the following property.
+
+Lemma Zis_gcd_for_euclid :
+ forall a b d q:Z, Zis_gcd b (a - q * b) d -> Zis_gcd a b d.
+
+Lemma Zis_gcd_for_euclid2 :
+ forall b d q r:Z, Zis_gcd r b d -> Zis_gcd b (b * q + r) d.
+
+We implement the extended version of Euclid's algorithm, i.e. the one computing Bezout's coefficients as it computes the gcd. We follow the algorithm given in Knuth's "Art of Computer Programming", vol 2, page 325.
+
+Section extended_euclid_algorithm.
+
+ Variables a b : Z.
+
+The specification of Euclid's algorithm is the existence of u, v and d such that ua+vb=d and (gcd a b d).
+
+ Inductive Euclid : Set :=
+ Euclid_intro :
+ forall u v d:Z, u * a + v * b = d -> Zis_gcd a b d -> Euclid.
+
+The recursive part of Euclid's algorithm uses well-founded recursion of non-negative integers. It maintains 6 integers u1,u2,u3,v1,v2,v3 such that the following invariant holds: u1*a+u2*b=u3 and v1*a+v2*b=v3 and gcd(u3,v3)=gcd(a,b).
+
+ Lemma euclid_rec :
+ forall v3:Z,
+ 0 <= v3 ->
+ forall u1 u2 u3 v1 v2:Z,
+ u1 * a + u2 * b = u3 ->
+ v1 * a + v2 * b = v3 ->
+ (forall d:Z, Zis_gcd u3 v3 d -> Zis_gcd a b d) -> Euclid.
+
+We get Euclid's algorithm by applying euclid_rec on 1,0,a,0,1,b when b>=0 and 1,0,a,0,-1,-b when b<0.
+
+ Lemma euclid : Euclid.
+
+End extended_euclid_algorithm.
+
+Theorem Zis_gcd_uniqueness_apart_sign :
+ forall a b d d':Z, Zis_gcd a b d -> Zis_gcd a b d' -> d = d' \/ d = - d'.
+
+Bezout's coefficients
+
+Inductive Bezout (a b d:Z) : Prop :=
+ Bezout_intro : forall u v:Z, u * a + v * b = d -> Bezout a b d.
+
+Existence of Bezout's coefficients for the gcd of a and b
+
+Lemma Zis_gcd_bezout : forall a b d:Z, Zis_gcd a b d -> Bezout a b d.
+
+gcd of ca and cb is c gcd(a,b).
+
+Lemma Zis_gcd_mult :
+ forall a b c d:Z, Zis_gcd a b d -> Zis_gcd (c * a) (c * b) (c * d).
+
+Relative primality
+
+Definition rel_prime (a b:Z) : Prop := Zis_gcd a b 1.
+
+Bezout's theorem: a and b are relatively prime if and only if there exist u and v such that ua+vb = 1.
+
+Lemma rel_prime_bezout : forall a b:Z, rel_prime a b -> Bezout a b 1.
+
+Lemma bezout_rel_prime : forall a b:Z, Bezout a b 1 -> rel_prime a b.
+
+Gauss's theorem: if a divides bc and if a and b are relatively prime, then a divides c.
+
+Theorem Gauss : forall a b c:Z, (a | b * c) -> rel_prime a b -> (a | c).
+
+If a is relatively prime to b and c, then it is to bc
+
+Lemma rel_prime_mult :
+ forall a b c:Z, rel_prime a b -> rel_prime a c -> rel_prime a (b * c).
+
+Lemma rel_prime_cross_prod :
+ forall a b c d:Z,
+ rel_prime a b ->
+ rel_prime c d -> b > 0 -> d > 0 -> a * d = b * c -> a = c /\ b = d.
+
+After factorization by a gcd, the original numbers are relatively prime.
+
+Lemma Zis_gcd_rel_prime :
+ forall a b g:Z,
+ b > 0 -> g >= 0 -> Zis_gcd a b g -> rel_prime (a / g) (b / g).
+
+Theorem rel_prime_sym: forall a b, rel_prime a b -> rel_prime b a.
+
+Theorem rel_prime_div: forall p q r,
+ rel_prime p q -> (r | p) -> rel_prime r q.
+
+Theorem rel_prime_1: forall n, rel_prime 1 n.
+
+Theorem not_rel_prime_0: forall n, 1 < n -> ~ rel_prime 0 n.
+
+Theorem rel_prime_mod: forall p q, 0 < q ->
+ rel_prime p q -> rel_prime (p mod q) q.
+
+Theorem rel_prime_mod_rev: forall p q, 0 < q ->
+ rel_prime (p mod q) q -> rel_prime p q.
+
+Theorem Zrel_prime_neq_mod_0: forall a b, 1 < b -> rel_prime a b -> a mod b <> 0.
+
+Primality
+
+Inductive prime (p:Z) : Prop :=
+ prime_intro :
+ 1 < p -> (forall n:Z, 1 <= n < p -> rel_prime n p) -> prime p.
+
+The sole divisors of a prime number p are -1, 1, p and -p.
+
+Lemma prime_divisors :
+ forall p:Z,
+ prime p -> forall a:Z, (a | p) -> a = -1 \/ a = 1 \/ a = p \/ a = - p.
+
+A prime number is relatively prime with any number it does not divide
+
+Lemma prime_rel_prime :
+ forall p:Z, prime p -> forall a:Z, ~ (p | a) -> rel_prime p a.
+
+Hint Resolve prime_rel_prime: zarith.
+
+As a consequence, a prime number is relatively prime with smaller numbers
+
+Theorem rel_prime_le_prime:
+ forall a p, prime p -> 1 <= a < p -> rel_prime a p.
+
+If a prime p divides ab then it divides either a or b
+
+Lemma prime_mult :
+ forall p:Z, prime p -> forall a b:Z, (p | a * b) -> (p | a) \/ (p | b).
+
+Lemma not_prime_0: ~ prime 0.
+
+Lemma not_prime_1: ~ prime 1.
+
+Lemma prime_2: prime 2.
+
+Theorem prime_3: prime 3.
+
+Theorem prime_ge_2 p : prime p -> 2 <= p.
+
+Definition prime' p := 1 ~ (n|p)).
+
+Lemma Z_0_1_more x : 0<=x -> x=0 \/ x=1 \/ 1 prime p.
+
+Theorem square_not_prime: forall a, ~ prime (a * a).
+
+Theorem prime_div_prime: forall p q,
+ prime p -> prime q -> (p | q) -> p = q.
+
+we now prove that Z.gcd is indeed a gcd in the sense of Zis_gcd.
+
+Notation Zgcd_is_pos := Z.gcd_nonneg (compat "8.3").
+
+Lemma Zgcd_is_gcd : forall a b, Zis_gcd a b (Z.gcd a b).
+
+Theorem Zgcd_spec : forall x y : Z, {z : Z | Zis_gcd x y z /\ 0 <= z}.
+
+Theorem Zdivide_Zgcd: forall p q r : Z,
+ (p | q) -> (p | r) -> (p | Z.gcd q r).
+
+Theorem Zis_gcd_gcd: forall a b c : Z,
+ 0 <= c -> Zis_gcd a b c -> Z.gcd a b = c.
+
+Notation Zgcd_inv_0_l := Z.gcd_eq_0_l (compat "8.3").
+Notation Zgcd_inv_0_r := Z.gcd_eq_0_r (compat "8.3").
+
+Theorem Zgcd_div_swap0 : forall a b : Z,
+ 0 < Z.gcd a b ->
+ 0 < b ->
+ (a / Z.gcd a b) * b = a * (b/Z.gcd a b).
+
+Theorem Zgcd_div_swap : forall a b c : Z,
+ 0 < Z.gcd a b ->
+ 0 < b ->
+ (c * a) / Z.gcd a b * b = c * a * (b/Z.gcd a b).
+
+Notation Zgcd_comm := Z.gcd_comm (compat "8.3").
+
+Lemma Zgcd_ass a b c : Z.gcd (Z.gcd a b) c = Z.gcd a (Z.gcd b c).
+
+Notation Zgcd_Zabs := Z.gcd_abs_l (compat "8.3").
+Notation Zgcd_0 := Z.gcd_0_r (compat "8.3").
+Notation Zgcd_1 := Z.gcd_1_r (compat "8.3").
+
+Hint Resolve Z.gcd_0_r Z.gcd_1_r : zarith.
+
+Theorem Zgcd_1_rel_prime : forall a b,
+ Z.gcd a b = 1 <-> rel_prime a b.
+
+Definition rel_prime_dec: forall a b,
+ { rel_prime a b }+{ ~ rel_prime a b }.
+
+Definition prime_dec_aux:
+ forall p m,
+ { forall n, 1 < n < m -> rel_prime n p } +
+ { exists n, 1 < n < m /\ ~ rel_prime n p }.
+
+Definition prime_dec: forall p, { prime p }+{ ~ prime p }.
+
+Theorem not_prime_divide:
+ forall p, 1 < p -> ~ prime p -> exists n, 1 < n < p /\ (n | p).
+
+\end{verbatim}
+
\chapter{LEAN proof of GCD}
This is the proof of GCD\cite{Avig14} in the LEAN\cite{Avig16} sources:
\begin{verbatim}
diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 28b745a..6cc5602 100644
--- a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ -5526,6 +5526,28 @@ Martin, U.
\end{chunk}
+\index{Coquand, Thierry}
+\index{Huet, G\'erard}
+\index{Paulin, Christine}
+\begin{chunk}{axiom.bib}
+@misc{COQx16,
+ author = {Coquand, Thierry and Huet, G\'erard and Paulin, Christine},
+ title = "The COQ Proof Assistant",
+ year = "2016",
+ url = "https://coq.inria.fr"
+}
+
+\index{Coquand, Thierry}
+\index{Huet, G\'erard}
+\index{Paulin, Christine}
+\begin{chunk}{axiom.bib}
+@misc{COQx16a,
+ author = {Coquand, Thierry and Huet, G\'erard and Paulin, Christine},
+ title = "COQ Proof Assistant Library Coq.ZArith.Znumtheory",
+ year = "2016",
+ url = "https://coq.inria.fr/library/Coq.ZArith.Znumtheory.html"
+}
+
\index{Mahboubi, Assia}
\index{Tassi, Enrico}
\index{Bertot, Yves}
@@ -5661,6 +5683,38 @@ Martin, U.
\end{chunk}
+\index{Coquand, Thierry}
+\index{Huet, G\'erard}
+\begin{chunk}{axiom.bib}
+@techreport{Coqu86,
+ author = {Coquand, Thierry and Huet, G\'erard},
+ title = "The Calculus of Constructions",
+ year = "1986",
+ institution = "INRIA Centre de Rocquencourt",
+ number = "530",
+ url = "https://hal.inria.fr/inria-00076024/document",
+ abstract =
+ "The Calculus of Constructions is a higher-order formalism for
+ constructive proofs in natural deduction style. Every proof is a
+ $\lambda$-expression, typed with propositions of the underlying
+ logic. By removing types we get a pure $\lambda$-expression,
+ expressing its associated algorithm. Computing this
+ $\lambda$-expression corresponds roughly to cut-elimination. It is our
+ thesis that (as already advocated by Martin-Lof) the Curry-Howard
+ correspondence between propositions and types is a powerful paradigm
+ for Computer Science. In the case of Constructions, we obtain the
+ notion of a very high-level functional programming language, with
+ complex polymorphism well-suited for modules specification. The notion
+ of type encompasses the usual notioin of data type, but allows as well
+ arbitrarily complex algorithmic specifications. We develop the basic
+ theory of a Calculus of Constructions, and prove a strong
+ normalization theorem showing that all computations terminate.
+ Finally, we suggest various extensions to stronger calculi.",
+ paper = "Coqu86.pdf"
+}
+
+\end{chunk}
+
\index{DeMilo, Richard A.}
\index{Lipton, Richard J.}
\index{Perlis, Alan J.}
@@ -5979,6 +6033,117 @@ Martin, U.
\end{chunk}
+\index{Parent, Catherine}
+\begin{chunk}{axiom.bib}
+@inproceedings{Pare93,
+ author = "Parent, Catherine",
+ title = "Developing Certified Programs in the System Coq: The Program
+ Tactic",
+ booktitle = "Proc. Int. Workshop on Types for Proofs and Programs",
+ publisher = "Springer-Verlag",
+ isbn = "3-540-58085-9",
+ pages = "291-312",
+ year = "1993",
+ abstract =
+ "The system {\sl Coq} is an environment for proof development based on
+ the Calculus of Constructions extended by inductive definitions. The
+ specification of a program can be represented by a logical formula and
+ the program itself can be extracted from the constructive proof of the
+ specification. In this paper, we look at the possibility of inverting
+ the specification and a program, builds the logical condition to be
+ verified in order to obtain a correctness proof of the program. We
+ build a proof of the specification from the program from which the
+ program can be extracted. Since some information cannot automatically
+ be inferred, we show how to annotate the program by specifying some of
+ its parts in order to guide the search for the proof.",
+ paper = "Pare93.ps"
+}
+
+\end{chunk}
+
+\index{Parent, Catherine}
+\begin{chunk}{axiom.bib}
+@techreport{Pare94,
+ author = "Parent, Catherine",
+ title = "Synthesizing proofs from programs in the Calculus of Inductive
+ Constructions",
+ year = "1994",
+ institution = {Ecole Normale Sup\'erieure de Lyon},
+ abstract =
+ "In type theory, a proof can be represented as a typed $\lambda$-term.
+ There exist methods to mark logical parts in proofs and extract their
+ algorithmic contents. The result is a correct program with respect to
+ a specification. This paper focuses on the inverse problem: how to
+ generate a proof from its specification. The framework is the Calculus
+ of Inductive Constructions. A notion of coherence is introduced between
+ a specification and a program containing types but no logical proofs.
+ This notion is based on the definition of an extraction function called
+ the weak extraction. Such a program can give a method to reconstruct a
+ set of logical properties needed to have a proof of the initial
+ specification. This can be seen either as a method of proving programs
+ or as a method of synthetically describing proofs.",
+ paper = "Pare94.pdf"
+}
+
+\end{chunk}
+
+\index{Parent-Vigouroux, Catherine}
+\begin{chunk}{axiom.bib}
+@misc{Pare96,
+ author = "Parent-Vigouroux, Catherine",
+ title = "Natural proofs versus programs optimization in the
+ Calculus of Inductive Constructions",
+ year = "1996",
+ abstract =
+ "This paper presents how to automatically prove that an 'optimized'
+ program is correct with respect to a set of given properties that is a
+ specification. Proofs of specifications contain logical and
+ computational parts. Programs can be seen as computational parts of
+ proofs. They can thus be extracted from proofs and be certified to be
+ correct. The inverse problem can be solved: it is possible to
+ reconstruct proof obligations from a program and its specification.
+ The framework is a type theory where a proof can be represented as a
+ typed $\lambda$-term and, particularly, the Calculus of Inductive
+ Constructions. This paper shows how programs can be simplified in
+ order to be written in a much closer way to the ML one's. Indeed,
+ proofs structures are often much more heavy than program structures.
+ The problem is consequently to consider natural programs (in a ML sense)
+ and see how to retrieve natural structures of proofs from them.",
+ paper = "Pare96.pdf"
+}
+
+\end{chunk}
+
+\index{Parent-Vigouroux, Catherine}
+\begin{chunk}{axiom.bib}
+@article{Pare97,
+ author = "Parent-Vigouroux, Catherine",
+ title = "Verifying programs in the Calculus of Inductive Constructions",
+ year = "1997",
+ journal = "Formal Aspects of Computing",
+ volume = "9",
+ number = "5",
+ pages = "484-517",
+ abstract =
+ "This paper deals with a particular approach to the verification of
+ functional programs. A specification of a program can be represented
+ by a logical formula. In a constructive framework, developing a program
+ then corresponds to proving this formula. Given a specification and a
+ program, we focus on reconstructing a proof of the specification whose
+ algorithmic contents corresponds to the given program. The best we can
+ hope is to generate proof obligations on atomic parts of the program
+ corresponding to logical properties to be verified. First, this paper
+ studies a weak extraction of a program from a proof that keeps track
+ of intermediate specifications. From such a program, we prove the
+ determinism of retrieving proof obligations. Then, heuristic methods
+ are proposed for retrieving the proof from a natural program containing
+ only partial annotations. Finally, the implementation of this methos as
+ a tactic of the {\sl Coq} proof assistant is presented.",
+ paper = "Pare97.pdf"
+}
+
+\end{chunk}
+
\index{Poll, Erik}
\index{Thompson, Simon}
\begin{chunk}{axiom.bib}
diff --git a/changelog b/changelog
index 3348c53..fee9455 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,6 @@
+20170103 tpd src/axiom-website/patches.html 20170103.01.tpd.patch
+20170103 tpd books/bookvol13 COQ proof of GCD
+20170103 tpd books/bookvolbib COQ Program Construction papers
20170102 tpd src/axiom-website/patches.html 20170102.01.tpd.patch
20170102 tpd books/bookvolbib LEAN source code and GCD proof references
20170102 tpd books/bookvol13 LEAN source code and GCD proof
diff --git a/patch b/patch
index 0d362e9..f87b0c8 100644
--- a/patch
+++ b/patch
@@ -1,28 +1,169 @@
-books/bookvol13 LEAN source code and GCD proof
+books/bookvolbib COQ Program Construction papers
Goal: Proving Axiom Correct
-From a discussion with Jeremy Avigad re: LEAN and GCD:
-\index{Avigad, Jeremy}
+\index{Coquand, Thierry}
+\index{Huet, G\'erard}
+\index{Paulin, Christine}
\begin{chunk}{axiom.bib}
-@misc{Avig14,
- author = "Avigad, Jeremy",
- title = "LEAN proof of GCD",
- url =
- "http://github.com/leanprover/lean2/blob/master/library/data/nat/gcd.lean",
- year = "2014"
+@misc{COQx16,
+ author = {Coquand, Thierry and Huet, G\'erard and Paulin, Christine},
+ title = "The COQ Proof Assistant",
+ year = "2016",
+ url = "https://coq.inria.fr"
+}
+
+\index{Coquand, Thierry}
+\index{Huet, G\'erard}
+\index{Paulin, Christine}
+\begin{chunk}{axiom.bib}
+@misc{COQx16a,
+ author = {Coquand, Thierry and Huet, G\'erard and Paulin, Christine},
+ title = "COQ Proof Assistant Library Coq.ZArith.Znumtheory",
+ year = "2016",
+ url = "https://coq.inria.fr/library/Coq.ZArith.Znumtheory.html"
+}
+
+\index{Parent, Catherine}
+\begin{chunk}{axiom.bib}
+@techreport{Pare94,
+ author = "Parent, Catherine",
+ title = "Synthesizing proofs from programs in the Calculus of Inductive
+ Constructions",
+ year = "1994",
+ institution = {Ecole Normale Sup\'erieure de Lyon},
+ abstract =
+ "In type theory, a proof can be represented as a typed $\lambda$-term.
+ There exist methods to mark logical parts in proofs and extract their
+ algorithmic contents. The result is a correct program with respect to
+ a specification. This paper focuses on the inverse problem: how to
+ generate a proof from its specification. The framework is the Calculus
+ of Inductive Constructions. A notion of coherence is introduced between
+ a specification and a program containing types but no logical proofs.
+ This notion is based on the definition of an extraction function called
+ the weak extraction. Such a program can give a method to reconstruct a
+ set of logical properties needed to have a proof of the initial
+ specification. This can be seen either as a method of proving programs
+ or as a method of synthetically describing proofs.",
+ paper = "Pare94.pdf"
+}
+
+\end{chunk}
+
+\index{Parent-Vigouroux, Catherine}
+\begin{chunk}{axiom.bib}
+@article{Pare97,
+ author = "Parent-Vigouroux, Catherine",
+ title = "Verifying programs in the Calculus of Inductive Constructions",
+ year = "1997",
+ journal = "Formal Aspects of Computing",
+ volume = "9",
+ number = "5",
+ pages = "484-517",
+ abstract =
+ "This paper deals with a particular approach to the verification of
+ functional programs. A specification of a program can be represented
+ by a logical formula. In a constructive framework, developing a program
+ then corresponds to proving this formula. Given a specification and a
+ program, we focus on reconstructing a proof of the specification whose
+ algorithmic contents corresponds to the given program. The best we can
+ hope is to generate proof obligations on atomic parts of the program
+ corresponding to logical properties to be verified. First, this paper
+ studies a weak extraction of a program from a proof that keeps track
+ of intermediate specifications. From such a program, we prove the
+ determinism of retrieving proof obligations. Then, heuristic methods
+ are proposed for retrieving the proof from a natural program containing
+ only partial annotations. Finally, the implementation of this methos as
+ a tactic of the {\sl Coq} proof assistant is presented.",
+ paper = "Pare97.pdf"
+}
+
+\end{chunk}
+
+\index{Parent-Vigouroux, Catherine}
+\begin{chunk}{axiom.bib}
+@misc{Pare96,
+ author = "Parent-Vigouroux, Catherine",
+ title = "Natural proofs versus programs optimization in the
+ Calculus of Inductive Constructions",
+ year = "1996",
+ abstract =
+ "This paper presents how to automatically prove that an 'optimized'
+ program is correct with respect to a set of given properties that is a
+ specification. Proofs of specifications contain logical and
+ computational parts. Programs can be seen as computational parts of
+ proofs. They can thus be extracted from proofs and be certified to be
+ correct. The inverse problem can be solved: it is possible to
+ reconstruct proof obligations from a program and its specification.
+ The framework is a type theory where a proof can be represented as a
+ typed $\lambda$-term and, particularly, the Calculus of Inductive
+ Constructions. This paper shows how programs can be simplified in
+ order to be written in a much closer way to the ML one's. Indeed,
+ proofs structures are often much more heavy than program structures.
+ The problem is consequently to consider natural programs (in a ML sense)
+ and see how to retrieve natural structures of proofs from them.",
+ paper = "Pare96.pdf"
+}
+
+\end{chunk}
+
+\index{Parent, Catherine}
+\begin{chunk}{axiom.bib}
+@inproceedings{Pare93,
+ author = "Parent, Catherine",
+ title = "Developing Certified Programs in the System Coq: The Program
+ Tactic",
+ booktitle = "Proc. Int. Workshop on Types for Proofs and Programs",
+ publisher = "Springer-Verlag",
+ isbn = "3-540-58085-9",
+ pages = "291-312",
+ year = "1993",
+ abstract =
+ "The system {\sl Coq} is an environment for proof development based on
+ the Calculus of Constructions extended by inductive definitions. The
+ specification of a program can be represented by a logical formula and
+ the program itself can be extracted from the constructive proof of the
+ specification. In this paper, we look at the possibility of inverting
+ the specification and a program, builds the logical condition to be
+ verified in order to obtain a correctness proof of the program. We
+ build a proof of the specification from the program from which the
+ program can be extracted. Since some information cannot automatically
+ be inferred, we show how to annotate the program by specifying some of
+ its parts in order to guide the search for the proof.",
+ paper = "Pare93.ps"
}
\end{chunk}
-\index{Avigad, Jeremy}
+\index{Coquand, Thierry}
+\index{Huet, G\'erard}
\begin{chunk}{axiom.bib}
-@misc{Avig16,
- author = "Avigad, Jeremy",
- title = "LEAN github repository",
- url = "http://github.com/leanprover",
- year = "2016"
+@techreport{Coqu86,
+ author = {Coquand, Thierry and Huet, G\'erard},
+ title = "The Calculus of Constructions",
+ year = "1986",
+ institution = "INRIA Centre de Rocquencourt",
+ number = "530",
+ url = "https://hal.inria.fr/inria-00076024/document",
+ abstract =
+ "The Calculus of Constructions is a higher-order formalism for
+ constructive proofs in natural deduction style. Every proof is a
+ $\lambda$-expression, typed with propositions of the underlying
+ logic. By removing types we get a pure $\lambda$-expression,
+ expressing its associated algorithm. Computing this
+ $\lambda$-expression corresponds roughly to cut-elimination. It is our
+ thesis that (as already advocated by Martin-Lof) the Curry-Howard
+ correspondence between propositions and types is a powerful paradigm
+ for Computer Science. In the case of Constructions, we obtain the
+ notion of a very high-level functional programming language, with
+ complex polymorphism well-suited for modules specification. The notion
+ of type encompasses the usual notioin of data type, but allows as well
+ arbitrarily complex algorithmic specifications. We develop the basic
+ theory of a Calculus of Constructions, and prove a strong
+ normalization theorem showing that all computations terminate.
+ Finally, we suggest various extensions to stronger calculi.",
+ paper = "Coqu86.pdf"
}
\end{chunk}
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index 6a766f0..e059e98 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -5618,6 +5618,8 @@ books/bookvolbib Mahboubi Mathematical Components

books/bookvolbib Stephane Delliere Phd Thesis

20170102.01.tpd.patch
books/bookvol13 LEAN source code and GCD proof

+20170103.01.tpd.patch
+books/bookvolbib COQ Program Construction papers

--
1.7.5.4