Commits · 034d1d23fc28246eff9e2555d77a62234f3ef8da · Pierre Roux / Iris

Oct 20, 2020
- remove algebra/ dependency on base_logic/ · cbcb1baf
  Ralf Jung authored 4 years ago
  
  cbcb1baf
Oct 09, 2020
- prove a funny consequence of Löb induction · 9a6976e2
  Ralf Jung authored 4 years ago
  
  9a6976e2
Oct 08, 2020
- Take comments into account. · 89d172ed
  Robbert Krebbers authored 4 years ago
  
  89d172ed
- Make the proof closer to the jungle proof. · 7b460868
  Robbert Krebbers authored 4 years ago
  
  7b460868
- Cite jungle paper. · 13e8dee5
  Robbert Krebbers authored 4 years ago
  
  13e8dee5
- Counterexamples for Affine+EM and Löb+EM. · a3f1b72e
  Robbert Krebbers authored 4 years ago
  
  a3f1b72e
Oct 01, 2020
- More Coqdoc. · 377c2d14
  Robbert Krebbers authored 4 years ago
  
  377c2d14
- Remove ¬ notation in counterexamples. · 256de028
  Robbert Krebbers authored 4 years ago
  
  256de028
- ASCII notation for negation in bi_scope. · 82a75fc2
  Robbert Krebbers authored 4 years ago
  
  82a75fc2
- Add BI notation for negation. · f73319e8
  Robbert Krebbers authored 4 years ago
  
  f73319e8
- Prove that `BiPureForall` holds if we assume classical logic in Coq. · 3e51bdd7
  Robbert Krebbers authored 4 years ago
  
  3e51bdd7
- Remove property `(∀ a, ⌜ φ a ⌝) ⊢ ⌜ ∀ a, φ a ⌝` from the BI canonical structure and · 6e334252
  Robbert Krebbers authored 4 years ago
  
  put it into a type class `BiPureForall`. This property does not hold for embeddings of classical logic into Coq.
  6e334252
Sep 30, 2020
- Lemmas about big op on lists for !485 · bd11cf26
  Michael Sammler authored 4 years ago
  
  bd11cf26
Sep 29, 2020
- Break long line. · 7c72fcce
  Robbert Krebbers authored 4 years ago
  
  7c72fcce
Sep 28, 2020
- apply review and fix and improve proof · e72da74c
  Ralf Jung authored 4 years ago
  
  e72da74c
Sep 10, 2020
- fix a bunch of typos (thanks Tej) · ad1ab485
  Ralf Jung authored 4 years ago
  
  ad1ab485
- make sure we import 'options' everywhere · 9291076e
  Ralf Jung authored 4 years ago
  
  9291076e
- use options file everywhere that we so far set 'Proof using' · e252709e
  Ralf Jung authored 4 years ago
  
  e252709e
Aug 30, 2020
- Definition -> Lemma · 45c14ba9
  Ralf Jung authored 4 years ago
  
  45c14ba9
Aug 29, 2020
- name more arguments in Arguments · 280725d6
  Ralf Jung authored 4 years ago
  
  280725d6
Aug 12, 2020
- do not eta-expand when sealing · 89e2c153
  Ralf Jung authored 4 years ago
  
  89e2c153
- update for Coq 8.10 deprecations · 75ed8394
  Ralf Jung authored 4 years ago
  
  75ed8394
Jul 02, 2020
- tweak comments and changelog · 0ad40ef9
  Ralf Jung authored 4 years ago
  
  0ad40ef9
Jun 29, 2020
- Do not require bi to be affine unnecessarily · 5e7d8f0b
  Simon Friis Vindum authored 4 years ago
  
  5e7d8f0b
- Add lemmas for creating big op from duplicable resource · a86906f4
  Simon Friis Vindum authored 4 years ago
  
  a86906f4
Jun 26, 2020
- remove 3-mask step-taking fupd notation · 818c9480
  Ralf Jung authored 4 years ago
  
  818c9480
- adjust notation for step-taking updates · e2a06f1c
  Ralf Jung authored 4 years ago
  
  e2a06f1c
Jun 19, 2020
- Port to Coq #12512. · 4c6a9a18
  Robbert Krebbers authored 4 years ago
  
  4c6a9a18
Jun 18, 2020
- Add Proper mono instances for make_laterable · 5f98a0bf
  Ralf Jung authored 4 years ago
  
  5f98a0bf
- Add make_laterable_mono · b6d1946d
  Ralf Jung authored 4 years ago
  
  b6d1946d
Jun 11, 2020
- Introduce notation `BiLaterContractive PROP` for `Contractive (bi_later (PROP:=PROP))`. · b57797ee
  Robbert Krebbers authored 4 years ago
  
  b57797ee
- Use `löb_weak` for BiLöb class. · ee49d97b
  Robbert Krebbers authored 4 years ago
  
  ee49d97b
- Factor out lemma `löb_weak`. · 725ffc11
  Robbert Krebbers authored 4 years ago
  
  725ffc11
Jun 07, 2020
- remove the weaker counterexample (now that the other one only requires a boring cinv_alloc) · 56e966fd
  Ralf Jung authored 4 years ago
  
  56e966fd
- linear counterexample: we do not actually need cinv_alloc to be that powerful · 827f464c
  Ralf Jung authored 4 years ago
  
  827f464c
May 29, 2020
- change |-- to |- · 7b7d3336
  Gregory Malecha authored 4 years ago and Robbert Krebbers committed 4 years ago
  
  - it doesn't seem to conflict with anything in Ltac
  7b7d3336
May 28, 2020
- Fix `forall` parsing. using the stdpp change · 6ada4936
  Gregory Malecha authored 4 years ago
  
  6ada4936
- Fix scopes for `plainly` following !456. · 7458fa67
  Paolo G. Giarrusso authored 4 years ago
  
  Verified
  
  7458fa67
- Fix scopes of bupd and fupd · a3cc36e4
  Paolo G. Giarrusso authored 4 years ago and Robbert Krebbers committed 4 years ago
  
  a3cc36e4
May 25, 2020
- Prove different versions of Löb rule. · 7253dafb
  Robbert Krebbers authored 4 years ago
  
  7253dafb