This bit of theory comes from our Vellvm project, and has hence been co-authored with @Chobbes, @euisuny and @Zdancewic . It's been long due cleaning up things and porting it to the itree library.
We define in the PR a unary program logic defined as the diagonal of eutt.
We prove the elementary structural theory, as well as proof rules w.r.t. basic logical connectors, bind and iter.
The main result we derive is a stronger cut rule than [eutt_clo_bind]: one can leverage any functional fact about the involved computations, as captured by eutt_post_bind and eutt_post_bind_eq.
Note that in all generality, these should be combined with the generalization from PR#211
I stored this file in Eq, let me know if anyone thinks there's a better place. More generally, any complaints or requests before merge are welcome!
Hey everyone,
This bit of theory comes from our Vellvm project, and has hence been co-authored with @Chobbes, @euisuny and @Zdancewic . It's been long due cleaning up things and porting it to the itree library.
We define in the PR a unary program logic defined as the diagonal of
eutt. We prove the elementary structural theory, as well as proof rules w.r.t. basic logical connectors, bind and iter.The main result we derive is a stronger cut rule than [eutt_clo_bind]: one can leverage any functional fact about the involved computations, as captured by
eutt_post_bindandeutt_post_bind_eq. Note that in all generality, these should be combined with the generalization from PR#211I stored this file in
Eq, let me know if anyone thinks there's a better place. More generally, any complaints or requests before merge are welcome!Best, Yannick