Definition of Induction.WellFounded.WfRec

[jamesmckinna]

Currently, the definition:

WfRec : Rel A r → ∀ {ℓ} → RecStruct A ℓ _
WfRec _<_ P x = ∀ y → y < x → P y

suffers from two (unfortunate) defects:

• the use of the name RecStruct, when this type is nothing more or less than that of PredicateTransformer (or: what you will...) which only really takes on the role of being a structure-for-recursion once a given such T : PredicateTransformer is accompanied by a proof that T P ⊆′ P for suitable P...; ADDRESSED by Predicate transformers: Reconciling Induction.RecStruct with Relation.Unary.PredicateTransformer.PT #2140
• the explicit quantification over y in WfRec, which leads, infectively, to a profusion of (almost-?)always-inferrable arguments when working with subsequent Accessibility and WellFoundedness proofs. ADDRESSED by Changes explicit argument y to implicit in Induction.WellFounded.WfRec #2084

The first of these is, indeed, unfortunate but ignorable.

The second is, frankly, a complete pain, but likewise (almost) completely avoidable.

PROPOSAL: to make the breaking change for v2.0 that the definition be changed to:

WfRec _<_ P x = ∀ {y} → y < x → P y

together with all of its downstream consequences... including the in-progress #2077 #2082 etc.

[jamesmckinna]

A separate issue exposed by this proposal: in Data.Vec.Relation.Binary.Lex.Strict, the following lemma proposed in #602 and added in #1672 and its immediate corollary (ditto. for List in #1648)

  xs≮[] : ∀ {n} (xs : Vec A n) → ¬ xs < []
  xs≮[] _ (base ())

  ¬[]<[] : ¬ [] < []
  ¬[]<[] = xs≮[] []

should, likewise, make the xs argument implicit. FIXED by #2085

[JacquesCarette]

Both of these explicit proposals make sense to me.

[MatthewDaggitt]

the explicit quantification over y in WfRec, which leads, infectively, to a profusion of (almost-?)always-inferrable arguments when working with subsequent Accessibility and WellFoundedness proofs. FIXED by #2084

I'm not sure I agree with this. What happens when A is a record type and < is a strict partial order over it that only inspects some of the fields? Then you're not going to be able to infer the values of the missing fields right?

[jamesmckinna]

Well, actually, the ...flip... proof introduced in #2077 is an example of the phenomenon, and is handled in #2084 by deploying 2/8 instances where an implicit argument needed to be supplied but can in fact be dealt with by the typechecker. Compared to nearly 90 others in stdlib which justify the 'almost-always-inferrable' claim... so it is a trade-off, to be sure. But your corner case is/seems 'rare' in practice.

UPDATED: detailed comments on the PR. TL;DR: the only uses made are when proving properties of functions defined by wfRec in Induction.WellFounded. It turns out, actually even to my surprise, that all the other uses of the inferrable argument are in fact eliminable!

'In the wild'... I'm not sure.

[jamesmckinna]

So, I have been thinking/trying to think through the substance of @MatthewDaggitt 's critique, and I think there is something I don't understand about his thought experiment: suppose we do define a strict partial order on a record based only on some of its fields. Then, in any subsequent wfRec definition wrt such an ordering, aren't we really defining a recursion on the derived notion of WF for that record type obtained via Relation.Binary.Construct.On.wellFounded?

That is to say, (I think that) there should be no consideration of trying to reconstruct any fields at all: the relevant wellfoundedness obtains by projection, and hence the relevant recursion/recursor only need focus on the fields of the projected record... Or am I (still) missing something here?

The 'tricky' example of Codata.Musical.Colist.infinite-merge (recently fixed as part of merge conflict resolution) seems to bear this out?

[MatthewDaggitt]

That is to say, (I think that) there should be no consideration of trying to reconstruct any fields at all: the relevant wellfoundedness obtains by projection, and hence the relevant recursion/recursor only need focus on the fields of the projected record... Or am I (still) missing something here?

Agreed that's what should be going on! But my question was really is Agda smart enough to realise that it doesn't need to re-infer the "irrelevant" information. The fact that it goes through the library fine, suggests that it is in most cases...

[jamesmckinna]

I'm crossing my fingers!
But non-existence of counterexamples does not constitute proof, alas, only suggestive anecdotal evidence towards the conjecture!