[ refactor ] make i ≢ j argument to Data.Fin.Base.punchOut irrelevant

[jamesmckinna]

Another downstream consequence of #2785 .
This time the ergonomics are slightly less clear as to whether this improves matters, but the definitional proof-irrelevance pays off in a couple of places, but with a corresponding need to be explicit about the exact proof of inequality in others. Perhaps these proofs can all be simplified further, but I went for the minimal fixes necessary.
UPDATED Perhaps they can! (See below)

I think, as @JacquesCarette touches on below, the real reason this might be problematic is that we end up with a function of three arguments, two of which are implicit, and the third of which is now irrelevant, so it's perhaps not so surprising that in various places, Agda needs a nudge to be able to figure things out...

UPDATED: wait on the merge of #2794 in order to be able to simplify proofs of monotonicity as well...? DONE

[JacquesCarette]

I'm torn over this one. The code is fine. It's the pain that goes along with the design that's causing me to have doubts.

It seems that Agda is much weaker at inferring irrelevant things, so by explicitly making some things irrelevant, we're making our lives harder. So I wonder if the extra precision is worth the pain.

[jamesmckinna]

I'm torn over this one. The code is fine. It's the pain that goes along with the design that's causing me to have doubts.

It seems that Agda is much weaker at inferring irrelevant things, so by explicitly making some things irrelevant, we're making our lives harder. So I wonder if the extra precision is worth the pain.

I, too, am torn. I think that it is in any case instructive to uncover such gnarly cases... but on balance, I think the equations proofs that do fall to refl outweigh the cost. But you might be right!

UPDATED: some sleep, and reconsideration, shows that the old proofs can be simplified! Indeed, I've begun to wonder if the right refactoring would go all the way, and simply have

punchOut-cong : ∀ (i : Fin (suc n)) {j k} .{i≢j : i ≢ j} .{i≢k : i ≢ k} →
                j ≡ k → punchOut i≢j ≡ punchOut i≢k
punchOut-cong i refl = refl

and with it the deprecation of punchOut-cong′, instead of the ornate case analysis currently, which nevertheless (still?) seems necessary for punchOut-injective etc.

[JacquesCarette]

The cleaned up proofs are very nice. But still dubious overall.

[jamesmckinna]

The cleaned up proofs are very nice. But still dubious overall.

Well, do matters improve if instead we deprecate the existing version of punchOut in favour of one of type

punchOut : ∀ (i j : Fin (suc n)) → .(i ≢ j) → Fin n

or even

punchOut-< : ∀ (i j : Fin (suc n)) → .(i < j) → Fin n

?

[MatthewDaggitt]

This is definitely a breaking change right as you're forced to change the types of e.g. punchOut-cong?

Is there anyway we can see the actual breaking changes (i.e. those that we're forced to make from this change) vs the additional refactoring that is unlocked by this?

[jamesmckinna]

@MatthewDaggitt writes:

This is definitely a breaking change right as you're forced to change the types of e.g. punchOut-cong?

Well, on that basis, so too is the type of the function itself changed?

I think that this is (yet) another instance where the line between

• bug fix (the type was too specific before, and this was a mistake)
• non-backwards-compatible (the type was too specific before, and we've changed it, with... consequences)
• breaking (we changed it, and client code actually breaks)

seems a bit hard for me to draw, and hence whether it should be v2.4 or v3.0?

Is there anyway we can see the actual breaking changes (i.e. those that we're forced to make from this change) vs the additional refactoring that is unlocked by this?

Oooh, that's tricky. Hmmm... scratches head!? I might have make a clean version, and see what breaks?
The additional refactoring is in fact quite small: two steps of equational reasoning become ≡⟨⟩ (corresponding to a punchOut-cong ... refl), but that's because I didn't (yet) push harder on what else might be possible?