Adding permutations on N-indexed Sets aka "Upto Renaming"

[ajrouvoet]

I'm opening this issue to get some early feedback on an addition:
a general notion of applying a Fin permutation to a Nat-indexed term.

record Rename {ℓ₁}(T : ℕ → Set ℓ₁) : Set ℓ₁ where
  field
    rename : ∀ {m n} → Permutation m n → T m → T n

If you prove that rename is well-behaved w.r.t. identity and composition then this provides a notion of "equality upto renaming" for T.

An implementation of this can be found here

One gets permutations of vectors via Renaming as shown here

Feedback is welcome on the design and the placement of the code.

[gallais]

This structure looks a lot like the Thinnable we have in generic-syntax.

Closed is a generalisation of that to any preorder. It would be interesting to see how many generic results we can get for the special case of a Setoid.

We could create Relation.Unary.Closure.Setoid.

[ajrouvoet]

Sounds good. I'd still argue for including this particular instance, because there are many interesting applications and proofs that seem relevant to have. E.g. the interaction between this type of renaming of free variables and Data.Fin.Substitution.

[gallais]

Oh sure, I didn't mean that we should not include this particular instance. But it'd be interesting to see how much of the content we can generalise to closure wrt to any setoid and then see what is left for us to prove about Permutations in particular.

[xekoukou]

I also want to have an equality up to permutation. (though I do not understand your code). The good thing about Fin is that given two non-abstract functions f , g , the proof that they are a bijection can be automated with instance resolution. Thus the burden of proving that f , g are a permutation is reduced a bit since InverseOf is automatic.

With this , we can easily prove equality up to permutation for all permutable data types.

module rol where

open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality hiding (sym)
open import Relation.Nullary
open import Data.Empty
open import Data.Unit hiding (_≤_)
open import Data.Nat hiding (_⊔_)
open import Data.Nat.Properties
open import Data.Fin hiding (_≤_)
open import Function.Inverse hiding (sym)
open import Data.Fin.Permutation
open import Level renaming (zero to lzero ; suc to lsuc ; Lift to ℓ↑)

it : {A : Set} → {{a : A}} → A
it {{a}} = a

data _≤ᵢ_ : Rel ℕ 0ℓ where
  instance
    z≤n : ∀ {n}                   → zero  ≤ᵢ n
    s≤s : ∀ {m n} {{m≤n : m ≤ᵢ n}} → suc m ≤ᵢ suc n

≤ᵢ-to-≤ : ∀{a b} → a ≤ᵢ b → a ≤ b 
≤ᵢ-to-≤ z≤n = z≤n
≤ᵢ-to-≤ s≤s = s≤s (≤ᵢ-to-≤ it)

≤-to-≤ᵢ : ∀{a b} → a ≤ b → a ≤ᵢ b
≤-to-≤ᵢ z≤n = z≤n
≤-to-≤ᵢ (s≤s x) = s≤s {{≤-to-≤ᵢ x}}

data SInverseFin {k} (f g : Fin (suc k) → Fin (suc k)) : (m : ℕ) → {{m≤k : m ≤ᵢ k}} → Set where
  instance
    pzero : {{eq : f (g zero) ≡ zero }} → SInverseFin f g zero
    psuc : ∀{a} → {{sa≤k : suc a ≤ᵢ k}} → let fn = fromℕ≤ (s≤s (≤ᵢ-to-≤ sa≤k)) in {{eq : f (g fn) ≡ fn }}
           → let e = ≤-to-≤ᵢ (≤⇒pred≤ (≤ᵢ-to-≤ sa≤k)) in {{ind : SInverseFin f g a {{e}}}} → SInverseFin f g (suc a)

SInverseFin′ : ∀{k} (f g : Fin (suc k) → Fin (suc k)) → (m : ℕ) → m ≤ k → Set
SInverseFin′ f g m x = SInverseFin f g m {{≤-to-≤ᵢ x}}

r : ∀{k} → {f g : Fin (suc k) → Fin (suc k)} → (m : ℕ) → (m≤k : m ≤ k) → SInverseFin′ f g k ≤-refl
    → f (g (fromℕ≤ (s≤s m≤k) )) ≡ fromℕ≤ (s≤s m≤k)
r {k} {f} {g} m m≤k x = t k (k ∸ m) (m∸[m∸n]≡n m≤k) ≤-refl x m≤k where
  t : ∀ nk l → nk ∸ l ≡ m → (nk≤k : nk ≤ k) → SInverseFin′ f g nk nk≤k
      → (m≤k : m ≤ k) → f (g (fromℕ≤ (s≤s m≤k) )) ≡ fromℕ≤ (s≤s m≤k)
  t zero zero refl z≤n pzero z≤n = it
  t zero (suc l) refl z≤n pzero z≤n = it
  t (suc nk) zero refl nklk psuc mlk
    = subst (λ z → f (g (fromℕ≤ (s≤s z))) ≡ fromℕ≤ (s≤s z)) (≤-irrelevance ((≤ᵢ-to-≤ (≤-to-≤ᵢ nklk))) mlk) it
  t (suc nk) (suc l) neq (s≤s nklk) (psuc {{sa≤k}} {{ind = ind}}) mlk = t nk l neq (≤-step nklk) w mlk where
    w = subst (λ z → SInverseFin′ f g nk z) (≤-irrelevance (≤-trans (≤-step (≤-reflexive refl))
                                                              (s≤s (≤ᵢ-to-≤ (≤-to-≤ᵢ nklk)))) (≤-step nklk)) ind

w : ∀{k} → (x : Fin (suc k)) → toℕ x ≤ k 
w zero = z≤n
w {zero} (suc ())
w {suc k} (suc x) = s≤s (w x)

e : ∀{k} → (x : Fin (suc k)) → fromℕ≤ (s≤s (w x)) ≡ x
e zero = refl
e {zero} (suc ())
e {suc k} (suc x) = cong suc (e x)

open _InverseOf_

invOf : ∀{k} → (f g : Fin (suc k) → Fin (suc k)) → SInverseFin′ f g k ≤-refl → SInverseFin′ g f k ≤-refl →
              (→-to-⟶ f) InverseOf (→-to-⟶ g)
left-inverse-of (invOf f g sinv sinv′) x = subst (λ z → f (g z) ≡ z) (e x) (r {f = f} {g} (toℕ x) (w x) sinv) 
right-inverse-of (invOf f g sinv sinv′) x =  subst (λ z → g (f z) ≡ z) (e x) (r {f = g} {f} (toℕ x) (w x) sinv′) 

-- Example

g : Fin 3 → Fin 3
g zero = suc zero
g (suc zero) = suc (suc zero)
g (suc (suc zero)) = zero
g (suc (suc (suc ())))

f : Fin 3 → Fin 3
f zero = suc (suc zero)
f (suc zero) = zero
f (suc (suc zero)) = suc zero
f (suc (suc (suc ())))

fgSI : SInverseFin f g (suc (suc zero))
fgSI = it

gfSI : SInverseFin g f (suc (suc zero))
gfSI = it

re : (→-to-⟶ f) InverseOf (→-to-⟶ g)
re = invOf f g fgSI gfSI

[ajrouvoet]

@xekoukou the equality up to permutation is part of the code I linked and is called _≈_.