How many kinds of `updateP` lemmas do we want?
Context: !960 (comment 98523)
There currently are two ways of specifying the updateP
behavior of our resource algebras.
For example, for prod
, the lemma characterizing updateP
are the following:
Lemma prod_updateP P1 P2 (Q : A * B → Prop) x :
x.1 ~~>: P1 → x.2 ~~>: P2 → (∀ a b, P1 a → P2 b → Q (a,b)) → x ~~>: Q.
Lemma prod_updateP' P1 P2 x :
x.1 ~~>: P1 → x.2 ~~>: P2 → x ~~>: λ y, P1 (y.1) ∧ P2 (y.2).
Basically, we have the "explicit" style of prod_updateP'
, where the set of potential update target values is explicitly stated, and we have the "Texan" style of prod_updateP
, which has built-in weakening and looks more predicate-transformery. We also note that either is easily proven from the other (one direction uses weakening, the other just directly chooses Q := λ y, P1 (y.1) ∧ ..
).
The question is: Do we always want both? Perhaps, one of these laws is barely used and can be removed, so that in future, only one of these laws needs to be maintained. And then, this law should be consistently used everywhere.