[ add ] Relation.Nullary.Decidable.dec-yes-recompute

[jamesmckinna]

This PR sharpens the type of Relation.Nullary.Decidable.dec-yes by supplying an explicit existential witness:

• dec-yes-recompute weakens the hypothesis to allow irrelevant argument .(a : A)
• by witnessing the existential with recompute a? a
• dec-yes then follows immediately.

It introduces two new lemmas:

• Relation.Nullary.Recomputable.recompute-irrelevant-id: for propositionally irrelevant A, recompute is the identity
• Relation.Nullary.Decidable.Core.recompute-irrelevant-id, encapsulating the above

UPDATED:

• refactors Relation.Nullary.Recomputable to lift definitions and basic properties out into Relation.Nullary.Recomputable.Core.

[JacquesCarette]

As this is likely a rather obscure bit of functionality with few users, I don't mind the name churn.

[jamesmckinna]

As this is likely a rather obscure bit of functionality with few users, I don't mind the name churn.

Well, I'm not thrilled by the name churn, but I wasn't quite prepared to just grab the old name and give it the new type... UPDATED but in a breaking v3.0 change, I might be tempted to rethink all the various names of these highly niche lemmas?

As it is, and seeing the single downstream use of the new construct, I think it can even be avoided altogether (or rather: it is still useful, but localised to its use as a step on a better path to dec-yes-irr, which is the enabling technology in Relation.Binary.PropositionalEquality for leveraging UIP for DecidableEquality...)... see #2740

UPDATED: the use of the new lemma in Data.Fin.Permutation is superseded by the changes in #2740 but I think that these two PRs are orthogonal, modulo rebasing, so I've removed the blocked-by-issue label. Think that this would be good to merge now, unless the right thing to do is revert the knock-on changes to Data.Fin.Permutation?

[MatthewDaggitt]

Otherwise looks good!

[jamesmckinna]

I suppose that the last step would be to make the breaking change, and simply give dec-yes the new type of dec-yes-recompute... but then we'd be bumping to v3.0 rather than v2.3. Still, worth considering downstream? NB. There are now no uses of dec-yes elsewhere in stdlib.

[MatthewDaggitt]

How about leaving the existing definition as is?

[jamesmckinna]

Latest commits should fix things as agreed 2025-06-25.