1. 26 Feb, 2016 2 commits
• Simplify CMRA axioms. · aa947529
Robbert Krebbers authored
```I have simplified the following CMRA axioms:

cmra_unit_preservingN n x y : x ≼{n} y → unit x ≼{n} unit y;
cmra_op_minus n x y : x ≼{n} y → x ⋅ y ⩪ x ≡{n}≡ y;

By dropping off the step-index, so into:

cmra_unit_preservingN x y : x ≼ y → unit x ≼ unit y;
cmra_op_minus x y : x ≼ y → x ⋅ y ⩪ x ≡ y;

The old axioms can be derived.```
2. 25 Feb, 2016 1 commit
3. 24 Feb, 2016 4 commits
4. 20 Feb, 2016 1 commit
5. 18 Feb, 2016 1 commit
6. 17 Feb, 2016 2 commits
• Rename simplify_equality like tactics. · 65ab1289
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.```
• Use scheme - then + then * for bullets. · 685148ab
Robbert Krebbers authored
7. 13 Feb, 2016 2 commits
8. 12 Feb, 2016 1 commit
9. 11 Feb, 2016 2 commits
• Shorter names for common math notions. · 8c96ad4e
Robbert Krebbers authored
`Also do some minor clean up.`
• No longer use option for local updates. · bee413b8
Robbert Krebbers authored
```Instead, I separate it into a total function and a predicate
describe whether the action is allowed or not. This has some

* It is much easier to deal with total functions and predicates
in Coq than with functions into option.
when using a local update you end up with a sensible side
condition as a Coq Prop.
* The definition of local updates (and all CMRA instances) no
longer depend on option.```
10. 10 Feb, 2016 3 commits
11. 05 Feb, 2016 1 commit
12. 04 Feb, 2016 3 commits
13. 03 Feb, 2016 1 commit
14. 02 Feb, 2016 2 commits
15. 01 Feb, 2016 1 commit
• Remove RA from the hierarchy. · b936a5ca
Robbert Krebbers authored
```Instead, we have just a construction to create a CMRA from a RA. This
construction is also slightly generalized, it now works for RAs over any
timeless COFE instead of just the discrete COFE.

Also:
* Put tactics and big_ops for CMRAs in a separate file.
* Valid is now a derived notion (as the limit of validN), so it does not have
to be defined by hand for each CMRA.

Todo:
Make the constructions DRA -> CMRA and RA -> CMRA more uniform.```
16. 19 Jan, 2016 1 commit
17. 18 Jan, 2016 1 commit
18. 16 Jan, 2016 2 commits
19. 15 Jan, 2016 1 commit
20. 14 Jan, 2016 1 commit
21. 13 Jan, 2016 1 commit
22. 15 Dec, 2015 3 commits
23. 11 Dec, 2015 1 commit
24. 23 Nov, 2015 1 commit
25. 22 Nov, 2015 1 commit
• More CMRAs · 5696cb01
Robbert Krebbers authored
```* Framepreserving updates are now on CMRAs rather than RAs
* Excl and auth are now CMRAs
* Show that excl and auth are functors
* STS is now an CMRA```