[ add ] clean version of Data.Fin.Properties.searchMinimalCounterexample

[jamesmckinna]

Revised version of the relevant code from #2744 incorporating: UPDATED

• MinimalCounterexample/Least⟨¬_⟩ Least⟨_⟩ now defined as a record, not as syntax
• infix versions now as (duplicate) definitions of the removed verbose CamelCase versions
• use of inject deprecated in favour of _<_; add inject-< as lemma to smooth the path

Outstanding issues, if this PR gets merged:

• lemmas ¬∀⟶∃¬-smallest and ¬∀⟶∃¬ should be deprecated, as superseded by search-least⟨¬_⟩?
• even if not, their names should be changed to ¬∀⇒∃¬-smallest and ¬∀⇒∃¬, cf. ¬∃⇒∀¬ #2831 etc. UPDATED: see [ deprecate ] names for deMorgan lemmas in Data.Fin.Properties #2837

[JacquesCarette]

I like all of this, except for the name μ. It's a cute pun, but caters to a rather small crowd.

How about calling the constructor least instead? If you want a pun, then μ⟨_⟩ can be called the-least. I don't think μ⟨¬_⟩ passes the Fairbairn threshold.

[jamesmckinna]

I like all of this, except for the name μ. It's a cute pun, but caters to a rather small crowd.

It was absolutely not intended as a pun:

• for the 'small crowd' of recursion theorists/computer scientists who know or care about recursion theory, I regard μ as absolutely conventional usage denoting the Godel-Kleene minimisation operator, here specialised to the (much) easier case of Fin;
• Relation.Unary defines a number of 'Greek' short form syntaxes/definitions ∃⟨_⟩, ∀[_] for things which otherwise would be more verbose, and I'm conscious that there are at least two schools of thought about their appropriateness for stdlib, viz. favouring ASCII/CamelCase or else 'Greek' forms, and this PR follows that model: long-form names, with short-form 'abbreviations'

How about calling the constructor least instead? If you want a pun, then μ⟨_⟩ can be called the-least. I don't think μ⟨¬_⟩ passes the Fairbairn threshold.

Well...

• the use of μ as a constructor for the two records introduced here is, of course, both optional (no constructor required), and replaceable, so I'd be happy to change it for something, but 'least' seems itself to be working a bit too hard cognitively/semantically, and above all, I wanted something 'minimum ink' (following Wadler, whose taste in these matters usually seems reliable...)
• the Fairbairn objection to μ⟨¬_⟩ I actively disagree with: because the types MinimalExample and MinimalCounterexample are subtly different, to try to (more) accurately reflect the computation irrelevance of fields/arguments. So if they are to have short-form abbreviation, then they each deserve one!
• but again, maybe (short) ASCII alternative would be better, but then I'd be tempted simply to resort only to the existing camelCase : CamelCase idiomatics, but at the (quite high!) cost of adding some very long names... :-(

[jamesmckinna]

@JacquesCarette You were right, and I was wrong!
Latest commits hopefully simplify the code enough to answer (most of) your outstanding criticisms.
I couldn't tackle the Fairbairn one, though: irrelevant-projections warning/errors stymied me at an awkward moment.
If you're able to simplify further, I'd be happy to see the details!

[JacquesCarette]

@JacquesCarette You were right

I somehow never tire of hearing that 😏 . I'm quite happy with the current results.