search

DeepSpec / InteractionTrees

A Library for Representing Recursive and Impure Programs in Coq
MIT License
204 stars 51 forks source link

Dijkstra pull request #217

Closed lag47 closed 2 years ago

lag47 commented 3 years ago

One of three pull requests intended to bring the secure branch into master. This branch introduces the main body of code implementing the Dijkstra Monads Forever paper. This includes a formalization of Dijkstra Monads and their laws as a type classes, the StateSpecT state transform over Dijkstra Monads, and TraceSpec a Dijkstra Monad over ITrees with arbitrary uninterpreted events built on top of ITraces.

Lysxia commented 2 years ago

Here's a general way to avoid axioms in Type like strong excluded middle: wrap it in inhabited, e.g., classicT_inhabited : inhabited (forall T, T + (T -> False)). When defining (noncomputable) functions that actually need it, take it as a parameter. Then in proofs (that are in Prop), we can first destruct classicT_inhabited as [classicT], and use the given parameter in to call those noncomputable functions.

Lysxia commented 2 years ago

Another trick I found is that if we make resp_eutt a notation for Proper (eutt ==> iff), then we can simply rewrite instead of applying these assumptions manually.