Mercurial > cpdt > repo

changeset 568:81d63d9c1cc5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Port to Coq 8.9.0
author Adam Chlipala <adam@chlipala.net>
date Sun, 20 Jan 2019 15:16:29 -0500
parents ec0ce5129fc4
children 0ce9829efa3b
files .hgignore src/Coinductive.v src/DataStruct.v src/DepList.v src/Equality.v src/GeneralRec.v src/InductiveTypes.v src/Intro.v src/MoreDep.v src/ProgLang.v src/Universes.v
diffstat 11 files changed, 42 insertions(+), 41 deletions(-) [+]
line wrap: on
line diff
--- a/.hgignore	Sun Jan 20 15:00:32 2019 -0500
+++ b/.hgignore	Sun Jan 20 15:16:29 2019 -0500
@@ -38,3 +38,4 @@
 *.ind
 *.out
 src/.coq-native
+.coqdeps.d
--- a/src/Coinductive.v	Sun Jan 20 15:00:32 2019 -0500
+++ b/src/Coinductive.v	Sun Jan 20 15:16:29 2019 -0500
@@ -253,7 +253,7 @@
 Theorem ones_eq : stream_eq ones ones'.
   (** Coq does not support tactical co-inductive proofs as well as it supports tactical inductive proofs.  The usual starting point is the [cofix] tactic, which asks to structure this proof as a co-fixpoint. *)
 
