Commits · 51c4156fbddde439949dd822c2a8d89b58c9e1c5 · Lennard Gäher / Iris

27 May, 2020 3 commits
- update dependencies · 51c4156f
  Ralf Jung authored May 27, 2020
  
  51c4156f
- Merge branch 'lemma-not-instance' into 'master' · f050d84a
  Robbert Krebbers authored May 27, 2020
```
Turn local instances ne_proper and ne_proper_2 into lemmas

See merge request iris/iris!454
```
  f050d84a
- Turn local instances ne_proper and ne_proper_2 into lemmas · 329b8c2c
  Paolo G. Giarrusso authored May 27, 2020
  
  329b8c2c
26 May, 2020 2 commits
- Merge branch 'ralf/heap-lang-rename' into 'master' · d80e7abf
  Ralf Jung authored May 26, 2020
```
rename heap_lang modules

See merge request iris/iris!452
```
  d80e7abf
- fix ex_mapsto fractional handling · e3f87a95
  Ralf Jung authored May 26, 2020
  
  e3f87a95
25 May, 2020 15 commits
- review feedback · 01d2e142
  Ralf Jung authored May 25, 2020
  
  01d2e142
- changelog · 97b9de6c
  Ralf Jung authored May 25, 2020
  
  97b9de6c
- rename heap_lang modules · 5d754755
  Ralf Jung authored May 25, 2020
  
  5d754755
- Merge branch 'robbert/loeb' into 'master' · 7186900b
  Robbert Krebbers authored May 25, 2020
```
Prove different versions of Löb rule

See merge request iris/iris!451
```
  7186900b
- Merge branch 'robbert/inv_combine' into 'master' · a5ffb5e8
  Ralf Jung authored May 25, 2020
```
Add lemma `inv_combine`.

See merge request iris/iris!431
```
  a5ffb5e8
- CHANGELOG entry. · a74ff3bf
  Robbert Krebbers authored May 24, 2020
  
  a74ff3bf
- Add lemma `inv_combine_dup_l`. · 1dc2aecd
  Robbert Krebbers authored May 24, 2020
```
Thanks to @tchajed for the initial version of this proof.
```
  1dc2aecd
- Add lemma `inv_combine`. · ea29f3a0
  Robbert Krebbers authored Apr 21, 2020
  
  ea29f3a0
- Rename `inv_sep` into `env_split`. · 725d4329
  Robbert Krebbers authored May 24, 2020
  
  725d4329
- Merge branch 'ci/ralf/dealloc' into 'master' · e49f76e7
  Ralf Jung authored May 25, 2020
```
heap_lang: support deallocation

Closes #313

See merge request !439
```
  e49f76e7
- Simplify proof of `tac_löb` using new lemma `löb_wand_intuitionistically`. · 016cd820
  Robbert Krebbers authored May 25, 2020
  
  016cd820
- Prove different versions of Löb rule. · 7253dafb
  Robbert Krebbers authored May 25, 2020
  
  7253dafb
- Name a variable in a `destruct`. · d2a0e5d1
  Robbert Krebbers authored May 25, 2020
  
  d2a0e5d1
- Add lemma `intuitionistically_impl_wand_2 P Q : □ (P -∗ Q) ⊢ □ (P → Q)`. · b433bf12
  Robbert Krebbers authored May 25, 2020
```
This lemma is similar to `persistently_impl_wand_2`.
```
  b433bf12
- rename array_tools -> array; update CHANGELOG · b7efc7bd
  Ralf Jung authored May 25, 2020
  
  b7efc7bd
24 May, 2020 7 commits
- Merge branch 'robbert/cleanup' into 'master' · af5e50e7
  Robbert Krebbers authored May 24, 2020
```
Cleanup following the BI and SBI merge

See merge request !449
```
  af5e50e7
- Fine-grained split of `class_instances` based on the structure of the `bi` folder. · cd5f38bf
  Robbert Krebbers authored May 24, 2020
  
  cd5f38bf
- Reorganize `big_op` file to remove `sbi` section. · 7a0ed0f8
  Robbert Krebbers authored May 24, 2020
  
  7a0ed0f8
- Reorganize `coq_tactics` file to remove `sbi` section. · 290363a5
  Robbert Krebbers authored May 24, 2020
  
  290363a5
- Rename `derived_laws_bi` → `derived_laws` and `derived_laws_sbi` → `derived_laws_later`. · 15ce289f
  Robbert Krebbers authored May 24, 2020
  
  15ce289f
- Merge branch 'ci/robbert/merge_sbi_new' into 'master' · 76bec8b7
  Ralf Jung authored May 24, 2020
```
Merge BI and SBI canonical structures

See merge request !441
```
  76bec8b7
- Merge branch 'robbert/done' into 'master' · 9bb018b3
  Robbert Krebbers authored May 24, 2020
```
More documentation of `done` in proof mode docs

See merge request !448
```
  9bb018b3
23 May, 2020 12 commits
- CHANGELOG entry. · dec51a18
  Robbert Krebbers authored May 23, 2020
  
  dec51a18
- Comment for `internal_eq` file. · 5628ac55
  Robbert Krebbers authored May 23, 2020
  
  5628ac55
- Comment about `BiLaterMixin`. · 380e2651
  Robbert Krebbers authored May 23, 2020
  
  380e2651
- Explain axiom `⎡P⎤ ≡ ⎡Q⎤ ⊢@{PROP'} (P ≡ Q)` of embeddings. · d3ab1088
  Robbert Krebbers authored May 23, 2020
  
  d3ab1088
- Add test file for a simple non step-indexed linear separation logic. · 8d9e60ca
  Robbert Krebbers authored May 23, 2020
  
  8d9e60ca
- Remove `Local` that is incompatible with Coq 8.9. · b9390e69
  Robbert Krebbers authored May 14, 2020
  
  b9390e69
- Add smart constructor `BiMixin → BiLaterMixin`. · 799c84b1
  Robbert Krebbers authored May 13, 2020
  
  799c84b1
- Use type class for internal equality. · 45eb1be5
  Robbert Krebbers authored May 13, 2020
  
  45eb1be5
- Comment about `BiLöb`. · abbe9f56
  Robbert Krebbers authored May 12, 2020
  
  abbe9f56
- Tweak error message and test case of `iLöb`. · 39e504e3
  Robbert Krebbers authored May 12, 2020
  
  39e504e3
- Add instances for Löb and contractiveness of later for monPred. · 6c1297e7
  Robbert Krebbers authored Apr 21, 2020
  
  6c1297e7
- Merge sbi canonical structure into the bi canonical structure. · cfac1295
  Robbert Krebbers authored Apr 20, 2020
  
  cfac1295
22 May, 2020 1 commit
- clarify comment · 218d8b33
  Ralf Jung authored May 22, 2020
  
  218d8b33