Infrastructures and proofs using paco

DeepSpec / InteractionTrees

A Library for Representing Recursive and Impure Programs in Coq

MIT License

204 stars 51 forks source link

Infrastructures and proofs using paco #41

Closed gilhur closed 5 years ago

gilhur commented 5 years ago

Remove "Promitive Projections" for better automation.
Add infrastructures for coinductive proofs.
Prove key lemmas.

gilhur commented 5 years ago

I just committed a version with primitive projections on but with the itree_unfold (called, itree_eta) axiom. The update was very mechanical and easy. The proof scripts remained almost identical.

If the Coq developers accept the eta expansion for coinductive types as intensional equality, all problems are solved. I suggested this in the discussion post and am waiting to hear from them.

gmalecha commented 5 years ago

Thanks for the discussion today @gilhur & @Zdancewic . I know that I at least need to walk through the proofs by hand to really understand what is going on, but I'm wondering if we should merge this and try to simplify things more with additional pull requests. What do you guys think?