coqutil It would be better if coqutil used no axioms

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.

Apr 10 '20 04:04 JasonGross

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

Apr 10 '20 13:04 samuelgruetter

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.

Apr 11 '20 00:04 JasonGross

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

Apr 21 '20 09:04 mdempsky

Merged, thanks!

Apr 21 '20 12:04 andres-erbsen

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

Apr 21 '20 13:04 andres-erbsen