Iris merge requestshttps://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests2023-08-28T12:02:37Zhttps://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/972Draft: experiment: use coq's ability to infer more canonical structures2023-08-28T12:02:37ZRalf Jungjung@mpi-sws.orgDraft: experiment: use coq's ability to infer more canonical structuresI wonder if we should recommend this style, once all Coq versions we support can handle it. It is certainly much nicer, we could entirely hide these `R`/`UR` terms from users. Unfortunately in one case already in this repo, it requires m...I wonder if we should recommend this style, once all Coq versions we support can handle it. It is certainly much nicer, we could entirely hide these `R`/`UR` terms from users. Unfortunately in one case already in this repo, it requires more type annotations. I don't understand why Coq cannot infer that any more.https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/933Make bi fields non-canonical2023-10-13T14:37:45ZPaolo G. GiarrussoMake bi fields non-canonicalSuggested by @janno .Suggested by @janno .https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/869Draft: Fix #497: avoid Hint Immediate2023-05-02T15:30:45ZPaolo G. GiarrussoDraft: Fix #497: avoid Hint ImmediateUses the same strategy as https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/424. Draft since for now I'm duplicating the tactic.Uses the same strategy as https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/424. Draft since for now I'm duplicating the tactic.https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/842Make* class tweaks2023-07-25T16:00:31ZRalf Jungjung@mpi-sws.orgMake* class tweaksRalf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/820Dune build files2023-03-07T14:58:46ZPaolo G. GiarrussoDune build filesRequires https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/387.Requires https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/387.https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/771Draft: Add simplification machinery for ✓ and ≼.2023-05-25T11:45:27ZIke MulderDraft: Add simplification machinery for ✓ and ≼.This merge request partially addresses issue #251 .
Concretely, this merge request adds an `iCombineOwn` tactic. In the following environment:
```
"Hγ1" : own γ (q1, GSet E1)
"Hγ2" : own γ (q2, GSet E2)
```
executing `iCombineOwn "Hγ1 ...This merge request partially addresses issue #251 .
Concretely, this merge request adds an `iCombineOwn` tactic. In the following environment:
```
"Hγ1" : own γ (q1, GSet E1)
"Hγ2" : own γ (q2, GSet E2)
```
executing `iCombineOwn "Hγ1 Hγ2" as "Hγ" gives %[Hq HE]` should replace "Hγ1" and "Hγ2" with a new hypothesis `"Hγ" : own γ (q1 + q2, GSet (E1 ∪ E2))` and two pure hypotheses: `Hq : q1 + q2 ≤ 1` and `HE : E1 ## E2`.
The "as" clause is optional. This is especially useful when you want to combine validity information for a ● and a ◯. In the following environment:
```
"Hγ1" : own γ (◯ (Some (q1, GSet E1)))
"Hγ2" : own γ (● (Some (q2, GSet E2)))
```
executing `iCombineOwn "Hγ1 Hγ2" gives %H` should give you a new pure hypotheses `H : q1 ≤ q2 ∧ E1 ⊆ E2 ∧ ((q1 < q2) ∨ (q1 ≡ q2 ∧ E1 ≡ E2))`.
It works by adding three typeclasses, `IsValidOp`, `IsValidGives` and `IsIncluded`, which try to determine an iProp that simplifies ✓ or ≼. Since we are looking for an iProp, not a pure proposition, this approach also works for higher-order ghost state.
Some current issues:
- Does not simplify equivalences. If directly using rewrites in introduction patterns, may cause slowdowns. Currently an explicit `%leibniz_equiv` on the equality is needed for faster rewrites.
- Some lemmas I used on validity and equivalence of views are still lying around in an awkward place.
- Documentation is missing
- Does not yet have instances for all CMRA building blocks provided in `iris/algebra`, but at least supports the ones used inside the iris repository, and some others I have used in the past.
Feedback is most welcome! I wasn't really sure where to place some of this stuff, so it currently resides in `iris/base_logic/`.https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/677make Z.of_nat not a Coercion any more2023-01-12T11:55:48ZRalf Jungjung@mpi-sws.orgmake Z.of_nat not a Coercion any moreFixes https://gitlab.mpi-sws.org/iris/stdpp/-/issues/102Fixes https://gitlab.mpi-sws.org/iris/stdpp/-/issues/102https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/599Prefix iDestruct automatic names with an underscore2021-03-18T09:19:00ZTej Chajedtchajed@gmail.comPrefix iDestruct automatic names with an underscoreAvoids conflicts with user-provided names while still giving existential
witnesses meaningful names for readability (which can be used if
desired).
Fixes incompatibility coming from !479 where automatic names required
the user to change...Avoids conflicts with user-provided names while still giving existential
witnesses meaningful names for readability (which can be used if
desired).
Fixes incompatibility coming from !479 where automatic names required
the user to change their choice of manually-written names, even if they
weren't referring the automatic names at all.https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/480WIP: Prepend introduction pattern `H.ipat`.2021-03-18T09:15:25ZRobbert KrebbersWIP: Prepend introduction pattern `H.ipat`.The new introduction pattern `H.ipat` prepends the name `H` to all names appearing in `ipat`.
For example:
```coq
Lemma test_iDestruct_prepend_1 P Q :
P ∗ Q -∗ Q ∗ P.
Proof. iIntros "H.[P Q]".
```
This will give hypotheses `HP` and ...The new introduction pattern `H.ipat` prepends the name `H` to all names appearing in `ipat`.
For example:
```coq
Lemma test_iDestruct_prepend_1 P Q :
P ∗ Q -∗ Q ∗ P.
Proof. iIntros "H.[P Q]".
```
This will give hypotheses `HP` and `HQ`.
This feature will be particularly useful with the record-like syntax that @tchajed @jtassaro @jung and me are working on.
**TODO**
- [ ] Bikeshed about the syntax. The period `.` may cause annoyances with the electric terminator in Emacs?