agda
Refactor `List.Membership.*` and `List.Relation.Unary.Any`
By contrast with #2323 this adds to the List.* API, and extensively refactors proofs about Membership and Any in the light of the addition of two 'obviously missing' combinators.
Highlights of the refactoring:
- extensive debugging of
importdependencies throughout - revision of qualified imports in accordance with the new style guidelines #2280
- revision of
withusage in favour of 'irrefutable' style #2123 UPDATED but these should themselves be rewritten in terms oflet... where possible. DONE.
The changes are mostly cosmetic, although there were some interesting pain points around eta-conversion (or lack of it!?), wrt strictness in (the structure of) values of dependent Σ-types.
So the only unresolved issue left, I think is of course: naming. Will continue to experiment over the coming day(s), and see if we can agree!
Happy to let @JacquesCarette work on further refactoring as he finds time/space for, but in the meantime, can we try to agree on the names (ironic given that this PR started 'small' with the choice of such things... and then, only emulating what was already present... sigh)?
Besides using what we have (or else Box and Diamond plus syntax), I guess my preference currently would be for the redundantly verbose ...
∃[x∈xs] P xs = ∃ λ x → x ∈ xs × P x
Regarding Box and Diamond syntax... I realise we don't have these ($\subseteq$-monotone/functorial in each argument!) definitions in full generality for R : REL A B _, where they're usually written $\forall_{R}{Q}$ (for Q : Pred B _) and $\exists_{R}{P}$ (for P : pred A _), subject to an adjointness characterisation $$\exists_{R}{P}\subseteq{Q} \Leftrightarrow {P}\subseteq\forall_{R}{Q}$$
The symbols box and diamond come from later/subsequent uses in modal logic (IIRC, but my sense of the exact history of concepts in the field is a bit sketchy).
If we were to add these concepts to the library, what should we call them? And would that help shed light on what to call them in the special case R = _∈_?
UPDATED: hmmm... I may have got my typings wrong, so I'd better figure out the dteails, and post a separate PR ;-)
Re: ∃[x∈xs] P xs = ∃ λ x → x ∈ xs × P x. This still doesn't strongly hint to me that there's a P coming after that. Though I guess if I "swap in" the version of [_] that I've seen Conor use a lot (not claiming he's author, just popularizer), this does make sense. But that would have to become part of our naming conventions to make wider sense?
I'm not familiar with Conor's (use of) [_] (and in any case, such notation is wildly overloaded... I'd much rather it stood solely for 'singleton' container, and maybe it does for him, but I'm not seeing it...). What's the actual name being proposed here, and its parameterisation?
[_] : {I : Set} (I -> Set) -> Set
[ P ] = forall {i} -> P i
It's really infix Box in ASCII.
Ah! Thanks... though as with my attempted use in #2126 of the syntax for
-
Relation.Unary.IUniversal:syntax IUniversal P = ∀[ P ]and -
Relation.Unary.Satisfiable:syntax Satisfiable P = ∃⟨ P ⟩(which are likewiseBoxandDiamond-like...)
I might expect some pushback from @MatthewDaggitt who I think is not a fan of 'clever' combinatory abbreviations...
Regarding Box and Diamond syntax... I realise we don't have these (-monotone/functorial in each argument!) definitions in full generality for R : REL A B _, where they're usually written (for Q : Pred B _) and (for P : pred A _), subject to an adjointness characterisation
Indeed, we only have it for homogeneous relations: http://agda.github.io/agda-stdlib/v2.0/Relation.Unary.Closure.Base.html
Re:
∃[x∈xs] P xs = ∃ λ x → x ∈ xs × P x. This still doesn't strongly hint to me that there's aPcoming after that.
@JacquesCarette returning to this comment of yours after few weeks of inactivity on this PR.
I think I don't really understand your comment: from the perspective of the Pred/subobject fibration, each quantifier is (a suitable adjoint to something) functorial between Pred foo and Pred bar... so why would a 'visibly obvious' quantifier such as ∃[x∈xs] not suggest to you that it's going to be followed by a P : Pred baz and then a suitable argument to the resulting transformed P?
Your first perspective (as true as it may be) doesn't seem to bear onto the problem: it's about usability. The fancier the explanation, the less likely it's going to communicate the intent to mere mortals.
But from the usability perspective... I don't know why I wasn't seeing it! Looking at it again today, it's clearly a quantifier that's still waiting for a predicate. Sigh. So: go for this notation.
@MatthewDaggitt lots of food for thought in your recent round of comments. I'm travelling this week, so may not have time to weed through, but I take the criticism on board, as well as the hint to factor out the 'controversial' parts (which of course started the whole thing off in the first place, in terms of 'here's a property without the accompanying definition which might make sense of it'...) as well as my own views, which I hadn't previously indulged, about finding the whole lose/find naming scheme somewhat irritating...
Will update as soon as I get time to focus properly on it. DONE
@MatthewDaggitt I've not opened a PR for the syntax extensions... yet. I'll scratch my head for a bit about the relational operator generalisations sketched above, and then try to fashion a focused PR introducing them, and specialising their syntax, if necessary, to the _∈_ case...
... but in the meantime, I think this should now be ready to go!?