Iris merge requestshttps://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests2020-12-04T20:41:22Zhttps://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/591Make iDestruct consume wands when it's supposed to2020-12-04T20:41:22ZTej Chajedtchajed@gmail.comMake iDestruct consume wands when it's supposed to`iDestruct ("H" with "HP")` where "H" is persistent is supposed to
consume "H" if it isn't a forall. Due to a bug in the tactic, this
behavior was never triggered and "H" was always left alone.`iDestruct ("H" with "HP")` where "H" is persistent is supposed to
consume "H" if it isn't a forall. Due to a bug in the tactic, this
behavior was never triggered and "H" was always left alone.https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/141add iSplitWith tactic for convenient conjunction monotonicity2018-07-13T08:51:49ZRalf Jungjung@mpi-sws.orgadd iSplitWith tactic for convenient conjunction monotonicityWhen dealing with logically atomic triples, a common situation is to have some hypothesis which is a conjunction, and a goal which is a conjunction, and one wants to prove the left-hand side of the goal using the left-hand side of the as...When dealing with logically atomic triples, a common situation is to have some hypothesis which is a conjunction, and a goal which is a conjunction, and one wants to prove the left-hand side of the goal using the left-hand side of the assumption and vice versa.
This adds a tactic to make that convenient.https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/130rename affinely_persistently -> intuitionistically; and make it a TC-opaque d...2018-03-22T12:02:29ZRalf Jungjung@mpi-sws.orgrename affinely_persistently -> intuitionistically; and make it a TC-opaque definitionI am very unsure about the instances in `class_instances.v` -- both about what I added (necessary to make it all compile again), and about what else I should add because the modality commutes with various things.
This will break rever...I am very unsure about the instances in `class_instances.v` -- both about what I added (necessary to make it all compile again), and about what else I should add because the modality commutes with various things.
This will break reverse dependencies if they relied on "intuitionitsically" to be syntactically equal (and not just convertible) to "affinely persistently".
Fixes #126Generalized Proofmode Mergerhttps://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/115Set mode for update modalities2018-02-14T15:11:45ZRalf Jungjung@mpi-sws.orgSet mode for update modalitiesI think this also fixes #146 by using `typeclasses eauto` instead of `apply _`.I think this also fixes #146 by using `typeclasses eauto` instead of `apply _`.https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/114Make `FromPure` depend on an affinity parameter2018-07-13T08:51:48ZJacques-Henri JourdanMake `FromPure` depend on an affinity parameterIn a linear logic, a pure premise usually appear under an `affinely` modality.
That is, an hypothesis could probably look like `bi_affinely ⌜φ⌝ -∗ P`. However, the `[%]` specialization pattern will not allow to discharge this premise....In a linear logic, a pure premise usually appear under an `affinely` modality.
That is, an hypothesis could probably look like `bi_affinely ⌜φ⌝ -∗ P`. However, the `[%]` specialization pattern will not allow to discharge this premise. The solution is to make `FromPure` depend on an affinity Boolean.
In the way, I fixed two bugs in the proofmode:
- `tac_assert_pure` was no longer working. The corresponding Ltac code did not have the right number of parameters
- `into_forall_wand_pure` had an unnecessary `Absorbing` assumptionhttps://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/104Consistent handling of pure implication and forall2017-12-21T16:00:07ZRobbert KrebbersConsistent handling of pure implication and forallIt required a bunch of additional proof mode type class instances and a hack for `iSpecialize` to deal with an inconsistent behavior of `refine`.
I hope this covers all cases.It required a bunch of additional proof mode type class instances and a hack for `iSpecialize` to deal with an inconsistent behavior of `refine`.
I hope this covers all cases.https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/100Proof mode support for monotonous predicates.2018-07-13T08:51:48ZJacques-Henri JourdanProof mode support for monotonous predicates.Also, developed a notion of "BI embedding", which is a general notion that is useful for supporting monPred in proofmode.Also, developed a notion of "BI embedding", which is a general notion that is useful for supporting monPred in proofmode.https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/98Factor plainly out of main BI interface2018-03-03T10:39:00ZRalf Jungjung@mpi-sws.orgFactor plainly out of main BI interfaceThe intention is to make the axioms compatible with
`plainly P r := forall s, P s` in linear BIs. This
is needed to obtain propositional extensionality.The intention is to make the axioms compatible with
`plainly P r := forall s, P s` in linear BIs. This
is needed to obtain propositional extensionality.Generalized Proofmode Mergerhttps://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/95Remove plainly_exist_1 from the BI axioms.2018-07-13T08:51:49ZJacques-Henri JourdanRemove plainly_exist_1 from the BI axioms.Added a `PlainlyExist1BI` class for BIs that do have the property.
One slight annoyance is that this class has to appear in `interface.v`. Otherwise, we have to add a dependency `uPred.v` -> `bi/derived.v`, which kill parallelism. Jus...Added a `PlainlyExist1BI` class for BIs that do have the property.
One slight annoyance is that this class has to appear in `interface.v`. Otherwise, we have to add a dependency `uPred.v` -> `bi/derived.v`, which kill parallelism. Just tell me if you prefer this over the current alternative.https://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/50WIP: Strong framing2024-02-13T13:52:02ZRobbert KrebbersWIP: Strong framingThis MR makes an attempt at closing #71. Todo:
# Syntax
I am not sure I like what we have now:
```coq
Lemma demo_17 (M : ucmraT) (P Q R : uPred M) :
P -∗ Q -∗ R -∗ (P ∗ Q ∨ R ∗ False).
Proof.
iIntros "^$ HQ HR {^$HR}".
...This MR makes an attempt at closing #71. Todo:
# Syntax
I am not sure I like what we have now:
```coq
Lemma demo_17 (M : ucmraT) (P Q R : uPred M) :
P -∗ Q -∗ R -∗ (P ∗ Q ∨ R ∗ False).
Proof.
iIntros "^$ HQ HR {^$HR}".
iAssert (Q ∨ False)%I with "[^$HQ]" as "[HQ|[]]".
iFrame "^HQ".
Qed.
```
Note that we have syntax for framing in 1.) introduction patterns to frame introduced hypotheses on the fly 2.) The clear syntax `{sel_pat}` in introduction patterns 3.) specialization patterns 4.) the frame tactic. I tried to get some form of consistency, but suggestions for improvements are very welcome.
As I mentioned in #71:
> It would be nice to have a "do more" modifier that we can also in other places.
>
> For example, we have `iIntros "!>"` to introduce a modality. In #48 it is proposed to make the modality introduction behave like `iNext` (i.e. also strip modalities from the context). This will probably be costly, so in that case we may to keep `!>` letting introduce a modality, but have something like `DO_MORE!>` to also strip the modalities from all hypotheses.
The `^` token plays that role.
# Approach
As I wrote in #71 this can be implemented in at least two ways:
1. Have an additional hint database `strong_frame` for dangerous frame instances.
2. Extend the `Frame` type class with a Boolean `strong`.
In this MR I went for (1) because it requires the least modifications. One has to be a bit careful about not introducing overlapping instances (and hence unneeded backtracking on failures) when using the `typeclass_instances` and `strong_frame` hint database together, but I think I managed.
# Documentation
The new `MaybeFrame` type class and `strong_frame` hint database should be documented. Also `ProofMode.md` should be modified.
@janno @haidang @jung @jjourdanhttps://gitlab.rts.mpi-sws.org/iris/iris/-/merge_requests/29ProofMode intro patterns: accept _ as part of variable names2016-11-24T08:18:17ZRalf Jungjung@mpi-sws.orgProofMode intro patterns: accept _ as part of variable names@robbertkrebbers beat this. ;)@robbertkrebbers beat this. ;)