Commits · master · Jonas Kastberg / stdpp

14 Jan, 2022 13 commits
- Merge branch 'robbert/app_cons_eq_inv_lr' into 'master' · f71300ea
  Robbert Krebbers authored Jan 14, 2022
```
Add lemmas `app_cons_eq_inv_{l,r}`.

See merge request !363
```
  f71300ea
- Add lemmas `app_cons_eq_inv_{l,r}`. · 59468247
  Robbert Krebbers authored Jan 14, 2022
  
  59468247
- Move `reverse` lemmas above `elem_of` ones. · 0e155310
  Robbert Krebbers authored Jan 14, 2022
  
  0e155310
- Move `elem_of_suffix` to other suffix lemmas. · 74d21e01
  Robbert Krebbers authored Jan 14, 2022
  
  74d21e01
- Merge branch 'last_lemma' into 'master' · e58dd720
  Robbert Krebbers authored Jan 14, 2022
```
Add `last_cons_Some_ne` lemma for the `last` function

See merge request iris/stdpp!361
```
  e58dd720
- Add `last_cons_Some_ne` lemma for the `last` function · b66b5311
  Jonas Kastberg authored Jan 14, 2022 and Robbert Krebbers committed Jan 14, 2022
  
  b66b5311
- Merge branch 'list_subseteq_lemmas' into 'master' · 9f6f8c38
  Robbert Krebbers authored Jan 14, 2022
```
Added some useful lemmas about [list_subseteq]

See merge request iris/stdpp!359
```
  9f6f8c38
- Merge branch 'pr-13969-take3' into 'master' · ac02dbbd
  Robbert Krebbers authored Jan 14, 2022
```
Set the priority of the rewrite relation for sqsubseteq to not take precedence over...

See merge request iris/stdpp!362
```
  ac02dbbd
- Apply 1 suggestion(s) to 1 file(s) · 03bdbb8d
  Robbert Krebbers authored Jan 14, 2022
  
  03bdbb8d
- Apply 2 suggestion(s) to 1 file(s) · 0eb7c546
  Robbert Krebbers authored Jan 14, 2022
  
  0eb7c546
- Merge branch 'filter_lemmas' into 'master' · ff11f3b2
  Robbert Krebbers authored Jan 14, 2022
```
Add lemmas about empty `filter` on list, map, and set

See merge request iris/stdpp!358
```
  ff11f3b2
- Leave more room for priorities between equiv and sqsubseteq · 4dd6ec09
  Matthieu Sozeau authored Jan 14, 2022
  
  4dd6ec09
- Fix sqsubseteq_rewrite's priority, making it lower than equiv · 36bc5009
  Matthieu Sozeau authored Jan 14, 2022
  
  36bc5009
13 Jan, 2022 2 commits
- Merge branch 'pr-13969-take2' into 'master' · 607ee2b1
  Robbert Krebbers authored Jan 13, 2022
```
Set the priority of the rewrite relation for equiv to not take precedence over...

See merge request iris/stdpp!360
```
  607ee2b1
- Set the priority of the rewrite relation for equiv to not take precedence over... · 00daaf86
  Matthieu Sozeau authored Jan 13, 2022 and Robbert Krebbers committed Jan 13, 2022
  
  00daaf86
12 Jan, 2022 9 commits
- Renamed lemmas to be more consistent with existing ones · 1633b3dd
  Jonas Kastberg authored Jan 12, 2022
  
  1633b3dd
- Added some useful lemmas about [list_subseteq] · 80bc3965
  Jonas Kastberg authored Jan 12, 2022
  
  80bc3965
- Add similar filter lemmas for maps and sets. · 0e3ba050
  Robbert Krebbers authored Jan 12, 2022
  
  0e3ba050
- Shorten proof and make lemma name consistent. · 34945717
  Robbert Krebbers authored Jan 12, 2022
  
  34945717
- Merge branch 'elem_of_prefix' into 'master' · f23a05c3
  Robbert Krebbers authored Jan 12, 2022
```
Add lemmas `elem_of_prefix` and `elem_of_suffix`

See merge request iris/stdpp!354
```
  f23a05c3
