| Age | Commit message (Collapse) | Author |
|---|
|
This removes various compatibility notations.
Closes #8374
This commit was mostly created by running `./dev/tools/update-compat.py
--release`. There's a bit of manual spacing adjustment around all of the
removed compatibility notations, and some test-suite updates were done
manually.
The update to CHANGES.md was manual.
|
|
|
|
This work makes it possible to take advantage of a compact
representation for integers in the entire system, as opposed to only
in some reduction machines. It is useful for heavily computational
applications, where even constructing terms is not possible without such
a representation.
Concretely, it replaces part of the retroknowledge machinery with
a primitive construction for integers in terms, and introduces a kind of
FFI which maps constants to operators (on integers). Properties of these
operators are expressed as explicit axioms, whereas they were hidden in
the retroknowledge-based approach.
This has been presented at the Coq workshop and some Coq Working Groups,
and has been used by various groups for STM trace checking,
computational analysis, etc.
Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr>
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
This commit was created via `./dev/tools/update-compat.py --master`
|
|
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
|
|
|
|
|
|
|
|
|
|
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).
|
|
This parsing/printing method for nat should be just as fast as
the previous dedicated code. Moreover, we could now parse large
literals as nat numbers, by leaving them in a half-abstract form
such as (Nat.of_uint 123456). This form is convertible to the
closed (S (S (S ...))) form, so it shouldn't be a big deal for
compatibility, except for if some Ltac stuff relies on (S ...) to be
present after parsing. Of course, forcing the computation of
a (Nat.of_uint ....) may take a while or raise a Stack Overflow.
|
|
|
|
This closes #6598
|
|
|
|
|
|
|
|
|
|
See now https://github.com/coq/bignums
Int31 is still in the stdlib.
Some proofs there has be adapted to avoid the need for BigNumPrelude.
|
|
|
|
Also integrating suggestions from Théo.
|
|
choice of a representative in a partition of bool.
Also move a result about propositional extensionality from
ClassicalFacts.v to PropExtensionalityFacts.v, generalizing it by
symmetry.
Also spotting typos (thanks to Théo).
|
|
We also add a Coq86.v compat file.
|
|
|
|
|
|
enough
In particular, its interface might still change (in interaction with interested
colleagues). So let's not give it too much visibility yet. Instead, I'll turn
it as an opam packages for now.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
documentation)
This commit r14895 comes apparently itself from commit r12010 in branch v8.2
|
|
Renamed Fan.v into WeakFan.v since this was a proof of Weak Fan Theorem
after all.
|
|
- The earlier proof-of-concept file NPeano (which instantiates
the "Numbers" framework for nat) becomes now the entry point
in the Arith lib, and gets renamed PeanoNat. It still provides
an inner module "Nat" which sums up everything about type nat
(functions, predicates and properties of them).
This inner module Nat is usable as soon as you Require Import Arith,
or just Arith_base, or simply PeanoNat.
- Definitions of operations over type nat are now grouped in a new
file Init/Nat.v. This file is meant to be used without "Import",
hence providing for instance Nat.add or Nat.sqrt as soon as coqtop
starts (but no proofs about them).
- The definitions that used to be in Init/Peano.v (pred, plus, minus, mult)
are now compatibility notations (for Nat.pred, Nat.add, Nat.sub, Nat.mul
where here Nat is Init/Nat.v).
- This Coq.Init.Nat module (with only pure definitions) is Include'd
in the aforementioned Coq.Arith.PeanoNat.Nat. You might see Init.Nat
sometimes instead of just Nat (for instance when doing "Print plus").
Normally it should be ok to just ignore these "Init" since
Init.Nat is included in the full PeanoNat.Nat. I'm investigating if
it's possible to get rid of these "Init" prefixes.
- Concerning predicates, orders le and lt are still defined in Init/Peano.v,
with their notations "<=" and "<". Properties in PeanoNat.Nat directly
refer to these predicates in Peano. For instantation reasons, PeanoNat.Nat
also contains a Nat.le and Nat.lt (defined via "Definition le := Peano.le",
we cannot yet include an Inductive to implement a Parameter), but these
aliased predicates won't probably be very convenient to use.
- Technical remark: I've split the previous property functor NProp in
two parts (NBasicProp and NExtraProp), it helps a lot for building
PeanoNat.Nat incrementally. Roughly speaking, we have the following schema:
Module Nat.
Include Coq.Init.Nat. (* definition of operations : add ... sqrt ... *)
... (** proofs of specifications for basic ops such as + * - *)
Include NBasicProp. (** generic properties of these basic ops *)
... (** proofs of specifications for advanced ops (pow sqrt log2...)
that may rely on proofs for + * - *)
Include NExtraProp. (** all remaining properties *)
End Nat.
- All other files in directory Arith are now taking advantage of PeanoNat :
they are now filled with compatibility notations (when earlier lemmas
have exact counterpart in the Nat module) or lemmas with one-line proofs
based on the Nat module. All hints for database "arith" remain declared
in these old-style file (such as Plus.v, Lt.v, etc). All the old-style
files are still Require'd (or not) by Arith.v, just as before.
- Compatibility should be almost complete. For instance in the stdlib,
the only adaptations were due to .ml code referring to some Coq constant
name such as Coq.Init.Peano.pred, which doesn't live well with the
new compatibility notations.
|
|
|
|
- Fix hasheq which didn't have a case for Proj making hashconsing exponentially slower.
Conflicts:
kernel/constr.ml
kernel/univ.ml
proofs/proof_global.ml
|
|
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16557 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15632 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
After discovering a rewrite in Ergo that takes a loooong time due
to a bad interaction with the instances of Permutation and PermutationA :
- PermutationA is now in a separate file SetoidPermutation
- File Permutation.v isn't Require'd by SetoidList anymore
nor MergeSort.v, just the definitions in Sorted.v
- Attempt to put a priority on these instances.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15584 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
One slight point to check someday : fourier used to
launch a tactic called Ring.polynom in some cases.
It it crucial ? If so, how to replace with the setoid_ring
equivalent ?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15524 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
arc tangent and computations of PI approximations
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15436 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Initial contribution by Andrew Appel, many ulterior modifications
by myself.
Interest: red-black trees maintain logarithmic depths as AVL,
but they do not rely on integer height annotations as AVL,
allowing interesting performance when computing in Coq or after
standard extraction. More on this topic in the article by A. Appel.
The common parts of MSetAVL and MSetRBT are shared in a new file
MSetGenTree which include the definition of tree and functions
such as mem fold elements compare subset.
Note that the height of AVL trees is now the first arg of the
Node constructor instead of the last one.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15168 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Made generation of index page fail if a file is missing in list or
listed but unbound in existing theories
- Added a file hidden-files to optionally list library files not to show
in the index page (though it is currently empty)
- Added directory Unicode (why not to have it after all?)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14957 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14955 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14255 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14112 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
probably inadvertantly since it is not reported in the commit log.
(Thanks to Cédric who noticed it.)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13877 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
This library is no longer used anywhere, and its contents is
very... let's say historical... More seriously, many (and presumably
the most useful) stuff that used to be there are in List, now.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13828 85f007b7-540e-0410-9357-904b9bb8a0f7
|
