Some lemmas to do with transposition lists #1744
Conversation
src/Data/Fin/Permutation.agda
Outdated
| @@ -223,6 +223,13 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′ | |||
| ------------------------------------------------------------------------ | |||
| -- Other properties | |||
|
|
|||
| transpose-self-inverse : ∀ (i j : Fin n) → transpose i j ≈ transpose j i | |||
There was a problem hiding this comment.
Also it's not in the CHANGELOG
There was a problem hiding this comment.
It's more of a commutativity property than a symmetry property (the type is the same as Commutative _≈_ transpose I think, modulo unresolved metas). Would you be OK with transpose-comm?
There was a problem hiding this comment.
Since #1914 why not call this transpose-selfInverse?
Hmm... not exactly, but I would in any case be tempted to prove (transpose i j) ⁻¹ = transpose j i as well?
|
|
||
| TranspositionList : ℕ → Set | ||
| TranspositionList n = List (Fin n × Fin n) | ||
| TranspositionList n = List (Σ[ i ∈ Fin n ] ∃[ j ] i ≢ j) |
There was a problem hiding this comment.
Maybe List (∃₂ λ i j → i ≢ j)? Could also write (∃₂ _≢_) but I'm not sure how clear that is?
There was a problem hiding this comment.
You need a hint that they have type Fin n rather than some other type, sadly.
There was a problem hiding this comment.
List (∃₂ λ (i j : Fin n) → i ≢ j) then?
|
|
||
| ------------------------------------------------------------------------ | ||
| -- Operations on transposition lists | ||
|
|
||
| lift₀ : TranspositionList n → TranspositionList (suc n) | ||
| lift₀ xs = map (λ (i , j) → (suc i , suc j)) xs | ||
| lift₀ xs = map (λ (i , j , i≢j) → (suc i , suc j , λ si≡sj → i≢j (suc-injective si≡sj))) xs |
There was a problem hiding this comment.
Maybe i≢j ∘ suc-injective instead?
|
Apologies for taking so long for a review! |
|
@Taneb any progress on this? |
|
I started addressing the comments, but I've been very distracted lately (and have broken my wrist in the meantime). I don't know when I can get back to it |
|
Oh no, sorry to hear that! I can see why that'd make typing a little difficulty. Okay no worries, I'll leave it up and see if I have the time to fiddle with it in the meantime.... |
|
|
||
| TranspositionList : ℕ → Set | ||
| TranspositionList n = List (Fin n × Fin n) | ||
| TranspositionList n = List (∃₂ λ (i j : Fin n) → i ≢ j) |
There was a problem hiding this comment.
Hmm I'm sorry to reopen the discussion, but looking at this with a fresh pair of eyes, wouldn't a more modular and reusable solution be to keep the definition as is and then define a predicate:
NonTrivialEntries : TranspositionList n → Set
NonTrivialEntries xs = All (curry _≢_) xs
which could then be taken as an argument in the proofs that need it. The advantages of this would be:
- Preserves backwards compatibility
- Provides more choice to the user - I can imagine a scenario where the reflexive entries do hold semantic information.
- Allows us to reuse lemmas from
Data.List.Relation.Unary.All
I'm open to suggestions about the name NonTrivialEntries?
There was a problem hiding this comment.
I really want to argue against this, but the truth is that for everything currently existing, that the transposition list has no trivial entries is completely irrelevant. I think the right thing to do for now might be to not talk about that constraint until we've got something that actually uses it.
There was a problem hiding this comment.
Yup, happy with that solution!
There was a problem hiding this comment.
So what needs to be done to implement that solution?
|
Now that #1852 is in, I'd like to continue work on this PR to where I wanted to get it to, proving that there's a group homomorphism from permutations to their parity (this will let us define alternating groups and is useful for implementing Liebniz's formula for matrix determinants) |
Taneb
force-pushed
the
transposition-stuff
branch
from
40e4888 to
cf1451b
Compare
| @@ -28,17 +28,32 @@ open ≡-Reasoning | |||
|
|
|||
| -- 'tranpose i j' swaps the places of 'i' and 'j'. | |||
|
|
|||
| {- | |||
There was a problem hiding this comment.
Remove this commented-out code before actually merging.
|
|
||
| -------------------------------------------------------------------------------- | ||
| -- Properties | ||
| -------------------------------------------------------------------------------- | ||
|
|
||
| transpose-comm : ∀ {n} (i j : Fin n) → transpose i j ≗ transpose j i |
There was a problem hiding this comment.
This is now both here and in Data.Fin.Permutation. I think here is a better place for it.
|
|
||
| TranspositionList : ℕ → Set | ||
| TranspositionList n = List (Fin n × Fin n) | ||
| TranspositionList n = List (∃₂ λ (i j : Fin n) → i ≢ j) |
There was a problem hiding this comment.
So what needs to be done to implement that solution?
| prop : transpose i j ∘ₚ transpose iₕ jₕ ∘ₚ eval xs ≈ eval xs | ||
| prop k rewrite iₕ≡j rewrite jₕ≡i = cong (eval xs ⟨$⟩ʳ_) (PC.transpose-inverse j i) | ||
|
|
||
| {- |
There was a problem hiding this comment.
delete commented out code
| @@ -75,6 +75,9 @@ module _ {x y : A} {xs ys : List A} where | |||
| ≡-dec _≟_ [] (y ∷ ys) = no λ() | |||
| ≡-dec _≟_ (x ∷ xs) (y ∷ ys) = ∷-dec (x ≟ y) (≡-dec _≟_ xs ys) | |||
|
|
|||
| length[xs]≡0⇒xs≡[] : {xs : List A} → length xs ≡ 0 → xs ≡ [] | |||
There was a problem hiding this comment.
Personally I would decouple this simple property from this PR and make it a separate tiny PR.
|
@Taneb I'm afraid in the end I didn't get a chance to look at it, and no real prospect of it happening soon. Any likelihood of you picking this backup in the next month? Otherwise I propose to close. |
|
It's always been on my to-do list, but I want it to include the parity theorem. Feel free to close it and I'll open a new PR when it's ready |
|
Or you could rebase this PR and then subsequently re-open once you have Parity working...? |
This is largely preliminaries for #1741, which I'm still playing with how to implement.