- Add lemmas `elem_of_prefix` and `elem_of_suffix` · 2381ee32
  Jonas Kastberg authored Jan 12, 2022 and Robbert Krebbers committed Jan 12, 2022
  
  2381ee32
- Merge branch 'last_lemmas' into 'master' · 50117aa6
  Robbert Krebbers authored Jan 12, 2022
```
Added some useful lemmas for the [last] function

See merge request iris/stdpp!355
```
  50117aa6
- Added some useful lemmas for the [last] function · e921d245
  Jonas Kastberg authored Jan 12, 2022 and Robbert Krebbers committed Jan 12, 2022
  
  e921d245
- Added a useful lemma about [filter] on list · a727a797
  Jonas Kastberg authored Jan 12, 2022
  
  a727a797
11 Jan, 2022 2 commits
- Merge branch 'coq-13969' into 'master' · 2af35753
  Robbert Krebbers authored Jan 11, 2022
```
Declare `equiv` as a rightful rewrite relation, when an `Equiv` instance is available.

See merge request iris/stdpp!273
```
  2af35753
- Declare `equiv` as a rightful rewrite relation, when an `Equiv` instance is available. · 309a7a57
  Matthieu Sozeau authored Jan 11, 2022 and Robbert Krebbers committed Jan 11, 2022
  
  309a7a57
22 Dec, 2021 1 commit
- Merge branch 'glen/pred_finite' into 'master' · b593cbdd
  Robbert Krebbers authored Dec 22, 2021
```
add some lemmas about `Finite` and `pred_finite`

See merge request iris/stdpp!351
```
  b593cbdd
21 Dec, 2021 7 commits
- add comment about Qed/Defined for `finite_sig_dec` · 6dcccf06
  Glen Mével authored Dec 21, 2021
  
  6dcccf06
- simplify proof of `finite_sig_dec`, remove lemmas about `pred_finite_alt` · 1d70662e
  Glen Mével authored Dec 15, 2021
  
  1d70662e
- comment about `dec_pred_finite_alt` and prove related lemmas · 66c1acb6
  Glen Mével authored Dec 13, 2021
```
Also, rename `dec_pred_finite{,_set}` to `dec_pred_finite{,_set}_alt`.
```
  66c1acb6
- remove lemma `finite_dec` · 79830523
  Glen Mével authored Dec 13, 2021
  
  79830523
- shorten the proof of `dec_pred_finite` · 10d52cfd
  Robbert Krebbers authored Dec 13, 2021 and Glen Mével committed Dec 21, 2021
  
  10d52cfd
- clean some statements and improve formatting of one proof · 5ce93607
  Robbert Krebbers authored Dec 13, 2021 and Glen Mével committed Dec 21, 2021
  
  5ce93607
- add some lemmas about `Finite` and `pred_finite` · e3415663
  Glen Mével authored Dec 12, 2021
  
  e3415663
16 Dec, 2021 4 commits
- Merge branch 'robbert/destruct_select' into 'master' · cf7c2c41
  Robbert Krebbers authored Dec 16, 2021
```
Add tactics `destruct select <pat>` and `destruct select <pat> as <intro_pat>`.

See merge request iris/stdpp!352
```
  cf7c2c41
- CHANGELOG. · 924782c8
  Robbert Krebbers authored Dec 16, 2021
  
  924782c8
- Add test for `destruct select`. · 723ad25f
  Robbert Krebbers authored Dec 16, 2021
  
  723ad25f
- Add tactics `destruct select`. · a1272450
  Robbert Krebbers authored Dec 16, 2021
  
  a1272450
13 Dec, 2021 2 commits
- Merge branch 'ralf/no-global' into 'master' · d9e55d3d
  Robbert Krebbers authored Dec 13, 2021
```
remove a Global Arguments Pos.of_nat from the middle of a proof

See merge request iris/stdpp!350
```
  d9e55d3d
- remove a Global Arguments Pos.of_nat from the middle of a proof · df9b4add
  Ralf Jung authored Dec 12, 2021
  
  df9b4add