| Age | Commit message (Collapse) | Author |
|---|
|
|
|
ie default goal selector !
How to do this:
- change the default value of default goal selector in goal_select.ml
- eval the emacs code in this commit message
- compile Coq and in each erroring file repeatedly run
[C-c f] (my/maybe-fix-buller-error) then [C-c C-b] (proof-process-buffer)
until there are no errors (NB the first [C-c f] has no effect).
You need to watch for 2 cases:
- overly deep proofs where the bullets need to go beyond the list in
my/bullet-stack (6 layers is enough the vast majority of the time
though). The system will give you an error and you need to finish
the lemma manually.
- weird indentation when a bullet starts in the middle of a line and
doesn't end in that line. Just reindent as you like then go to the
next error and continue.
~~~emacs-lisp
(defconst my/bullet-stack (list "-" "+" "*" "--" "++" "**")
"Which bullets should be used, in order.")
(defvar-local my/bullet-count nil
"The value in the car indicates how many goals remain in the
bullet at (length-1), and so on recursively. nil means we
haven't started bulleting the current proof.")
(defvar-local my/last-seen-qed nil)
(defun my/get-maybe-bullet-error ()
"Extract the number of focused goals from the ! selector error message."
(when-let* ((rbuf (get-buffer "*response*"))
(str (with-current-buffer "*response*" (buffer-string)))
(_ (string-match
(rx "Error: Expected a single focused goal but " (group (+ digit)))
str))
(ngoals (string-to-number (match-string 1 str))))
ngoals))
(defun my/bullet-fix-indent ()
"Auto indent until the next Qed/Defined, and update my/last-seen-qed."
;; (insert (format "(* %s -> %s *)\n" my/prev-count my/bullet-count))
(when-let ((qed (save-excursion (search-forward-regexp (rx (or "Defined." "Qed.")) nil t))))
(set-marker my/last-seen-qed qed)
(indent-region (- (point) 1) qed)))
(defun my/nth-bullet (n)
"Get nth bullet, erroring if n >= length my/bullet-stack"
(or (nth n my/bullet-stack)
(error "Too many bullets.")))
(defun my/maybe-fix-bullet-error (&optional arg)
"Main function for porting a file to strict focusing.
Repeatedly process your file in proof general until you get a
focusing error, then run this function. Once there are no more
errors you're done.
Indentation commonly looks bad in the middle of fixing a proof,
but will be fixed unless you start a bullet in the middle of a
line and don't finish it in that line. ie in 'tac1. - tac2.\n
tac3.' tac3 will get indented to align with tac2, but if tac2
finished the bullet the next action will reindent.
This is a stateful process. The state is automatically reset when
you get to the next proof, but if you get an error or take manual
action which breaks the algorithm's expectation you can call with
prefix argument to reset."
(interactive "P")
(unless my/last-seen-qed
(setq my/last-seen-qed (set-marker (make-marker) 0)))
(when (or arg (> (point) my/last-seen-qed))
(setq my/bullet-count nil)
(set-marker my/last-seen-qed 0))
(when-let ((ngoals (my/get-maybe-bullet-error)))
(setq my/prev-count (format "%s %s" ngoals my/bullet-count))
(if (= ngoals 0)
(progn
(while (and my/bullet-count (= (car my/bullet-count) 0))
(pop my/bullet-count))
(insert (concat (my/nth-bullet (- (length my/bullet-count) 1)) " "))
(setq my/bullet-count (cons (- (car my/bullet-count) 1) (cdr my/bullet-count)))
(my/bullet-fix-indent))
(setq my/bullet-count (cons (- ngoals 1) my/bullet-count))
(insert (concat (my/nth-bullet (- (length my/bullet-count) 1)) " "))
(my/bullet-fix-indent))))
(bind-key "C-c f" #'my/maybe-fix-bullet-error coq-mode-map)
~~~
|
|
|
|
|
|
|
|
|
|
As reported in #9060, the STM does not handle such constructions
properly. They are anyway fragile, for example Guarded reports a failure
if run at the end of the scripts, so this patch is an improvement.
|
|
|
|
Exists_impl
|
|
We encode the conversion to bits with little-endian right-associative
tuples to ensure that the head of the tuple (the `fst` element) is the
least significant bit. We still enforce that the ordering of bits
matches the order of the `bool`s in the `ascii` inductive type.
|
|
We already have roundtrip proofs for byte<->nat, byte<->N, byte<->ascii,
N<->nat, ascii<->N, ascii<->nat, and this commit shows that all
roundtrips involving byte commute appropriately. This ensures, e.g.,
that we don't mess up and reverse the bits in conversion between byte
and ascii.
|
|
We could move another ~ 1s from Init.Byte to Strings.Byte by moving
`of_bits_to_bits` and `to_bits_of_bits`, but I figured it's probably not
worth it.
After | File Name | Before || Change | % Change
----------------------------------------------------------------------------------
1m16.75s | Total | 1m21.45s || -0m04.70s | -5.77%
----------------------------------------------------------------------------------
0m08.95s | Strings/Byte | 0m12.41s || -0m03.46s | -27.88%
0m07.24s | Byte | 0m08.76s || -0m01.51s | -17.35%
0m06.37s | plugins/setoid_ring/Ring_polynom | 0m06.24s || +0m00.12s | +2.08%
0m03.14s | Numbers/Integer/Abstract/ZBits | 0m03.20s || -0m00.06s | -1.87%
0m02.44s | ZArith/BinInt | 0m02.44s || +0m00.00s | +0.00%
0m02.24s | Numbers/Natural/Abstract/NBits | 0m02.20s || +0m00.04s | +1.81%
0m01.97s | Lists/List | 0m01.93s || +0m00.04s | +2.07%
0m01.85s | Numbers/NatInt/NZLog | 0m01.82s || +0m00.03s | +1.64%
0m01.78s | PArith/BinPos | 0m01.78s || +0m00.00s | +0.00%
0m01.74s | plugins/setoid_ring/InitialRing | 0m01.63s || +0m00.11s | +6.74%
0m01.73s | Strings/Ascii | 0m01.58s || +0m00.14s | +9.49%
0m01.39s | NArith/BinNat | 0m01.34s || +0m00.04s | +3.73%
0m01.32s | Numbers/NatInt/NZPow | 0m01.24s || +0m00.08s | +6.45%
0m01.22s | Numbers/NatInt/NZSqrt | 0m01.15s || +0m00.07s | +6.08%
0m01.11s | Arith/PeanoNat | 0m01.16s || -0m00.04s | -4.31%
0m01.10s | Numbers/Integer/Abstract/ZDivTrunc | 0m01.11s || -0m00.01s | -0.90%
0m01.02s | Specif | 0m01.04s || -0m00.02s | -1.92%
0m00.96s | Numbers/NatInt/NZMulOrder | 0m00.84s || +0m00.12s | +14.28%
0m00.95s | Numbers/Integer/Abstract/ZDivFloor | 0m00.97s || -0m00.02s | -2.06%
0m00.85s | plugins/setoid_ring/Ring_theory | 0m00.86s || -0m00.01s | -1.16%
0m00.82s | Structures/GenericMinMax | 0m00.85s || -0m00.03s | -3.52%
0m00.72s | Numbers/Integer/Abstract/ZLcm | 0m00.82s || -0m00.09s | -12.19%
0m00.69s | Numbers/NatInt/NZParity | 0m00.69s || +0m00.00s | +0.00%
0m00.68s | Numbers/NatInt/NZDiv | 0m00.71s || -0m00.02s | -4.22%
0m00.68s | Strings/String | 0m00.65s || +0m00.03s | +4.61%
0m00.64s | Numbers/Integer/Abstract/ZSgnAbs | 0m00.64s || +0m00.00s | +0.00%
0m00.64s | ZArith/Zeven | 0m00.48s || +0m00.16s | +33.33%
0m00.63s | ZArith/Zorder | 0m00.61s || +0m00.02s | +3.27%
0m00.57s | Numbers/Integer/Abstract/ZMulOrder | 0m00.67s || -0m00.10s | -14.92%
0m00.56s | Classes/Morphisms | 0m00.58s || -0m00.01s | -3.44%
0m00.55s | Numbers/NatInt/NZOrder | 0m00.51s || +0m00.04s | +7.84%
0m00.48s | ZArith/BinIntDef | 0m00.48s || +0m00.00s | +0.00%
0m00.46s | Classes/CMorphisms | 0m00.48s || -0m00.01s | -4.16%
0m00.46s | Numbers/Integer/Abstract/ZGcd | 0m00.46s || +0m00.00s | +0.00%
0m00.46s | Numbers/Natural/Abstract/NSub | 0m00.48s || -0m00.01s | -4.16%
0m00.45s | Logic | 0m00.44s || +0m00.01s | +2.27%
0m00.45s | Numbers/Natural/Abstract/NGcd | 0m00.48s || -0m00.02s | -6.24%
0m00.42s | Numbers/Natural/Abstract/NLcm | 0m00.40s || +0m00.01s | +4.99%
0m00.42s | Structures/OrdersFacts | 0m00.48s || -0m00.06s | -12.50%
0m00.41s | ZArith/Zbool | 0m00.38s || +0m00.02s | +7.89%
0m00.38s | Numbers/Integer/Abstract/ZPow | 0m00.34s || +0m00.03s | +11.76%
0m00.36s | Bool/Bool | 0m00.36s || +0m00.00s | +0.00%
0m00.36s | Numbers/NatInt/NZGcd | 0m00.35s || +0m00.01s | +2.85%
0m00.36s | ZArith/ZArith_dec | 0m00.38s || -0m00.02s | -5.26%
0m00.34s | Numbers/Integer/Abstract/ZAdd | 0m00.33s || +0m00.01s | +3.03%
0m00.34s | PArith/Pnat | 0m00.31s || +0m00.03s | +9.67%
0m00.32s | Numbers/Natural/Abstract/NOrder | 0m00.32s || +0m00.00s | +0.00%
0m00.32s | PArith/BinPosDef | 0m00.31s || +0m00.01s | +3.22%
0m00.32s | ZArith/Zcompare | 0m00.28s || +0m00.03s | +14.28%
0m00.30s | Classes/RelationClasses | 0m00.29s || +0m00.01s | +3.44%
0m00.30s | NArith/Nnat | 0m00.30s || +0m00.00s | +0.00%
0m00.29s | Numbers/Natural/Abstract/NAxioms | 0m00.26s || +0m00.02s | +11.53%
0m00.28s | Numbers/Integer/Abstract/ZAddOrder | 0m00.28s || +0m00.00s | +0.00%
0m00.28s | Structures/Orders | 0m00.30s || -0m00.01s | -6.66%
0m00.27s | Numbers/Integer/Abstract/ZAxioms | 0m00.23s || +0m00.04s | +17.39%
0m00.27s | Numbers/NatInt/NZAxioms | 0m00.26s || +0m00.01s | +3.84%
0m00.26s | Numbers/Integer/Abstract/ZMaxMin | 0m00.25s || +0m00.01s | +4.00%
0m00.26s | Numbers/NatInt/NZAdd | 0m00.28s || -0m00.02s | -7.14%
0m00.26s | Numbers/Natural/Abstract/NMaxMin | 0m00.24s || +0m00.02s | +8.33%
0m00.26s | Numbers/Natural/Abstract/NParity | 0m00.31s || -0m00.04s | -16.12%
0m00.26s | plugins/setoid_ring/ArithRing | 0m00.22s || +0m00.04s | +18.18%
0m00.26s | plugins/setoid_ring/Ring_tac | 0m00.24s || +0m00.02s | +8.33%
0m00.25s | Logic/Decidable | 0m00.26s || -0m00.01s | -3.84%
0m00.25s | Structures/OrdersTac | 0m00.25s || +0m00.00s | +0.00%
0m00.24s | Classes/Equivalence | 0m00.25s || -0m00.01s | -4.00%
0m00.24s | Datatypes | 0m00.27s || -0m00.03s | -11.11%
0m00.24s | Numbers/NatInt/NZMul | 0m00.25s || -0m00.01s | -4.00%
0m00.24s | plugins/setoid_ring/Ring | 0m00.20s || +0m00.03s | +19.99%
0m00.23s | Numbers/NatInt/NZAddOrder | 0m00.33s || -0m00.10s | -30.30%
0m00.23s | Numbers/Natural/Abstract/NAdd | 0m00.17s || +0m00.06s | +35.29%
0m00.22s | Arith/Compare_dec | 0m00.22s || +0m00.00s | +0.00%
0m00.22s | Classes/CRelationClasses | 0m00.25s || -0m00.03s | -12.00%
0m00.22s | Logic/EqdepFacts | 0m00.19s || +0m00.03s | +15.78%
0m00.22s | NArith/BinNatDef | 0m00.25s || -0m00.03s | -12.00%
0m00.22s | plugins/setoid_ring/Ring_base | 0m00.23s || -0m00.01s | -4.34%
0m00.21s | Arith/Arith | 0m00.19s || +0m00.01s | +10.52%
0m00.21s | Numbers/Natural/Abstract/NDiv | 0m00.19s || +0m00.01s | +10.52%
0m00.20s | Numbers/Integer/Abstract/ZProperties | 0m00.23s || -0m00.03s | -13.04%
0m00.20s | Relations/Relation_Operators | 0m00.17s || +0m00.03s | +17.64%
0m00.19s | Arith/Between | 0m00.22s || -0m00.03s | -13.63%
0m00.18s | Arith/Wf_nat | 0m00.24s || -0m00.06s | -25.00%
0m00.17s | Arith/Plus | 0m00.16s || +0m00.01s | +6.25%
0m00.17s | Nat | 0m00.18s || -0m00.00s | -5.55%
0m00.17s | Numbers/Natural/Abstract/NProperties | 0m00.22s || -0m00.04s | -22.72%
0m00.17s | Relations/Relation_Definitions | 0m00.08s || +0m00.09s | +112.50%
0m00.16s | Numbers/Integer/Abstract/ZLt | 0m00.16s || +0m00.00s | +0.00%
0m00.16s | Numbers/Natural/Abstract/NBase | 0m00.19s || -0m00.03s | -15.78%
0m00.16s | Numbers/Natural/Abstract/NPow | 0m00.15s || +0m00.01s | +6.66%
0m00.15s | Classes/Morphisms_Prop | 0m00.18s || -0m00.03s | -16.66%
0m00.14s | Arith/Mult | 0m00.12s || +0m00.02s | +16.66%
0m00.14s | Arith/Peano_dec | 0m00.16s || -0m00.01s | -12.49%
0m00.14s | Numbers/NatInt/NZBase | 0m00.13s || +0m00.01s | +7.69%
0m00.14s | Numbers/Natural/Abstract/NMulOrder | 0m00.13s || +0m00.01s | +7.69%
0m00.14s | Relations/Operators_Properties | 0m00.13s || +0m00.01s | +7.69%
0m00.14s | plugins/setoid_ring/BinList | 0m00.16s || -0m00.01s | -12.49%
0m00.13s | Arith/EqNat | 0m00.18s || -0m00.04s | -27.77%
0m00.13s | Structures/Equalities | 0m00.17s || -0m00.04s | -23.52%
0m00.12s | Arith/Lt | 0m00.11s || +0m00.00s | +9.09%
0m00.12s | Arith/Minus | 0m00.13s || -0m00.01s | -7.69%
0m00.12s | Decimal | 0m00.16s || -0m00.04s | -25.00%
0m00.12s | Numbers/Integer/Abstract/ZBase | 0m00.09s || +0m00.03s | +33.33%
0m00.12s | Numbers/Integer/Abstract/ZMul | 0m00.12s || +0m00.00s | +0.00%
0m00.12s | Numbers/Integer/Abstract/ZParity | 0m00.11s || +0m00.00s | +9.09%
0m00.12s | Numbers/Natural/Abstract/NAddOrder | 0m00.12s || +0m00.00s | +0.00%
0m00.11s | Arith/Factorial | 0m00.11s || +0m00.00s | +0.00%
0m00.11s | Lists/ListTactics | 0m00.13s || -0m00.02s | -15.38%
0m00.11s | Logic/Eqdep_dec | 0m00.12s || -0m00.00s | -8.33%
0m00.11s | Numbers/Natural/Abstract/NLog | 0m00.10s || +0m00.00s | +9.99%
0m00.11s | Peano | 0m00.10s || +0m00.00s | +9.99%
0m00.11s | Program/Basics | 0m00.07s || +0m00.03s | +57.14%
0m00.10s | Arith/Gt | 0m00.13s || -0m00.03s | -23.07%
0m00.10s | Bool/Sumbool | 0m00.10s || +0m00.00s | +0.00%
0m00.10s | Numbers/Natural/Abstract/NSqrt | 0m00.12s || -0m00.01s | -16.66%
0m00.10s | Wf | 0m00.11s || -0m00.00s | -9.09%
0m00.09s | Arith/Arith_base | 0m00.09s || +0m00.00s | +0.00%
0m00.09s | Logic_Type | 0m00.08s || +0m00.00s | +12.49%
0m00.08s | Arith/Le | 0m00.11s || -0m00.03s | -27.27%
0m00.08s | Numbers/BinNums | 0m00.06s || +0m00.02s | +33.33%
0m00.08s | Numbers/NatInt/NZBits | 0m00.12s || -0m00.03s | -33.33%
0m00.08s | Numbers/NatInt/NZProperties | 0m00.09s || -0m00.00s | -11.11%
0m00.08s | Program/Tactics | 0m00.08s || +0m00.00s | +0.00%
0m00.07s | Tactics | 0m00.10s || -0m00.03s | -30.00%
0m00.06s | Classes/SetoidTactics | 0m00.06s || +0m00.00s | +0.00%
0m00.06s | Numbers/NumPrelude | 0m00.06s || +0m00.00s | +0.00%
0m00.05s | Classes/Init | 0m00.04s || +0m00.01s | +25.00%
0m00.05s | Prelude | 0m00.09s || -0m00.03s | -44.44%
0m00.05s | Setoids/Setoid | 0m00.08s || -0m00.03s | -37.50%
0m00.04s | Relations/Relations | 0m00.04s || +0m00.00s | +0.00%
0m00.04s | Tauto | 0m00.09s || -0m00.05s | -55.55%
0m00.02s | Notations | 0m00.04s || -0m00.02s | -50.00%
|
|
Users can now register string notations for custom inductives.
Much of the code and documentation was copied from numeral notations.
I chose to use a 256-constructor inductive for primitive string syntax
because (a) it is easy to convert between character codes and
constructors, and (b) it is more efficient than the existing `ascii`
type.
Some choices about proofs of the new `byte` type were made based on
efficiency. For example, https://github.com/coq/coq/issues/8517 means
that we cannot simply use `Scheme Equality` for this type, and I have
taken some care to ensure that the proofs of decidable equality and
conversion are fast. (Unfortunately, the `Init/Byte.v` file is the
slowest one in the prelude (it takes a couple of seconds to build), and
I'm not sure where the slowness is.)
In String.v, some uses of `0` as a `nat` were replaced by `O`, because
the file initially refused to check interactively otherwise (it
complained that `0` could not be interpreted in `string_scope` before
loading `Coq.Strings.String`).
There is unfortunately a decent amount of code duplication between
numeral notations and string notations.
I have not put too much thought into chosing names; most names have been
chosen to be similar to numeral notations, though I chose the name
`byte` from
https://github.com/coq/coq/issues/8483#issuecomment-421671785.
Unfortunately, this feature does not support declaring string syntax for
`list ascii`, unless that type is wrapped in a record or other inductive
type. This is not a fundamental limitation; it should be relatively
easy for someone who knows the API of the reduction machinery in Coq to
extend both this and numeral notations to support any type whose hnf
starts with an inductive type. (The reason for needing an inductive
type to bottom out at is that this is how the plugin determines what
constructors are the entry points for printing the given notation.
However, see also https://github.com/coq/coq/issues/8964 for
complications that are more likely to arise if inductive type families
are supported.)
N.B. I generated the long lists of constructors for the `byte` type with
short python scripts.
Closes #8853
|
|
|
|
Forall_inv to assert that a property that is true for every element of a list is true for every element in the tail of the list. The second, Exists_impl, parallels Forall_impl and proves that if there exists an element in a list that satisfies a given predicate, and the predicate implies another proposition, then there exists an element in the list that satisfies the implied proposition. Both of these proofs fill natural gaps within the List library.
|
|
|
|
|
|
|
|
|
|
|
|
Previously, hints added without a specified database where implicitly
put in the "core" database, which was discouraged by the user manual
(because of the lack of modularity of this approach).
|
|
|
|
module
|
|
The compilation to bytecode of the elimination schemes for int31 must
happen after the int31 type is registered to the retroknowledge.
Otherwise, the “decompint” instruction is not emitted.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
We refactor the `Coqlib` API to locate objects over a namespace
`module.object.property`.
This introduces the vernacular command `Register g as n` to expose the
Coq constant `g` under the name `n` (through the `register_ref`
function). The constant can then be dynamically located using the
`lib_ref` function.
Co-authored-by: Emilio Jesús Gallego Arias <e+git@x80.org>
Co-authored-by: Maxime Dénès <mail@maximedenes.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
Mostly via `dev/tools/update-compat.py --cur-version=8.9`
We just remove test-suite/success/FunindExtraction_compat86.v because,
except for the `Extraction iszero.` line at the bottom, it is a
duplicate of `test-suite/success/Funind.v` (except with `-compat 8.6`).
We also manually update a number of test-suite files to pre-emptively
remove compatibility notations (which used to be compat 8.6, but are now
compat 8.7).
|
|
All changes done with
```
git grep --name-only 'compat "8.6"' | xargs sed -i s'/compat "8.6"/compat "8.7"/g'
```
As per https://github.com/coq/coq/pull/8374#issuecomment-426202818 and
https://github.com/coq/coq/issues/8383#issuecomment-426200497
|
|
|
|
|
|
* ext_in_map
* map_ext_in_iff
* firstn_skipn_comm
* skipn_firstn_comm
* skipn_O
* skipn_nil
* skipn_cons
* skipn_none
* skipn_all
* skipn_all2
* skipn_app
* seq_ap
* skipn_app
* skipn_length
* firstn_skipn_rev
* firstn_rev
* skipn_rev
* seq_app
All proofs by Anton Trunov.
|
|
This broke the build so it should be merged quickly.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