-  cofix.
+  cofix ones_eq.
   (** [[
   ones_eq : stream_eq ones ones'
   ============================
@@ -323,7 +323,7 @@
 (** But, miraculously, this theorem turns out to be just what we needed. *)
 
 Theorem ones_eq : stream_eq ones ones'.
-  cofix.
+  cofix ones_eq.
 
   (** We can use the theorem to rewrite the two streams. *)
 
@@ -379,7 +379,7 @@
    One common source of difficulty with co-inductive proofs is bad interaction with standard Coq automation machinery.  If we try to prove [ones_eq'] with automation, like we have in previous inductive proofs, we get an invalid proof. *)
 
 Theorem ones_eq' : stream_eq ones ones'.
-  cofix; crush.
+  cofix one_eq'; crush.
   (** %\vspace{-.25in}%[[
   Guarded.
   ]]
@@ -418,7 +418,7 @@
   (** Now it is straightforward to prove the principle, which says that any stream pair in [R] is equal.  The reader may wish to step through the proof script to see what is going on. *)
 
   Theorem stream_eq_coind : forall s1 s2, R s1 s2 -> stream_eq s1 s2.
-    cofix; destruct s1; destruct s2; intro.
+    cofix stream_eq_coind; destruct s1; destruct s2; intro.
     generalize (Cons_case_hd H); intro Heq; simpl in Heq; rewrite Heq.
     constructor.
     apply stream_eq_coind.
@@ -615,7 +615,7 @@
   (** The proof is routine.  We make use of a form of %\index{tactics!destruct}%[destruct] that takes an%\index{intro pattern}% _intro pattern_ in an [as] clause.  These patterns control how deeply we break apart the components of an inductive value, and we refer the reader to the Coq manual for more details. *)
 
   Theorem evalCmd_coind : forall vs1 c vs2, R vs1 c vs2 -> evalCmd vs1 c vs2.
-    cofix; intros; destruct c.
+    cofix evalCmd_coind; intros; destruct c.
     rewrite (AssignCase H); constructor.
     destruct (SeqCase H) as [? [? ?]]; econstructor; eauto.
     destruct (WhileCase H) as [[? ?] | [? [? [? ?]]]]; subst; econstructor; eauto.
--- a/src/DataStruct.v	Sun Jan 20 15:00:32 2019 -0500
+++ b/src/DataStruct.v	Sun Jan 20 15:16:29 2019 -0500
@@ -117,8 +117,8 @@
 (* end thide *)
 End ilist.
 
-Implicit Arguments Nil [A].
-Implicit Arguments First [n].
+Arguments Nil [A].
+Arguments First [n].
 
 (** A few examples show how to make use of these definitions. *)
 
@@ -242,11 +242,11 @@
 End hlist.
 
 (* begin thide *)
-Implicit Arguments HNil [A B].
-Implicit Arguments HCons [A B x ls].
+Arguments HNil [A B].
+Arguments HCons [A B x ls].
 
-Implicit Arguments HFirst [A elm ls].
-Implicit Arguments HNext [A elm x ls].
+Arguments HFirst [A elm ls].
+Arguments HNext [A elm x ls].
 (* end thide *)
 
 (** By putting the parameters [A] and [B] in [Type], we enable fancier kinds of polymorphism than in mainstream functional languages.  For instance, one use of [hlist] is for the simple heterogeneous lists that we referred to earlier. *)
@@ -302,7 +302,7 @@
 | Abs : forall ts dom ran, exp (dom :: ts) ran -> exp ts (Arrow dom ran).
 (* end thide *)
 
-Implicit Arguments Const [ts].
+Arguments Const [ts].
 
 (** We write a simple recursive function to translate [type]s into [Set]s. *)
 
@@ -481,7 +481,7 @@
 
 End fhlist.
 
-Implicit Arguments fhget [A B elm ls].
+Arguments fhget [A B elm ls].
 
 (** How does one choose between the two data structure encoding strategies we have presented so far?  Before answering that question in this chapter's final section, we introduce one further approach. *)
 
@@ -592,7 +592,7 @@
 
 End tree.
 
-Implicit Arguments Node [A n].
+Arguments Node [A n].
 
 (** We can redefine [sum] and [inc] for our new [tree] type.  Again, it is useful to define a generic fold function first.  This time, it takes in a function whose domain is some [ffin] type, and it folds another function over the results of calling the first function at every possible [ffin] value. *)
 
@@ -608,7 +608,7 @@
     end.
 End rifoldr.
 
-Implicit Arguments rifoldr [A B n].
+Arguments rifoldr [A B] f i [n].
 
 Fixpoint sum (t : tree nat) : nat :=
   match t with
@@ -708,7 +708,7 @@
     end.
 End cond.
 
-Implicit Arguments cond [A n].
+Arguments cond [A] default [n].
 (* end thide *)
 
 (** Now the expression interpreter is straightforward to write. *)
@@ -797,7 +797,7 @@
     end.
 End cfoldCond.
 
-Implicit Arguments cfoldCond [t n].
+Arguments cfoldCond [t] default [n].
 (* end thide *)
 
 (** Like for the interpreters, most of the action was in this helper function, and [cfold] itself is easy to write. *)
--- a/src/DepList.v	Sun Jan 20 15:00:32 2019 -0500
+++ b/src/DepList.v	Sun Jan 20 15:16:29 2019 -0500
@@ -107,8 +107,8 @@
   End fold.
 End ilist.
 
-Implicit Arguments INil [A].
-Implicit Arguments First [n].
+Arguments INil [A].
+Arguments First [n].
 
 Section imap.
   Variables A B : Type.
@@ -197,12 +197,12 @@
   Qed.
 End hlist.
 
-Implicit Arguments HNil [A B].
-Implicit Arguments HCons [A B x ls].
-Implicit Arguments hmake [A B].
+Arguments HNil [A B].
+Arguments HCons [A B x ls].
+Arguments hmake [A B].
 
-Implicit Arguments HFirst [A elm ls].
-Implicit Arguments HNext [A elm x ls].
+Arguments HFirst [A elm ls].
+Arguments HNext [A elm x ls].
 
 Infix ":::" := HCons (right associativity, at level 60).
 Infix "+++" := happ (right associativity, at level 60).
@@ -233,4 +233,4 @@
   Qed.
 End hmap.
 
-Implicit Arguments hmap [A B1 B2 ls].
+Arguments hmap [A B1 B2] f [ls].
--- a/src/Equality.v	Sun Jan 20 15:00:32 2019 -0500
+++ b/src/Equality.v	Sun Jan 20 15:16:29 2019 -0500
@@ -214,7 +214,7 @@
     end.
 End fhlist.
 
-Implicit Arguments fhget [A B elm ls].
+Arguments fhget [A B elm ls].
 
 (* begin hide *)
 (* begin thide *)
@@ -235,7 +235,7 @@
       | _ :: _ => fun hls => (f (fst hls), fhmap _ (snd hls))
     end.
 
-  Implicit Arguments fhmap [ls].
+  Arguments fhmap [ls].
 
   (* begin hide *)
   (* begin thide *)
@@ -496,7 +496,7 @@
       | _ :: _ => fun hls1 hls2 => (fst hls1, fhapp _ _ (snd hls1) hls2)
     end.
 
-  Implicit Arguments fhapp [ls1 ls2].
+  Arguments fhapp [ls1 ls2].
 
   (* EX: Prove that fhapp is associative. *)
 (* begin thide *)
@@ -676,7 +676,7 @@
 (* end thide *)
 End fhapp.
 
-Implicit Arguments fhapp [A B ls1 ls2].
+Arguments fhapp [A B ls1 ls2].
 
 (** This proof strategy was cumbersome and unorthodox, from the perspective of mainstream mathematics.  The next section explores an alternative that leads to simpler developments in some cases. *)
 
--- a/src/GeneralRec.v	Sun Jan 20 15:00:32 2019 -0500
+++ b/src/GeneralRec.v	Sun Jan 20 15:16:29 2019 -0500
@@ -654,7 +654,7 @@
        end.
 
   Theorem thunk_eq_coind : forall m1 m2, P m1 m2 -> thunk_eq m1 m2.
-    cofix; intros;
+    cofix thunk_eq_coind; intros;
       match goal with
         | [ H' : P _ _ |- _ ] => specialize (H H'); clear H'
       end; destruct m1; destruct m2; subst; repeat constructor; auto.
--- a/src/InductiveTypes.v	Sun Jan 20 15:00:32 2019 -0500
+++ b/src/InductiveTypes.v	Sun Jan 20 15:16:29 2019 -0500
@@ -479,9 +479,9 @@
 (* end thide *)
 End list.
 
-Implicit Arguments Nil [T].
+Arguments Nil [T].
 
-(** After we end the section, the [Variable]s we used are added as extra function parameters for each defined identifier, as needed.  With an [Implicit Arguments]%~\index{Vernacular commands!Implicit Arguments}% command, we ask that [T] be inferred when we use [Nil]; Coq's heuristics already decided to apply a similar policy to [Cons], because of the [Set Implicit Arguments]%~\index{Vernacular commands!Set Implicit Arguments}% command elided at the beginning of this chapter.  We verify that our definitions have been saved properly using the [Print] command, a cousin of [Check] which shows the definition of a symbol, rather than just its type. *)
+(** After we end the section, the [Variable]s we used are added as extra function parameters for each defined identifier, as needed.  With an [Arguments]%~\index{Vernacular commands!Arguments}% command, we ask that [T] be inferred when we use [Nil]; Coq's heuristics already decided to apply a similar policy to [Cons], because of the [Set Implicit Arguments]%~\index{Vernacular commands!Set Implicit Arguments}% command elided at the beginning of this chapter.  We verify that our definitions have been saved properly using the [Print] command, a cousin of [Check] which shows the definition of a symbol, rather than just its type. *)
 
 Print list.
 (** %\vspace{-.15in}% [[
--- a/src/Intro.v	Sun Jan 20 15:00:32 2019 -0500
+++ b/src/Intro.v	Sun Jan 20 15:16:29 2019 -0500
@@ -186,7 +186,7 @@
 (** ** Installation and Emacs Set-Up *)
 
 (**
-At the start of the next chapter, I assume that you have installed Coq and Proof General.  The code in this book is tested with Coq versions 8.6.1 and 8.7.1.  Though parts may work with other versions, it is expected that the book source will fail to build with _earlier_ versions.
+At the start of the next chapter, I assume that you have installed Coq and Proof General.  The code in this book is tested with Coq version 8.9.0.  Though parts may work with other versions, it is expected that the book source will fail to build with many _earlier_ versions.
 
 %\index{Proof General|(}%To set up your Proof General environment to process the source to the next chapter, a few simple steps are required.
 
--- a/src/MoreDep.v	Sun Jan 20 15:00:32 2019 -0500
+++ b/src/MoreDep.v	Sun Jan 20 15:16:29 2019 -0500
@@ -647,7 +647,7 @@
 
   (** We modify Coq's default choice of implicit arguments for [makeRbtree], so that we do not need to specify the [c] and [n] arguments explicitly in later calls. *)
 
-  Implicit Arguments makeRbtree [c n].
+  Arguments makeRbtree [c n].
 
   (** Finally, we define [insert] as a simple composition of [ins] and [makeRbtree]. *)
 
@@ -917,7 +917,7 @@
   Defined.
 End split.
 
-Implicit Arguments split [P1 P2].
+Arguments split [P1 P2].
 
 (* begin hide *)
 Lemma app_empty_end : forall s, s ++ "" = s.
--- a/src/ProgLang.v	Sun Jan 20 15:00:32 2019 -0500
+++ b/src/ProgLang.v	Sun Jan 20 15:16:29 2019 -0500
@@ -105,7 +105,7 @@
 
   | Let : forall G t1 t2, term G t1 -> term (t1 :: G) t2 -> term G t2.
 
-  Implicit Arguments Const [G].
+  Arguments Const [G].
 
   (** Here are two example term encodings, the first of addition packaged as a two-argument curried function, and the second of a sample application of addition to constants. *)
 
@@ -266,7 +266,7 @@
                 end
     end.
 
-  Implicit Arguments insertAtS [t G].
+  Arguments insertAtS [t] x [G].
 
   (** Next we prove that [liftVar] is correct.  That is, a lifted variable retains its value with respect to a substitution when we perform an analogue to lifting by inserting a new mapping into the substitution. *)
 
@@ -355,9 +355,9 @@
     | Let : forall t1 t2, term t1 -> (var t1 -> term t2) -> term t2.
   End var.
 
-  Implicit Arguments Var [var t].
-  Implicit Arguments Const [var].
-  Implicit Arguments Abs [var dom ran].
+  Arguments Var [var t].
+  Arguments Const [var].
+  Arguments Abs [var dom ran].
 
   (** Coq accepts this definition because our embedded functions now merely take _variables_ as arguments, instead of arbitrary terms.  One might wonder whether there is an easy loophole to exploit here, instantiating the parameter [var] as [term] itself.  However, to do that, we would need to choose a variable representation for this nested mention of [term], and so on through an infinite descent into [term] arguments.
 
--- a/src/Universes.v	Sun Jan 20 15:00:32 2019 -0500
+++ b/src/Universes.v	Sun Jan 20 15:16:29 2019 -0500
@@ -1165,7 +1165,7 @@
     destruct n; simpl; unfold error; congruence.
   Defined.
 
-  Implicit Arguments nth_error_nil [A n x].
+  Arguments nth_error_nil [A n x].
 
   Lemma Some_inj : forall A (x y : A),
     Some x = Some y