1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
|
Changes from V8.0
=================
Environment variables
- COQREMOTEBROWSER to set the command invoked to start the remote browser
both in Coq and coqide. Standard syntax: "%s" is the placeholder for the
URL (doc TODO)
Vernacular commands
- Added "Print Ltac qualid" to print a user defined tactic (doc TODO)
- Added "Print Rewrite HintDb" to print the content of a DB used by
autorewrite (doc TODO)
- Added "Print Canonical Projections" (doc TODO)
Gallina
- Added disjunctive patterns in match-with patterns
Ltac
- New primitive "external" for communication with tool external to Coq
- Semantics of "match t with" changed: if a clause returns a
tactic, it is now applied to the current goal. If it fails, the next
clause or next matching subterm is tried (i.e. it behaves as "match
goal with").
- New modifier "lazy" (TODO) for "match t with" and "match goal with" telling
to delay the evaluation of tactic expression.
Tactics
- New implementation and generalization of [setoid_]* (setoid_rewrite,
setoid_symmetry, setoid_transitivity, setoid_reflexivity and autorewite).
New syntax for declaring relations and morphisms (old syntax still working
with minor modifications, but deprecated) (doc TODO)
- Added "clear - id" to clear all hypotheses except the ones depending in id.
- Added "dependent rewrite term" and "dependent rewrite term in hyp" (doc TODO)
- The argument of Declare Left Step and Declare Right Step is now a term
(it used to be a reference) (doc TODO)
- Omega now handles arbitrary precision integers
- Idtac can now be left implicit in a [...|...] construct: for instance,
[ foo | | bar ] stands for [ foo | idtac | bar ]. (doc TODO).
- "Tactic Notation" extended to allow notations of tacticals (doc TODO).
- Added "autorewrite with ... in hyp [using ...]" (doc TODO).
- Added entry constr_may_eval for tactic extensions (new syntax).
- Fixed a "fold" bug (non critical and possible source of incompatibilities).
- Added classical_left and classical_right which transforms |- A \/ B into
~B |- A and ~A |- B respectively.
- Added command "Declare Implicit Tactic" to set up a default tactic to be
used to solve unresolved subterms of term arguments of tactics.
- Better support for coercions to Sortclass in tactics expecting type arguments
- Low-priority term printer made available in ML-written tactic extensions
Modules
- Added "Locate Module qualid" to get the full path of a module.
- Module/Declare Module syntax made more uniform (doc TODO)
- Added syntactic sugar "Declare Module Export/Import" and
"Module Export/Import" (doc TODO)
- Added syntactic sugar "Module M(Export/Import X Y: T)" and
"Module Type M(Export/Import X Y: T)"
(only for interactive definitions) (doc TODO)
- Construct "with" generalized to module paths:
T with (Definition|Module) M1.M2....Mn.l := l'. (doc TODO)
Notations
- "format" option aware of recursive notations
- no more automatic printing box in case of user-provided printing "format"
Library
- Few improvements in ZArith potentially exceptionally breaking the
compatibility (useless hypothesys of Zgt_square_simpl and
Zlt_square_simpl removed; fixed names mentioning letter O instead of
digit 0; weaken premises in Z_lt_induction)
Changes from V8.0beta to V8.0
=============================
Vernacular commands
- New option "Set Printing All" to deactivate all high-level forms of
printing (implicit arguments, coercions, destructing let,
if-then-else, notations, projections)
- "Functional Scheme" and "Functional Induction" extended to polymorphic
types and dependent types
- Notation now allows recursive patterns, hence recovering parts of the
fonctionalities of pre-V8 Grammar/Syntax commands
- Command "Print." discontinued.
- Redundant syntax "Implicit Arguments On/Off" discontinued
New syntax
- Semantics change of the if-then-else construction in new syntax:
"if c then t1 else t2" now stands for
"match c with c1 _ ... _ => t1 | c2 _ ... _ => t2 end"
with no dependency of t1 and t2 in the arguments of the constructors;
this may cause incompatibilities for files translated using coq 8.0beta
Interpretation scopes
- Delimiting key %bool for bool_scope added
- Import no more needed to activate argument scopes from a module
Tactics and the tactic Language
- Semantics of "assert" is now consistent with the reference manual
- New tactics stepl and stepr for chaining transitivity steps
- Tactic "replace ... with ... in" added
- Intro patterns now supported in Ltac (parsed with prefix "ipattern:")
Executables and tools
- Added option -top to change the name of the toplevel module "Top"
- Coqdoc updated to new syntax and now part of Coq sources
- XML exportation tool now exports the structure of vernacular files
(cf chapter 13 in the reference manual)
User contributions
- User contributions have been updated to the new syntax
Bug fixes
- Many bugs have been fixed (cf coq-bugs web page)
Changes from V8.0beta old syntax to V8.0beta
============================================
New concrete syntax
- A completely new syntax for terms
- A more uniform syntax for tactics and the tactic language
- A few syntactic changes for vernacular commands
- A smart automatic translator translating V8.0 files in old syntax to
files valid for V8.0
Syntax extensions
- "Grammar" for terms disappears
- "Grammar" for tactics becomes "Tactic Notation"
- "Syntax" disappears
- Introduction of a notion of interpretation scope allowing to use the
same notations in various contexts without using specific delimiters
(e.g the same expression "4<=3+x" is interpreted either in "nat",
"positive", "N" (previously "entier"), "Z", "R", depending on which
interpretation scope is currently open) [see documentation for details]
- Notation now mandatorily requires a precedence and associativity
(default was to set precedence to 1 and associativity to none)
Revision of the standard library
- Many lemmas and definitions names have been made more uniform mostly
in Arith, NArith, ZArith and Reals (e.g : "times" -> "Pmult",
"times_sym" -> "Pmult_comm", "Zle_Zmult_pos_right" ->
"Zmult_le_compat_r", "SUPERIEUR" -> "Gt", "ZERO" -> "Z0")
- Order and names of arguments of basic lemmas on nat, Z, positive and R
have been made uniform.
- Notions of Coq initial state are declared with (strict) implicit arguments
- eq merged with eqT: old eq disappear, new eq (written =) is old eqT
and new eqT is syntactic sugar for new eq (notation == is an alias
for = and is written as it, exceptional source of incompatibilities)
- Similarly, ex, ex2, all, identity are merged with exT, exT2, allT, identityT
- Arithmetical notations for nat, positive, N, Z, R, without needing
any backquote or double-backquotes delimiters.
- In Lists: new concrete notations; argument of nil is now implicit
- All changes in the library are taken in charge by the translator
Semantical changes during translation
- Recursive keyword set by default (and no longer needed) in Tactic Definition
- Set Implicit Arguments is strict by default in new syntax
- reductions in hypotheses of the form "... in H" now apply to the type
also if H is a local definition
- etc
Gallina
- New syntax of the form "Inductive bool : Set := true, false : bool." for
enumerated types
- Experimental syntax of the form p.(fst) for record projections
(activable with option "Set Printing Projections" which is
recognized by the translator)
Known problems of the automatic translation
- iso-latin-1 characters are no longer supported: move your files to
7-bits ASCII or unicode before translation (swith to unicode is
automatically done if a file is loaded and saved again by coqide)
- Renaming in ZArith: incompatibilities in Coq user contribs due to
merging names INZ, from Reals, and inject_nat.
- Renaming and new lemmas in ZArith: may clash with names used by users
- Restructuration of ZArith: replace requirement of specific modules
in ZArith by "Require Import ZArith_base" or "Require Import ZArith"
- Some implicit arguments must be made explicit before translation: typically
for "length nil", the implicit argument of length must be made explicit
- Grammar rules, Infix notations and V7.4 Notations must be updated wrt the
new scheme for syntactic extensions (see translator documentation)
- Unsafe for annotation Cases when constructors coercions are used or when
annotations are eta-reduced predicates
Changes from V7.4 to V8.0beta old syntax
========================================
Logic
- Set now predicative by default
- New option -impredicative-set to set Set impredicative
- The standard library doesn't need impredicativity of Set and is
compatible with the classical axioms which contradict Set impredicativity
Syntax for arithmetic
- Notation "=" and "<>" in Z and R are no longer implicitly in Z or R
(with possible introduction of a coercion), use <Z>...=... or
<Z>...<>... instead
- Locate applied to a simple string (e.g. "+") searches for all
notations containing this string
Vernacular commands
- "Declare ML Module" now allows to import .cma files. This avoids to use a
bunch of "Declare ML Module" statements when using several ML files.
- "Set Printing Width n" added, allows to change the size of width printing
(TODO : doc).
- "Implicit Variables Type x,y:t" (new syntax: "Implicit Types x y:t")
assigns default types for binding variables.
- Declarations of Hints and Notation now accept a "Local" flag not to
be exported outside the current file even if not in section
- "Print Scopes" prints all notations
- New command "About name" for light printing of type, implicit arguments, etc.
- New command "Admitted" to declare incompletely proven statement as axioms
- New keyword "Conjecture" to declare an axiom intended to be provable
- SearchAbout can now search for lemmas referring to more than one constant
and on substrings of the name of the lemma
- "Print Implicit" displays the implicit arguments of a constant
- Locate now searches for all names having a given suffix
- New command "Functional Scheme" for building an induction principle
from a function defined by case analysis and fix.
Commands
- new coqtop/coqc option -dont-load-proofs not to load opaque proofs in memory
Implicit arguments
- Inductive in sections declared with implicits now "discharged" with
implicits (like constants and variables)
- Implicit Arguments flags are now synchronous with reset
- New switch "Unset/Set Printing Implicits" (new syntax: "Unset/Set Printing
Implicit") to globally control printing of implicits
Grammar extensions
- UTF-8 encoded unicode blocks 0380-03FF (greek letters) and 2100-214F
(letter-like, including aleph and double N,Z,Q,R) are supported
identifiers; UTF-8 unicode blocs 2200-22FF (mathematical operators),
2A00-2AFF (supplemental mathematical operators) 2300-23FF
(miscellaneous technical, including sqrt symbol), 2600-26FF
(miscellaneous symbols) 2190-21FF (arrows A) and 2900-297F (arrows B)
are supported symbols
Library
- New file about the factorial function in Arith
- An additional elimination Acc_iter for Acc, simplier than Acc_rect.
This new elimination principle is used for definition well_founded_induction.
- New library NArith on binary natural numbers
- R is now of type Set
- Restructuration in ZArith library
- "true_sub" used in Zplus now a definition, not a local one (source
of incompatibilities in proof referring to true_sub, may need extra Unfold)
- Some lemmas about minus moved from fast_integer to Arith/Minus.v
(le_minus, lt_mult_left) (theoretical source of incompatibilities)
- Several lemmas moved from auxiliary.v and zarith_aux.v to
fast_integer.v (theoretical source of incompatibilities)
- Variables names of iff_trans changed (source of incompatibilities)
- ZArith lemmas named OMEGA something or fast_ something, and lemma new_var
are now out of ZArith (except OMEGA2)
- Redundant ZArith lemmas have been renamed: for the following pairs,
use the second name (Zle_Zmult_right2, Zle_mult_simpl), (OMEGA2,
Zle_0_plus), (Zplus_assoc_l, Zplus_assoc), (Zmult_one, Zmult_1_n),
(Zmult_assoc_l, Zmult_assoc), (Zmult_minus_distr, Zmult_Zminus_distr_l)
(add_un_double_moins_un_xO, is_double_moins_un),
(Rlt_monotony_rev,Rlt_monotony_contra) (source of incompatibilities)
- Few minor changes (no more implicit arguments in
Zmult_Zminus_distr_l and Zmult_Zminus_distr_r, lemmas moved from
Zcomplements to other files) (rare source of incompatibilities)
- New lemmas provided by users added
Tactic language
- Fail tactic now accepts a failure message
- Idtac tactic now accepts a message
- New primitive tactic "FreshId" (new syntax: "fresh") to generate new names
- Debugger prints levels of calls
Tactics
- Replace can now replace proofs also
- Fail levels are now decremented at "Match Context" blocks only and
if the right-hand-side of "Match term With" are tactics, these
tactics are never evaluated immediately and do not induce
backtracking (in contrast with "Match Context")
- Quantified names now avoid global names of the current module (like
Intro names did) [source of rare incompatibilities: 2 changes in the set of
user contribs]
- NewDestruct/NewInduction accepts intro patterns as introduction names
- NewDestruct/NewInduction now work for non-inductive type using option "using"
- A NewInduction naming bug for inductive types with functional
arguments (e.g. the accessibility predicate) has been fixed (source
of incompatibilities)
- Symmetry now applies to hypotheses too
- Inversion now accept option "as [ ... ]" to name the hypotheses
- Contradiction now looks also for contradictory hypotheses stating ~A and A
(source of incompatibility)
- "Contradiction c" try to find an hypothesis in context which
contradicts the type of c
- Ring applies to new library NArith (require file NArithRing)
- Field now works on types in Set
- Auto with reals now try to replace le by ge (Rge_le is no longer an
immediate hint), resulting in shorter proofs
- Instantiate now works in hyps (syntax : Instantiate in ...)
- Some new tactics : EConstructor, ELeft, Eright, ESplit, EExists
- New tactic "functional induction" to perform case analysis and
induction following the definition of a function.
- Clear now fails when trying to remove a local definition used by
a constant appearing in the current goal
Extraction (See details in contrib/extraction/CHANGES)
- The old commands: (Recursive) Extraction Module M.
are now: (Recursive) Extraction Library M.
To use these commands, M should come from a library M.v
- The other syntax Extraction & Recursive Extraction now accept
module names as arguments.
Bugs
- see coq-bugs server for the complete list of fixed bugs
Miscellaneous
- Implicit parameters of inductive types definition now taken into
account for infering other implicit arguments
Incompatibilities
- Persistence of true_sub (4 incompatibilities in Coq user contributions)
- Variable names of some constants changed for a better uniformity (2 changes
in Coq user contributions)
- Naming of quantified names in goal now avoid global names (2 occurrences)
- NewInduction naming for inductive types with functional arguments
(no incompatibility in Coq user contributions)
- Contradiction now solve more goals (source of 2 incompatibilities)
- Merge of eq and eqT may exceptionally result in subgoals now
solved automatically
- Redundant pairs of ZArith lemmas may have different names: it may
cause "Apply/Rewrite with" to fail if using the first name of a pair
of redundant lemmas (this is solved by renaming the variables bound by
"with"; 3 incompatibilities in Coq user contribs)
- ML programs referring to constants from fast_integer.v must use
"Coqlib.gen_constant_modules Coqlib.zarith_base_modules" instead
Changes from V7.3.1 to V7.4
===========================
Symbolic notations
- Introduction of a notion of scope gathering notations in a consistent set;
a notation sets has been developped for nat, Z and R (undocumented)
- New command "Notation" for declaring notations simultaneously for
parsing and printing (see chap 10 of the reference manual)
- Declarations with only implicit arguments now handled (e.g. the
argument of nil can be set implicit; use !nil to refer to nil
without arguments)
- "Print Scope sc" and "Locate ntn" allows to know to what expression a
notation is bound
- New defensive strategy for printing or not implicit arguments to ensure
re-type-checkability of the printed term
- In Grammar command, the only predefined non-terminal entries are ident,
global, constr and pattern (e.g. nvar, numarg disappears); the only
allowed grammar types are constr and pattern; ast and ast list are no
longer supported; some incompatibilities in Grammar: when a syntax is a
initial segment of an other one, Grammar does not work, use Notation
Library
- Lemmas in Set from Compare_dec.v (le_lt_dec, ...) and Wf_nat.v
(lt_wf_rec, ...) are now transparent. This may be source of
incompatibilities.
- Syntactic Definitions Fst, Snd, Ex, All, Ex2, AllT, ExT, ExT2,
ProjS1, ProjS2, Error, Value and Except are turned to
notations. They now must be applied (incompatibilities only in
unrealistic cases).
- More efficient versions of Zmult and times (30% faster)
- Reals: the library is now divided in 6 parts (Rbase, Rfunctions,
SeqSeries, Rtrigo, Ranalysis, Integration). New tactics: Sup and
RCompute. See Reals.v for details.
Modules
- Beta version, see doc chap 2.5 for commands and chap 5 for theory
Language
- Inductive definitions now accept ">" in constructor types to declare
the corresponding constructor as a coercion.
- Idem for assumptions declarations and constants when the type is mentionned.
- The "Coercion" and "Canonical Structure" keywords now accept the
same syntax as "Definition", i.e. "hyps :=c (:t)?" or "hyps :t".
- Theorem-like declaration now accepts the syntax "Theorem thm [x:t;...] : u".
- Remark's and Fact's now definitively behave as Theorem and Lemma: when
sections are closed, the full name of a Remark or a Fact has no longer a
section part (source of incompatibilities)
- Opaque Local's (i.e. built by tactics and ended by Qed), do not
survive section closing any longer; as a side-effect, Opaque Local's
now appear in the local context of proofs; their body is hidden
though (source of incompatibilities); use one of Remark/Fact/Lemma/Theorem
instead to simulate the old behaviour of Local (the section part of
the name is not kept though)
ML tactic and vernacular commands
- "Grammar tactic" and "Grammar vernac" of type "ast" are no longer
supported (only "Grammar tactic simple_tactic" of type "tactic"
remains available).
- Concrete syntax for ML written vernacular commands and tactics is
now declared at ML level using camlp4 macros TACTIC EXTEND et VERNAC
COMMAND EXTEND.
- "Check n c" now "n:Check c", "Eval n ..." now "n:Eval ..."
- "Proof with T" (* no documentation *)
- SearchAbout id - prints all theorems which contain id in their type
Tactic definitions
- Static globalisation of identifiers and global references (source of
incompatibilities, especially, Recursive keyword is required for
mutually recursive definitions).
- New evaluation semantics: no more partial evaluation at definition time;
evaluation of all Tactic/Meta Definition, even producing terms, expect
a proof context to be evaluated (especially "()" is no longer needed).
- Debugger now shows the nesting level and the reasons of failure
Tactics
- Equality tactics (Rewrite, Reflexivity, Symmetry, Transitivity) now
understand JM equality
- Simpl and Change now apply to subterms also
- "Simpl f" reduces subterms whose head constant is f
- Double Induction now referring to hypotheses like "Intros until"
- "Inversion" now applies also on quantified hypotheses (naming as
for Intros until)
- NewDestruct now accepts terms with missing hypotheses
- NewDestruct and NewInduction now accept user-provided elimination scheme
- NewDestruct and NewInduction now accept user-provided introduction names
- Omega could solve goals such as ~`x<y` |- `x>=y` but failed when the
hypothesis was unfolded to `x < y` -> False. This is fixed. In addition,
it can also recognize 'False' in the hypothesis and use it to solve the
goal.
- Coercions now handled in "with" bindings
- "Subst x" replaces all ocurrences of x by t in the goal and hypotheses
when an hypothesis x=t or x:=t or t=x exists
- Fresh names for Assert and Pose now based on collision-avoiding
Intro naming strategy (exceptional source of incompatibilities)
- LinearIntuition (* no documentation *)
- Unfold expects a correct evaluable argument
- Clear expects existing hypotheses
Extraction (See details in contrib/extraction/CHANGES and README):
- An experimental Scheme extraction is provided.
- Concerning Ocaml, extracted code is now ensured to always type-check,
thanks to automatic inserting of Obj.magic.
- Experimental extraction of Coq new modules to Ocaml modules.
Proof rendering in natural language
- Export of theories to XML for publishing and rendering purposes now
includes proof-trees (see http://www.cs.unibo.it/helm)
Miscellaneous
- Printing Coercion now used through the standard keywords Set/Add, Test, Print
- "Print Term id" is an alias for "Print id"
- New switch "Unset/Set Printing Symbols" to control printing of
symbolic notations
- Two new variants of implicit arguments are available
- "Unset/Set Contextual Implicits" tells to consider implicit also the
arguments inferable from the context (e.g. for nil or refl_eq)
- "Unset/Set Strict Implicits" tells to consider implicit only the
arguments that are inferable in any case (i.e. arguments that occurs
as argument of rigid constants in the type of the remaining arguments;
e.g. the witness of an existential is not strict since it can vanish when
applied to a predicate which does not use its argument)
Incompatibilities
- "Grammar tactic ... : ast" and "Grammar vernac ... : ast" are no
longer supported, use TACTIC EXTEND and VERNAC COMMAND EXTEND on the
ML-side instead
- Transparency of le_lt_dec and co (leads to some simplification in
proofs; in some cases, incompatibilites is solved by declaring locally
opaque the relevant constant)
- Opaque Local do not now survive section closing (rename them into
Remark/Lemma/... to get them still surviving the sections; this
renaming allows also to solve incompatibilites related to now
forbidden calls to the tactic Clear)
- Remark and Fact have no longer (very) long names (use Local instead in case
of name conflict)
Bugs
- Improved localisation of errors in Syntactic Definitions
- Induction principle creation failure in presence of let-in fixed (#238)
- Inversion bugs fixed (#212 and #220)
- Omega bug related to Set fixed (#180)
- Type-checking inefficiency of nested destructuring let-in fixed (#216)
- Improved handling of let-in during holes resolution phase (#239)
Efficiency
- Implementation of a memory sharing strategy reducing memory
requirements by an average ratio of 3.
Changes from V7.3 to V7.3.1
===========================
Bug fixes
- Corrupted Field tactic and Match Context tactic construction fixed
- Checking of names already existing in Assert added (PR#182)
- Invalid argument bug in Exact tactic solved (PR#183)
- Colliding bound names bug fixed (PR#202)
- Wrong non-recursivity test for Record fixed (PR#189)
- Out of memory/seg fault bug related to parametric inductive fixed (PR#195)
- Setoid_replace/Setoid_rewrite bug wrt "==" fixed
Misc
- Ocaml version >= 3.06 is needed to compile Coq from sources
- Simplification of fresh names creation strategy for Assert, Pose and
LetTac (PR#192)
Changes from V7.2 to V7.3
=========================
Language
- Slightly improved compilation of pattern-matching (slight source of
incompatibilities)
- Record's now accept anonymous fields "_" which does not build projections
- Changes in the allowed elimination sorts for certain class of inductive
definitions : an inductive definition without constructors
of Sort Prop can be eliminated on sorts Set and Type A "singleton"
inductive definition (one constructor with arguments in the sort Prop
like conjunction of two propositions or equality) can be eliminated
directly on sort Type (In V7.2, only the sorts Prop and Set were allowed)
Tactics
- New tactic "Rename x into y" for renaming hypotheses
- New tactics "Pose x:=u" and "Pose u" to add definitions to local context
- Pattern now working on partially applied subterms
- Ring no longer applies irreversible congruence laws of mult but
better applies congruence laws of plus (slight source of incompatibilities).
- Field now accepts terms to be simplified as arguments (as for Ring). This
extension has been also implemented using the toplevel tactic language.
- Intuition does no longer unfold constants except "<->" and "~". It
can be parameterized by a tactic. It also can introduce dependent
product if needed (source of incompatibilities)
- "Match Context" now matching more recent hypotheses first and failing only
on user errors and Fail tactic (possible source of incompatibilities)
- Tactic Definition's without arguments now allowed in Coq states
- Better simplification and discrimination made by Inversion (source
of incompatibilities)
Bugs
- "Intros H" now working like "Intro H" trying first to reduce if not a product
- Forward dependencies in Cases now taken into account
- Known bugs related to Inversion and let-in's fixed
- Bug unexpected Delta with let-in now fixed
Extraction (details in contrib/extraction/CHANGES or documentation)
- Signatures of extracted terms are now mostly expunged from dummy arguments.
- Haskell extraction is now operational (tested & debugged).
Standard library
- Some additions in [ZArith]: three files (Zcomplements.v, Zpower.v
and Zlogarithms.v) moved from contrib/omega in order to be more
visible, one Zsgn function, more induction principles (Wf_Z.v and
tail of Zcomplements.v), one more general Euclid theorem
- Peano_dec.v and Compare_dec.v now part of Arith.v
Tools
- new option -dump-glob to coqtop to dump globalizations (to be used by the
new documentation tool coqdoc; see http://www.lri.fr/~filliatr/coqdoc)
User Contributions
- CongruenceClosure (congruence closure decision procedure)
[Pierre Corbineau, ENS Cachan]
- MapleMode (an interface to embed Maple simplification procedures over
rational fractions in Coq)
[David Delahaye, Micaela Mayero, Chalmers University]
- Presburger: A formalization of Presburger's algorithm
[Laurent Thery, INRIA Sophia Antipolis]
- Chinese has been rewritten using Z from ZArith as datatype
ZChinese is the new version, Chinese the obsolete one
[Pierre Letouzey, LRI Orsay]
Incompatibilities
- Ring: exceptional incompatibilities (1 above 650 in submitted user
contribs, leading to a simplification)
- Intuition: does not unfold any definition except "<->" and "~"
- Cases: removal of some extra Cases in configurations of the form
"Cases ... of C _ => ... | _ D => ..." (effects on 2 definitions of
submitted user contributions necessitating the removal of now superfluous
proof steps in 3 different proofs)
- Match Context, in case of incompatibilities because of a now non
trapped error (e.g. Not_found or Failure), use instead tactic Fail
to force Match Context trying the next clause
- Inversion: better simplification and discrimination may occasionally
lead to less subgoals and/or hypotheses and different naming of hypotheses
- Unification done by Apply/Elim has been changed and may exceptionally lead
to incompatible instantiations
- Peano_dec.v and Compare_dec.v parts of Arith.v make Auto more
powerful if these files were not already required (1 occurrence of
this in submitted user contribs)
Changes from V7.1 to V7.2
=========================
Language
- Automatic insertion of patterns for local definitions in the type of
the constructors of an inductive types (for compatibility with V6.3
let-in style)
- Coercions allowed in Cases patterns
- New declaration "Canonical Structure id = t : I" to help resolution of
equations of the form (proj ?)=a; if proj(e)=a then a is canonically
equipped with the remaining fields in e, i.e. ? is instantiated by e
Tactics
- New tactic "ClearBody H" to clear the body of definitions in local context
- New tactic "Assert H := c" for forward reasoning
- Slight improvement in naming strategy for NewInduction/NewDestruct
- Intuition/Tauto do not perform useless unfolding and work up to conversion
Extraction (details in contrib/extraction/CHANGES or documentation)
- Syntax changes: there are no more options inside the extraction commands.
New commands for customization and options have been introduced instead.
- More optimizations on extracted code.
- Extraction tests are now embedded in 14 user contributions.
Standard library
- In [Relations], Rstar.v and Newman.v now axiom-free.
- In [Sets], Integers.v now based on nat
- In [Arith], more lemmas in Min.v, new file Max.v, tail-recursive
plus and mult added to Plus.v and Mult.v respectively
- New directory [Sorting] with a proof of heapsort (dragged from 6.3.1 lib)
- In [Reals], more lemmas in Rbase.v, new lemmas on square, square root and
trigonometric functions (R_sqr.v - Rtrigo.v); a complementary approach
and new theorems about continuity and derivability in Ranalysis.v; some
properties in plane geometry such as translation, rotation or similarity
in Rgeom.v; finite sums and Chasles property in Rsigma.v
Bugs
- Confusion between implicit args of locals and globals of same base name fixed
- Various incompatibilities wrt inference of "?" in V6.3.1 fixed
- Implicits in infix section variables bug fixed
- Known coercions bugs fixed
- Apply "universe anomaly" bug fixed
- NatRing now working
- "Discriminate 1", "Injection 1", "Simplify_eq 1" now working
- NewInduction bugs with let-in and recursively dependent hypotheses fixed
- Syntax [x:=t:T]u now allowed as mentioned in documentation
- Bug with recursive inductive types involving let-in fixed
- Known pattern-matching bugs fixed
- Known Cases elimination predicate bugs fixed
- Improved errors messages for pattern-matching and projections
- Better error messages for ill-typed Cases expressions
Incompatibilities
- New naming strategy for NewInduction/NewDestruct may affect 7.1 compatibility
- Extra parentheses may exceptionally be needed in tactic definitions.
- Coq extensions written in Ocaml need to be updated (see dev/changements.txt
for a description of the main changes in the interface files of V7.2)
- New behaviour of Intuition/Tauto may exceptionally lead to incompatibilities
----------------------------------------------------------------------------
Changes from V6.3.1 and V7.0 to V7.1
====================================
Notes:
- items followed by (**) are important sources of incompatibilities
- items followed by (*) may exceptionally be sources of incompatibilities
- items followed by (+) have been introduced in version 7.0
Main novelties
==============
References are to Coq V7.1 reference manual
- New primitive let-in construct (see sections 1.2.8 and )
- Long names (see sections 2.6 and 2.7)
- New high-level tactic language (see chapter 10)
- Improved search facilities (see section 5.2)
- New extraction algorithm managing the Type level (see chapter 17)
- New rewriting tactic for arbitrary equalities (see chapter 19)
- New tactic Field to decide equalities on commutative fields (see 7.11)
- New tactic Fourier to solve linear inequalities on reals numbers (see 7.11)
- New tactics for induction/case analysis in "natural" style (see 7.7)
- Deep restructuration of the code (safer, simpler and more efficient)
- Export of theories to XML for publishing and rendering purposes
(see http://www.cs.unibo.it/helm)
Details of changes
==================
Language: new "let-in" construction
-----------------------------------
- New construction for local definitions (let-in) with syntax [x:=u]t (*)(+)
- Local definitions allowed in Record (a.k.a. record à la Randy Pollack)
Language: long names
--------------------
- Each construction has a unique absolute names built from a base
name, the name of the module in which they are defined (Top if in
coqtop), and possibly an arbitrary long sequence of directory (e.g.
"Coq.Lists.PolyList.flat_map" where "Coq" means that "flat_map" is part
of Coq standard library, "Lists" means it is defined in the Lists
library and "PolyList" means it is in the file Polylist) (+)
- Constructions can be referred by their base name, or, in case of
conflict, by a "qualified" name, where the base name is prefixed
by the module name (and possibly by a directory name, and so
on). A fully qualified name is an absolute name which always refer
to the construction it denotes (to preserve the visibility of
all constructions, no conflict is allowed for an absolute name) (+)
- Long names are available for modules with the possibility of using
the directory name as a component of the module full name (with
option -R to coqtop and coqc, or command Add LoadPath) (+)
- Improved conflict resolution strategy (the Unix PATH model),
allowing more constructions to be referred just by their base name
Language: miscellaneous
-----------------------
- The names of variables for Record projections _and_ for induction principles
(e.g. sum_ind) is now based on the first letter of their type (main
source of incompatibility) (**)(+)
- Most typing errors have now a precise location in the source (+)
- Slightly different mechanism to solve "?" (*)(+)
- More arguments may be considered implicit at section closing (*)(+)
- Bug with identifiers ended by a number greater than 2^30 fixed (+)
- New visibility discipline for Remark, Fact and Local: Remark's and
Fact's now survive at the end of section, but are only accessible using a
qualified names as soon as their strength expires; Local's disappear and
are moved into local definitions for each construction persistent at
section closing
Language: Cases
---------------
- Cases no longer considers aliases inferable from dependencies in types (*)(+)
- A redundant clause in Cases is now an error (*)
Reduction
---------
- New reduction flags "Zeta" and "Evar" in Eval Compute, for inlining of
local definitions and instantiation of existential variables
- Delta reduction flag does not perform Zeta and Evar reduction any more (*)
- Constants declared as opaque (using Qed) can no longer become
transparent (a constant intended to be alternatively opaque and
transparent must be declared as transparent (using Defined)); a risk
exists (until next Coq version) that Simpl and Hnf reduces opaque
constants (*)
New tactics
-----------
- New set of tactics to deal with types equipped with specific
equalities (a.k.a. Setoids, e.g. nat equipped with eq_nat) [by C. Renard]
- New tactic Assert, similar to Cut but expected to be more user-friendly
- New tactic NewDestruct and NewInduction intended to replace Elim
and Induction, Case and Destruct in a more user-friendly way (see
restrictions in the reference manual)
- New tactic ROmega: an experimental alternative (based on reflexion) to Omega
[by P. Crégut]
- New tactic language Ltac (see reference manual) (+)
- New versions of Tauto and Intuition, fully rewritten in the new Ltac
language; they run faster and produce more compact proofs; Tauto is
fully compatible but, in exchange of a better uniformity, Intuition
is slightly weaker (then use Tauto instead) (**)(+)
- New tactic Field to decide equalities on commutative fields (as a
special case, it works on real numbers) (+)
- New tactic Fourier to solve linear inequalities on reals numbers
[by L. Pottier] (+)
- New tactics dedicated to real numbers: DiscrR, SplitRmult, SplitAbsolu (+)
Changes in existing tactics
---------------------------
- Reduction tactics in local definitions apply only to the body
- New syntax of the form "Compute in Type of H." to require a reduction on
the types of local definitions
- Inversion, Injection, Discriminate, ... apply also on the
quantified premises of a goal (using the "Intros until" syntax)
- Decompose has been fixed but hypotheses may get different names (*)(+)
- Tauto now manages uniformly hypotheses and conclusions of the form
"t=t" which all are considered equivalent to "True". Especially,
Tauto now solves goals of the form "H : ~ t = t |- A".
- The "Let" tactic has been renamed "LetTac" and is now based on the
primitive "let-in" (+)
- Elim can no longer be used with an elimination schema different from
the one defined at definition time of the inductive type. To overload
an elimination schema, use "Elim <hyp> using <name of the new schema>"
(*)(+)
- Simpl no longer unfolds the recursive calls of a mutually defined
fixpoint (*)(+)
- Intro now fails if the hypothesis name already exists (*)(+)
- "Require Prolog" is no longer needed (i.e. it is available by default) (*)(+)
- Unfold now fails on a non unfoldable identifier (*)(+)
- Unfold also applies on definitions of the local context
- AutoRewrite now deals only with the main goal and it is the purpose of
Hint Rewrite to deal with generated subgoals (+)
- Redundant or incompatible instantiations in Apply ... with ... are now
correctly managed (+)
Efficiency
----------
- Excessive memory uses specific to V7.0 fixed
- Sizes of .vo files vary a lot compared to V6.3 (from -30% to +300%
depending on the developments)
- An improved reduction strategy for lazy evaluation
- A more economical mechanism to ensure logical consistency at the Type level;
warning: this is experimental and may produce "universes" anomalies
(please report)
Concrete syntax of constructions
--------------------------------
- Only identifiers starting with "_" or a letter, and followed by letters,
digits, "_" or "'" are allowed (e.g. "$" and "@" are no longer allowed) (*)
- A multiple binder like (a:A)(a,b:(P a))(Q a) is no longer parsed as
(a:A)(a0:(P a))(b:(P a))(Q a0) but as (a:A)(a0:(P a))(b:(P a0))(Q a0) (*)(+)
- A dedicated syntax has been introduced for Reals (e.g ``3+1/x``) (+)
- Pretty-printing of Infix notations fixed. (+)
Parsing and grammar extension
-----------------------------
- More constraints when writing ast
- "{...}" and the macros $LIST, $VAR, etc. now expect a metavariable
(an identifier starting with $) (*)
- identifiers should starts with a letter or "_" and be followed
by letters, digits, "_" or "'" (other characters are still
supported but it is not advised to use them) (*)(+)
- Entry "command" in "Grammar" and quotations (<<...>> stuff) is
renamed "constr" as in "Syntax" (+)
- New syntax "[" sentence_1 ... sentence_n"]." to group sentences (useful
for Time and to write grammar rules abbreviating several commands) (+)
- The default parser for actions in the grammar rules (and for
patterns in the pretty-printing rules) is now the one associated to
the grammar (i.e. vernac, tactic or constr); no need then for
quotations as in <:vernac:<...>>; to return an "ast", the grammar
must be explicitly typed with tag ": ast" or ": ast list", or if a
syntax rule, by using <<...>> in the patterns (expression inside
these angle brackets are parsed as "ast"); for grammars other than
vernac, tactic or constr, you may explicitly type the action with
tags ": constr", ": tactic", or ":vernac" (**)(+)
- Interpretation of names in Grammar rule is now based on long names,
which allows to avoid problems (or sometimes tricks;) related to
overloaded names (+)
New commands
------------
- New commands "Print XML All", "Show XML Proof", ... to show or
export theories to XML to be used with Helm's publishing and rendering
tools (see http://www.cs.unibo.it/helm) (by Claudio Sacerdoti Coen) (+)
- New commands to manually set implicit arguments (+)
- "Implicits ident." to activate the implicit arguments mode just for ident
- "Implicits ident [num1 num2 ...]." to explicitly give which
arguments have to be considered as implicit
- New SearchPattern/SearchRewrite (by Yves Bertot) (+)
- New commands "Debug on"/"Debug off" to activate/deactivate the tactic
language debugger (+)
- New commands to map physical paths to logical paths (+)
- Add LoadPath physical_dir as logical_dir
- Add Rec LoadPath physical_dir as logical_dir
Changes in existing commands
----------------------------
- Generalization of the usage of qualified identifiers in tactics
and commands about globals, e.g. Decompose, Eval Delta;
Hints Unfold, Transparent, Require
- Require synchronous with Reset; Require's scope stops at Section ending (*)
- For a module indirectly loaded by a "Require" but not exported,
the command "Import module" turns the constructions defined in the
module accessible by their short name, and activates the Grammar,
Syntax, Hint, ... declared in the module (+)
- The scope of the "Search" command can be restricted to some modules (+)
- Final dot in command (full stop/period) must be followed by a blank
(newline, tabulation or whitespace) (+)
- Slight restriction of the syntax for Cbv Delta: if present, option [-myconst]
must immediately follow the Delta keyword (*)(+)
- SearchIsos currently not supported
- Add ML Path is now implied by Add LoadPath (+)
- New names for the following commands (+)
AddPath -> Add LoadPath
Print LoadPath -> Print LoadPath
DelPath -> Remove LoadPath
AddRecPath -> Add Rec LoadPath
Print Path -> Print Coercion Paths
Implicit Arguments On -> Set Implicit Arguments
Implicit Arguments Off -> Unset Implicit Arguments
Begin Silent -> Set Silent
End Silent -> Unset Silent.
Tools
-----
- coqtop (+)
- Two executables: coqtop.byte and coqtop.opt (if supported by the platform)
- coqtop is a link to the more efficient executable (coqtop.opt if present)
- option -full is obsolete (+)
- do_Makefile renamed into coq_makefile (+)
- New option -R to coqtop and coqc to map a physical directory to a logical
one (+)
- coqc no longer needs to create a temporary file
- No more warning if no initialization file .coqrc exists
Extraction
----------
- New algorithm for extraction able to deal with "Type" (+)
(by J.-C. Filliâtre and P. Letouzey)
Standard library
----------------
- New library on maps on integers (IntMap, contributed by Jean Goubault)
- New lemmas about integer numbers [ZArith]
- New lemmas and a "natural" syntax for reals [Reals] (+)
- Exc/Error/Value renamed into Option/Some/None (*)
New user contributions
----------------------
- Constructive complex analysis and the Fundamental Theorem of Algebra [FTA]
(Herman Geuvers, Freek Wiedijk, Jan Zwanenburg, Randy Pollack,
Henk Barendregt, Nijmegen)
- A new axiomatization of ZFC set theory [Functions_in_ZFC]
(C. Simpson, Sophia-Antipolis)
- Basic notions of graph theory [GRAPHS-BASICS] (Jean Duprat, Lyon)
- A library for floating-point numbers [Float] (Laurent Théry, Sylvie Boldo,
Sophia-Antipolis)
- Formalisation of CTL and TCTL temporal logic [CtlTctl] (Carlos
Daniel Luna,Montevideo)
- Specification and verification of the Railroad Crossing Problem
in CTL and TCTL [RailroadCrossing] (Carlos Daniel Luna,Montevideo)
- P-automaton and the ABR algorithm [PAutomata]
(Christine Paulin, Emmanuel Freund, Orsay)
- Semantics of a subset of the C language [MiniC]
(Eduardo Giménez, Emmanuel Ledinot, Suresnes)
- Correctness proofs of the following imperative algorithms:
Bresenham line drawing algorithm [Bresenham], Marché's minimal edition
distance algorithm [Diff] (Jean-Christophe Filliâtre, Orsay)
- Correctness proofs of Buchberger's algorithm [Buchberger] and RSA
cryptographic algorithm [Rsa] (Laurent Théry, Sophia-Antipolis)
- Correctness proof of Stalmarck tautology checker algorithm
[Stalmarck] (Laurent Théry, Pierre Letouzey, Sophia-Antipolis)
|