 03 Mar, 2019 40 commits


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 40 commits


Robbert Krebbers authored

Robbert Krebbers authored

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") ```

 29 Jan, 2019 40 commits


Robbert Krebbers authored

 04 Oct, 2018 40 commits


Robbert Krebbers authored
This makes some proress on #21. Still, the question remains if a more generic solution exists.

 05 Apr, 2018 40 commits


Robbert Krebbers authored

Robbert Krebbers authored

 27 Mar, 2018 40 commits


Robbert Krebbers authored

 01 Nov, 2017 40 commits


Johannes Kloos authored
Also make the instances nonglobal, to prevent multiple instance problems.

Johannes Kloos authored

Johannes Kloos authored
This implements a simple linear search for fresh elements.

 27 Oct, 2017 40 commits


JacquesHenri Jourdan authored

 21 Sep, 2017 40 commits


Robbert Krebbers authored
This allows for more control over `Hint Mode`.

 17 Sep, 2017 40 commits


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`.

 15 Mar, 2017 40 commits


Robbert Krebbers authored

 31 Jan, 2017 40 commits


Robbert Krebbers authored
This fixes issue #65.

Robbert Krebbers authored

Robbert Krebbers authored
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 ⊆+

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

 23 Nov, 2016 40 commits


Robbert Krebbers authored

 22 Nov, 2016 40 commits


Robbert Krebbers authored

 21 Nov, 2016 40 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

 20 Nov, 2016 40 commits


Robbert Krebbers authored

 28 Sep, 2016 40 commits


Robbert Krebbers authored

 27 Sep, 2016 40 commits


Robbert Krebbers authored

 22 Jul, 2016 40 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
These just make things more complicated, it would be more useful to declare (efficient) decision procedures for each instance, so that we can properly predict which instance we will get.

 23 Mar, 2016 40 commits


Robbert Krebbers authored

 17 Feb, 2016 40 commits


Robbert Krebbers authored
It is doing much more than just dealing with ∈, it solves all kinds of goals involving set operations (including ≡ and ⊆).

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

Robbert Krebbers authored

 13 Feb, 2016 40 commits


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

 11 Feb, 2016 40 commits


Robbert Krebbers authored
Also do some minor clean up.

 16 Jan, 2016 40 commits


Robbert Krebbers authored
This one (previously solve_elem_of) was hardly used. The tactic that uses naive_solver (previously esolve_elem_of, now solve_elem_of) has been extended with flags to say which hypotheses should be cleared/kept.

 12 Jan, 2016 40 commits


Robbert Krebbers authored
