[ refactor ] make n≢i : n ≢ toℕ i argument to lower₁ irrelevant
#2783
Conversation
| @@ -561,6 +561,17 @@ lower-injective {n = suc n} zero zero eq = refl | |||
| lower-injective {n = suc n} (suc i) (suc j) eq = | |||
| cong suc (lower-injective i j (suc-injective eq)) | |||
|
|
|||
| lower₁≗lower : ∀ (i : Fin (suc n)) .(n≢i : n ≢ toℕ i) → | |||
There was a problem hiding this comment.
These lemmas feel odd: basically saying lower₁ is the same as lower with 2nd argument an utter mess. Can't that argument be replaced with something much more generic, i.e. because here too we shouldn't care exactly what proof we get of that fact?
There was a problem hiding this comment.
Maybe, but we want something that will typecheck with toℕ i < n in a context where all we know is n≢i : n ≢ toℕ i... the fact that the actual form is irrelevant is part of the reason to want dotted hypotheses, but we still have to be able to instantiate them!
Is this an argument in favour of irrelevant instances instead? A more drastic change in the type signature, though...
There was a problem hiding this comment.
In a way, the two lemmas are really the justification for subsequent deprecation of lower₁, but I held off doing so for now. Happy to be nudged towards that path, though!?
There was a problem hiding this comment.
If these lemmas are, in a sense, meta-theorems that justify something else, but not really important / useful on their own, then I'd erase them from the library and put them only in the github-level comments for the PR that deprecates lower₁
jamesmckinna
added
the
status: blocked-by-issue
PRs #2725 / #2748 made me rethink whether
Data.Fin.Base.lower₁is fit-for-purpose (as an inverse toinject₁), or could instead be deprecated in favour of the newData.Fin.Base.lower...This PR doesn't entirely solve that issue, but does prove the two definitions extensionally equal on their domains, as a consequence, perhaps more importantly, of weakening the type of
lower₁so that its precondition is made irrelevant.Two (possibly more downstream) knock-on consequences:
lemmaavoided in favour of [ refactor ] weaken type oflower₁-¬0≢0 : ∀ {ℓ} {A : Set ℓ} → .(0 ≢ 0) → Aencapsulates a repeated pattern of (¬-recompute) reasoning, which ideally would be madeprivate, but is needed in bothBaseandProperties... so, reluctantly, has been added;Relation.Nullary.Negation.Core.contradiction-irr#2785 on which this PR is nowblocked.lower₁could/should be simplified by delegation to those forlower...?Data.Fin.Base.punchOutand its properties could similarly be weakened by making itsi≢j : i ≢ jargument irrelevant! What else might be susceptible to this kind of refactoring?NB. As observed/observable in
README.Data.Fin.Relation.Unary.Top, we can actually avoid having any uses oflower₁in the library, sodeprecationseems possible/desirable?