[ refactor ] Data.Fin.Properties of decidable equality, plus knock-ons
#2740
Conversation
|
In the absence of a review yet, I'll lift out the bug fixes as a separate PR, as per @JacquesCarette 's comment on #2743 |
| punchOut {i = i} {πˡ (πʳ (punchIn i j))} _ ≡⟨ punchOut-cong i (inverseˡ π) ⟩ | ||
| punchOut {i = i} {punchIn i j} _ ≡⟨ punchOut-punchIn i ⟩ | ||
| j ∎ | ||
| from (to j) |
There was a problem hiding this comment.
I know the original is likely too wide, but it is oh so much more readable! Could we refrain from reformatting in those cases?
There was a problem hiding this comment.
Ok, but I can't help but disagree, not Keats given that in Feijen's original presentation, the justifications were indeed supposed to be interleaved with the expressions being calculated. The long lines break any kind of readability.
But happy to revert against a downstream discussion issue/PR.
| punchOut {i = πʳ i} {πʳ (πˡ (punchIn (πʳ i) j))} _ ≡⟨ punchOut-cong (πʳ i) (inverseʳ π) ⟩ | ||
| punchOut {i = πʳ i} {punchIn (πʳ i) j} _ ≡⟨ punchOut-punchIn (πʳ i) ⟩ | ||
| j ∎ | ||
| to (from j) |
| @@ -42,17 +35,31 @@ transpose i j k with does (k ≟ i) | |||
| -- Properties | |||
| ------------------------------------------------------------------------ | |||
|
|
|||
| transpose-iij : ∀ {n} (i j : Fin n) → transpose i i j ≡ j | |||
| transpose-iij i j with j ≟ i in j≟i | |||
| ... | true because [j≡i] = sym (invert [j≡i]) | |||
There was a problem hiding this comment.
since you're actually using the proof here, does laziness (i.e. avoiding yes) matter?
| ≡-irrelevant : Irrelevant {A = Fin n} _≡_ | ||
| ≡-irrelevant = Decidable⇒UIP.≡-irrelevant _≟_ | ||
|
|
||
| ≟-diag : (eq : i ≡ j) → (i ≟ j) ≡ yes eq |
There was a problem hiding this comment.
I almost commented on the CHANGELOG that surely these lemmas are instances of things that are true about combinations of Decidable and Irrelevant, but decided to wait until I saw the proofs... and indeed.
So, do these pay for themselves? I do agree that at the use-site, it sure looks nicer. I'm inclined to say yes.
| @@ -110,6 +110,12 @@ m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n)) | |||
| ≟-diag : (eq : m ≡ n) → (m ≟ n) ≡ yes eq | |||
| ≟-diag = ≡-≟-identity _≟_ | |||
|
|
|||
| ≟-diag-refl : ∀ n → (n ≟ n) ≡ yes refl | |||
| ≟-diag-refl _ = ≟-diag refl | |||
There was a problem hiding this comment.
This one, on the other hand, seems to fail the Fairbairn test.
There was a problem hiding this comment.
Well, the reflexive case us what I use for Fin, and I dislike having the APIs for Nat and Fin diverging... what is really prefer would be to only have diag refer to the refl version but... legacy!
This PR supersedes the knock-on changes for
Permutationin #2738 and adds some new lemmas abouttransposewhich simplify the dependency graph. The contribution can be seen as a belated corollary to the changes introduced in #645 / #1732 .Downstream, we might want to revisit the dependency graph now between
Relation.Nullary.DecidableAxiom.UniquenessOfIdentityProofsRelation.Binary.PropositionalEqualityin putting these pieces together?
Outstanding (naming) issue: I followed the existing
Data.Nat.Properties.≟-diagconvention inData.Fin.Properties, and then backported thereflinstantiation of this toData.Nat.Properties.≟-diag-refl... but it occurs to me that it's hard to imagine instances of≟-diagwhich would use a general equality, and even if they were to, the use ofdiagought (?) to be a codeword for a repeated argument/reflexive equality? I just couldn't face the deprecation headache though... so a v3.0 downstreambreakingchange might be in order?