mit-plv/coqutil

It would be better if coqutil used no axioms

Opened this issue · 5 comments

JasonGross commented

coqchk gives:

CONTEXT SUMMARY
===============

* Theory: Set is predicative

* Axioms:
    Coq.ssr.ssrunder.Under_rel.Over_rel
    Coq.ssr.ssrunder.Under_rel.Under_rel_from_rel
    Coq.ssr.ssrunder.Under_rel.over_rel
    Coq.Logic.FunctionalExtensionality.functional_extensionality_dep
    coqutil.Map.SortedList.TODO_andres
    Coq.ssr.ssrunder.Under_rel.over_rel_done
    Coq.ssr.ssrunder.Under_rel.Under_rel
    Coq.Logic.PropExtensionality.propositional_extensionality
    Coq.ssr.ssrunder.Under_rel.Under_relE
    coqutil.Map.SortedListString.TODO_andres
    Coq.ssr.ssrunder.Under_rel.under_rel_done

* Constants/Inductives relying on type-in-type: <none>

* Constants/Inductives relying on unsafe (co)fixpoints: <none>

* Inductives whose positivity is assumed: <none>

You can ignore the ssr.ssrunder ones (coq/coq#5030), but it'd be nice to remove the other ones.

samuelgruetter commented

The TODOs in coqutil.Map are scheduled to be fixed soon, but we weren't planning to remove functional and prop extensionality

JasonGross commented

What's the reason you use Leibniz equality on sets rather than defining your own equivalence relation on them? As far as I can tell, doing this would allow you to remove all your uses of propext and most of your uses of funext.

mdempsky commented

I sent PR #26 to remove coqutil.Map.SortedList.TODO_andres.

andres-erbsen commented

Merged, thanks!

  • 🎉1
andres-erbsen commented

Trickling down at mit-plv/bedrock2#153 ...