- 27 Aug, 2019 1 commit
-
-
Michael Sammler authored
-
- 16 Jun, 2019 1 commit
-
-
Robbert Krebbers authored
Used the following script: sed ' s/\bCofeMor/OfeMor/g; s/\-c>/\-d>/g; s/\bcFunctor/oFunctor/g; s/\bCFunctor/OFunctor/g; s/\b\%CF/\%OF/g; s/\bconstCF/constOF/g; s/\bidCF/idOF/g s/\bdiscreteC/discreteO/g; s/\bleibnizC/leibnizO/g; s/\bunitC/unitO/g; s/\bprodC/prodO/g; s/\bsumC/sumO/g; s/\bboolC/boolO/g; s/\bnatC/natO/g; s/\bpositiveC/positiveO/g; s/\bNC/NO/g; s/\bZC/ZO/g; s/\boptionC/optionO/g; s/\blaterC/laterO/g; s/\bofe\_fun/discrete\_fun/g; s/\bdiscrete\_funC/discrete\_funO/g; s/\bofe\_morC/ofe\_morO/g; s/\bsigC/sigO/g; s/\buPredC/uPredO/g; s/\bcsumC/csumO/g; s/\bagreeC/agreeO/g; s/\bauthC/authO/g; s/\bnamespace_mapC/namespace\_mapO/g; s/\bcmra\_ofeC/cmra\_ofeO/g; s/\bucmra\_ofeC/ucmra\_ofeO/g; s/\bexclC/exclO/g; s/\bgmapC/gmapO/g; s/\blistC/listO/g; s/\bvecC/vecO/g; s/\bgsetC/gsetO/g; s/\bgset\_disjC/gset\_disjO/g; s/\bcoPsetC/coPsetO/g; s/\bgmultisetC/gmultisetO/g; s/\bufracC/ufracO/g s/\bfracC/fracO/g; s/\bvalidityC/validityO/g; s/\bbi\_ofeC/bi\_ofeO/g; s/\bsbi\_ofeC/sbi\_ofeO/g; s/\bmonPredC/monPredO/g; s/\bstateC/stateO/g; s/\bvalC/valO/g; s/\bexprC/exprO/g; s/\blocC/locO/g; ' -i $(find theories -name "*.v")
-
- 03 Jun, 2019 1 commit
-
-
Robbert Krebbers authored
This allows one to make use of recursive ghost state obtained from the recursive domain equation solver.
-
- 04 May, 2019 3 commits
-
-
Robbert Krebbers authored
This proof also more easily scales to other recursive types, like trees etc.
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- 05 Mar, 2019 1 commit
-
-
Ralf Jung authored
-
- 10 Dec, 2018 1 commit
-
-
Robbert Krebbers authored
-
- 20 Jun, 2018 1 commit
-
-
Ralf Jung authored
-
- 29 May, 2018 1 commit
-
-
Ralf Jung authored
-
- 20 Feb, 2018 3 commits
-
-
Jacques-Henri Jourdan authored
The finiteness was needed to have the axiom of choice over the domain. This axiom is not needed if cmra_extend is in Type.
-
Jacques-Henri Jourdan authored
Revert "Remove the domain finiteness hypothesis for the function CMRA, and put cmra_extend in Type." This reverts commit fa897ff5.
-
Jacques-Henri Jourdan authored
The finiteness was needed to have the axiom of choice over the domain. This axiom is not needed if cmra_extend is in Type.
-
- 29 Nov, 2017 1 commit
-
-
Robbert Krebbers authored
-
- 25 Oct, 2017 4 commits
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Rename `UCMRA` → `Ucmra` Rename `CMRA` → `Cmra` Rename `OFE` → `Ofe` (`Ofe` was already used partially, but many occurences were missing) Rename `STS` → `Sts` Rename `DRA` → `Dra`
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- 17 Sep, 2017 3 commits
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
For obsolete reasons, that no longer seem to apply, we used ∅ as the unit.
-
Robbert Krebbers authored
-
- 07 Apr, 2017 1 commit
-
-
Jacques-Henri Jourdan authored
-
- 24 Mar, 2017 1 commit
-
-
Robbert Krebbers authored
Instead, I have introduced a type class `Monoid` that is used by the big operators: Class Monoid {M : ofeT} (o : M → M → M) := { monoid_unit : M; monoid_ne : NonExpansive2 o; monoid_assoc : Assoc (≡) o; monoid_comm : Comm (≡) o; monoid_left_id : LeftId (≡) monoid_unit o; monoid_right_id : RightId (≡) monoid_unit o; }. Note that the operation is an argument because we want to have multiple monoids over the same type (for example, on `uPred`s we have monoids for `∗`, `∧`, and `∨`). However, we do bundle the unit because: - If we would not, the unit would appear explicitly in an implicit argument of the big operators, which confuses rewrite. By bundling the unit in the `Monoid` class it is hidden, and hence rewrite won't even see it. - The unit is unique. We could in principle have big ops over setoids instead of OFEs. However, since we do not have a canonical structure for bundled setoids, I did not go that way.
-
- 09 Feb, 2017 1 commit
-
-
Robbert Krebbers authored
-
- 06 Feb, 2017 1 commit
-
-
Ralf Jung authored
-
- 27 Jan, 2017 1 commit
-
-
Ralf Jung authored
-
- 05 Jan, 2017 1 commit
-
-
Ralf Jung authored
-
- 03 Jan, 2017 1 commit
-
-
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
-
- 09 Dec, 2016 2 commits
- 22 Nov, 2016 1 commit
-
-
Ralf Jung authored
Use COFEs only for the recursive domain equation solver
-
- 25 Oct, 2016 1 commit
-
-
Robbert Krebbers authored
-
- 06 Oct, 2016 1 commit
-
-
Robbert Krebbers authored
-
- 28 Sep, 2016 1 commit
-
-
Robbert Krebbers authored
This allows us to factor out properties about connectives that commute with the big operators.
-
- 21 Sep, 2016 2 commits
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- 20 Aug, 2016 1 commit
-
-
Robbert Krebbers authored
This requirement was useful in Iris 2.0: in order to ensure that ownership of the physical state was timeless, we required the ghost CMRA to have a timeless unit. To avoid having additional type class parameters, or having to extend the algebraic hierarchy, we required the units of any CMRA to be timeless. In Iris 3.0, this issue no longer applies: ownership of the physical state is ghost ownership in the global CMRA, whose unit is always timeless. Thanks to Jeehoon Kang for spotting this unnecessary requirement.
-
- 14 Aug, 2016 1 commit
-
-
Robbert Krebbers authored
This is more consistent with the definition of the extension order, which is also defined in terms of an existential.
-
- 08 Aug, 2016 1 commit
-
-
Robbert Krebbers authored
-
- 27 Jul, 2016 1 commit
-
-
Robbert Krebbers authored
This reverts commit 20b4ae55, which does not seem to work with Coq 8.5pl2 (I accidentally tested with 8.5pl1).
-