[ new ] generic "diag" for decidable equality

[gallais]

Realised we might as well include the fact that if propositional equality
is decidable then the decision procedure always succeeds on values
known to be equal.

[bch29]

Why not make these generic to Dec?

module Relation.Nullary.Decidable where

-- ...

isWitness : ∀ {p} {P : Set p} {Q : Dec P} (p : P) → Q ≡ yes (toWitness {Q = Q} (fromWitness p))
isWitness {Q = yes p} _ = refl
isWitness {Q = no ¬p} p = ⊥-elim (¬p p)

isWitnessFalse : ∀ {p} {P : Set p} {Q : Dec P} (¬p : ¬ P) → Q ≡ no (toWitnessFalse {Q = Q} (fromWitnessFalse ¬p))
isWitnessFalse {Q = yes p} ¬p = ⊥-elim (¬p p)
isWitnessFalse {Q = no ¬p} _ = refl

-- ...

[gallais]

Using ≡-≟-identity _≟_ a b refl you'll get yes refl rather than the more complex
yes (toWitness (a ≟ b) (fromWitness refl)) and it is usually what you want. But I
suppose it could be defined as a corollary of the more general lemmas.

[bch29]

I'm not sure if yes refl is in most cases more useful than "yes eq for some eq". If we're using this to prove things about functions defined by pattern matching on a ≟ b, then yes (toWitness (a ≟ b) (fromWitness refl)) is good enough. Besides, ≡-irrelevance makes me uncomfortable.

[gallais]

The stdlib relies in at least 3 places on yes refl rather than yes eq and a subst
on the right hand side (found using find . -name "*.agda" | xargs grep "| yes refl").

[MatthewDaggitt]

I agree that the reduction behaviour of the current versions is more desirable.

@gallais is there any reason why a and b aren't implicit? In my (admittedly brief) tests I can't find an example where they're not inferrable...

[MatthewDaggitt]

Thanks!

[bch29]

All three of those instances are in proofs of decidable equality, for binary and unary numbers. They don't use K, and more importantly they're proofs (rather than functions that we might need to prove theorems about).

If someone does want yes refl they can invoke irrelevance manually with trans (isWitness refl) (cong yes (≡-irrelevance _ _)).

[gallais]

If someone does want yes refl they can invoke irrelevance manually with
trans (isWitness refl) (cong yes (≡-irrelevance _ _)).

A lot of things can be obtained by combining more basic functions but that doesn't
mean we shouldn't give them names to make one's life easier e.g. cong₂ P eq1 eq2
is "just" cong (P _) eq2 (cong (\ x -> P x _) eq1).

As for K, as you've observed it's already used in the same file because of the
presence of ≡-irrelevance. I do agree however that the more general functions
you have suggested could have their place in Relation.Nullary.Decidable.

[JacquesCarette]

Opinion: Please avoid ≡-irrelevance as much as possible. I think it is obvious that 'proof relevance' is ascending, and that use of proof-irrelevance (when it isn't strictly needed) will become something that needs "fixed".

[gallais]

That's why I'm saying it would make sense to also have the Relation.Nullary.Decidable
versions in the standard library. However I think it's rather unreasonable to expect people
to write rewrite trans (isWitness refl) (cong yes (≡-irrelevance _ _)) when they want a stuck
a ≟ a to reduce to refl.

[JacquesCarette]

I agree. I did not understand that that is what your previous comments meant. Thanks for clarifying.