Skip to content

Instantly share code, notes, and snippets.

@AndrasKovacs
Last active April 5, 2020 09:56
Show Gist options
  • Save AndrasKovacs/0d7bcc3aba513c29ef73 to your computer and use it in GitHub Desktop.
Save AndrasKovacs/0d7bcc3aba513c29ef73 to your computer and use it in GitHub Desktop.
Permutation relation in Agda. In the indiuctive definition we have insertions on both sides, as opposed to one side. This makes the transitivity proof *horrible* (or at least I couldn't do better).
open import Data.List
open import Data.Nat
open import Relation.Binary.PropositionalEquality
open import Function
open import Data.Product
open import Data.Sum
data _▶_≡_ {A : Set}(x : A) : List A → List A → Set where
here : ∀ {xs} → x ▶ xs ≡ (x ∷ xs)
there : ∀ {y xs ys} → x ▶ xs ≡ ys → x ▶ (y ∷ xs) ≡ (y ∷ ys)
data Perm {A : Set} (xs : List A) : List A → Set where
refl : Perm xs xs
ins : ∀ {x ys xs' ys'} → Perm xs' ys' → x ▶ xs' ≡ xs → x ▶ ys' ≡ ys → Perm xs ys
▶-inv :
∀ {A}{a : A}{b as bs cs}
→ a ▶ as ≡ cs
→ b ▶ bs ≡ cs
→ (a ≡ b × as ≡ bs) ⊎ (∃ λ ds → b ▶ ds ≡ as × a ▶ ds ≡ bs)
▶-inv here here = inj₁ (refl , refl)
▶-inv here (there p2) = inj₂ (_ , p2 , here)
▶-inv (there p1) here = inj₂ (_ , here , p1)
▶-inv (there p1) (there p2) with ▶-inv p1 p2
... | inj₁ (refl , refl) = inj₁ (refl , refl)
... | inj₂ (ds , ias , ibs) = inj₂ (_ ∷ ds , there ias , there ibs)
▶-exch :
∀ {A}{x : A}{y xs xxs yxxs}
→ x ▶ xs ≡ xxs → y ▶ xxs ≡ yxxs → ∃ λ yxs → (y ▶ xs ≡ yxs) × (x ▶ yxs ≡ yxxs)
▶-exch p1 here = _ , here , there p1
▶-exch here (there p2) = _ , p2 , here
▶-exch (there p1) (there p2) with ▶-exch p1 p2
... | _ , p1' , p2' = _ , there p1' , there p2'
l1 : ∀ {A x xs xys} → Perm {A} (x ∷ xs) xys → ∃ λ ys → x ▶ ys ≡ xys × Perm xs ys
l1 refl = _ , here , refl
l1 (ins p here iys) = _ , iys , p
l1 (ins p (there ixs) iys) with l1 p
l1 {x = x}(ins {x = y}p (there ixs) iys) | ys , i , perm with ▶-exch i iys
l1 (ins p (there ixs) iys) | ys , i , perm | proj₁ , proj₂ , proj₃
= proj₁ , proj₃ , ins perm ixs proj₂
▶-len : ∀ {A}{x : A}{xs ys} → x ▶ xs ≡ ys → suc (length xs) ≡ length ys
▶-len here = refl
▶-len (there p) rewrite ▶-len p = refl
extract-perm :
∀ {A x xs xys xxs}
→ (l : ℕ)
→ length xxs ≡ l
→ x ▶ xs ≡ xxs
→ Perm {A} xxs xys
→ ∃ λ ys → (x ▶ ys ≡ xys) × (Perm xs ys)
extract-perm zero () here p2
extract-perm zero () (there p1) p2
extract-perm (suc l) lp here refl = _ , here , refl
extract-perm (suc l) lp here (ins p2 here iys) = _ , iys , p2
extract-perm (suc l) lp here (ins p2 (there ixs) iys) with l1 p2
... | proj₁ , proj₂ , proj₃ with ▶-exch proj₂ iys
extract-perm (suc l) lp here (ins p2 (there ixs) iys) | proj₁ , proj₂ , proj₆ | proj₃ , proj₄ , proj₅
= proj₃ , proj₅ , ins proj₆ ixs proj₄
extract-perm (suc l) lp (there p1) refl = _ , there p1 , refl
extract-perm (suc l) lp (there p1) (ins p2 here iys) with extract-perm l (cong pred lp) p1 p2
extract-perm (suc l) lp (there p1) (ins p2 here iys) | proj₁ , proj₂ , proj₃ with ▶-exch proj₂ iys
extract-perm (suc l) lp (there p1) (ins p2 here iys) | proj₁ , proj₂ , proj₆ | proj₃ , proj₄ , proj₅
= proj₃ , proj₅ , ins proj₆ here proj₄
extract-perm (suc l) lp (there p1) (ins p2 (there ixs) iys) with ▶-inv p1 ixs
extract-perm (suc l) lp (there p1) (ins p2 (there ixs) iys) | inj₁ (refl , refl) = _ , iys , p2
extract-perm (suc l) lp (there p1) (ins p2 (there ixs) iys) | inj₂ (proj₁ , proj₂ , proj₃) with l1 p2
extract-perm (suc zero) lp (there {y} {xs₁} {[]} p1) (ins p2 (there ()) iys) | inj₂ (proj₄ , proj₅ , proj₆) | proj₁ , proj₂ , proj₃
extract-perm (suc zero) () (there {y} {xs₁} {x₁ ∷ ys} p1) (ins p2 (there ixs) iys) | inj₂ (proj₄ , proj₅ , proj₆) | proj₁ , proj₂ , proj₃
extract-perm (suc (suc l)) lp (there p1) (ins p2 (there ixs) iys) | inj₂ (proj₄ , proj₅ , proj₆) | proj₁ , proj₂ , proj₃ with extract-perm l (cong pred $ trans (▶-len ixs) (cong pred lp)) proj₆ proj₃
extract-perm (suc (suc l)) lp (there p1) (ins p2 (there ixs) iys) | inj₂ (proj₄ , proj₉ , proj₆) | proj₁ , proj₈ , proj₃ | proj₂ , proj₅ , proj₇ with ▶-exch proj₅ proj₈
extract-perm (suc (suc l)) lp (there p1) (ins p2 (there ixs) iys) | inj₂ (proj₉ , proj₁₂ , proj₁₀) | proj₁ , proj₈ , proj₇ | proj₂ , proj₅ , proj₁₁ | proj₃ , proj₄ , proj₆ with ▶-exch proj₆ iys
extract-perm (suc (suc l)) lp (there p1) (ins p2 (there ixs) iys) | inj₂ (proj₁₂ , proj₁₅ , proj₁₃) | proj₅ , proj₉ , proj₁₁ | proj₇ , proj₈ , proj₁₄ | proj₃ , proj₁₀ , proj₆ | proj₁ , proj₂ , proj₄ = proj₁ , proj₄ , ins (ins proj₁₄ here proj₁₀) (there proj₁₅) proj₂
perm-sym : ∀ {A xs ys} → Perm {A} xs ys → Perm ys xs
perm-sym refl = refl
perm-sym (ins p ix iy) = ins (perm-sym p) iy ix
perm-trans : ∀ {A xs ys zs} → Perm {A} xs ys → Perm ys zs → Perm xs zs
perm-trans refl p2 = p2
perm-trans p1 refl = p1
perm-trans {ys = ys} (ins xy ix iy) p2 with extract-perm (length ys) refl iy p2
perm-trans (ins xy ix iy) p2 | proj₁ , proj₂ , proj₃ = ins (perm-trans xy proj₃) ix proj₂
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment