pm.agda

{-# OPTIONS --cubical-compatible --safe #-}
module pm where

open import Level hiding ( suc ; zero )
open import Data.Fin hiding ( _<_  ; _≤_ ; _-_ ; _+_ ; _≟_)
open import Data.Fin.Permutation
open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n )
open import Relation.Binary.PropositionalEquality hiding ( [_] )

open import Relation.Nullary
open import Data.Empty


shlem→ : {n  : ℕ} → (perm : Permutation (suc n) (suc n) ) → (p0=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0 ) → (x : Fin (suc n) ) →  perm ⟨$⟩ˡ x ≡ zero → x ≡ zero
shlem→ perm p0=0 x px=0 = begin
          x                                  ≡⟨ sym ( inverseʳ perm ) ⟩
          perm ⟨$⟩ʳ ( perm ⟨$⟩ˡ x)           ≡⟨ cong (λ k →  perm ⟨$⟩ʳ k ) px=0 ⟩
          perm ⟨$⟩ʳ zero                     ≡⟨ cong (λ k →  perm ⟨$⟩ʳ k ) (sym p0=0) ⟩
          perm ⟨$⟩ʳ ( perm ⟨$⟩ˡ zero)        ≡⟨ inverseʳ perm  ⟩
          zero
       ∎  where open ≡-Reasoning

shlem← : {n  : ℕ} → (perm : Permutation (suc n) (suc n) ) → (p0=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0 ) → (x : Fin (suc n)) → perm ⟨$⟩ʳ x ≡ zero → x ≡ zero
shlem← perm p0=0 x px=0 =  begin
          x                                  ≡⟨ sym (inverseˡ perm ) ⟩
          perm ⟨$⟩ˡ ( perm ⟨$⟩ʳ x )          ≡⟨ cong (λ k →  perm ⟨$⟩ˡ k ) px=0 ⟩
          perm ⟨$⟩ˡ zero                     ≡⟨ p0=0  ⟩
          zero
       ∎  where open ≡-Reasoning

sh2 : {n  : ℕ} → (perm : Permutation (suc n) (suc n) ) → (p0=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0 ) → {x : Fin n} → ¬ perm ⟨$⟩ˡ (suc x) ≡ zero
sh2 perm p0=0 {x} eq with shlem→ perm p0=0 (suc x) eq
sh2 perm p0=0 {x} eq | ()

sh1 : {n  : ℕ} → (perm : Permutation (suc n) (suc n) ) → (p0=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0 ) → {x : Fin n} → ¬ perm ⟨$⟩ʳ (suc x) ≡ zero
sh1 perm p0=0 {x} eq with shlem← perm p0=0 (suc x) eq
sh1 perm p0=0 {x} eq | ()


-- 0 ∷ 1 ∷ 2 ∷ 3 ∷ [] → 0 ∷ 1 ∷ 2 ∷ [] 
shrink : {n  : ℕ} → (perm : Permutation (suc n) (suc n) ) → perm ⟨$⟩ˡ (# 0) ≡ # 0 → Permutation n n
shrink {n} perm p0=0  = permutation p→ p← piso← piso→  where

   p→ : Fin n → Fin n 
   p→ x with perm ⟨$⟩ʳ (suc x) in eq 
   p→ x | zero  = ⊥-elim ( sh1 perm p0=0 {x} eq )
   p→ x | suc t = t

   p← : Fin n → Fin n 
   p← x with perm ⟨$⟩ˡ (suc x) in eq
   p← x | zero  = ⊥-elim ( sh2 perm p0=0 {x} eq )
   p← x | suc t = t

   p01 : (x : Fin n) → ?
   p01 x with perm ⟨$⟩ˡ (suc x) 
   ... | t = ?

   bad1 : (x : Fin n) → Fin (suc n)
   bad1 x = perm ⟨$⟩ˡ (suc x) 


   bad : (x : Fin n) → p← x ≡ ?
   bad with bad1 x
   ... | t = ?
   -- bad x with perm ⟨$⟩ˡ (suc x) 
   -- ... | t = ?


   --  using "with" something binded in ≡ is prohibited
   piso← : (x : Fin n ) → p→ ( p← x ) ≡ x
   piso← x  = ?

   piso→ : (x : Fin n ) → p← ( p→ x ) ≡ x
   piso→ x = ?