It would be better if coqutil used no axioms

JasonGross commented 4 years ago

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 (https://github.com/coq/coq/issues/5030), but it'd be nice to remove the other ones.

samuelgruetter commented 4 years ago

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

JasonGross commented 4 years ago

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 4 years ago

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

andres-erbsen commented 4 years ago

Merged, thanks!

andres-erbsen commented 4 years ago

Trickling down at https://github.com/mit-plv/bedrock2/pull/153 ...

mit-plv / coqutil

It would be better if coqutil used no axioms #25