Commits · 230b2a6beab7cccfc1de70139a35b1748dd62282 · William Mansky / Iris

Nov 28, 2016
- Some nits. · 230b2a6b
  Robbert Krebbers authored 8 years ago
  
  230b2a6b
- Add a local update for auth (needed for nested auth) · 692b8570
  Ralf Jung authored 8 years ago
  
  Proof was done by Hai & me
  692b8570
Nov 25, 2016
- list-based agreement · 29c097c6
  Ralf Jung authored 8 years ago
  
  29c097c6
- Make auth_frag_op a Leibniz equality. · 6923de66
  Robbert Krebbers authored 8 years ago
  
  6923de66
Nov 22, 2016
- make deprecated notation only parsing · d04287bc
  Ralf Jung authored 8 years ago
  
  d04287bc
- add missing file... · ef3a26d0
  Ralf Jung authored 8 years ago
  
  ef3a26d0
- use OFEs instead of COFEs everywhere · 75518c9a
  Ralf Jung authored 8 years ago
  
  Use COFEs only for the recursive domain equation solver
  75518c9a
Nov 21, 2016
- Big op over set union. · 32abe0c0
  Robbert Krebbers authored 8 years ago
  
  32abe0c0
- Add some missing Proper instances on big ops. · 83996ca3
  Robbert Krebbers authored 8 years ago
  
  83996ca3
Nov 20, 2016
- More big op lemmas. · 3663aaf3
  Robbert Krebbers authored 8 years ago
  
  3663aaf3
Nov 19, 2016
- Homomorphism properties for big ops on multisets. · 1097ab91
  Robbert Krebbers authored 8 years ago
  
  1097ab91
Nov 17, 2016
- More big_opMS lemmas. · 85697195
  Robbert Krebbers authored 8 years ago
  
  85697195
- Fix projection-no-head-constant warning and clean up proofs. · bd6ca353
  Robbert Krebbers authored 8 years ago
  
  bd6ca353
Nov 15, 2016
- Big ops on multisets. · 8f33e282
  Robbert Krebbers authored 8 years ago
  
  Many useful properties are probably still missing.
  8f33e282
Oct 25, 2016
- Move base_logic stuff to its own folder: base_logic. · fc3ac148
  Robbert Krebbers authored 8 years ago
  
  fc3ac148
- Use notation |==> instead of |=r=> for basic update modality. · 568f6b7a
  Robbert Krebbers authored 8 years ago
  
  568f6b7a
- Rename rvs -> bupd (basic update), pvs -> fupd (fancy update). · 1b85d654
  Robbert Krebbers authored 8 years ago
  
  And also rename the corresponding proof mode tactics.
  1b85d654
Oct 14, 2016
- Only one direction of assoc and comm for separating conjunction is needed. · b20fd842
  Robbert Krebbers authored 8 years ago
  
  b20fd842
Oct 10, 2016
- Make validity of STS fragments require a witness. · 9c5a95d3
  Janno authored 8 years ago
  
  Initial proof by Jan-Oliver Kaiser, adapted by Robbert Krebbers.
  9c5a95d3
- Add PersistentP instances for own(S). · 121a4a75
  Janno authored 8 years ago
  
  Initial proof by Jan-Oliver Kaiser, adapted by Robbert Krebbers.
  121a4a75
- Add rewrite lemma for frac_op · ad0c229d
  Zhen Zhang authored 8 years ago
  
  ad0c229d
Oct 07, 2016
- Avoid camelcased names. · 7de50f87
  Robbert Krebbers authored 8 years ago
  
  7de50f87
- soundness -> consistency · a1398f31
  Ralf Jung authored 8 years ago
  
  a1398f31
Oct 06, 2016
- New notion of local updates. · d34f5890
  Robbert Krebbers authored 8 years ago
  
  d34f5890
- More properties about Some _ ≼ Some _. · 45954c6f
  Robbert Krebbers authored 8 years ago
  
  These are very useful when dealing with the authoritative CMRA.
  45954c6f
- Prove that the dec_agree CMRA is total. · 143fbc52
  Robbert Krebbers authored 8 years ago
  
  143fbc52
- Prove soundness result as stated in the appendix. · a31e05be
  Robbert Krebbers authored 8 years ago
  
  a31e05be
Oct 05, 2016
- Internalized versions of the equality on funC and morC. · 126d54c3
  Robbert Krebbers authored 8 years ago
  
  126d54c3
- IntoOp and FromOp instances for the authoritative fragment. · 2ea5d210
  Robbert Krebbers authored 8 years ago
  
  2ea5d210
- Functor for function space cofes. · 8e126e96
  Jacques-Henri Jourdan authored 8 years ago
  
  8e126e96
- Fix the lemma Some_included' for total CMRAs. · fc77fc3a
  Robbert Krebbers authored 8 years ago
  
  fc77fc3a
Oct 04, 2016
- tweak the Qp lemmas · f5082bd5
  Zhen Zhang authored 8 years ago
  
  f5082bd5
- appendix: base logic is now up-to-date · 9df1dae0
  Ralf Jung authored 8 years ago
  
  9df1dae0
- Add lemmas about Qp and fraction · 2e98600d
  Zhen Zhang authored 8 years ago
  
  2e98600d
Oct 03, 2016
- Non step-indexed laws about exclusive and Some. · 2227cd66
  Robbert Krebbers authored 8 years ago
  
  2227cd66
- Prove that the auth fragment is a UCMRA homomorphism. · 233aa0fa
  Robbert Krebbers authored 8 years ago
  
  233aa0fa
- Unfolding lemmas for big ops over lists with Z indices. · 1bbe5d15
  Robbert Krebbers authored 8 years ago
  
  1bbe5d15
- Extensionality (for Leibniz equality) of big ops. · 834c66e0
  Robbert Krebbers authored 8 years ago
  
  834c66e0
- Deallocation local updates for gset. · c3c31e88
  Robbert Krebbers authored 8 years ago
  
  c3c31e88
Oct 02, 2016
- Prove fact about exclusive and included. · d6875e7d
  Robbert Krebbers authored 8 years ago
  
  d6875e7d