From 6263c7cea5e8340ab6d8d03397e87e920a6bfd72 Mon Sep 17 00:00:00 2001
From: Thomas Letan
Date: Tue, 18 Feb 2020 22:02:27 +0100
Subject: Do not extract Coq terms in StronglySpecified Functions part 2

site/posts/StronglySpecifiedFunctions.v  10 +++++
site/posts/StronglySpecifiedFunctionsProgram.v  20 +++
2 files changed, 8 insertions(+), 22 deletions()
diff git a/site/posts/StronglySpecifiedFunctions.v b/site/posts/StronglySpecifiedFunctions.v
index 3adfe50..55af679 100644
 a/site/posts/StronglySpecifiedFunctions.v
+++ b/site/posts/StronglySpecifiedFunctions.v
@@ 1,9 +1,9 @@
(** # StronglySpecified Functions in Coq, part 1: using the refine
Tactic
#
+(** #StronglySpecified Functions in Coq, part 1: using the refine
Tactic
#
 This is the first article (initially published on #January
 11, 2015#) of a series of two on how to write stronglyspecified
 functions in Coq. You can read the next part #here#. *)
+ This is the first article (initially published on #January 11, 2015#) of a series of two on how to write
+ stronglyspecified functions in Coq. You can read the next part #here#. *)
(** I started to play with Coq, the interactive theorem prover
developed by Inria, a few weeks ago. It is a very powerful tool,
diff git a/site/posts/StronglySpecifiedFunctionsProgram.v b/site/posts/StronglySpecifiedFunctionsProgram.v
index 037b0dd..ae996e7 100644
 a/site/posts/StronglySpecifiedFunctionsProgram.v
+++ b/site/posts/StronglySpecifiedFunctionsProgram.v
@@ 246,14 +246,8 @@ Defined.
[{ v': vector A e  forall (i : nat  i < e), nth v' i = nth v i
}]. However, this made the goals and hypotheses become very hard
to read and to use. Sigmatypes in sigmatypes: not a good
 idea. *)
+ idea.
From Coq Require Import Extraction.

Extraction Implicit take [a n].
Extraction take.

(**
<<
(** val take : 'a1 vector > nat > 'a1 vector **)
@@ 298,13 +292,9 @@ Next Obligation.
now apply PeanoNat.Nat.nle_succ_0 in H.
Defined.
(*begin hide *)
Extraction Implicit drop [a n].
Extraction drop.
(* end hide *)
(** The proofs are easy to write, and the extracted code is exactly what one might
 want it to be: *)
(**
+ want it to be:
+
<<
(** val drop : 'a1 vector > nat > 'a1 vector **)
let rec drop v = function
@@ 342,10 +332,6 @@ Next Obligation.
lia.
Defined.
(*begin hide *)
Extraction Implicit extract [a n].
Extraction extract.
(* end hide *)
(** The proofs are straightforward because the specifications of [drop] and
[take] are precise enough, and we do not need to have a look at their
implementations. The extracted version of [extract] is as clean as we can

cgit v1.2.3