search

Lysxia / coq-ceres

Coq library for serialization to S-expressions
MIT License
18 stars 1 forks source link

WIP: decidable equality instances #15

Closed liyishuai closed 4 years ago

liyishuai commented 4 years ago

Need help with Decidable_eq_sexp proof.

Lysxia commented 4 years ago

You can't use induction on sexp because the default induction principle is broken. You first have to manually state and prove a better induction principle using fix (I don't know whether there are any tools or commands to automate that).

Since you're not familiar with that, it might be a little easier to directly prove these Decidable instances with fix, but you still have to keep in mind exactly what the proof term being constructed looks like... Maybe I can show you how to do it some time Thursday.

Lysxia commented 4 years ago

Thanks a lot!