 21 Nov, 2019 1 commit


Paolo G. Giarrusso authored
 Ensure gmap wellformedness proofs are fully opaque.  Use patternmatching lambdas over lets.

 19 Sep, 2019 1 commit


Robbert Krebbers authored
For example, change `(!! i)` into `(.!! x)` so that `!!` can also be used as a prefix, as done in VST for example. This closes issue #42. I have used the `sed` script below. This script took care of nearly all uses apart from a few occurrences where a space was missing, e.g. `(,foo)`. In this case, `coqc` will just fail, allowing one to patch up things manually. The script is slightly too eager on Iris developments, where it also replaces `($ ...)` introduction patterns. When porting Iris developments you thus may want to remove the line for `$`. ``` sed ' s/(= /(.= /g; s/ =)/ =.)/g; s/(≠ /(.≠ /g; s/ ≠)/ ≠.)/g; s/(≡ /(.≡ /g; s/ ≡)/ ≡.)/g; s/(≢ /(.≢ /g; s/ ≢)/ ≢.)/g; s/(∧ /(.∧ /g; s/ ∧)/ ∧.)/g; s/(∨ /(.∨ /g; s/ ∨)/ ∨.)/g; s/(
↔ /(.↔ /g; s/↔ )/↔ .)/g; s/(→ /(.→ /g; s/ →)/ →.)/g; s/($ /(.$ /g; s/(∘ /(.∘ /g; s/ ∘)/ ∘.)/g; s/(, /(., /g; s/ ,)/ ,.)/g; s/(∘ /(.∘ /g; s/ ∘)/ ∘.)/g; s/(∪ /(.∪ /g; s/ ∪)/ ∪.)/g; s/(⊎ /(.⊎ /g; s/ ⊎)/ ⊎.)/g; s/(∩ /(.∩ /g; s/ ∩)/ ∩.)/g; s/(∖ /(.∖ /g; s/ ∖)/ ∖.)/g; s/(⊆ /(.⊆ /g; s/ ⊆)/ ⊆.)/g; s/(⊈ /(.⊈ /g; s/ ⊈)/ ⊈.)/g; s/(⊂ /(.⊂ /g; s/ ⊂)/ ⊂.)/g; s/(⊄ /(.⊄ /g; s/ ⊄)/ ⊄.)/g; s/(∈ /(.∈ /g; s/ ∈)/ ∈.)/g; s/(∉ /(.∉ /g; s/ ∉)/ ∉.)/g; s/(≫= /(.≫= /g; s/ ≫=)/ ≫=.)/g; s/(!! /(.!! /g; s/ !!)/ !!.)/g; s/(⊑ /(.⊑ /g; s/ ⊑)/ ⊑.)/g; s/(⊓ /(.⊓ /g; s/ ⊓)/ ⊓.)/g; s/(⊔ /(.⊔ /g; s/ ⊔)/ ⊔.)/g; s/(:: /(.:: /g; s/ ::)/ ::.)/g; s/(++ /(.++ /g; s/ ++)/ ++.)/g; s/(≡ₚ /(.≡ₚ /g; s/ ≡ₚ)/ ≡ₚ.)/g; s/(≢ₚ /(.≢ₚ /g; s/ ≢ₚ)/ ≢ₚ.)/g; s/(::: /(.::: /g; s/ :::)/ :::.)/g; s/(+++ /(.+++ /g; s/ +++)/ +++.)/g; ' i $(find name "*.v") ```

 14 Aug, 2019 1 commit


Paulo Emílio de Vilhena authored

 25 Apr, 2019 1 commit


 24 Apr, 2019 1 commit


Robbert Krebbers authored
This closes issue #25.

 14 Mar, 2019 1 commit


Robbert Krebbers authored

 03 Mar, 2019 1 commit


Robbert Krebbers authored
 The class `Infinite A` is now defined as having a function `fresh : list A → A`, that given a list `xs`, gives an element `x ∉ xs`.  For most types this `fresh` function has a sensible computable behavior, for example: + For numbers, it yields one added to the maximal element in `xs`. + For strings, it yields the first string representation of a number that is not in `xs`.  For any type `C` of finite sets with elements of infinite type `A`, we lift the fresh function to `C → A`. As a consequence:  It is now possible to pick fresh elements from _any_ finite set and from _any_ list with elements of an infinite type. Before it was only possible for specific finite sets, e.g. `gset`, `pset`, ...  It makes the code more uniform. There was a lot of overlap between having a `Fresh` and an `Infinite` instance. This got unified.

 20 Feb, 2019 2 commits


Robbert Krebbers authored
 Rename `gmap.to_gmap` into `gset_to_gmap`.  Rename `gmap.of_gset` into `gset_to_propset`.  Rename `coPset.to_Pset` into `coPset_to_Pset`.  Rename `coPset.of_Pset` into `coPset_to_gset`.  Rename `coPset.to_gset` into `coPset_to_gset`.  Rename `coPset.of_gset` into `gset_to_coPset`. The following `sed` script can be used for the first rename: ``` sed i 's/to\_gmap/gset\_to\_gmap/g' $(find ./theories name \*.v) ``` The latter is context sensitive, so was done manually.

Robbert Krebbers authored
Get rid of using `Collection` and favor `set` everywhere. Also, prefer conversion functions that are called `X_to_Y`. The following sed script performs most of the renaming, with the exception of:  `set`, which has been renamed into `propset`. I couldn't do this rename using `sed` since it's too context sensitive.  There was a spurious rename of `Vec.of_list`, which I correctly manually.  Updating some section names and comments. ``` sed ' s/SimpleCollection/SemiSet/g; s/FinCollection/FinSet/g; s/CollectionMonad/MonadSet/g; s/Collection/Set\_/g; s/collection\_simple/set\_semi\_set/g; s/fin\_collection/fin\_set/g; s/collection\_monad\_simple/monad\_set\_semi\_set/g; s/collection\_equiv/set\_equiv/g; s/\bbset/boolset/g; s/mkBSet/BoolSet/g; s/mkSet/PropSet/g; s/set\_equivalence/set\_equiv\_equivalence/g; s/collection\_subseteq/set\_subseteq/g; s/collection\_disjoint/set\_disjoint/g; s/collection\_fold/set\_fold/g; s/collection\_map/set\_map/g; s/collection\_size/set\_size/g; s/collection\_filter/set\_filter/g; s/collection\_guard/set\_guard/g; s/collection\_choose/set\_choose/g; s/collection\_ind/set\_ind/g; s/collection\_wf/set\_wf/g; s/map\_to\_collection/map\_to\_set/g; s/map\_of\_collection/set\_to\_map/g; s/map\_of\_list/list\_to\_map/g; s/map\_of\_to_list/list\_to\_map\_to\_list/g; s/map\_to\_of\_list/map\_to\_list\_to\_map/g; s/\bof\_list/list\_to\_set/g; s/\bof\_option/option\_to\_set/g; s/elem\_of\_of\_list/elem\_of\_list\_to\_set/g; s/elem\_of\_of\_option/elem\_of\_option\_to\_set/g; s/collection\_not\_subset\_inv/set\_not\_subset\_inv/g; s/seq\_set/set\_seq/g; s/collections/sets/g; s/collection/set/g; ' i $(find name "*.v") ```

 06 Feb, 2019 1 commit


Robbert Krebbers authored

 29 Jan, 2019 1 commit


Robbert Krebbers authored

 28 May, 2018 1 commit


Ralf Jung authored

 27 Oct, 2017 2 commits


Robbert Krebbers authored

Robbert Krebbers authored

 20 Oct, 2017 1 commit


Hai Dang authored

 16 Oct, 2017 1 commit


JacquesHenri Jourdan authored

 29 Sep, 2017 3 commits
 17 Sep, 2017 1 commit


Robbert Krebbers authored
This provides significant robustness against looping type class search. As a consequence, at many places throughout the library we had to add additional typing information to lemmas. This was to be expected, since most of the old lemmas were ambiguous. For example: Section fin_collection. Context `{FinCollection A C}. size_singleton (x : A) : size {[ x ]} = 1. In this case, the lemma does not tell us which `FinCollection` with elements `A` we are talking about. So, `{[ x ]}` could not only refer to the singleton operation of the `FinCollection A C` in the section, but also to any other `FinCollection` in the development. To make this lemma unambigious, it should be written as: Lemma size_singleton (x : A) : size ({[ x ]} : C) = 1. In similar spirit, lemmas like the one below were also ambiguous: Lemma lookup_alter_None {A} (f : A → A) m i j : alter f i m !! j = None
↔ m !! j = None. It is not clear which finite map implementation we are talking about. To make this lemma unambigious, it should be written as: Lemma lookup_alter_None {A} (f : A → A) (m : M A) i j : alter f i m !! j = None↔ m !! j = None. That is, we have to specify the type of `m`.

 08 Sep, 2017 1 commit


Robbert Krebbers authored
See also Coq bug #5712.

 15 Mar, 2017 1 commit


Robbert Krebbers authored

 07 Feb, 2017 1 commit


Robbert Krebbers authored

 31 Jan, 2017 4 commits


Robbert Krebbers authored

Robbert Krebbers authored

Ralf Jung authored

Ralf Jung authored
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 editing

 21 Nov, 2016 1 commit


Robbert Krebbers authored

 20 Nov, 2016 1 commit


Robbert Krebbers authored

 15 Nov, 2016 1 commit


Robbert Krebbers authored
(These instances are not defined for any FinMap to avoid overlapping instances for EqDecision, which may have awkward consequences for type class search).

 20 Sep, 2016 1 commit


Robbert Krebbers authored

 29 Aug, 2016 1 commit


Robbert Krebbers authored
This happened for example in <[i:=x]>∅, where simpl unfold insert (despite it being declared simpl never) because ∅ reduces to a constructor.

 27 Jul, 2016 2 commits


Robbert Krebbers authored
This reverts commit 20b4ae55bdf00edb751ccdab3eb876cb9b13c99f, which does not seem to work with Coq 8.5pl2 (I accidentally tested with 8.5pl1).

Robbert Krebbers authored
This makes type checking more directed, and somewhat more predictable. On the downside, it makes it impossible to declare the singleton on lists as an instance of SingletonM and the insert and alter operations on functions as instances of Alter and Insert. However, these were not used often anyway.

 22 Jul, 2016 1 commit


Robbert Krebbers authored
Similar files (gmap, listset, ...) were already in singular form and matched the name of the set/map data type.

 29 Mar, 2016 1 commit


Robbert Krebbers authored

 17 Feb, 2016 2 commits


Robbert Krebbers authored
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.

Robbert Krebbers authored

 16 Feb, 2016 1 commit


Robbert Krebbers authored

 13 Feb, 2016 1 commit


Robbert Krebbers authored
Also, make our redefinition of done more robust under different orders of Importing modules.
