 05 Jun, 2019 1 commit


Robbert Krebbers authored

 03 Jun, 2019 1 commit


Robbert Krebbers authored
This allows one to make use of recursive ghost state obtained from the recursive domain equation solver.

 30 May, 2019 1 commit


Robbert Krebbers authored
We never make canonical instances of them.

 28 May, 2019 1 commit


Robbert Krebbers authored

 26 May, 2019 1 commit


Robbert Krebbers authored

 24 May, 2019 2 commits


Ralf Jung authored

Robbert Krebbers authored
This MR is a follow up on the renamings performed (implicitly) as part of !215. This MR makes the following changes:  `auth_both_frac_valid` and `auth_both_valid` are now of the same shape as `auth_both_frac_validN` and `auth_both_validN`. That is, both are now biimplications.  The lefttoright direction of `auth_both_frac_valid` and `auth_both_valid` only holds in case the camera is discrete. The righttoleft versions for nondiscrete cameras are prefixed `_2`, the convention that we use throughout the development.  Change the direction of lemmas like `auth_frag_valid` and `auth_auth_valid` so that it's consistent with the other lemmas. I.e. make sure that the ◯ and ● are always on the LHS of the biimplication.

 23 May, 2019 1 commit


Hai Dang authored

 21 May, 2019 1 commit


Robbert Krebbers authored

 04 May, 2019 3 commits


Robbert Krebbers authored
This proof also more easily scales to other recursive types, like trees etc.

Robbert Krebbers authored

Robbert Krebbers authored

 02 May, 2019 1 commit


Robbert Krebbers authored

 01 May, 2019 1 commit


Robbert Krebbers authored
Notably, `big_andL_andL` and `big_andL_and` where a ⊣⊢ and ⊢ version of the same lemma. I favored the `big_opL_op` naming scheme.

 29 Apr, 2019 1 commit


Paolo G. Giarrusso authored
This comment wasn't updated after 866cad62.

 25 Apr, 2019 1 commit


 06 Mar, 2019 1 commit


Dan Frumin authored

 05 Mar, 2019 1 commit


Ralf Jung authored

 04 Mar, 2019 1 commit


Robbert Krebbers authored

 03 Mar, 2019 1 commit


Ralf Jung authored

 21 Feb, 2019 1 commit


Robbert Krebbers authored

 20 Feb, 2019 1 commit


Robbert Krebbers authored

 18 Feb, 2019 1 commit


Ralf Jung authored

 05 Feb, 2019 1 commit


Dan Frumin authored

 24 Jan, 2019 1 commit


Maxime Dénès authored
This is in preparation for coq/coq#9274.

 21 Dec, 2018 1 commit


Robbert Krebbers authored

 12 Dec, 2018 1 commit


Robbert Krebbers authored

 10 Dec, 2018 6 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
This lemma allows one to get the witness out of a later, without having to use `later_car`, i.e. in a way that works in the onpaper version of the logic.

Robbert Krebbers authored

 08 Dec, 2018 1 commit


Robbert Krebbers authored

 03 Dec, 2018 1 commit


Robbert Krebbers authored

 29 Nov, 2018 1 commit


Tej Chajed authored
Adding a hint without a database now triggers a deprecation warning in Coq master (https://github.com/coq/coq/pull/8987).

 26 Nov, 2018 1 commit


Robbert Krebbers authored

 06 Nov, 2018 1 commit


Robbert Krebbers authored

 01 Nov, 2018 2 commits


Robbert Krebbers authored

Dan Frumin authored
