Design: connecting booleans to their meaning

[andres-erbsen]

Here is a proposal for what to do about definitions and proofs for equality deciders and other cases where a boolean carries propositional meaning.

In definitions, it seems preferable to refer (syntactically) to boolean predicates as opposed to the propositions they decide. This is important for both efficient reduction and to avoid the need for dependently-typed reasoning in code that is otherwise simply typed. Higher-order definitions that take predicates as arguments should take them as boolean functions, and relevant proofs should assume a BoolSpec about these arguments.

Proofs about this code then need to find the appropriate meaning of that boolean. Usually, it decides a property, but sometimes the answer may be incomplete. To find these bool-Prop relationships automatically, I've had a good experience with tactics that automatically look up proofs of BoolSpec. For example, coqutil declares BoolSpec to be typeclass here and then has a wrapper of destruct look it up.

For code that needs the properties of the boolean (for e.g. termination of dependent typing) I think it's possible to used the same hint in terms: (if eb as b return (if b then _ else _) -> _ then fun _ => x else fun _ => y) (if'_get_boolspec _)) . In particular, destructing the wrapper just works when reasoning about definitions thus created, and gives prop hypotheses. For definitions where this is the only dependently typed aspect, this technique would reduce the goal to a simply-typed one.

Transparent equality deciders are still needed when the proof they return is casted over. This happens in e.g. when using Nat.eq_dec to decide the equality of the length of two vectors. However, theses cases are few, and we'd keep doing what we have: manually writing and referencing T.eq_dec.

At a higher level, I think we want to:

• Decide on the format of the lemmas connecting booleans to propositions (this proposal: BoolSpec)
• Decide on a way to look up these lemmas (this proposal: typeclasses eauto)
• Decide on how to use these lemmas in definitions (this proposal: typeclasses eauto + wrapper definition)
• Figure out what to do about proofs that need to be transparent (this proposal: nothing new)
• Add definitions and proofs of the new form to stdlib, e.g. for list
• Deprecate alternatives that are then duplicative

Let's use this issue to discuss. My primary interest is in finding an actionable plan within stdlib, hopefully relatively quickly, and without depending on future changes elsewhere.