| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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)
~~~
|
|
|
|
|
|
|
|
|
|
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14238 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
|
|
(floor convention).
We follow Haskell naming convention: quot and rem are for
Round-Toward-Zero (a.k.a Trunc, what Ocaml, C, Asm do by default, cf.
the ex-ZOdiv file), while div and mod are for Round-Toward-Bottom
(a.k.a Floor, what Coq does historically in Zdiv). We use unicode ÷
for quot, and infix rem for rem (which is actually remainder in
full). This way, both conventions can be used at the same time.
Definitions (and proofs of specifications) for div mod quot rem are
migrated in a new file Zdiv_def. Ex-ZOdiv file is now Zquot. With
this new organisation, no need for functor application in Zdiv and
Zquot.
On the abstract side, ZAxiomsSig now provides div mod quot rem.
Zproperties now contains properties of them. In NZDiv, we stop
splitting specifications in Common vs. Specific parts. Instead,
the NZ specification is be extended later, even if this leads to
a useless mod_bound_pos, subsumed by more precise axioms.
A few results in ZDivTrunc and ZDivFloor are improved (sgn stuff).
A few proofs in Nnat, Znat, Zabs are reworked (no more dependency
to Zmin, Zmax).
A lcm (least common multiple) is derived abstractly from gcd and
division (and hence available for nat N BigN Z BigZ :-).
In these new files NLcm and ZLcm, we also provide some combined
properties of div mod quot rem gcd.
We also provide a new file Zeuclid implementing a third division
convention, where the remainder is always positive. This file
instanciate the abstract one ZDivEucl. Operation names are
ZEuclid.div and ZEuclid.modulo.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13633 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
We temporary use a hack to convert a module type into a module
Module M := T is refused, so we force an include via
Module M := Nop <+ T where Nop is an empty module.
To be fixed later more beautifully...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13602 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Initially, I was using notation 1 := (S 0) and so on. But then, when
implementing by NArith or ZArith, some lemmas statements were filled
with Nsucc's and Zsucc's instead of 1 and 2's.
Concerning BigN, things are rather complicated: zero, one, two
aren't inlined during the functor application creating BigN.
This is deliberate, at least for the other operations like BigN.add.
And anyway, since zero, one, two are defined too early in NMake,
we don't have 0%bigN in the body of BigN.zero but something complex that
reduce to 0%bigN, same for one and two. Fortunately, apply or
rewrite of generic lemmas seem to work, even if there's BigZ.zero
on one side and 0 on the other...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13555 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Simplification of functor names, e.g. ZFooProp instead of ZFooPropFunct
- The axiomatisations of the different fonctions are now in {N,Z}Axioms.v
apart for Z division (three separate flavours in there own files).
Content of {N,Z}AxiomsSig is extended, old version is {N,Z}AxiomsMiniSig.
- In NAxioms, the recursion field isn't that useful, since we axiomatize
other functions and not define them (apart in the toy NDefOps.v).
We leave recursion there, but in a separate NAxiomsFullSig.
- On Z, the pow function is specified to behave as Zpower : a^(-1)=0
- In BigN/BigZ, (power:t->N->t) is now pow_N, while pow is t->t->t
These pow could be more clever (we convert 2nd arg to N and use pow_N).
Default "^" is now (pow:t->t->t). BigN/BigZ ring is adapted accordingly
- In BigN, is_even is now even, its spec is changed to use Zeven_bool.
We add an odd. In BigZ, we add even and odd.
- In ZBinary (implem of ZAxioms by ZArith), we create an efficient Zpow
to implement pow. This Zpow should replace the current linear Zpower
someday.
- In NPeano (implem of NAxioms by Arith), we create pow, even, odd functions,
and we modify the div and mod functions for them to be linear, structural,
tail-recursive.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13546 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@12704 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
NB: for declaring div and mod as a morphism, even when divisor is zero,
I've slightly changed the definition of div_eucl: it now starts by a
check of whether the divisor is zero. Not very nice, but this way
we can say that BigN.div and BigZ.div _always_ answer like Zdiv.Zdiv.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12646 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
without scope.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12639 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
by ...")
Application in some proofs of Numbers's abstract division
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12630 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Properties are now rather passed as functor arg instead of via Include or
some inner modules.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12629 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
This used to be convenient in FSets, but since we now try to integrate
DecidableType and OrderedType as foundation for other part of the stdlib,
this should be avoided, otherwise some eauto take a _long_ time.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12626 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
particular about eq)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12625 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12624 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
NB: the grammar entry is placed in vernac:command on purpose
even if it should have gone into vernac:gallina_ext. Camlp4
isn't factorising rules starting by "Declare" in a correct way
otherwise...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12623 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12591 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- For Z, we propose 3 conventions for the sign of the remainder...
- Instanciation for nat in NPeano.
- Beginning of instanciation in ZOdiv.
Still many proofs to finish, etc, etc, but soon we will have a decent
properties database for all divisions of all instances of Numbers (e.g. BigZ).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12590 85f007b7-540e-0410-9357-904b9bb8a0f7
|
