Commits · 0b4a2a55c825b2fa55b9c783d659e9b7347448b2 · Iris / stdpp

Jan 20, 2021
- remove unused find_pat tactic · 00e29c8b
  Ralf Jung authored 4 years ago
  
  00e29c8b
- add rename-by-pattern tactic · 609de3aa
  Ralf Jung authored 4 years ago
  
  609de3aa
Jan 19, 2021
- Remove hint db and import of omega, since omega will be removed from Coq. · 1c2e6891
  Robbert Krebbers authored 4 years ago
  
  See https://github.com/coq/coq/pull/13741#issuecomment-762761112
  1c2e6891
- add zip_with_diag and zip_diag · 8f69a159
  Ralf Jung authored 4 years ago
  
  8f69a159
- fix and reject warnings on Coq 8.13 · e7a7f588
  Ralf Jung authored 4 years ago
  
  e7a7f588
Jan 17, 2021
- Add lemmas `map_fmap_zip_with_{l,r}`. · fc52ac53
  Robbert Krebbers authored 4 years ago
  
  fc52ac53
Jan 15, 2021
- Apply 1 suggestion(s) to 1 file(s) · c4b14c58
  Ralf Jung authored 4 years ago
  
  c4b14c58
- add some singleton and snoc lemmas · 5e5b2d17
  Ralf Jung authored 4 years ago
  
  5e5b2d17
- add set_map_empty · e37b4e68
  Ralf Jung authored 4 years ago
  
  e37b4e68
- add set_map_union, set_map_singleton · bf59b1eb
  Ralf Jung authored 4 years ago
  
  bf59b1eb
Jan 11, 2021
- Shorten proof. · c5676b11
  Robbert Krebbers authored 4 years ago
  
  c5676b11
- Fix compilation with Coq 8.10 (which has a weaker `lia`). · d7732dcb
  Robbert Krebbers authored 4 years ago
  
  d7732dcb
- Rename `seq_S_snoc` into `seq_S` to be consistent with Coq's stdlib. · 9782eda9
  Robbert Krebbers authored 4 years ago
  
  9782eda9
- simplify proofs (by Robbert) · c57fe844
  Ralf Jung authored 4 years ago
  
  c57fe844
- adjust map_size_delete statement · 83901f25
  Ralf Jung authored 4 years ago
  
  83901f25
- simplify proof (by Robbert) · c4875672
  Ralf Jung authored 4 years ago
  
  c4875672
- simplify proof (by Robbert) · c111795c
  Ralf Jung authored 4 years ago
  
  c111795c
- add seqZ_S · 794ce99a
  Ralf Jung authored 4 years ago
  
  794ce99a
- adjust variable names and remove redundant scope · 59b248ed
  Ralf Jung authored 4 years ago
  
  59b248ed
- rename seq_S_end_app -> seq_S_snoc · 8d8a0f0a
  Ralf Jung authored 4 years ago
  
  8d8a0f0a
- add elem_of_seq, elem_of_seqZ, seqZ_app · d5b1ae21
  Ralf Jung authored 4 years ago
  
  Proofs by Tej
  d5b1ae21
- prove take_0 · 3c4993d2
  Ralf Jung authored 4 years ago
  
  3c4993d2
- prove map_size_delete, map_size_insert_Some, map_to_list_delete · 65ddd0da
  Ralf Jung authored 4 years ago
  
  65ddd0da
Jan 07, 2021
- also adjust Hint · 3081c441
  Ralf Jung authored 4 years ago
  
  3081c441
- explicit Local/Global for all Instance and Arguments · 8709344e
  Ralf Jung authored 4 years ago
  
  8709344e
Jan 04, 2021
- Indent nested sections in `fin_maps` file. · 794f33f6
  Robbert Krebbers authored 4 years ago
  
  794f33f6
- Add lemma `bind_Some_equiv`. · abe0ec66
  Robbert Krebbers authored 4 years ago
  
  abe0ec66
- Remove duplicate `map_fmap_empty` of `fmap_empty`, and rename... · 46b16f58
  Robbert Krebbers authored 4 years ago
  
  Remove duplicate `map_fmap_empty` of `fmap_empty`, and rename `map_fmap_empty_inv` into `fmap_empty_inv` for consistency's sake.
  46b16f58
Dec 24, 2020
- Add `pretty` instance for `positive`. · 7bf7c7fa
  Robbert Krebbers authored 4 years ago
  
  7bf7c7fa
Dec 04, 2020
- better proof by Robbert · 4a5f19ed
  Ralf Jung authored 4 years ago
  
  4a5f19ed
- add insert_subseteq_l · 5acbf503
  Ralf Jung authored 4 years ago
  
  5acbf503
Nov 23, 2020
- Replace unused pattern variables with underscore · b920e707
  Tej Chajed authored 4 years ago
  
  Addresses new unused-pattern-matching-variable warning on Coq master.
  Verified
  
  b920e707
Nov 20, 2020
- Add explicit Global to hints at top level · 8e8f3a41
  Tej Chajed authored 4 years ago
  
  Fixes new Coq master warning deprecated-hint-without-locality.
  Verified
  
  8e8f3a41
Nov 12, 2020
- Set `Hint Mode` for `pretty`. · 00e2ceeb
  Robbert Krebbers authored 4 years ago
  
  00e2ceeb
Nov 10, 2020
- Refactor proof of list_to_map_snoc · 4f541628
  Simon Friis Vindum authored 4 years ago
  
  4f541628
- Fix `pretty` for `Z` and prove `injectivity` of it. · 359bdf0f
  Robbert Krebbers authored 4 years ago
  
  359bdf0f
- Fix `pretty` for `N`. · 1855e425
  Robbert Krebbers authored 4 years ago
  
  This fix is inspired by !198.
  1855e425
Nov 09, 2020
- Add lemmas about list_to_map · 1b9b1ef7
  Simon Friis Vindum authored 4 years ago
  
  1b9b1ef7
Oct 29, 2020
- Tweaks based on feedback Ralf. · c7012583
  Robbert Krebbers authored 4 years ago
  
  c7012583
- Add lemmas for 1/4 + 1/4. · f106ebdd
  Robbert Krebbers authored 4 years ago
  
  f106ebdd