This repository has been archived by the owner on Nov 13, 2021. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 0
/
CHANGES
1700 lines (1368 loc) · 75 KB
/
CHANGES
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
Changes since V8.2
==================
- "discriminate" now performs intros before trying to discriminate an
hypothesis of the goal (previously it applied intro only if the goal
had the form t1<>t2).
Changes from V8.1 to V8.2
=========================
Language
- If a fixpoint is not written with an explicit { struct ... }, then
all arguments are tried successively (from left to right) until one is
found that satisfies the structural decreasing condition.
- New experimental typeclass system giving ad-hoc polymorphism and
overloading based on dependent records and implicit arguments.
- New syntax "let 'pat := b in c" for let-binding using irrefutable patterns.
- New syntax "forall {A}, T" for specifying maximally inserted implicit
arguments in terms.
- Sort of Record/Structure, Inductive and CoInductive defaults to Type
if omitted.
- Record/Structure now usable for defining coinductive types
(e.g. "Record stream := { hd : nat; tl : stream }.")
- New syntax "Theorem id1:t1 ... with idn:tn" for proving mutually dependent
statements.
- Support for sort-polymorphism on constants denoting inductive types.
- Several evolutions of the module system (handling of module aliases,
functorial module types, an Include feature, etc). (TODO: Say more!)
- Prop now a subtype of Set (predicative and impredicative forms).
Vernacular commands
- Added option Global to "Arguments Scope" for section surviving. (DOC TODO)
- Added option "Unset Elimination Schemes" to deactivate the automatic
generation of elimination schemes.
- Modification of the Scheme command so you can ask for the name to be
automatically computed (e.g. Scheme Induction for nat Sort Set).
- New command "Combined Scheme" to build combined mutual induction
principles from existing mutual induction principles.
- New command "Scheme Equality" to build a decidable (boolean) equality
for simple inductive datatypes and a decision property over this equality
(e.g. Scheme Equality for nat).
- Added option "Set Equality Scheme" to make automatic the declaration
of the boolean equality when possible.
- Source of universe inconsistencies now printed when option
"Set Printing Universes" is activated.
- New option "Set Printing Existential Instances" for making the display of
existential variable instances explicit.
- Support for option "[id1 ... idn]", and "-[id1 ... idn]", for the
"compute"/"cbv" reduction strategy, respectively meaning reduce only, or
everything but, the constants id1 ... idn. "lazy" alone or followed by
"[id1 ... idn]", and "-[id1 ... idn]" also supported, meaning apply
all of beta-iota-zeta-delta, possibly restricting delta.
- New command "Strategy" to control the expansion of constants during
conversion tests. It generalizes commands Opaque and Transparent by
introducing a range of levels. Lower levels are assigned to constants
that should be expanded first.
- New command "Print Assumptions" to display all variables, parameters
or axioms a theorem or definition relies on.
Libraries (DOC TO CHECK)
- Several parts of the libraries are now in Type, in particular FSets,
SetoidList, ListSet, Sorting, Zmisc. This may induce a few
incompatibilities. In case of trouble while fixing existing development,
it may help to simply declare Set as an alias for Type (see file
SetIsType).
- New arithmetical library in theories/Numbers. It contains:
* an abstract modular development of natural and integer arithmetics
in Numbers/Natural/Abstract and Numbers/Integer/Abstract
* an implementation of efficient computational bounded and unbounded
integers that can be mapped to processor native arithmetics.
See Numbers/Cyclic/Int31 for 31-bit integers and Numbers/Natural/BigN
for unbounded natural numbers and Numbers/Integer/BigZ for unbounded
integers.
* some proofs that both older libraries Arith, ZArith and NArith and
newer BigN and BigZ implement the abstract modular development.
This allows in particular BigN and BigZ to already come with a
large database of basic lemmas and some generic tactics (ring),
This library has still an experimental status, as well as the
processor-acceleration mechanism, but both its abstract and its
concrete parts are already quite usable and could challenge the use
of nat, N and Z in actual developments. Moreover, an extension of
this framework to rational numbers is ongoing, and an efficient
Q structure is already provided (see Numbers/Rational/BigQ), but
this part is currently incomplete (no abstract layer and generic
lemmas).
- Many changes in FSets/FMaps. In practice, compatibility with earlier
version should be fairly good, but some adaptations may be required.
* Interfaces of unordered ("weak") and ordered sets have been factorized
thanks to new features of Coq modules (in particular Include), see
FSetInterface. Same for maps. Hints in these interfaces have been
reworked (they are now placed in a "set" database).
* FSetDecide, contributed by Aaron Bohannon, contains a decision
procedure allowing to solve basic set-related goals (for instance,
is a point in a particular set ?). See FSetProperties for examples.
* Functors of properties have been improved, especially the ones about
maps, that now propose some induction principles. Some properties
of fold need less hypothesis.
* More uniformity in implementations of sets and maps: they all use
implicit arguments, and no longer export unnecessary scopes (see
bug #1347)
* Internal parts of the implementations based on AVL have evolved a
lot. The main files FSetAVL and FMapAVL are now much more
lightweight now. In particular, minor changes in some functions
has allowed to fully separate the proofs of operational
correctness from the proofs of well-balancing: well-balancing is
critical for efficiency, but not anymore for proving that these
trees implement our interfaces, hence we have moved these proofs
into appendix files FSetFullAVL and FMapFullAVL. Moreover, a few
functions like union and compare have been modified in order to be
structural yet efficient. The appendix files also contains
alternative versions of these few functions, much closer to the
initial Ocaml code and written via the Function framework.
- Library IntMap, subsumed by FSets/FMaps, has been removed from
Coq Standard Library and moved into a user contribution Cachan/IntMap
- Better computational behavior of some constants (eq_nat_dec and
le_lt_dec more efficient, Z_lt_le_dec and Positive_as_OT.compare
transparent, ...) (exceptional source of incompatibilities).
- Boolean operators moved from module Bool to module Datatypes (may need
to rename qualified references in script and force notations || and &&
to be at levels 50 and 40 respectively).
- The constructors xI and xO of type positive now have postfix notations
"~1" and "~0", allowing to write numbers in binary form easily, for instance
6 is 1~1~0 and 4*p is p~0~0 (see BinPos.v).
- Improvements to NArith (Nminus, Nmin, Nmax), and to QArith (in particular
a better power function).
- Changes in ZArith: several additional lemmas (used in theories/Numbers),
especially in Zdiv, Znumtheory, Zpower. Moreover, many results in
Zdiv have been generalized: the divisor may simply be non-null
instead of strictly positive (see lemmas with name ending by
"_full"). An alternative file ZOdiv proposes a different behavior
(the one of Ocaml) when dividing by negative numbers.
- Changes in Arith: EqNat and Wf_nat now exported from Arith, some
constructions on nat that were outside Arith are now in (e.g. iter_nat).
- In SetoidList, eqlistA now expresses that two lists have similar elements
at the same position, while the predicate previously called eqlistA
is now equivlistA (this one only states that the lists contain the same
elements, nothing more).
- Changes in Reals:
* Most statement in "sigT" (including the
completeness axiom) are now in "sig" (in case of incompatibility,
use proj1_sig instead of projT1, sig instead of sigT, etc).
* More uniform naming scheme (identifiers in French moved to English,
consistent use of 0 -- zero -- instead of O -- letter O --, etc).
* Lemma on prod_f_SO is now on prod_f_R0.
* Useless hypothesis of ln_exists1 dropped.
* New Rlogic.v states a few logical properties about R axioms.
* RIneq.v extended and made cleaner.
- Slight restructuration of the Logic library regarding choice and classical
logic. Addition of files providing intuitionistic axiomatizations of
descriptions: Epsilon.v, Description.v and IndefiniteDescription.v.
- Definition of pred and minus made compatible with the structural
decreasing criterion for use in fixpoints.
Notations, coercions, implicit arguments and type inference
- More automation in the inference of the return clause of dependent
pattern-matching problems.
- Experimental allowance for omission of the clauses easily detectable as
impossible in pattern-matching problems.
- Improved inference of implicit arguments.
- New options "Set Maximal Implicit Insertion", "Set Reversible Pattern
Implicit", "Set Strongly Strict Implicit" and "Set Printing Implicit
Defensive" for controlling inference and use of implicit arguments.
- New modifier in "Implicit Arguments" to force an implicit argument to
be maximally inserted.
- New modifier of "Implicit Arguments" to enrich the set of implicit arguments.
(DOC TODO?)
- New options Global and Local to "Implicit Arguments" for section
surviving or non export outside module.
- Level "constr" moved from 9 to 8. (DOC TODO?)
- Structure/Record now printed as Record (unless option Printing All is set).
- Support for parametric notations defining constants.
- Insertion of coercions below product types refrains to unfold
constants (possible source of incompatibility).
- New support for fix/cofix in notations.
Tactic Language
- Second-order pattern-matching now working in Ltac "match" clauses
(syntax for second-order unification variable is "@?X").
- Ltac accepts integer arguments (syntax is "ltac:nnn" for nnn an integer).
- The general sequence tactical "expr_0 ; [ expr_1 | ... | expr_n ]"
is extended so that at most one expr_i may have the form "expr .."
or just "..". Also, n can be different from the number of subgoals
generated by expr_0. In this case, the value of expr (or idtac in
case of just "..") is applied to the intermediate subgoals to make
the number of tactics equal to the number of subgoals. (DOC TODO)
- A name used as the name of the parameter of a lemma (like f in
"apply f_equal with (f:=t)") is now interpreted as a ltac variable
if such a variable exists (this is a possible source of
incompatibility and it can be fixed by renaming the variables of a
ltac function into names that do not clash with the lemmas
parameter names used in the tactic).
- New syntax "Ltac tac ::= ..." to rebind a tactic to a new expression.
- "let rec ... in ... " now supported for expressions without explicit
parameters; interpretation is lazy to the contrary of "let ... in ...";
hence, the "rec" keyword can be used to turn the argument of a
"let ... in ..." into a lazy one.
- Patterns for hypotheses types in "match goal" are now interpreted in
type_scope.
Tactics
- New tactics "apply -> term", "apply <- term", "apply -> term in
ident", "apply <- term in ident" for applying equivalences (iff). (DOC TODO)
- Slight improvement of the hnf and simpl tactics when applied on
expressions with explicit occurrences of match or fix.
- New tactics "eapply in", "erewrite", "erewrite in".
- New tactics "ediscriminate", "einjection", "esimplify_eq".
- Tactics "discriminate", "injection", "simplify_eq" now support any
term as argument. Clause "with" is also supported.
- Unfoldable references can be given by notation's string rather than by name
in unfold.
- The "with" arguments are now typed using informations from the current goal:
allows support for coercions and more inference of implicit arguments.
- Application of "f_equal"-style lemmas works better.
- Tactics elim, case, destruct and induction now support variants eelim,
ecase, edestruct and einduction.
- Tactics destruct and induction now support the "with" option and the
"in" clause option. If the option "in" is used, an equality is added
to remember the term to which the induction or case analysis applied
(possible source of parsing incompatibilities when destruct or induction is
part of a let-in expression in Ltac; extra parentheses are then required).
- Some new intro patterns:
* intro pattern "?A" genererates a fresh name based on A.
Caveat about a slight loss of compatibility:
Some intro patterns don't need space between them. In particular
intros ?a?b used to be legal and equivalent to intros ? a ? b. Now it
is still legal but equivalent to intros ?a ?b.
* intro pattern "(A & ... & Y & Z)" synonym to "(A,....,(Y,Z)))))"
for right-associative constructs like /\ or exists.
- Several syntax extensions concerning "rewrite": (DOC TODO)
* "rewrite A,B,C" can be used to rewrite A, then B, then C. These rewrites
occur only on the first subgoal: in particular, side-conditions of the
"rewrite A" are not concerned by the "rewrite B,C".
* "rewrite A by tac" allows to apply tac on all side-conditions generated by
the "rewrite A".
* "rewrite A at n" allows to select occurrences to rewrite: rewrite only
happen at the n-th exact occurrence of the first successful matching of
A in the goal.
* "rewrite 3 A" or "rewrite 3!A" is equivalent to "rewrite A,A,A".
* "rewrite !A" means rewriting A as long as possible (and at least once).
* "rewrite 3?A" means rewriting A at most three times.
* "rewrite ?A" means rewriting A as long as possible (possibly never).
* many of the above extensions can be combined with each other.
- New syntax "rename a into b, c into d" for "rename a into b; rename c into d"
- New tactics "dependent induction/destruction H [ generalizing id_1 .. id_n ]"
to do induction-inversion on instantiated inductive families à la BasicElim.
- Tactic "apply" now able to reason modulo unfolding of constants
(possible source of incompatibility in situations where apply may fail,
e.g. as argument of a try or a repeat and in a ltac function);
version of apply that does not unfold is renamed into "simple apply"
(usable for compatibility or for automation).
- Tactic "apply" now able to traverse conjunctions and to select the first
matching lemma among the components of the conjunction; tactic apply also
able to apply lemmas of conclusion an empty type.
- Tactics "set" and "pose" can set functions using notation "(f x1..xn := c)".
- New tactic "instantiate" (without argument).
- Tactic firstorder "with" and "using" options have their meaning swapped for
consistency with auto/eauto (source of incompatibility).
- Tactic "generalize" now supports "at" options to specify occurrences
and "as" options to name the hypothesis.
- New tactic "specialize H with a" or "specialize (H a)" allows to transform
in-place a universally-quantified hypothesis (H : forall x, T x) into its
instantiated form (H : T a). Nota: "specialize" was in fact there in earlier
versions of Coq, but was undocumented, and had a slightly different behavior.
- New tactic "contradict H" can be used to solve any kind of goal as long as
the user can provide afterwards a proof of the negation of the hypothesis H.
If H is already a negation, say ~T, then a proof of T is asked.
If the current goal is a negation, say ~U, then U is saved in H afterwards,
hence this new tactic "contradict" extends earlier tactic "swap", which is
now obsolete.
- Tactics f_equal is now done in ML instead of Ltac: it now works on any
equality of functions, regardless of the arity of the function.
- Some more debug of reflexive omega (romega), and internal clarifications.
Moreover, romega now has a variant "romega with *" that can be also used
on non-Z goals (nat, N, positive) via a call to a translation tactic named
zify (its purpose is to Z-ify your goal...). This zify may also be used
independantly of romega.
- Tactic "remember" now supports an "in" clause to remember only selected
occurrences of a term.
Program
- Moved useful tactics in theories/Program and documented them.
- Add Program.Basics which contains standard definitions for functional
programming (id, apply, flip...)
- More robust obligation handling, dependent pattern-matching and
well-founded definitions.
- New syntax " dest term as pat in term " for destructing objects using
an irrefutable pattern while keeping equalities (use this instead of
"let" in Programs).
- Program CoFixpoint is accepted, Program Fixpoint uses the new way to infer
which argument decreases structurally.
- Program Lemma, Axiom etc... now permit to have obligations in the statement
iff they can be automatically solved by the default tactic.
- Renamed "Obligations Tactic" command to "Obligation Tactic".
- New command "Preterm [ of id ]" to see the actual term fed to Coq for
debugging purposes.
- New option "Transparent Obligations" to control the declaration of
obligations as transparent or opaque. All obligations are now transparent
by default, otherwise the system declares them opaque if possible.
- Changed the notations "left" and "right" to "in_left" and "in_right" to hide
the proofs in standard disjunctions, to avoid breaking existing scripts when
importing Program. Also, put them in program_scope.
Type Classes
- New "Class", "Instance" and "Program Instance" commands to define
classes and instances documented in the reference manual.
- New binding construct " [ Class_1 param_1 .. param_n, Class_2 ... ] "
for binding type classes, usable everywhere.
- New command " Print Classes " and " Print Instances some_class " to
print tables for typeclasses.
- New default eauto hint database "typeclass_instances" used by the default
typeclass instance search tactic.
- New theories directory "theories/Classes" for standard typeclasses
declarations. Module Classes.RelationClasses is a typeclass port of
Relation_Definitions plus a generic development of algebra on
n-ary heterogeneous predicates.
Setoid rewriting
- Complete (and still experimental) rewrite of the tactic
based on typeclasses. The old interface and semantics are
almost entirely respected, except:
- Import Setoid is now mandatory to be able to call setoid_replace
and declare morphisms.
- "-->", "++>" and "==>" are now right associative notations
declared at level 55 in scope signature_scope.
Their introduction may break existing scripts that defined
them as notations with different levels.
- One needs to use [Typeclasses unfold [cst]] if [cst] is used
as an abbreviation hiding products in types of morphisms,
e.g. if ones redefines [relation] and declares morphisms
whose type mentions [relation].
- The [setoid_rewrite]'s semantics change when rewriting with
a lemma: it can rewrite two different instantiations of the lemma
at once. Use [setoid_rewrite H at 1] for (almost) the usual semantics.
[setoid_rewrite] will also try to rewrite under binders now, and can
succeed on different terms than before. In particular, it will unify under
let-bound variables. When called through [rewrite], the semantics are
unchanged though.
- [Add Morphism term : id] has different semantics when used with
parametric morphism: it will try to find a relation on the parameters
too. The behavior has also changed with respect to default relations:
the most recently declared Setoid/Relation will be used, the documentation
explains how to customize this behavior.
- Parametric Relation and Morphism are declared differently, using the
new [Add Parametric] commands, documented in the manual.
- Setoid_Theory is now an alias to Equivalence, scripts building objects
of type Setoid_Theory need to unfold (or "red") the definitions
of Reflexive, Symmetric and Transitive in order to get the same goals
as before. Scripts which introduced variables explicitely will not break.
- The order of subgoals when doing [setoid_rewrite] with side-conditions
is always the same: first the new goal, then the conditions.
- New standard library modules Classes.Morphisms declares
standard morphisms on refl/sym/trans relations.
Classes.Morphisms_Prop declares morphisms on propositional
connectives and Classes.Morphisms_Relations on generalized predicate
connectives. Classes.Equivalence declares notations and tactics
related to equivalences and Classes.SetoidTactics defines the
setoid_replace tactics and some support for the "Add *" interface,
notably the tactic applied automatically before each "Add Morphism"
proof.
- User-defined subrelations are supported, as well as higher-order morphisms
and rewriting under binders. The tactic is also extensible entirely in Ltac.
The documentation has been updated to cover these features.
- [setoid_rewrite] and [rewrite] now support the [at] modifier to select
occurrences to rewrite, and both use the [setoid_rewrite] code, even when
rewriting with leibniz equality if occurrences are specified.
Extraction
- Improved behavior of the Caml extraction of modules: name clashes should
not happen anymore.
- The command Extract Inductive has now a syntax for infix notations. This
allows in particular to map Coq lists and pairs onto Caml ones:
Extract Inductive list => list [ "[]" "(::)" ].
Extract Inductive prod => "(*)" [ "(,)" ].
- In pattern matchings, a default pattern "| _ -> ..." is now used whenever
possible if several branches are identical. For instance, functions
corresponding to decidability of equalities are now linear instead of
quadratic.
CoqIDE
- CoqIDE font defaults to monospace so as indentation to be meaningful.
- CoqIDE supports nested goals and any other kind of declaration in the middle
of a proof.
- Undoing non-tactic commands in CoqIDE works faster.
- New CoqIDE menu for activating display of various implicit informations.
- Added the possibility to choose the location of tabs in coqide:
(in Edit->Preferences->Misc)
- New Open and Save As dialogs in CoqIDE which filter *.v files.
Tools
- New stand-alone .vo files verifier "coqchk".
Miscellaneous
- Coq installation provides enough files so that Ocaml's extensions need not
the Coq sources to be compiled (this assumes O'Caml 3.10 and Camlp5).
- New commands "Set Whelp Server" and "Set Whelp Getter" to customize the
Whelp search tool.
- Syntax of "Test Printing Let ref" and "Test Printing If ref" changed into
"Test Printing Let for ref" and "Test Printing If for ref".
- An overhauled build system (new Makefiles); see dev/doc/build-system.txt
Changes from V8.1gamma to V8.1
==============================
Bug fixes
- Many bugs have been fixed (cf coq-bugs web page)
Tactics
- New tactics ring, ring_simplify and new tactic field now able to manage
power to a positive integer constant. Tactic ring on Z and R, and
field on R manage power (may lead to incompatibilities with V8.1gamma).
- Tactic field_simplify now applicable in hypotheses.
- New field_simplify_eq for simplifying field equations into ring equations.
- Tactics ring, ring_simplify, field, field_simplify and field_simplify_eq
all able to apply user-given equations to rewrite monoms on the fly
(see documentation).
Libraries
- New file ConstructiveEpsilon.v defining an epsilon operator and
proving the axiom of choice constructively for a countable domain
and a decidable predicate.
Changes from V8.1beta to V8.1gamma
==================================
Syntax
- changed parsing precedence of let/in and fun constructions of Ltac:
let x := t in e1; e2 is now parsed as let x := t in (e1;e2).
Language and commands
- Added sort-polymorphism for definitions in Type (but finally abandonned).
- Support for implicit arguments in the types of parameters in
(co-)fixpoints and (co-)inductive declarations.
- Improved type inference: use as much of possible general information.
before applying irreversible unification heuristics (allow e.g. to
infer the predicate in "(exist _ 0 (refl_equal 0) : {n:nat | n=0 })").
- Support for Miller-Pfenning's patterns unification in type synthesis
(e.g. can infer P such that P x y = phi(x,y)).
- Support for "where" clause in cofixpoint definitions.
- New option "Set Printing Universes" for making Type levels explicit.
Tactics
- Improved implementation of the ring and field tactics. For compatibility
reasons, the previous tactics are renamed as legacy ring and legacy field,
but should be considered as deprecated.
- New declarative mathematical proof language.
- Support for argument lists of arbitrary length in Tactic Notation.
- [rewrite ... in H] now fails if [H] is used either in an hypothesis
or in the goal.
- The semantics of [rewrite ... in *] has been slightly modified (see doc).
- Support for "as" clause in tactic injection.
- New forward-reasoning tactic "apply in".
- Ltac fresh operator now builds names from a concatenation of its arguments.
- New ltac tactic "remember" to abstract over a subterm and keep an equality
- Support for Miller-Pfenning's patterns unification in apply/rewrite/...
(may lead to few incompatibilities - generally now useless tactic calls).
Bug fixes
- Fix for notations involving basic "match" expressions.
- Numerous other bugs solved (a few fixes may lead to incompatibilities).
Changes from V8.0 to V8.1beta
=============================
Logic
- Added sort-polymorphism on inductive families
- Allowance for recursively non uniform parameters in inductive types
Syntax
- No more support for version 7 syntax and for translation to version 8 syntax.
- In fixpoints, the { struct ... } annotation is not mandatory any more when
only one of the arguments has an inductive type
- Added disjunctive patterns in match-with patterns
- Support for primitive interpretation of string literals
- Extended support for Unicode ranges
Vernacular commands
- Added "Print Ltac qualid" to print a user defined tactic.
- Added "Print Rewrite HintDb" to print the content of a DB used by
autorewrite.
- Added "Print Canonical Projections".
- Added "Example" as synonym of "Definition".
- Added "Proposition" and "Corollary" as extra synonyms of "Lemma".
- New command "Whelp" to send requests to the Helm database of proofs
formalized in the Calculus of Inductive Constructions.
- Command "functional induction" has been re-implemented from the new
"Function" command.
Ltac and tactic syntactic extensions
- New primitive "external" for communication with tool external to Coq
- New semantics for "match t with": 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" does). The keyword "lazymatch" can be used to delay the
evaluation of tactics occurring in matching clauses.
- Hint base names can be parametric in auto and trivial.
- Occurrence values can be parametric in unfold, pattern, etc.
- Added entry constr_may_eval for tactic extensions.
- Low-priority term printer made available in ML-written tactic extensions.
- "Tactic Notation" extended to allow notations of tacticals.
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).
- New implementation (still experimental) of the ring tactic with a built-in
notion of coefficients and a better usage of setoids.
- New conversion tactic "vm_compute": evaluates the goal (or an hypothesis)
with a call-by-value strategy, using the compiled version of terms.
- When rewriting H where H is not directly a Coq equality, search first H for
a registered setoid equality before starting to reduce in H. This is unlikely
to break any script. Should this happen nonetheless, one can insert manually
some "unfold ... in H" before rewriting.
- Fixed various bugs about (setoid) rewrite ... in ... (in particular #1101)
- "rewrite ... in" now accepts a clause as place where to rewrite instead of
juste a simple hypothesis name. For instance:
rewrite H in H1,H2 |- * means rewrite H in H1; rewrite H in H2; rewrite H
rewrite H in * |- will do try rewrite H in Hi for all hypothesis Hi <> H.
- Added "dependent rewrite term" and "dependent rewrite term in hyp" (doc TODO)
- Added "autorewrite with ... in hyp [using ...]".
- Tactic "replace" now accepts a "by" tactic clause.
- Added "clear - id" to clear all hypotheses except the ones depending in id.
- The argument of Declare Left Step and Declare Right Step is now a term
(it used to be a reference).
- Omega now handles arbitrary precision integers.
- Several bug fixes in Reflexive Omega (romega).
- Idtac can now be left implicit in a [...|...] construct: for instance,
[ foo | | bar ] stands for [ foo | idtac | bar ].
- Fixed a "fold" bug (non critical but 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.
- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses.
- New tactic "pose proof" that generalizes "assert (id:=p)" with intro patterns.
- New introduction pattern "?" for letting Coq choose a name.
- Introduction patterns now support side hypotheses (e.g. intros [|] on
"(nat -> nat) -> nat" works).
- New introduction patterns "->" and "<-" for immediate rewriting of
introduced hypotheses.
- Introduction patterns coming after non trivial introduction patterns now
force full introduction of the first pattern (e.g. "intros [[|] p]" on
"nat->nat->nat" now behaves like "intros [[|?] p]")
- Added "eassumption".
- Added option 'using lemmas' to auto, trivial and eauto.
- Tactic "congruence" is now complete for its intended scope (ground
equalities and inequalities with constructors). Furthermore, it
tries to equates goal and hypotheses.
- New tactic "rtauto" solves pure propositional logic and gives a
reflective version of the available proof.
- Numbering of "pattern", "unfold", "simpl", ... occurrences in "match
with" made consistent with the printing of the return clause after
the term to match in the "match-with" construct (use "Set Printing All"
to see hidden occurrences).
- Generalization of induction "induction x1...xn using scheme" where
scheme is an induction principle with complex predicates (like the
ones generated by function induction).
- Some small Ltac tactics has been added to the standard library
(file Tactics.v):
* f_equal : instead of using the different f_equalX lemmas
* case_eq : a "case" without loss of information. An equality
stating the current situation is generated in every sub-cases.
* swap : for a negated goal ~B and a negated hypothesis H:~A,
swap H asks you to prove A from hypothesis B
* revert : revert H is generalize H; clear H.
Extraction
- All type parts should now disappear instead of sometimes producing _
(for instance in Map.empty).
- Haskell extraction: types of functions are now printed, better
unsafeCoerce mechanism, both for hugs and ghc.
- Scheme extraction improved, see http://www.pps.jussieu.fr/~letouzey/scheme.
- Many bug fixes.
Modules
- Added "Locate Module qualid" to get the full path of a module.
- Module/Declare Module syntax made more uniform.
- Added syntactic sugar "Declare Module Export/Import" and
"Module Export/Import".
- Added syntactic sugar "Module M(Export/Import X Y: T)" and
"Module Type M(Export/Import X Y: T)"
(only for interactive definitions)
- Construct "with" generalized to module paths:
T with (Definition|Module) M1.M2....Mn.l := l'.
Notations
- Option "format" aware of recursive notations.
- Added insertion of spaces by default in recursive notations w/o separators.
- No more automatic printing box in case of user-provided printing "format".
- New notation "exists! x:A, P" for unique existence.
- Notations for specific numerals now compatible with generic notations of
numerals (e.g. "1" can be used to denote the unit of a group without
hiding 1%nat)
Libraries
- New library on String and Ascii characters (contributed by L. Thery).
- New library FSets+FMaps of finite sets and maps.
- New library QArith on rational numbers.
- Small extension of Zmin.V, new Zmax.v, new Zminmax.v.
- Reworking and extension of the files on classical logic and
description principles (possible incompatibilities)
- Few other 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).
- Restructuration of Eqdep_dec.v and Eqdep.v: more lemmas in Type.
- Znumtheory now contains a gcd function that can compute within Coq.
- More lemmas stated on Type in Wf.v, removal of redundant Acc_iter and
Acc_iter2.
- Change of the internal names of lemmas in OmegaLemmas.
- Acc in Wf.v and clos_refl_trans in Relation_Operators.v now rely on
the allowance for recursively non uniform parameters (possible
source of incompatibilities: explicit pattern-matching on these
types may require to remove the occurrence associated to their
recursively non uniform parameter).
- Coq.List.In_dec has been set transparent (this may exceptionally break
proof scripts, set it locally opaque for compatibility).
- More on permutations of lists in List.v and Permutation.v.
- List.v has been much expanded.
- New file SetoidList.v now contains results about lists seen with
respect to a setoid equality.
- Library NArith has been expanded, mostly with results coming from
Intmap (for instance a bitwise xor), plus also a bridge between N and
Bitvector.
- Intmap has been reorganized. In particular its address type "addr" is
now N. User contributions known to use Intmap have been adapted
accordingly. If you're using this library please contact us.
A wrapper FMapIntMap now presents Intmap as a particular implementation
of FMaps. New developments are strongly encouraged to use either this
wrapper or any other implementations of FMap instead of using directly
this obsolete Intmap.
Tools
- New semantics for coqtop options ("-batch" expects option "-top dir"
for loading vernac file that contains definitions).
- Tool coq_makefile now removes custom targets that are file names in
"make clean"
- New environment variable 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.
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
- Many newly supported UTF-8 encoded unicode blocks
- Greek letters (0380-03FF), Hebrew letters (U05D0-05EF), letter-like
symbols (2100-214F, that includes double N,Z,Q,R), prime
signs (from 2080-2089) and characters from many written languages
are valid in identifiers
- mathematical operators (2200-22FF), supplemental mathematical
operators (2A00-2AFF), miscellaneous technical (2300-23FF that
includes sqrt symbol), miscellaneous symbols (2600-26FF), arrows
(2190-21FF and 2900-297F), invisible mathematical operators (from
2080-2089), ... are valid 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