stdpp:dc7a3a899b9360f610f7e2bbcddd347e11abe5e1 commitshttps://gitlab.mpi-sws.org/iris/stdpp/-/commits/dc7a3a899b9360f610f7e2bbcddd347e11abe5e12017-03-15T15:57:53+01:00https://gitlab.mpi-sws.org/iris/stdpp/-/commit/1dee15b36844f9f467c834d377a4a4f6245c9cb8Remove my name from the copyright headers.2017-03-15T15:57:53+01:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/stdpp/-/commit/a89c6d7899b9f76206248b0e65f2330f87e4d5abBump year in prelude copyright headers.2017-01-31T14:45:56+01:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/stdpp/-/commit/0158faa741d5c74620494c605dcfcce39e6a474dRenaming in prelude/list.2017-01-31T14:45:56+01:00Robbert Krebbersmail@robbertkrebbers.nl
Rename:
- prefix_of -> prefix and suffix_of -> suffix because that saves keystrokes
in lemma names. However, keep the infix notations with l1 `prefix_of` l2 and
l1 `suffix_of` l2 because those are easier to read.
- change the notation l1 `sublist` l2 into l1 `sublist_of` l2 to be consistent.
- rename contains -> submseteq and use the notation ⊆+https://gitlab.mpi-sws.org/iris/stdpp/-/commit/808b681cf102852b0920683685bde10d008fc613more restrictive Proof Using hints in (most files of the) prelude2017-01-31T14:45:56+01:00Ralf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/stdpp/-/commit/47e0f1c490297829c870ab247c184ded47e6718etune "Proof using" directives to minimize differences to previous types of al...2017-01-31T14:45:56+01:00Ralf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/stdpp/-/commit/108d1f8d031ed7eddced2b8808fed6b55aad2d7amake "make quick" quick by adding hints about the used section variables2017-01-31T14:45:56+01:00Ralf Jungjung@mpi-sws.org
This patch was created using
find -name *.v | xargs -L 1 awk -i inplace '{from = 0} /^From/{ from = 1; ever_from = 1} { if (from == 0 && seen == 0 && ever_from == 1) { print "Set Default Proof Using \"Type*\"."; seen = 1 } }1 '
and some minor manual editinghttps://gitlab.mpi-sws.org/iris/stdpp/-/commit/e17f9958c6bce51ac3711ac456d16c3b829b9312Don't use Let outside of a section2016-11-17T15:44:39+01:00Ralf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/stdpp/-/commit/8d7683ba13d55b9c0f6165a7945809be740c6457improve coq 8.6 compatibility2016-11-15T16:56:01+01:00Ralf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/stdpp/-/commit/db08223ada9017975c5989da9d0907186410be47Define shorthand EqDecision A := (∀ x y : A, Decision (x = y)).2016-09-20T10:56:04+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/stdpp/-/commit/9365ea8ba93d571c3b2b06c062540dd767fd1eecGeneralize from_option and define default using it.2016-05-27T11:27:42+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/stdpp/-/commit/db6bf44902379a04a67cd14085fb7080a62f2416Choice principle for finite types.2016-03-11T09:43:29+01:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/stdpp/-/commit/42e3e6def1d2a4649e459d5c4dbae5e94e6fc91cImprove and document split_and tactics.2016-02-19T11:46:27+01:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/stdpp/-/commit/20690605ffbf5709b5760560167e3adf9fa0602bRename simplify_equality like tactics.2016-02-17T16:21:26+01:00Robbert Krebbersmail@robbertkrebbers.nl
simplify_equality => simplify_eq
simplify_equality' => simplify_eq/=
simplify_map_equality => simplify_map_eq
simplify_map_equality' => simplify_map_eq/=
simplify_option_equality => simplify_option_eq
simplify_list_equality => simplify_list_eq
f_equal' => f_equal/=
The /= suffixes (meaning: do simpl) are inspired by ssreflect.https://gitlab.mpi-sws.org/iris/stdpp/-/commit/9774ce9cad21d62660b07ef54ab9abf8909f7fddUse scheme - then + then * for bullets.2016-02-17T01:03:30+01:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/stdpp/-/commit/7dd32d7d13355459a3f3095508bb8b80981241bcUse new Import/Export syntax everywhere.2016-02-13T12:39:54+01:00Robbert Krebbersmail@robbertkrebbers.nl
Also, make our redefinition of done more robust under different
orders of Importing modules.https://gitlab.mpi-sws.org/iris/stdpp/-/commit/44b18f4df008fefa1d9618d6725a63689942552dShorter names for common math notions.2016-02-11T22:48:51+01:00Robbert Krebbersmail@robbertkrebbers.nl
Also do some minor clean up.https://gitlab.mpi-sws.org/iris/stdpp/-/commit/a64b8e398e72096142c2d7fc962bd2140e2aadf3Set Obligation Tactic := idtac globally.2016-01-12T14:35:23+01:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/stdpp/-/commit/f13fcc91aac71f0c8fad557a7450170b264f15f7Inhabited now lives in Type rather than Prop.2015-11-17T18:24:37+01:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/stdpp/-/commit/dcff8ded2b64738c838a552487ae9e4d4630015bUse qualified module names and coqc -Q instead of -R.2015-11-16T11:38:22+01:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/stdpp/-/commit/5a73c4edfb423c4cbead774d288d97cabf71e049Update copyright headers.2015-02-08T19:38:19+01:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/stdpp/-/commit/b2109c25442e833f2bb398259a395a3ef0cb81caSupport function pointers and use a state monad in the frontend.2015-02-08T18:22:07+01:00Robbert Krebbersmail@robbertkrebbers.nl
Important changes in the core semantics:
* Types extended with function types. Since function types are a special kind
of pointer types, types now have an additional mutual part called "ptr_type".
* Pointers extended with function pointers. Theses are just names that refer
to an actual function in the function environment.
* Typing environments extended to assign argument and return types to function
names. Before we used a separate environment for these, but since the
argument and return types are already needed to type function pointers, this
environment would appear in pretty much every typing judgment.
As a side-effect, the frontend has been rewritten entirely. The important
changes are:
* Type checking of expressions is more involved: there is a special kind of
expression type corresponding to a function designator.
* To handle things like block scoped extern function, more state-fullness was
needed. To prepare for future extensions, the entire frontend now uses a
state monad.https://gitlab.mpi-sws.org/iris/stdpp/-/commit/da7a14bb509e8c561eff60fe71d17772233327fbMore accurate formalization of integer ranks.2014-11-15T14:51:12+01:00Robbert Krebbersmail@robbertkrebbers.nl
Integers with the same size, are no longer supposed to have the same rank. As a
result, the C integer types (char, short, int, long, long long) are different
(and thus cannot alias) even if they have the same size. We now have to use a
more involved definition of integer promotions and usual arithmetic conversions.
However, this new definition follows the C standard literally.https://gitlab.mpi-sws.org/iris/stdpp/-/commit/5912f8b1487d1e9547a34e11afbfdd5f465c5ffcLet simplify_equality perform injection less eagerly.2014-09-30T16:17:41-04:00Robbert Krebbersmail@robbertkrebbers.nl
Now it only performs injection on hypotheses of the shape f .. = f ..https://gitlab.mpi-sws.org/iris/stdpp/-/commit/3503a91f8c85b2a01a73ec5fea43cc67ee6c4006Changes in preparation of the C type system and C front-end language2014-06-16T14:49:04+02:00Robbert Krebbersmail@robbertkrebbers.nl
Major changes:
* Make void a base type, and include a proper void base value. This is necessary
because expressions (free, functions without return value) can yield a void.
We now also allow void casts conforming to the C standard.
* Various missing lemmas about typing, weakening, decidability, ...
* The operations "free" and "alloc" now operate on l-values instead of r-values.
This removes some duplication.
* Improve notations of expressions and statements. Change the presence of the
operators conforming to the C standard.
Small changes:
* Use the classes "Typed" and "TypeCheck" for validity of indexes in memory.
This gives more uniform notations.
* New tactic "typed_inversion" performs inversion on an inductive predicate
of type "Typed" and folds the premises.
* Remove a horrible hack in the definitions of the classes "FMap", "MBind",
"OMap", "Alter" that was used to let "simpl" behave better. Instead, we have
defined a tactic "csimpl" that folds the results after performing an
ordinary "simpl".
* Fast operation to remove duplicates from lists using hashsets.
* Make various type constructors (mainly finite map implementations) universe
polymorphic by packing them into an inductive. This way, the whole C syntax
can live in type, avoiding the need for (slow) universe checks.https://gitlab.mpi-sws.org/iris/stdpp/-/commit/d60affc0803db099f40479896f503a0fa1fbc021Preparation to port the master branch2014-06-05T14:15:46+02:00Robbert Krebbersmail@robbertkrebbers.nl
Major changes:
* A data structure to collect locked addresses in memory.
* Operations to lock and unlock addresses.
* Remove [ctree_Forall] and express it using [Forall] and [ctree_flatten]. This
saves a lot of lines of code.
* Add a [void] value. This value cannot be typed, but will be used as a dummy
return value for functions with return type [void].
Minor changes:
* Various deciders in preparation of the executable semantics.
* Improve naming and notations.
* Remove obsolete stuff.https://gitlab.mpi-sws.org/iris/stdpp/-/commit/83f05bf19970b5e75f9e23a80d7229f185b74adeUpdate copyright headers.2014-05-02T22:40:17+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/stdpp/-/commit/6aac4455ce7ba9788152e3dca5409db078474154Prove decidability of quantification over finite types.2013-08-27T10:40:31+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/stdpp/-/commit/5c785a10a18dbaa2cad808174a4cf7919f844433Prove better correspondence between Permutation and contains.2013-08-15T11:08:02+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/stdpp/-/commit/b0f5f6e6b0b33337fdbe7911dac1052a73b67cc1Type classes for finite and countable types.2013-06-17T23:51:28+02:00Robbert Krebbersmail@robbertkrebbers.nl