search

DeepSpec / InteractionTrees

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

Prove (or disprove) "iter after iter" equation #187

Open Lysxia opened 4 years ago

Lysxia commented 4 years ago

@YaZko wondered about this equation to rewrite the sequential composition of two iter:

iter f >>> iter g
=
inl_ >>> iter (case_ (f >>> inl_) (g >>> inr_ >>> assoc_l))

Because the equation looks similar to theorems we've already proved about loop rather than iter, I think it's provable from the iterative axioms but haven't succeeded at it. Another way is to specialize it to itree and construct the bisimulation explicitly.

It might actually be simpler and more interesting to implement a solver to settle this type of question once and for all, although I don't know whether the problem is decidable.

YaZko commented 4 years ago

I proved the equation in the special case of itrees (see https://github.com/DeepSpec/InteractionTrees/commit/db77cb964c2f7b140789b25385fe55203588adff).

I remain very curious as to whether it can be proved abstractly. Certainly investigating the decidability of all the equational theory sounds interesting!