iris:09741a0349b9746daa429652fc8e91d674caee2b commitshttps://gitlab.mpi-sws.org/tchajed/iris-coq/-/commits/09741a0349b9746daa429652fc8e91d674caee2b2017-12-20T12:09:33+01:00https://gitlab.mpi-sws.org/tchajed/iris-coq/-/commit/09741a0349b9746daa429652fc8e91d674caee2bComment on the `uPred` module trick.2017-12-20T12:09:33+01:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/tchajed/iris-coq/-/commit/8574d1eab3892ce04870849e9445e406975a7f09Hide the proof mode entailment behind a definition.2017-11-02T00:41:38+01:00Robbert Krebbersmail@robbertkrebbers.nl
This solves issue #100: the proof mode notation is sometimes not printed. As
Ralf discovered, the problem is that there are two overlapping notations:
```coq
Notation "P ⊢ Q" := (uPred_entails P Q).
```
And the "proof mode" notation:
```
Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ∗ Q" :=
(of_envs (Envs Γ Δ) ⊢ Q%I).
```
These two notations overlap, so, when having a "proof mode" goal of the shape
`of_envs (Envs Γ Δ) ⊢ Q%I`, how do we know which notation is Coq going to pick
for pretty printing this goal? As we have seen, this choice depends on the
import order (since both notations appear in different files), and as such, Coq
sometimes (unintendedly) uses the first notation instead of the latter.
The idea of this commit is to wrap `of_envs (Envs Γ Δ) ⊢ Q%I` into a definition
so that there is no ambiguity for the pretty printer anymore.https://gitlab.mpi-sws.org/tchajed/iris-coq/-/commit/b4567fbd5e062b72e370293a1647855da346a0e3Rename `always` → `persistently` (the persistent modality).2017-10-25T08:48:25+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/tchajed/iris-coq/-/commit/d6b49ab29e15031e47cb1644166172db52aea5camore restrictive Proof Using hints in base_logic, algebra2017-01-05T19:26:39+01:00Ralf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/tchajed/iris-coq/-/commit/71abda4d8480fc6528a1617aedbadde59705747bmake "make quick" quick by adding hints about the used section variables2017-01-03T17:50:02+01:00Ralf Jungjung@mpi-sws.org
This patch was created using
find -name *.v | xargs -L 1 awk -i inplace '{from = 0} /^From/{ from = 1; ever_from = 1} { if (from == 0 && seen == 0 && ever_from == 1) { print "Set Default Proof Using \"Type*\"."; seen = 1 } }1 '
and some minor manual editinghttps://gitlab.mpi-sws.org/tchajed/iris-coq/-/commit/766dbcd2415df9256f197dc562a0a15f9b0ddeacUse different module structuring of uPred.2016-12-13T18:03:41+01:00Robbert Krebbersmail@robbertkrebbers.nl
This fixes the following issue by JH Jourdan:
The fact of including uPred_[...] in the module uPred (in base_logic.v),
implies that typeclasses instances are declared twice. Once in module
uPred and once in module uPred_[...]. This has the unfortunate
consequence that it has to backtrack to both instances each time the
first one fails, making failure of type class search for e.g.
PersistentP potentially exponential.
Goal ((□ ∀ (x1 x2 x3 x4 x5: nat), True -∗ True) -∗ True : iProp Σ).
Time iIntros "#H".
Undo.
Remove Hints uPred_derived.forall_persistent : typeclass_instances.
Time iIntros "#H".
Thanks to Jason Gross @ Coq club for suggesting this fix.https://gitlab.mpi-sws.org/tchajed/iris-coq/-/commit/6b8069fa5af75e7e6faa4a0a516fd01e88a0309fmove everything to subfolder theories/2016-12-09T23:27:29+01:00Ralf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/tchajed/iris-coq/-/commit/e224e89101211478d7063a1eaf8ab90c26bf7ad5Rename uPred_eq into uPred_internal_eq.2016-10-25T15:43:07+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/tchajed/iris-coq/-/commit/fc3ac14835cba3cc39e751b14e08268b2099fd60Move base_logic stuff to its own folder: base_logic.2016-10-25T11:33:45+02:00Robbert Krebbersmail@robbertkrebbers.nl