Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2021-02-16T11:03:04Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/405Tracking issue for HeapLang interpreter2021-02-16T11:03:04ZRalf Jungjung@mpi-sws.orgTracking issue for HeapLang interpreterThis is the tracking issue for the HeapLang interpreter added in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/564. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
...This is the tracking issue for the HeapLang interpreter added in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/564. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
## Open issues
* Generalize the monad and move it to std++, and generalize the tactics for the monad.
* Find some way to avoid the `pretty_string` instance, or move it to std++.https://gitlab.mpi-sws.org/iris/iris/-/issues/407Tracking issue for list RA2021-03-17T11:50:01ZRalf Jungjung@mpi-sws.orgTracking issue for list RAThis is the tracking issue for the list RA that went to staging in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/654. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper....This is the tracking issue for the list RA that went to staging in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/654. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
## Open issues
* The laws of the list camera are kind of weird, because it's very awkward to deal with "holes" in the list, which typically occurs when separating ghost state.
* Is the list RA ever actually needed, or can we replace it by `gmap` + `map_seq`? That deals better with "holes", but [lacks some closure properties](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/371#note_62685) that can sometimes be useful.https://gitlab.mpi-sws.org/iris/iris/-/issues/414Tracking issue for monotone RA2021-05-07T08:49:48ZRalf Jungjung@mpi-sws.orgTracking issue for monotone RAThis is the tracking issue for the "monotone" RA from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/597. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
## Open iss...This is the tracking issue for the "monotone" RA from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/597. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
## Open issues
* How should the RA be called? `monotone` is a very general term, it would be good to find something more specific. Currently it is called `mra` which is short but cryptic. `principal` should then likely become `mra_principal` and all lemmas be prefixed with `mra` as well.
* Do a solid review of the API surface.
Cc @amintimany @robbertkrebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/352Tracking issue for records2021-03-18T09:21:04ZRalf Jungjung@mpi-sws.orgTracking issue for records@tchajed, @robbertkrebbers and me are discussing ideas for equipping Iris with support for "named records", based on a first implementation of sch a scheme by Tej for Perennial. This is a tracking issue where we track which pieces of wor...@tchajed, @robbertkrebbers and me are discussing ideas for equipping Iris with support for "named records", based on a first implementation of sch a scheme by Tej for Perennial. This is a tracking issue where we track which pieces of work depend on what, and what needs to be done next.
The current status is that some unforeseen issues came up after merging https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/479, but we'd rather not change the naming system until we have a way to reliably control the names used for existentials in a record. Record design itself [is blocked on some fundamental questions](https://gitlab.mpi-sws.org/iris/iris/-/issues/352#note_65075).
* [List of related MRs](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests?scope=all&utf8=%E2%9C%93&state=all&label_name[]=T-records)https://gitlab.mpi-sws.org/iris/iris/-/issues/78Trouble with iApply and typeclass inference order2019-11-01T13:16:44ZRalf Jungjung@mpi-sws.orgTrouble with iApply and typeclass inference orderThe following says it all:
```
Lemma test_iApply_1 (M : ucmraT) (P : nat → uPred M) :
▷ (∃ x, P x) -∗ ∃ x, ▷ P x.
Proof.
iIntros "H". Fail iApply uPred.later_exist.
rewrite -uPred.later_exist. by iNext.
Qed.
```The following says it all:
```
Lemma test_iApply_1 (M : ucmraT) (P : nat → uPred M) :
▷ (∃ x, P x) -∗ ∃ x, ▷ P x.
Proof.
iIntros "H". Fail iApply uPred.later_exist.
rewrite -uPred.later_exist. by iNext.
Qed.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/441Upstream later credits2021-12-07T12:16:56ZRalf Jungjung@mpi-sws.orgUpstream later credits@robbertkrebbers and me seem to agree that having @simonspies's later credits in Iris proper would be great, but there are still a lot of details to be worked out. Let's use this issue to collect relevant information.
In particular, I k...@robbertkrebbers and me seem to agree that having @simonspies's later credits in Iris proper would be great, but there are still a lot of details to be worked out. Let's use this issue to collect relevant information.
In particular, I keep forgetting what exactly are the `fupd` laws that we would lose by doing this, so maybe we can put that here. :)https://gitlab.mpi-sws.org/iris/iris/-/issues/399Upstream more big_op lemmas from Perennial2021-02-17T08:49:05ZRalf Jungjung@mpi-sws.orgUpstream more big_op lemmas from PerennialPerennial has a bunch of big_op lemmas at <https://github.com/mit-pdos/perennial/tree/master/src/algebra/big_op>. At least some of those are certainly worth upstreaming, but I find it hard to figure out where to draw the line.Perennial has a bunch of big_op lemmas at <https://github.com/mit-pdos/perennial/tree/master/src/algebra/big_op>. At least some of those are certainly worth upstreaming, but I find it hard to figure out where to draw the line.https://gitlab.mpi-sws.org/iris/iris/-/issues/427Upstreaming big_op lemmas2021-07-16T09:37:22ZMichael SammlerUpstreaming big_op lemmasRefinedC currently contains the following big_sepL lemmas that I would like to upstream, but I have no idea how to prove them without the proof mode:
```coq
Lemma big_sepL_impl' {B} Φ (Ψ : _ → B → _) (l1 : list A) (l2 : list B) :
len...RefinedC currently contains the following big_sepL lemmas that I would like to upstream, but I have no idea how to prove them without the proof mode:
```coq
Lemma big_sepL_impl' {B} Φ (Ψ : _ → B → _) (l1 : list A) (l2 : list B) :
length l1 = length l2 →
([∗ list] k↦x ∈ l1, Φ k x) -∗
□ (∀ k x1 x2, ⌜l1 !! k = Some x1⌝ -∗ ⌜l2 !! k = Some x2⌝ -∗ Φ k x1 -∗ Ψ k x2) -∗
[∗ list] k↦x ∈ l2, Ψ k x.
Proof.
iIntros (Hlen) "Hl #Himpl".
iInduction l1 as [|x1 l1] "IH" forall (Φ Ψ l2 Hlen); destruct l2 => //=; simpl in *.
iDestruct "Hl" as "[Hx1 Hl]". iSplitL "Hx1". by iApply "Himpl".
iApply ("IH" $! (Φ ∘ S) (Ψ ∘ S) l2 _ with "[] Hl").
iIntros "!>" (k y1 y2 ?) "Hl2 /= ?".
by iApply ("Himpl" with "[] [Hl2]").
Unshelve. lia.
Qed.
End sep_list.
Lemma big_sepL2_impl' {A B C D} (Φ : _ → _ → _ → PROP) (Ψ : _ → _ → _ → _) (l1 : list A) (l2 : list B) (l1' : list C) (l2' : list D) `{!BiAffine PROP} :
length l1 = length l1' → length l2 = length l2' →
([∗ list] k↦x;y ∈ l1; l2, Φ k x y) -∗
□ (∀ k x1 x2 y1 y2, ⌜l1 !! k = Some x1⌝ -∗ ⌜l2 !! k = Some x2⌝ -∗ ⌜l1' !! k = Some y1⌝ -∗ ⌜l2' !! k = Some y2⌝ -∗ Φ k x1 x2 -∗ Ψ k y1 y2) -∗
[∗ list] k↦x;y ∈ l1';l2', Ψ k x y.
Proof.
iIntros (Hlen1 Hlen2) "Hl #Himpl".
rewrite !big_sepL2_alt. iDestruct "Hl" as (Hl1) "Hl".
iSplit. { iPureIntro. congruence. }
iApply (big_sepL_impl' with "Hl"). { rewrite !zip_with_length. lia. }
iIntros "!>" (k [x1 x2] [y1 y2]).
rewrite !lookup_zip_with_Some.
iDestruct 1 as %(?&?&?&?).
iDestruct 1 as %(?&?&?&?). simplify_eq. destruct_and!.
by iApply "Himpl".
Qed.
```
How can one prove these lemmas in a way that they can be upstreamed?https://gitlab.mpi-sws.org/iris/iris/-/issues/135Use [notypeclasses refine] for all proofmode tactics2020-11-11T12:36:56ZRobbert KrebbersUse [notypeclasses refine] for all proofmode tacticsAs done ad-hoc for two tactics in 5249f4c488c0847f229b4d9e38f89145775933be to work around confusion of apply wrt canonical structures, it would be good to do this for all tactics.As done ad-hoc for two tactics in 5249f4c488c0847f229b4d9e38f89145775933be to work around confusion of apply wrt canonical structures, it would be good to do this for all tactics.https://gitlab.mpi-sws.org/iris/iris/-/issues/317Use `byte` based strings for proof mode2020-05-16T19:16:11ZRobbert KrebbersUse `byte` based strings for proof modeNewer versions of Coq have a type `byte` with 256 constructors. We could use strings based on `byte` in the proofmode. Maybe that gives a significant speed up compared to the current `ascii` based strings.
@tchajed said the construction...Newer versions of Coq have a type `byte` with 256 constructors. We could use strings based on `byte` in the proofmode. Maybe that gives a significant speed up compared to the current `ascii` based strings.
@tchajed said the construction of `byte` based strings does not exist in the Coq stdlib but can be defined as:
```
From Coq Require Import Init.Byte.
Record bytes := bytes_from_list { bytes_to_list : list byte }.
Declare Scope bytestring_scope.
Open Scope bytestring_scope.
String Notation bytes bytes_from_list bytes_to_list : bytestring_scope.
Definition foo : bytes := "foo".
```https://gitlab.mpi-sws.org/iris/iris/-/issues/398Use `dom` instead of `∀ k, is_Some (.. !! k) ...`2021-02-17T08:48:46ZRobbert KrebbersUse `dom` instead of `∀ k, is_Some (.. !! k) ...`See for example `big_sepM_sep_zip_with`, `big_sepM_sep_zip`, `big_sepM2_intuitionistically_forall`, `big_sepM2_forall`.
The version with `dom` is more intuitive, and likely easier to prove because one can reason equationally with lemmas...See for example `big_sepM_sep_zip_with`, `big_sepM_sep_zip`, `big_sepM2_intuitionistically_forall`, `big_sepM2_forall`.
The version with `dom` is more intuitive, and likely easier to prove because one can reason equationally with lemmas for `dom`. However, the fact that the set (here `gset`) has to specified explicitly might be annoying.
Note that if we perform this change, there are also some lemmas in std++ that need to be changed.https://gitlab.mpi-sws.org/iris/iris/-/issues/412Use dfrac everywhere2022-01-17T16:49:59ZRalf Jungjung@mpi-sws.orgUse dfrac everywhere`auth` and `view` support dfrac now, but many of the abstractions built on top of it do not yet:
* [x] `algebra.lib.gmap_view`
* [x] `algebra.lib.mono_nat`
* [ ] `base_logic.lib.ghost_map`
* [ ] `base_logic.lib.mono_nat`
There are more ...`auth` and `view` support dfrac now, but many of the abstractions built on top of it do not yet:
* [x] `algebra.lib.gmap_view`
* [x] `algebra.lib.mono_nat`
* [ ] `base_logic.lib.ghost_map`
* [ ] `base_logic.lib.mono_nat`
There are more `auth`-based abstractions in `algebra.lib` but those do not expose *any* fraction on their authoritative part yet.
Some more are not actually built on top of `view`, but these are or could be exposing fractions that it might be useful to turn into `dfrac`:
* [ ] `base_logic.lib.ghost_var`
* [ ] Cancelable invariants
* [ ] Saved propositions (could be made essentially "`ghost_var` with higher-order ghost state", supporting both persistent immutable and ephemeral mutable saved propositions)
However, before we do all this, we should figure out if there is a way to do that without making these APIs *harder* to use for the common case of only needing fraction `1`. For `gset_bij`, we are already in the situation that users need to write `DfracOwn 1` a lot; I wouldn't want the same to happen e.g. for `ghost_map`.https://gitlab.mpi-sws.org/iris/iris/-/issues/438Use HB.lock(-like) sealing2022-01-20T01:44:18ZRalf Jungjung@mpi-sws.orgUse HB.lock(-like) sealinghierarchy-builder offers a sealing mechanism that looks extremely syntactically lightweight, while doing module-based sealing under the hood (meaning it probably seals better than our `seal` type, though I am not sure if that makes a dif...hierarchy-builder offers a sealing mechanism that looks extremely syntactically lightweight, while doing module-based sealing under the hood (meaning it probably seals better than our `seal` type, though I am not sure if that makes a difference in practice.
Quoting from https://github.com/math-comp/hierarchy-builder/wiki/Locking:
```
HB.lock Definition new_concept := 999999.
Lemma test x : new_concept ^ x ^ new_concept = x ^ new_concept ^ new_concept.
Proof.
Time Fail reflexivity. (* takes 0s *)
rewrite new_concept.unlock.
Time Fail reflexivity. (* takes 7s, the original body is restored *)
Abort.
```
This is exactly the kind of locking API I always wanted: just adding a keyword in front of the `Definition`, done. This would make it a no-brainer to seal basically every `iProp` that our reusable libraries export.
TODO:
- Check if this actually works in Iris
- Decide if we want to do this, and how -- are we okay with a dependency on hierarchy-builder?https://gitlab.mpi-sws.org/iris/iris/-/issues/275use implicit arguments for lemmas in coq_tactics.v2019-11-22T16:30:29ZPaolo G. Giarrussouse implicit arguments for lemmas in coq_tactics.v- [ ] The following [discussion](https://gitlab.mpi-sws.org/iris/iris/merge_requests/338#note_42171) from !338 should be addressed:
> > I was tempted to use implicit arguments instead of (some of) these underscores to make the `refi...- [ ] The following [discussion](https://gitlab.mpi-sws.org/iris/iris/merge_requests/338#note_42171) from !338 should be addressed:
> > I was tempted to use implicit arguments instead of (some of) these underscores to make the `refine` more readable... does that cause problems? [@Blaisorblade]
> I have been thinking about this many times. However, we should not just do it locally here, but should do it globally for all proof mode tactics. First let's get #135 fixed and then do what you suggest. [@robbertkrebbers]https://gitlab.mpi-sws.org/iris/iris/-/issues/202Use of `Into`/`From`/`As`/`Is` prefixes of classes is inconsistent2020-11-06T14:42:49ZRobbert KrebbersUse of `Into`/`From`/`As`/`Is` prefixes of classes is inconsistentSee the discussion here: https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/159#note_28898See the discussion here: https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/159#note_28898https://gitlab.mpi-sws.org/iris/iris/-/issues/420Use siProp more in building the uPred (and BI) interfaces2021-06-30T17:27:28ZRalf Jungjung@mpi-sws.orgUse siProp more in building the uPred (and BI) interfacesuPred defines a few (primitive) connectives that could all be defined in terms of an `siProp` mbedding:
- internal equality
- pure embedding
- plainly modality
- CMRA validity
Then we can have CMRA validity in any logic with an `siProp`...uPred defines a few (primitive) connectives that could all be defined in terms of an `siProp` mbedding:
- internal equality
- pure embedding
- plainly modality
- CMRA validity
Then we can have CMRA validity in any logic with an `siProp` embedding. Going this route might also finally let us get rid of `base_logic.algebra` and instead prove these lemmas in `siProp` so they can be used "for free" in any BI with an `siProp` embedding. We might even want to use `siProp` to define some of our algebraic classes.
@haidang started working on this since some of this is useful for BedRock. Here's the full plan we came up with to stage that (not saying @haidang is doing all these stages, and the later ones are obviously subject to change):
1. Add uPred_si_embed and uPred_si_emp_valid to upred.v; remove uPred_pure, uPred_internal_eq, uPred_plainly. Re-define those in terms of that and re-derive all the old rules in bi.v. The interesting part will be figuring out the laws for the new connectives such that we can derive all the laws for the old things that got removed.
2. (depends on 1) Add proof mode support for embed and emp_valid.
3. (depends on 1) Define uPred_cmra_valid in terms of uPred_si_embed via some new siProp for CMRA validity.
4. (depends on 1) Add iris/base_logic/lib/monpred_si_embed.v and transitive embedding.
5. (depends on 3, 2) State base_logic.algebra lemmas in siProp so they work for all logics that have an siProp embedding.
6. (depends on 3; having 5 would be useful) Add BiOwn to abstract over RA ownership.
7. (depends on 1) State uPred_entails as an siProp.
8. (probably best after 5 or together with 5) Change CMRA axioms so that validity is defined as an siProp.
9. (depends on ?, speculative) Use siProp in BI interface? For what exactly? Get rid of pure so we can define it in general for all BIs with an siProp embedding? Use siProp entailments?
10. (depends on ?, probably best after 8, highly speculative) Change OFE axioms to use `siProp` for dinstance? Still need to derive `Prop`-based version for setoid rewriting though.Hai DangHai Danghttps://gitlab.mpi-sws.org/iris/iris/-/issues/359Use the IPM to prove some example IPM extension theorems2020-10-21T11:00:32ZTej Chajedtchajed@mit.eduUse the IPM to prove some example IPM extension theoremsThe current proofs for some HeapLang tactics use a bunch of separation logic theorems manually, like this proof:
```coq
Lemma tac_wp_free Δ Δ' s E i K l v Φ :
MaybeIntoLaterNEnvs 1 Δ Δ' →
envs_lookup i Δ' = Some (false, l ↦ v)%I →
...The current proofs for some HeapLang tactics use a bunch of separation logic theorems manually, like this proof:
```coq
Lemma tac_wp_free Δ Δ' s E i K l v Φ :
MaybeIntoLaterNEnvs 1 Δ Δ' →
envs_lookup i Δ' = Some (false, l ↦ v)%I →
(let Δ'' := envs_delete false i false Δ' in
envs_entails Δ'' (WP fill K (Val $ LitV LitUnit) @ s; E {{ Φ }})) →
envs_entails Δ (WP fill K (Free (LitV l)) @ s; E {{ Φ }}).
Proof.
rewrite envs_entails_eq=> ? Hlk Hfin.
rewrite -wp_bind. eapply wand_apply; first exact: wp_free.
rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
rewrite -Hfin wand_elim_r (envs_lookup_sound' _ _ _ _ _ Hlk).
apply later_mono, sep_mono_r, wand_intro_r. rewrite right_id //.
Qed.
```
It would be much nicer to use the proof mode to do these proofs, which is also nicely circular because we're extending the proof mode using the proof mode. For example, the above proof can be written:
```coq
rewrite envs_entails_eq=> ? Hlk Hfin.
rewrite into_laterN_env_sound.
iIntros "HΔ'".
iApply wp_bind.
pose proof (envs_lookup_sound' _ false _ _ _ Hlk) as HΔ'split.
set (Δ'':=envs_delete false i false Δ') in *.
iDestruct (HΔ'split with "HΔ'") as "[Hl HΔ'']".
iApply (wp_free with "Hl").
iNext. iIntros "_".
iApply (Hfin with "HΔ''").
```
This proof isn't shorter but you can figure out how to write such a proof using only the proof mode rather than convoluted uses of theorems like `sep_mono_r` and `wand_intro_r`. This particular case become slightly messier because if you do `iDestruct envs_lookup_sound with "HΔ'"` then the proof mode reduces `envs_delete` and the result is horrendous.
I don't think we need to re-do all of the proofs; I'm thinking having a few such examples would go a long way as examples that demonstrate how to extend the IPM in a nice way. We couldn't port all of the theorems anyway since of course some of these theorems are actually used to implement the IPM.https://gitlab.mpi-sws.org/iris/iris/-/issues/300vs doesn't use FUpd2020-03-30T09:38:01ZGregory Malechavs doesn't use FUpdIs there a reason that the definition of `vs` explicitly mentions `iProp`? In practice it means that its notation can not be used in lifted logics such as `monPred`. For example, writing `P ==> Q` works at `iProp`, but doesn't work at `m...Is there a reason that the definition of `vs` explicitly mentions `iProp`? In practice it means that its notation can not be used in lifted logics such as `monPred`. For example, writing `P ==> Q` works at `iProp`, but doesn't work at `monPred x (iProp _)` even though all of the other notation (that are conceptually very simple) do work at `monPred`.https://gitlab.mpi-sws.org/iris/iris/-/issues/375We have some lonely notations2020-11-05T12:15:18ZRalf Jungjung@mpi-sws.orgWe have some lonely notationsThe following is the list of notations that are "lonely", which means they are not in a scope: (in some heap_lang file, so there might be things this does not import)
```
Lonely notations
"✓{ n } x" := validN n x
"◯V a" := view_frag a
"◯...The following is the list of notations that are "lonely", which means they are not in a scope: (in some heap_lang file, so there might be things this does not import)
```
Lonely notations
"✓{ n } x" := validN n x
"◯V a" := view_frag a
"◯ a" := auth_frag a
"●{ q } a" := auth_auth q a
"●V{ q } a" := view_auth q a
"●V a" := view_auth (pos_to_Qp xH) a
"● a" := auth_auth (pos_to_Qp xH) a
"↑ x" := up_close x
"'λne' x .. y , t" := OfeMor (fun x => .. (OfeMor (fun y => t)) ..)
"'λ' x .. y , t" := fun x => .. (fun y => t) ..
"x ◎ y" := ccompose x y
"x ≥ y" := ge x y
"x ≤ y" := le x y
"x ≡{ n }≡ y" := dist n x y
"x ≡{ n }@{ A }≡ y" := dist n x y
"x ~~>: y" := cmra_updateP x y
"x ~~> y" := cmra_update x y
"x ~l~> y" := local_update x y
"x ||* y" := zip_with orb x y
"x =.>* y" := Forall2 bool_le x y
"x =.> y" := bool_le x y
"x :b: y" := cons_binder x y
"p .2" := snd p
"p .1" := fst p
"ps .*2" := fmap snd ps
"ps .*1" := fmap fst ps
"TT -t> A" := tele_fun TT A
"A -n> B" := ofe_morO A B
"A -d> B" := discrete_funO (fun _ => B)
"x +b+ y" := app_binder x y
"x &&* y" := zip_with andb x y
"'[tele_arg' x ; .. ; z ]" := TargS x .. (TargS z TargO) ..
"'[tele_arg' ]" := TargO
"'[tele' x .. z ]" := TeleS (fun x => .. (TeleS (fun z => TeleO)) ..)
"'[tele' ]" := TeleO
"(||)" := orb
" () " := tt
"(&&)" := andb
"( H 'with' pat )" := {| itrm := H; itrm_vars := hlist.hnil; itrm_hyps := pat |}
"( H $! x1 .. xn 'with' pat )" := {|
itrm := H;
itrm_vars := hlist.hcons x1 .. (hlist.hcons xn hlist.hnil) ..;
itrm_hyps := pat |}
"( H $! x1 .. xn )" := {|
itrm := H;
itrm_vars := hlist.hcons x1 .. (hlist.hcons xn hlist.hnil) ..;
itrm_hyps := EmptyString |}
"#[ Σ1 ; .. ; Σn ]" := gFunctors.app Σ1 .. (gFunctors.app Σn gFunctors.nil) ..
"#[ ]" := gFunctors.nil
"# l" := LitV l
```
Many of those are from Iris or std++, and are probably oversights.https://gitlab.mpi-sws.org/iris/iris/-/issues/138wp_apply/Texan triple improvements2021-11-19T19:15:17ZRalf Jungjung@mpi-sws.orgwp_apply/Texan triple improvements* [ ] `wp_apply` could be able to apply a total WP when the goal is a partial WP, removing some duplication in heap_lang/lib.
* [ ] `wp_apply` could automatically try to prove that the expression is not a value, and then apply some varia...* [ ] `wp_apply` could be able to apply a total WP when the goal is a partial WP, removing some duplication in heap_lang/lib.
* [ ] `wp_apply` could automatically try to prove that the expression is not a value, and then apply some variant of `wp_step`. This would remove the need to have a `\later` in the definition of Texan triples, making them equivalent to a WP in all cases (as opposed to just the non-value case). I think right now I regret that we decided for Texan triples to contain the `\later`, this makes them slightly harder to teach and destroys their equivalence with WP/"normal" triples.
* [ ] [More far-fetched?] Make the precondition of Texan triples a list of assertions, so that we can (a) desugar them to something curried, and (b) not have silly `True` preconditions when the list is empty.
* [ ] When proving a triple, the postcondition could be wrapped in a fancy update, removing the need to `rewrite -wp_fupd` in some of our proofs. Of course, when applying a triple, that update must not be in the way.
* [ ] What about some support for introducing the postcondition into the context (avoiding a manual `iIntros` all the time)?
Blocked by #130