Commits · 8a8a3394f0d4f4e739682ac4d1b033f8fbe7df01 · Gaëtan Gilbert / Iris · GitLab

Snippets Groups Projects

Oct 04, 2016
- Try to use links in README. · 8a8a3394
  Robbert Krebbers authored 8 years ago
  
  8a8a3394
Oct 03, 2016
- Non step-indexed laws about exclusive and Some. · 2227cd66
  Robbert Krebbers authored 8 years ago
  
  2227cd66
- Alternative definition of is_Some. · d47d99dd
  Robbert Krebbers authored 8 years ago
  
  d47d99dd
- 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
- Cancelation for union. · 5631e485
  Robbert Krebbers authored 8 years ago
  
  5631e485
Oct 02, 2016
- Prove fact about exclusive and included. · d6875e7d
  Robbert Krebbers authored 8 years ago
  
  d6875e7d
- Big ops and None. · 9f3a376e
  Robbert Krebbers authored 8 years ago
  
  9f3a376e
- Looking up into a gmap is a homomorphism. · 7227cf28
  Robbert Krebbers authored 8 years ago
  
  7227cf28
- Prove that included on frac corresponds to the order on Qp. · b2ba69ee
  Robbert Krebbers authored 8 years ago
  
  Thanks to Aleš Bizjak.
  b2ba69ee
Sep 28, 2016
- Leibniz equality variants of the commute lemmas for big ops. · 1270ae08
  Robbert Krebbers authored 8 years ago
  
  1270ae08
- Introduce CMRA homomorphisms. · 61761380
  Robbert Krebbers authored 8 years ago
  
  This allows us to factor out properties about connectives that commute with the big operators.
  61761380
- Prove always_if_pure. · 7293e063
  Robbert Krebbers authored 8 years ago
  
  7293e063
- Generic decider for emptyness of finite maps. · 648f146d
  Robbert Krebbers authored 8 years ago
  
  648f146d
- Define big operators on uPred in terms of those on CMRAs. · a4383677
  Robbert Krebbers authored 8 years ago
  
  a4383677
- Proper instances for mononicity of CMRA op. · 204b6c8e
  Robbert Krebbers authored 8 years ago
  
  204b6c8e
- Relate included on uPred to entails. · 2308bb5c
  Robbert Krebbers authored 8 years ago
  
  2308bb5c
- Induction principle for finite sets with Leibniz equality. · 48d958f2
  Robbert Krebbers authored 8 years ago
  
  48d958f2
- Remove uPred_big_and, it only use just complicates stuff. · e4090611
  Robbert Krebbers authored 8 years ago
  
  e4090611
- Generic properties for commuting big ops. · 2c644a10
  Robbert Krebbers authored 8 years ago
  
  2c644a10
- Big ops over gmap without binder for the key. · 123a7c05
  Robbert Krebbers authored 8 years ago
  
  123a7c05
- Reorganize big ops for CMRA based on those for uPred. · 562b2c2b
  Robbert Krebbers authored 8 years ago
  
  562b2c2b
Sep 27, 2016
- Uniform syntax for selecting hypotheses. · d1ef32dd
  Robbert Krebbers authored 8 years ago
  
  Used in iRevert, iClear, iFrame, and for generalizing the IH in iInduction and iLöb.
  d1ef32dd
- Put notations for proofmode environment manipulation into a module. · 6d021c73
  Robbert Krebbers authored 8 years ago
  
  6d021c73
- Extend iClear to handle clearing of Coq-level variables. · f774d316
  Robbert Krebbers authored 8 years ago
  
  f774d316
- Use lazymatch in iClear to avoid backtracking on errors. · 06fad70e
  Robbert Krebbers authored 8 years ago
  
  06fad70e
- Rename the internal validity uPred_valid into uPred_cmra_valid. · 669cdfa5
  Robbert Krebbers authored 8 years ago
  
  This way we can use uPred_valid for validity of uPreds, which more sense.
  669cdfa5
- Consistent syntax for generalization in iLöb and iInduction. · 61e8aadd
  Robbert Krebbers authored 8 years ago
  
  As proposed by JH Jourdan in issue 34.
  61e8aadd
- CMRA structure on uPred. · 7c762be1
  Robbert Krebbers authored 8 years ago
  
  7c762be1
- Relate map_to_list to nil. · a01453ed
  Robbert Krebbers authored 8 years ago
  
  a01453ed
- Relate "elements" of a finite set to nil. · 8b9a96ad
  Robbert Krebbers authored 8 years ago
  
  8b9a96ad
- Alternative version of ownM_empty. · 65171af2
  Robbert Krebbers authored 8 years ago
  
  65171af2
- Insert and singleton maps are non-empty. · 1aac61c4
  Robbert Krebbers authored 8 years ago
  
  1aac61c4
- Binary mononicity property for CMRA op. · 01904806
  Robbert Krebbers authored 8 years ago
  
  01904806
Sep 21, 2016
- Reorganize frame preserving updates for lists. · ca8e04a3
  Robbert Krebbers authored 8 years ago
  
  ca8e04a3
- More properties for the list CMRA. · 324db1dc
  Robbert Krebbers authored 8 years ago
  
  324db1dc
Sep 20, 2016
- More derived auth properties. · f72340bc
  Robbert Krebbers authored 8 years ago
  
  f72340bc
- Mononicity of own. · 0024ac1f
  Robbert Krebbers authored 8 years ago
  
  0024ac1f