Commits · robbert/plausibly · Lennard Gäher / Iris

27 Oct, 2018 4 commits
- Show that bupd entails plausibly. · 3e4b87c2
  Robbert Krebbers authored Oct 27, 2018
  
  3e4b87c2
- The plausibly modality. · 5b084890
  Robbert Krebbers authored Oct 27, 2018
```
Much of this is based on https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/184#note_31510
by Amin Timany, but made to work for non-affine BIs and changed in
a way that it follows the Iris naming conventions.
```
  5b084890
- Some missing parameters. · 1f796221
  Robbert Krebbers authored Oct 27, 2018
  
  1f796221
- Some useful BI derived lemmas. · 625d60c3
  Robbert Krebbers authored Oct 27, 2018
  
  625d60c3
26 Oct, 2018 5 commits
- Remove spurious type annotations (there is a `Implicit Type` here). · ea07fcbc
  Robbert Krebbers authored Oct 26, 2018
  
  ea07fcbc
- Close issue #218. · 2e76d24c
  Robbert Krebbers authored Oct 26, 2018
  
  2e76d24c
- For the timing jobs, build our own ocaml · 8fd4b0ac
  Ralf Jung authored Oct 26, 2018
```
opam is broken beyond repair for system ocaml, it seems... see
<https://github.com/ocaml/opam/issues/3586>.
```
  8fd4b0ac
- Prove `E2 ⊆ E1 → P ={E1,E2}=∗ P`. · c148ac4d
  Robbert Krebbers authored Oct 26, 2018
  
  c148ac4d
- Notation `P ={E1,E2}▷=∗^n Q`. · b33a29de
  Robbert Krebbers authored Oct 26, 2018
  
  b33a29de
24 Oct, 2018 10 commits
- A comment explaining the `invG` submodule. · 66483b1d
  Robbert Krebbers authored Oct 25, 2018
  
  66483b1d
- Prove `(|==> ∀ x, Φ x) ⊣⊢ (∀ x, |==> Φ x)` for plain `Φ`. · b58adc74
  Robbert Krebbers authored Oct 24, 2018
  
  b58adc74
- Use new `|={E,E'}▷=>^n` notation at more places. · 44dc86c8
  Robbert Krebbers authored Oct 24, 2018
  
  44dc86c8
- Tweak a proof. · 97b304a0
  Robbert Krebbers authored Oct 24, 2018
  
  97b304a0
- Proper pretty printing of new `|={E,E'}▷=>^n` notation. · 00d7fbc1
  Robbert Krebbers authored Oct 24, 2018
  
  00d7fbc1
- Merge branch 'joe/fupd_adequacy' into 'master' · 82d7488b
  Robbert Krebbers authored Oct 24, 2018
```
Modify adequacy proof to not break the 'fancy update' abstraction.

See merge request FP/iris-coq!171
```
  82d7488b
- Use explicit names in some scripts, re-organize fupd plainly derived laws,... · 7ccbb8cd
  Joseph Tassarotti authored Oct 24, 2018
```
Use explicit names in some scripts, re-organize fupd plainly derived laws, adjust wsat import/export.
```
  7ccbb8cd
- Use plainly modality instead of typeclass in BiFUpdPlainly interface. · 334b689e
  Joseph Tassarotti authored Oct 20, 2018
  
  334b689e
- Modify adequacy proof to not break the 'fancy update' abstraction. Modify fupd... · 7c32c1ac
  Joseph Tassarotti authored Aug 13, 2018
```
Modify adequacy proof to not break the 'fancy update' abstraction. Modify fupd plainly interface and add new derived results.
```
  7c32c1ac
- Coq 8.9 is no longer broken · 1d34bda8
  Ralf Jung authored Oct 24, 2018
  
  1d34bda8
22 Oct, 2018 6 commits
- start testing with Coq 8.9 · 4842a060
  Ralf Jung authored Oct 22, 2018
  
  4842a060
- get rid of observations in ownP, they just make porting harder · 46e20e91
  Ralf Jung authored Oct 22, 2018
  
  46e20e91
- Remove spurious import. · 0acafd48
  Robbert Krebbers authored Oct 22, 2018
  
  0acafd48
- Replace more occurences of /\ by unicode ∧. · 3e21a838
  Robbert Krebbers authored Oct 22, 2018
  
  3e21a838
- Add type annotation. · bba7474e
  Robbert Krebbers authored Oct 22, 2018
  
  bba7474e
- Use unicide ∧ and ∃. · 49b5dd50
  Robbert Krebbers authored Oct 21, 2018
  
  49b5dd50
21 Oct, 2018 1 commit
- Add missing type in a signature. · f1f34470
  Robbert Krebbers authored Oct 21, 2018
  
  f1f34470
19 Oct, 2018 1 commit
- fix compatibility with Coq 8.7 · f238c358
  Ralf Jung authored Oct 19, 2018
  
  f238c358
18 Oct, 2018 9 commits
- Merge branch 'ralf/prophecy' into 'master' · e16140cf
  Ralf Jung authored Oct 18, 2018
```
Prophecy variables

See merge request FP/iris-coq!173
```
  e16140cf
- note some FIXMEs · 4d57af6b
  Ralf Jung authored Oct 18, 2018
  
  4d57af6b
- more nits · 41aaefe0
  Ralf Jung authored Oct 18, 2018
  
  41aaefe0
- use 'proph' instead of a notation, and rename type of prophecy variables to proph_id · 734bc0ab
  Ralf Jung authored Oct 18, 2018
  
  734bc0ab
- more nits · cc712c90
  Ralf Jung authored Oct 18, 2018
  
  cc712c90
- generalize to lists of observations per program step · 25ed5c9c
  Ralf Jung authored Oct 18, 2018
  
  25ed5c9c
- fix nits · fc59d6d0
  Ralf Jung authored Oct 18, 2018
  
  fc59d6d0
- use record for heap_lang state · 7fa7361b
  Ralf Jung authored Oct 18, 2018
  
  7fa7361b
- Merge remote-tracking branch 'origin/master' into ralf/prophecy · c91b93ac
  Ralf Jung authored Oct 18, 2018
  
  c91b93ac
13 Oct, 2018 1 commit
- `(P → Q) ⊣⊢ ∃ R, R ∧ <pers> (P ∧ R -∗ Q)` holds for general BIs. · 7041c043
  Robbert Krebbers authored Oct 13, 2018
  
  7041c043
11 Oct, 2018 1 commit
- fix typo · f426901d
  Ralf Jung authored Oct 11, 2018
  
  f426901d
07 Oct, 2018 1 commit
- test and support Coq 8.8.2 · 0f8ddc80
  Ralf Jung authored Oct 07, 2018
  
  0f8ddc80
05 Oct, 2018 1 commit
- Merge branch 'robbert/pure_exec_nsteps' into 'master' · 464c2449
  Robbert Krebbers authored Oct 05, 2018
```
Support multiple steps in `PureExec`.

See merge request FP/iris-coq!179
```
  464c2449