[ refactor ] Data.Fin.Properties following #2746

[jamesmckinna]

UPDATED:

• no CHANGELOG required! Only existing proofs have been refactored.
• issue below resolved moderately successfully via @andreasabel 's trick with flip contradiction cf. [ add ] new name for flipped version of Relation.Nullary.Negation.Core.contradiction #2784

NB. I tried to simplify the proof of injective⇒existsPivot to use <⇒notInjective instead, but it causes a weird explicit/implicit type inference error when trying to obtain a contradiction from f∘inject!-injective and <⇒notInjective...:

injective⇒existsPivot {f = f} f-injective i
  with any? (λ j → j ≤? i ×-dec i ≤? f j)
... | yes result = result
... | no ¬result = contradiction f∘inject!-injective (<⇒notInjective {f = f∘inject! } (ℕ.n<1+n (toℕ i)))
  where
  ...

yields

/home/james/RESEARCH/Agda-stdlib-dev-v2.3/src/Data/Fin/Properties.agda:1077.55-104: error: [UnequalHiding]
f∘inject! _x_4739 ≡ f∘inject! _y_4740 → _x_4739 ≡ _y_4740 !=
{x y : Fin (toℕ (suc i))} → f∘inject! x ≡ f∘inject! y → x ≡ y
because one is an implicit function type and the other is an
explicit function type
when checking that the expression
<⇒notInjective {f = f∘inject!} (ℕ.n<1+n (toℕ i)) has type
¬ (f∘inject! _x_4739 ≡ f∘inject! _y_4740 → _x_4739 ≡ _y_4740)

(this kind of thing really aggravates me: we have two sub-proofs of a : A and ¬a : ¬ A here, with A = Injective _≡_ _≡_ f∘inject!, but (re-)typechecking contradiction a ¬a causes a type error... :-( See agda/agda#8026

[JacquesCarette]

I'm fairly sure the reason for the error is that Agda eagerly inserts leading implicits but does not insert any past an explicit parameter. So 'indexed' cases such as this would possibly need its own version of 'indexed contradiction`.

[jamesmckinna]

I'm fairly sure the reason for the error is that Agda eagerly inserts leading implicits but does not insert any past an explicit parameter. So 'indexed' cases such as this would possibly need its own version of 'indexed contradiction`.

Well... maybe, but that's bad? (from a user/UX perspective? it might be tolerable from a developer perspective, but I don't think it should be...)

[JacquesCarette]

The follow-ups on the Agda issue shed quite a lot of light on this (and confirm my rough guess). Andreas' latest message agrees that the UX is bad, but that there are non-trivial technical reasons for it. And a nifty work-around!

[jamesmckinna]

Blocking on #2784 for the time being. Removed the block, so that the use of flip contradiction can instead be refactored in the course of that PR...