| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
By default Coq stdlib warnings raise an error, so this is really required.
|
|
|
|
|
|
The syntax of formulae is extended to support boolean constants (true,
false), boolean operators Bool.andb, Bool.orb, Bool.implb, Bool.negb,
Bool.eqb and comparison operators Z.eqb, Z.ltb, Z.gtb, Z.leb and
Z.ltb.
|
|
|
|
Reviewed-by: anton-trunov
Reviewed-by: herbelin
|
|
|
|
This addresses a question on gitter (April 4).
|
|
|
|
Add headers to a few files which were missing them.
|
|
|
|
|
|
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)
~~~
|
|
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).
|
|
This broke the build so it should be merged quickly.
|
|
|
|
Removing in passing two Local which are no-ops in practice.
|
|
|
|
|
|
|
|
|
|
automatically instead
|
|
This old compatibility hint database can be safely removed
now that coq-contribs do not depend on it anymore.
|
|
|
|
|
|
|
|
|
|
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Most of these heavyweight annotations were introduced a long time ago
by the automatic 7.x -> 8.0 translator
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15518 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15517 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- For instance, refl_equal --> eq_refl
- Npos, Zpos, Zneg now admit more uniform qualified aliases
N.pos, Z.pos, Z.neg.
- A new module BinInt.Pos2Z with results about injections from
positive to Z
- A result about Z.pow pushed in the generic layer
- Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l}
- Using tactic Z.le_elim instead of Zle_lt_or_eq
- Some cleanup in ring, field, micromega
(use of "Equivalence", "Proper" ...)
- Some adaptions in QArith (for instance changed Qpower.Qpower_decomp)
- In ZMake and ZMake, functor parameters are now named NN and ZZ
instead of N and Z for avoiding confusions
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14718 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- All statement using reflect are made transparent.
(Otherwise, since reflect isn't in Prop, extraction
complains now about opaque Type definition).
- remove two local Peqb_spec and Neqb_spec, now provided
globally as Pos.eqb_spec and N.eqb_spec.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14232 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
To avoid names¬ations clashs with list, Vector shouldn't be
"Import"ed but one can "Import Vector.VectorNotations." to have
notations.
SetoidVector at least remains to do.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13702 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
See NatInt/NZBits.v for the common axiomatization of bitwise functions
over naturals / integers. Some specs aren't pretty, but easier to
prove, see alternate statements in property functors {N,Z}Bits.
Negative numbers are considered via the two's complement convention.
We provide implementations for N (in Ndigits.v), for nat (quite dummy,
just for completeness), for Z (new file Zdigits_def), for BigN
(for the moment partly by converting to N, to be improved soon)
and for BigZ.
NOTA: For BigN.shiftl and BigN.shiftr, the two arguments are now in
the reversed order (for consistency with the rest of the world):
for instance BigN.shiftl 1 10 is 2^10.
NOTA2: Zeven.Zdiv2 is _not_ doing (Zdiv _ 2), but rather (Zquot _ 2)
on negative numbers. For the moment I've kept it intact, and have
just added a Zdiv2' which is truly equivalent to (Zdiv _ 2).
To reorganize someday ?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13689 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Initial plan was only to add shiftl/shiftr/land/... to N and
other number type, this is only partly done, but this work has
diverged into a big reorganisation and improvement session
of PArith,NArith,ZArith.
Bool/Bool: add lemmas orb_diag (a||a = a) and andb_diag (a&&a = a)
PArith/BinPos:
- added a power function Ppow
- iterator iter_pos moved from Zmisc to here + some lemmas
- added Psize_pos, which is 1+log2, used to define Nlog2/Zlog2
- more lemmas on Pcompare and succ/+/* and order, allow
to simplify a lot some old proofs elsewhere.
- new/revised results on Pminus (including some direct proof of
stuff from Pnat)
PArith/Pnat:
- more direct proofs (limit the need of stuff about Pmult_nat).
- provide nicer names for some lemmas (eg. Pplus_plus instead of
nat_of_P_plus_morphism), compatibility notations provided.
- kill some too-specific lemmas unused in stdlib + contribs
NArith/BinNat:
- N_of_nat, nat_of_N moved from Nnat to here.
- a lemma relating Npred and Nminus
- revised definitions and specification proofs of Npow and Nlog2
NArith/Nnat:
- shorter proofs.
- stuff about Z_of_N is moved to Znat. This way, NArith is
entirely independent from ZArith.
NArith/Ndigits:
- added bitwise operations Nand Nor Ndiff Nshiftl Nshiftr
- revised proofs about Nxor, still using functional bit stream
- use the same approach to prove properties of Nand Nor Ndiff
ZArith/BinInt: huge simplification of Zplus_assoc + cosmetic stuff
ZArith/Zcompare: nicer proofs of ugly things like Zcompare_Zplus_compat
ZArith/Znat: some nicer proofs and names, received stuff about Z_of_N
ZArith/Zmisc: almost empty new, only contain stuff about badly-named
iter. Should be reformed more someday.
ZArith/Zlog_def: Zlog2 is now based on Psize_pos, this factorizes
proofs and avoid slowdown due to adding 1 in Z instead of in positive
Zarith/Zpow_def: Zpower_opt is renamed more modestly Zpower_alt
as long as I dont't know why it's slower on powers of two.
Elsewhere: propagate new names + some nicer proofs
NB: Impact on compatibility is probably non-zero, but should be
really moderate. We'll see on contribs, but a few Require here
and there might be necessary.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13651 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Program in terms of implicit arguments to the rest of the library.
This commit only covers the case of list of implicit arguments that
have a different length in Program (e.g. inl, Vcons) but not the case of
implicit arguments which differs only in their maximality status
(e.g. pair).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13575 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13471 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13294 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13293 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13286 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
For the moment, almost no lemmas about (reflect P b), just the proofs
that it is equivalent with an P<->b=true.
is_true b is (b=true), and is meant to be added as a coercion
if one wants it. In the StdLib, this coercion is not globally
activated, but particular files are free to use Local Coercion...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13275 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Many of them were broken, some of them after Pierre B's rework
of mli for ocamldoc, but not only (many bad annotation, many files
with no svn property about Id, etc)
- Useless for those of us that work with git-svn (and a fortiori
in a forthcoming git-only setting)
- Even in svn, they seem to be of little interest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Bvector uses only Minus, so let's avoid loading Arith
(and hence ArithRing and hence parts of Z, N)
Program.Syntax no longer need Lists now that list is in Datatypes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12785 85f007b7-540e-0410-9357-904b9bb8a0f7
|
