1. 03 Mar, 2019 1 commit
    • Robbert Krebbers's avatar
      Overhaul of the `Infinite`/`Fresh` infrastructure. · 3184ef61
      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.
      3184ef61
  2. 20 Feb, 2019 1 commit
    • Robbert Krebbers's avatar
      Consistently use `set` and `map` names. · b7e31ce2
      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")
      ```
      b7e31ce2
  3. 29 Jan, 2019 1 commit
  4. 28 Nov, 2018 1 commit
  5. 24 May, 2018 1 commit
    • Ralf Jung's avatar
      Remove the `default` notation for options · e585be6d
      Ralf Jung authored
      The notation was parsing-only and all it did was reorder the arguments for
      from_option.  This creates just a needless divergence between what is written
      and what is printed.  Also, removing it frees the name for maybe introducing a
      function or notation `default` with a type like `T -> option T -> T`.
      e585be6d
  6. 05 Apr, 2018 1 commit
  7. 08 Sep, 2017 1 commit
  8. 15 Mar, 2017 1 commit
  9. 31 Jan, 2017 3 commits
  10. 15 Nov, 2016 1 commit
  11. 20 Sep, 2016 1 commit
  12. 27 Jul, 2016 2 commits
  13. 17 Feb, 2016 2 commits
  14. 13 Feb, 2016 1 commit
  15. 11 Feb, 2016 1 commit
  16. 18 Nov, 2015 2 commits
  17. 16 Nov, 2015 1 commit
  18. 11 Nov, 2015 1 commit
  19. 01 Feb, 2017 1 commit
    • Robbert Krebbers's avatar
      Port to Coq 8.5 beta 2. · 02f213ce
      Robbert Krebbers authored
      The port makes the following notable changes:
      
      * The carrier types of separation algebras and integer environments are no
        longer in Set. Now they have a type at a fixed type level above Set. This
        both works better in 8.5 and makes the formalization more general.
        I have tried putting them at polymorphic type levels, but that increased the
        compilation time by an order of magnitude.
      * I am using a custom f_equal tactic written in Ltac to circumvent bug #4069.
        That bug has been fixed, so this custom tactic can be removed when the next
        beta of 8.5 is out.
      02f213ce
  20. 21 May, 2015 1 commit
  21. 08 Feb, 2015 1 commit
  22. 16 Jun, 2014 1 commit
    • Robbert Krebbers's avatar
      Changes in preparation of the C type system and C front-end language · 3503a91f
      Robbert Krebbers authored
      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.
      3503a91f
  23. 02 May, 2014 2 commits
  24. 14 Aug, 2013 1 commit
  25. 12 Aug, 2013 1 commit
    • Robbert Krebbers's avatar
      Finite maps and sets using ordered association lists. · bc659ba4
      Robbert Krebbers authored
      This commit includes the following changes:
      * More theorems about pre-, partial and total orders.
      * Define the lexicographic order on various commonly used data types.
      * Mergesort and its correctness proof.
      * Implement finite maps and sets using ordered association lists.
      bc659ba4
  26. 07 May, 2013 1 commit
    • Robbert Krebbers's avatar
      Lots of refactoring. and new results on permutations and list containment. · 361308c7
      Robbert Krebbers authored
      The refactoring includes:
      * Use infix notations for the various list relations
      * More consistent naming
      * Put lemmas on one line whenever possible
      * Change proofs into one-liners when possible
      * Make better use of the "Implicit Types" command
      * Improve the order of the list module by placing all definitions at the start,
        then the proofs, and finally the tactics.
      
      Besides, there is some new machinery for proofs by reflection on lists. It is
      used for a decision procedure for permutations and list containment.
      361308c7
  27. 22 Feb, 2013 1 commit
  28. 19 Feb, 2013 1 commit
    • Robbert Krebbers's avatar
      Support sequence point, add permissions, and update prelude. · 415a4f1c
      Robbert Krebbers authored
      Both the operational and axiomatic semantics are extended with sequence points
      and a permission system based on fractional permissions. In order to achieve
      this, the memory model has been completely revised, and is now built on top
      of an abstract interface for permissions.
      
      Apart from these changed, the library on lists and sets has been heavily
      extended, and minor changed have been made to other parts of the prelude.
      415a4f1c
  29. 09 Jan, 2013 1 commit
  30. 05 Jan, 2013 1 commit
    • Robbert Krebbers's avatar
      Various small changes. · 507a150a
      Robbert Krebbers authored
      * Define the standard strict order on pre orders.
      * Prove that this strict order is well founded for finite sets and finite maps.
        We also provide some utilities to compute with well founded recursion.
      * Improve the "simplify_option_equality" tactic to handle more cases.
      * Axiomatize finiteness of finite maps by translation to lists, instead of by
        them having a finite domain.
      * Prove many additional properties of finite maps.
      * Add many functions and theorems on lists, including: permutations, resize,
        filter, ...
      507a150a
  31. 12 Nov, 2012 1 commit
    • Robbert Krebbers's avatar
      Many relatively small changes. · 50dfc148
      Robbert Krebbers authored
      Most interestingly:
      * Use [lia] instead of [omega] everywhere
      * More many generic lemmas on the memory to the theory on finite maps.
      * Many additional list lemmas.
      * A new interface for a monad for collections, which is now also used by the
        collection tactics.
      * Provide an additional finite collection implementation using unordered lists
        without duplicates removed. This implementation forms a monad (just the list
        monad in disguise).
      50dfc148
  32. 19 Oct, 2012 1 commit
    • Robbert Krebbers's avatar
      Add non-deterministic expressions with side-effects. · e82cda6c
      Robbert Krebbers authored
      The following things have been changed in this revision:
      
      * We now give a small step semantics for expressions. The denotational semantics
        only works for side-effect free expressions.
      * Dynamically allocated memory through alloc and free is now supported.
      * The following expressions are added: assignment, function call, unary
        operators, conditional, alloc, and free.
      * Some customary induction schemes for expressions are proven.
      * The axiomatic semantics (and its interpretation) have been changed in order
        to deal with non-deterministic expressions.
      * We have added inversion schemes based on small inversions for the operational
        semantics. Inversions using these schemes are much faster.
      * We improved the statement preservation proof of the operational semantics.
      * We now use a variant of SsReflect's [by] and [done], instead of Coq's [now]
        and [easy]. The [done] tactic is much faster as it does not perform
        inversions.
      * Add theory, definitions and notations on vectors.
      * Separate theory on contexts.
      * Change [Arguments] declarations to ensure better unfolding.
      e82cda6c
  33. 04 Sep, 2012 1 commit
  34. 29 Aug, 2012 1 commit