module bijection-syntax.Bijection-Fin where
open import Type
open import bijection-syntax.Bijection
open import Function.NP hiding (Cmp)
open import Relation.Binary.PropositionalEquality
open import Data.Empty
open import Data.Nat.NP
open import Data.Two
open import Data.Fin using (Fin ; zero ; suc ; fromℕ ; inject₁)
open import Data.Vec hiding ([_])
data `Syn : ℕ → ★ where
`id : ∀ {n} → `Syn n
`swap : ∀ {n} → `Syn (2 + n)
`tail : ∀ {n} → `Syn n → `Syn (1 + n)
_`∘_ : ∀ {n} → `Syn n → `Syn n → `Syn n
`Rep = Fin
`Ix = ℕ
`Tree : ★ → `Ix → ★
`Tree X = Vec X
`fromFun : ∀ {i X} → (`Rep i → X) → `Tree X i
`fromFun = tabulate
`toFun : ∀ {i X} → `Tree X i → (`Rep i → X)
`toFun T zero = head T
`toFun T (suc i) = `toFun (tail T) i
`toFun∘fromFun : ∀ {i X}(f : `Rep i → X) → f ≗ `toFun (`fromFun f)
`toFun∘fromFun f zero = refl
`toFun∘fromFun f (suc i) = `toFun∘fromFun (f ∘ suc) i
fin-swap : ∀ {n} → Endo (Fin (2 + n))
fin-swap zero = suc zero
fin-swap (suc zero) = zero
fin-swap (suc (suc i)) = suc (suc i)
fin-tail : ∀ {n} → Endo (Fin n) → Endo (Fin (1 + n))
fin-tail f zero = zero
fin-tail f (suc i) = suc (f i)
`evalArg : ∀ {i} → `Syn i → Endo (`Rep i)
`evalArg `id = id
`evalArg `swap = fin-swap
`evalArg (`tail f) = fin-tail (`evalArg f)
`evalArg (S `∘ S₁) = `evalArg S ∘ `evalArg S₁
vec-swap : ∀ {n}{X : ★} → Endo (Vec X (2 + n))
vec-swap xs = head (tail xs) ∷ head xs ∷ tail (tail xs)
vec-tail : ∀ {n}{X : ★} → Endo (Vec X n) → Endo (Vec X (1 + n))
vec-tail f xs = head xs ∷ f (tail xs)
`evalTree : ∀ {i X} → `Syn i → Endo (`Tree X i)
`evalTree `id = id
`evalTree `swap = vec-swap
`evalTree (`tail f) = vec-tail (`evalTree f)
`evalTree (S `∘ S₁) = `evalTree S ∘ `evalTree S₁
`eval-proof : ∀ {i X} S (T : `Tree X i) → `toFun T ≗ `toFun (`evalTree S T) ∘ `evalArg S
`eval-proof `id T i = refl
`eval-proof `swap T zero = refl
`eval-proof `swap T (suc zero) = refl
`eval-proof `swap T (suc (suc i)) = refl
`eval-proof (`tail S) T zero = refl
`eval-proof (`tail S) T (suc i) = `eval-proof S (tail T) i
`eval-proof (S `∘ S₁) T i rewrite
`eval-proof S₁ T i |
`eval-proof S (`evalTree S₁ T) (`evalArg S₁ i) = refl
`inv : ∀ {i} → Endo (`Syn i)
`inv `id = `id
`inv `swap = `swap
`inv (`tail S) = `tail (`inv S)
`inv (S `∘ S₁) = `inv S₁ `∘ `inv S
`inv-proof : ∀ {i} → (S : `Syn i) → `evalArg S ∘ `evalArg (`inv S) ≗ id
`inv-proof `id x = refl
`inv-proof `swap zero = refl
`inv-proof `swap (suc zero) = refl
`inv-proof `swap (suc (suc x)) = refl
`inv-proof (`tail S) zero = refl
`inv-proof (`tail S) (suc x) rewrite `inv-proof S x = refl
`inv-proof (S `∘ S₁) x rewrite
`inv-proof S₁ (`evalArg (`inv S) x) |
`inv-proof S x = refl
`RC : ∀ {i} → Cmp (`Rep i)
`RC zero zero = eq
`RC zero (suc j) = lt
`RC (suc i) zero = gt
`RC (suc i) (suc j) = `RC i j
insert : ∀ {n X} → Cmp X → X → Vec X n → Vec X (1 + n)
insert X-cmp x [] = x ∷ []
insert X-cmp x (x₁ ∷ xs) with X-cmp x x₁
insert X-cmp x (x₁ ∷ xs) | lt = x ∷ x₁ ∷ xs
insert X-cmp x (x₁ ∷ xs) | eq = x ∷ x₁ ∷ xs
insert X-cmp x (x₁ ∷ xs) | gt = x₁ ∷ insert X-cmp x xs
`sort : ∀ {i X} → Cmp X → Endo (`Tree X i)
`sort X-cmp [] = []
`sort X-cmp (x ∷ xs) = insert X-cmp x (`sort X-cmp xs)
insert-syn : ∀ {n X} → Cmp X → X → Vec X n → `Syn (1 + n)
insert-syn X-cmp x [] = `id
insert-syn X-cmp x (x₁ ∷ xs) with X-cmp x x₁
insert-syn X-cmp x (x₁ ∷ xs) | lt = `id
insert-syn X-cmp x (x₁ ∷ xs) | eq = `id
insert-syn X-cmp x (x₁ ∷ xs) | gt = `tail (insert-syn X-cmp x xs) `∘ `swap
`sort-syn : ∀ {i X} → Cmp X → `Tree X i → `Syn i
`sort-syn X-cmp [] = `id
`sort-syn X-cmp (x ∷ xs) = insert-syn X-cmp x (`sort X-cmp xs) `∘ `tail (`sort-syn X-cmp xs)
insert-proof : ∀ {n X}(X-cmp : Cmp X) x (T : Vec X n) → insert X-cmp x T ≡ `evalTree (insert-syn X-cmp x T) (x ∷ T)
insert-proof X-cmp x [] = refl
insert-proof X-cmp x (x₁ ∷ T) with X-cmp x x₁
insert-proof X-cmp x (x₁ ∷ T) | lt = refl
insert-proof X-cmp x (x₁ ∷ T) | eq = refl
insert-proof X-cmp x (x₁ ∷ T) | gt rewrite insert-proof X-cmp x T = refl
`sort-proof : ∀ {i X}(X-cmp : Cmp X)(T : `Tree X i) → `sort X-cmp T ≡ `evalTree (`sort-syn X-cmp T) T
`sort-proof X-cmp [] = refl
`sort-proof X-cmp (x ∷ T) rewrite
sym (`sort-proof X-cmp T)= insert-proof X-cmp x (`sort X-cmp T)
module Alt-Syn where
data ``Syn : ℕ → ★ where
`id : ∀ {n} → ``Syn n
_`∘_ : ∀ {n} → ``Syn n → ``Syn n → ``Syn n
`swap : ∀ {n} m → ``Syn (m + 2 + n)
swap-fin : ∀ {n} m → Endo (Fin (m + 2 + n))
swap-fin zero zero = suc zero
swap-fin zero (suc zero) = zero
swap-fin zero (suc (suc i)) = suc (suc i)
swap-fin (suc m) zero = zero
swap-fin (suc m) (suc i) = suc (swap-fin m i)
``evalArg : ∀ {n} → ``Syn n → Endo (`Rep n)
``evalArg `id = id
``evalArg (S `∘ S₁) = ``evalArg S ∘ ``evalArg S₁
``evalArg (`swap m) = swap-fin m
_``∘_ : ∀ {n} → ``Syn n → ``Syn n → ``Syn n
`id ``∘ y = y
(x `∘ x₁) ``∘ `id = x `∘ x₁
(x `∘ x₁) ``∘ (y `∘ y₁) = x `∘ (x₁ `∘ (y `∘ y₁))
(x `∘ x₁) ``∘ `swap m = x `∘ (x₁ ``∘ `swap m)
`swap m ``∘ y = `swap m `∘ y
``tail : ∀ {n} → ``Syn n → ``Syn (suc n)
``tail `id = `id
``tail (S `∘ S₁) = ``tail S ``∘ ``tail S₁
``tail (`swap m) = `swap (suc m)
translate : ∀ {n} → `Syn n → ``Syn n
translate `id = `id
translate `swap = `swap 0
translate (`tail S) = ``tail (translate S)
translate (S `∘ S₁) = translate S ``∘ translate S₁
``∘-p : ∀ {n}(A B : ``Syn n) → ``evalArg (A ``∘ B) ≗ ``evalArg (A `∘ B)
``∘-p `id B x = refl
``∘-p (A `∘ A₁) `id x = refl
``∘-p (A `∘ A₁) (B `∘ B₁) x = refl
``∘-p (A `∘ A₁) (`swap m) x rewrite ``∘-p A₁ (`swap m) x = refl
``∘-p (`swap m) B x = refl
``tail-p : ∀ {n} (S : ``Syn n) → fin-tail (``evalArg S) ≗ ``evalArg (``tail S)
``tail-p `id zero = refl
``tail-p `id (suc x) = refl
``tail-p (S `∘ S₁) zero rewrite ``∘-p (``tail S) (``tail S₁) zero
| sym (``tail-p S₁ zero) = ``tail-p S zero
``tail-p (S `∘ S₁) (suc x) rewrite ``∘-p (``tail S) (``tail S₁) (suc x)
| sym (``tail-p S₁ (suc x)) = ``tail-p S (suc (``evalArg S₁ x))
``tail-p (`swap m) zero = refl
``tail-p (`swap m) (suc x) = refl
`eval`` : ∀ {n} (S : `Syn n) → `evalArg S ≗ ``evalArg (translate S)
`eval`` `id x = refl
`eval`` `swap zero = refl
`eval`` `swap (suc zero) = refl
`eval`` `swap (suc (suc x)) = refl
`eval`` (`tail S) zero = ``tail-p (translate S) zero
`eval`` (`tail S) (suc x) rewrite `eval`` S x = ``tail-p (translate S) (suc x)
`eval`` (S `∘ S₁) x rewrite ``∘-p (translate S) (translate S₁) x | sym (`eval`` S₁ x) | `eval`` S (`evalArg S₁ x) = refl
data Fin-View : ∀ {n} → Fin n → ★ where
max : ∀ {n} → Fin-View (fromℕ n)
inject : ∀ {n} → (i : Fin n) → Fin-View (inject₁ i)
data _≤F_ : ∀ {n} → Fin n → Fin n → ★ where
z≤i : {n : ℕ}{i : Fin (suc n)} → zero ≤F i
s≤s : {n : ℕ}{i j : Fin n} → i ≤F j → suc i ≤F suc j
≤F-refl : ∀ {n} (x : Fin n) → x ≤F x
≤F-refl zero = z≤i
≤F-refl (suc i) = s≤s (≤F-refl i)
_<F_ : ∀ {n} → Fin n → Fin n → ★
i <F j = suc i ≤F inject₁ j
nsuc-inj : ∀ {x y} → Data.Nat.NP.suc x ≡ suc y → x ≡ y
nsuc-inj refl = refl
suc-inj : ∀ {n}{i j : Fin n} → Data.Fin.suc i ≡ suc j → i ≡ j
suc-inj refl = refl
data Sorted {X}(XC : Cmp X) : ∀ {l} → Vec X l → ★ where
[] : Sorted XC []
sing : ∀ x → Sorted XC (x ∷ [])
dbl-lt : ∀ {l} x y {xs : Vec X l} → lt ≡ XC x y → Sorted XC (y ∷ xs) → Sorted XC (x ∷ y ∷ xs)
dbl-eq : ∀ {l} x {xs : Vec X l} → Sorted XC (x ∷ xs) → Sorted XC (x ∷ x ∷ xs)
opposite : Ord → Ord
opposite lt = gt
opposite eq = eq
opposite gt = lt
flip-RC : ∀ {n}(x y : Fin n) → opposite (`RC x y) ≡ `RC y x
flip-RC zero zero = refl
flip-RC zero (suc y) = refl
flip-RC (suc x) zero = refl
flip-RC (suc x) (suc y) = flip-RC x y
eq=>≡ : ∀ {i} (x y : Fin i) → eq ≡ `RC x y → x ≡ y
eq=>≡ zero zero p = refl
eq=>≡ zero (suc y) ()
eq=>≡ (suc x) zero ()
eq=>≡ (suc x) (suc y) p rewrite eq=>≡ x y p = refl
insert-Sorted : ∀ {n l}{V : Vec (Fin n) l}(x : Fin n) → Sorted {Fin n} `RC V → Sorted {Fin n} `RC (insert `RC x V)
insert-Sorted x [] = sing x
insert-Sorted x (sing x₁) with `RC x x₁ | dbl-lt {XC = `RC} x x₁ {[]} | eq=>≡ x x₁ | flip-RC x x₁
insert-Sorted x (sing x₁) | lt | b | _ | _ = b refl (sing x₁)
insert-Sorted x (sing x₁) | eq | _ | p | _ rewrite p refl = dbl-eq x₁ (sing x₁)
insert-Sorted x (sing x₁) | gt | b | _ | l = dbl-lt x₁ x l (sing x)
insert-Sorted x (dbl-lt y y' {xs} prf xs₁) with `RC x y | dbl-lt {XC = `RC} x y {y' ∷ xs} | eq=>≡ x y | flip-RC x y
insert-Sorted x (dbl-lt y y' prf xs₁) | lt | b | p | l₁ = b refl (dbl-lt y y' prf xs₁)
insert-Sorted x (dbl-lt y y' prf xs₁) | eq | b | p | l₁ rewrite p refl = dbl-eq y (dbl-lt y y' prf xs₁)
insert-Sorted x (dbl-lt y y' {xs} prf xs₁) | gt | b | p | l₁ with `RC x y' | insert-Sorted x xs₁
insert-Sorted x (dbl-lt y y' prf xs₁) | gt | b | p | l₁ | lt | xs' = dbl-lt y x l₁ xs'
insert-Sorted x (dbl-lt y y' prf xs₁) | gt | b | p | l₁ | eq | xs' = dbl-lt y x l₁ xs'
insert-Sorted x (dbl-lt y y' prf xs₁) | gt | b | p | l₁ | gt | xs' = dbl-lt y y' prf xs'
insert-Sorted x (dbl-eq y {xs} xs₁) with `RC x y | inspect (`RC x) y | dbl-lt {XC = `RC} x y {y ∷ xs} | eq=>≡ x y | flip-RC x y | insert-Sorted x xs₁
insert-Sorted x (dbl-eq y xs₁) | lt | _ | b | p | l | _ = b refl (dbl-eq y xs₁)
insert-Sorted x (dbl-eq y xs₁) | eq | _ | b | p | l | _ rewrite p refl = dbl-eq y (dbl-eq y xs₁)
insert-Sorted x (dbl-eq y xs₁) | gt | [ prf ] | b | p | l | ss rewrite prf = dbl-eq y ss
sort-Sorted : ∀ {n l}(V : Vec (Fin n) l) → Sorted `RC (`sort `RC V)
sort-Sorted [] = []
sort-Sorted (x ∷ V) = insert-Sorted x (sort-Sorted V)
RC-refl : ∀ {i}(x : Fin i) → `RC x x ≡ eq
RC-refl zero = refl
RC-refl (suc x) = RC-refl x
STail : ∀ {X l}{XC : Cmp X}{xs : Vec X (suc l)} → Sorted XC xs → Sorted XC (tail xs)
STail (sing x) = []
STail (dbl-lt x y x₁ T) = T
STail (dbl-eq x T) = T
module sproof {X}(XC : Cmp X)(XC-refl : ∀ x → XC x x ≡ eq)
(eq≡ : ∀ x y → XC x y ≡ eq → x ≡ y)
(lt-trans : ∀ x y z → XC x y ≡ lt → XC y z ≡ lt → XC x z ≡ lt)
(XC-flip : ∀ x y → opposite (XC x y) ≡ XC y x)
where
open import Data.Sum
_≤X_ : X → X → ★
x ≤X y = XC x y ≡ lt ⊎ XC x y ≡ eq
≤X-trans : ∀ {x y z} → x ≤X y → y ≤X z → x ≤X z
≤X-trans (inj₁ x₁) (inj₁ x₂) = inj₁ (lt-trans _ _ _ x₁ x₂)
≤X-trans {_}{y}{z}(inj₁ x₁) (inj₂ y₁) rewrite eq≡ y z y₁ = inj₁ x₁
≤X-trans {x}{y} (inj₂ y₁) y≤z rewrite eq≡ x y y₁ = y≤z
h≤t : ∀ {n}{T : `Tree X (2 + n)} → Sorted XC T → head T ≤X head (tail T)
h≤t (dbl-lt x y x₁ ST) = inj₁ (sym x₁)
h≤t (dbl-eq x ST) rewrite XC-refl x = inj₂ refl
head-p : ∀ {n}{T : `Tree X (suc n)} i → Sorted XC T → head T ≤X `toFun T i
head-p {T = T} zero ST rewrite XC-refl (head T) = inj₂ refl
head-p {zero} (suc ()) ST
head-p {suc n} (suc i) ST = ≤X-trans (h≤t ST) (head-p i (STail ST))
toFun-p : ∀ {n}{T : `Tree X n}{i j : Fin n} → i ≤F j → Sorted XC T → `toFun T i ≤X `toFun T j
toFun-p {j = j} z≤i ST = head-p j ST
toFun-p (s≤s i≤Fj) ST = toFun-p i≤Fj (STail ST)
sort-proof : ∀ {i}{T : `Tree X i} → Sorted XC T → Is-Mono `RC XC (`toFun T)
sort-proof {T = T} T₁ zero zero rewrite XC-refl (head T) = _
sort-proof T₁ zero (suc y) with toFun-p (z≤i {i = suc y}) T₁
sort-proof T zero (suc y) | inj₁ x rewrite x = _
sort-proof T zero (suc y) | inj₂ y₁ rewrite y₁ = _
sort-proof {T = T} T₁ (suc x) zero with toFun-p (z≤i {i = suc x}) T₁ | XC-flip (head T) (`toFun (tail T) x)
sort-proof T (suc x) zero | inj₁ x₁ | l rewrite x₁ | sym l = _
sort-proof T (suc x) zero | inj₂ y | l rewrite y | sym l = _
sort-proof T₁ (suc x) (suc y) = sort-proof (STail T₁) x y
lt-trans-RC : ∀ {i} (x y z : Fin i) → `RC x y ≡ lt → `RC y z ≡ lt → `RC x z ≡ lt
lt-trans-RC zero zero zero x<y y<z = y<z
lt-trans-RC zero zero (suc z) x<y y<z = refl
lt-trans-RC zero (suc y) zero x<y ()
lt-trans-RC zero (suc y) (suc z) x<y y<z = refl
lt-trans-RC (suc x) zero zero x<y y<z = x<y
lt-trans-RC (suc x) zero (suc z) () y<z
lt-trans-RC (suc x) (suc y) zero x<y y<z = y<z
lt-trans-RC (suc x) (suc y) (suc z) x<y y<z = lt-trans-RC x y z x<y y<z
`sort-mono : ∀ {i}(T : `Tree (`Rep i) i) → Is-Mono `RC `RC (`toFun (`sort `RC T))
`sort-mono T x y = sproof.sort-proof `RC RC-refl (λ x₁ y₁ x₂ → eq=>≡ x₁ y₁ (sym x₂)) lt-trans-RC flip-RC (sort-Sorted T) x y
module toNat n (f : Endo (Fin (suc n)))(f-inj : Is-Inj f)(f-mono : Is-Mono `RC `RC f) where
open import Data.Nat.BoundedMonoInj-is-Id
open import Data.Sum
move-to-RC : ∀ {n}{x y : Fin n} → x ≤F y → `RC x y ≡ lt ⊎ `RC x y ≡ eq
move-to-RC {y = zero} z≤i = inj₂ refl
move-to-RC {y = suc y} z≤i = inj₁ refl
move-to-RC (s≤s x≤Fy) = move-to-RC x≤Fy
move-from-RC : ∀ {n}(x y : Fin n) → lt ≡ `RC x y ⊎ eq ≡ `RC x y → x ≤F y
move-from-RC zero zero prf = z≤i
move-from-RC zero (suc y) prf = z≤i
move-from-RC (suc x) zero (inj₁ ())
move-from-RC (suc x) zero (inj₂ ())
move-from-RC (suc x) (suc y) prf = s≤s (move-from-RC x y prf)
proper-mono : ∀ {x y} → x ≤F y → f x ≤F f y
proper-mono {x} {y} x≤Fy with `RC x y | `RC (f x) (f y) | move-to-RC x≤Fy | f-mono x y | move-from-RC (f x) (f y)
proper-mono x≤Fy | .lt | lt | inj₁ refl | r4 | r5 = r5 (inj₁ refl)
proper-mono x≤Fy | .lt | eq | inj₁ refl | r4 | r5 = r5 (inj₂ refl)
proper-mono x≤Fy | .lt | gt | inj₁ refl | () | r5
proper-mono x≤Fy | .eq | lt | inj₂ refl | () | r5
proper-mono x≤Fy | .eq | eq | inj₂ refl | r4 | r5 = r5 (inj₂ refl)
proper-mono x≤Fy | .eq | gt | inj₂ refl | () | r5
getFrom : ∀ n → ℕ → Fin (suc n)
getFrom zero i = zero
getFrom (suc n₁) zero = zero
getFrom (suc n₁) (suc i) = suc (getFrom n₁ i)
getInj : {n x y : ℕ} → x ≤ n → y ≤ n → getFrom n x ≡ getFrom n y → x ≡ y
getInj z≤n z≤n prf = refl
getInj z≤n (s≤s y≤n) ()
getInj (s≤s x≤n) z≤n ()
getInj (s≤s x≤n) (s≤s y≤n) prf rewrite (getInj x≤n y≤n (suc-inj prf)) = refl
getMono : {n x y : ℕ} → x ≤ y → y ≤ n → getFrom n x ≤F getFrom n y
getMono z≤n z≤n = ≤F-refl _
getMono z≤n (s≤s y≤n) = z≤i
getMono (s≤s x≤y) (s≤s y≤n) = s≤s (getMono x≤y y≤n)
forget : ∀ {n} → Fin n → ℕ
forget zero = zero
forget (suc i) = suc (forget i)
forgetInj : ∀ {n}{i j : Fin n} → forget i ≡ forget j → i ≡ j
forgetInj {.(suc _)} {zero} {zero} prf = refl
forgetInj {.(suc _)} {zero} {suc j} ()
forgetInj {.(suc _)} {suc i} {zero} ()
forgetInj {.(suc _)} {suc i} {suc j} prf rewrite forgetInj (nsuc-inj prf) = refl
getForget : ∀ {n}(i : Fin (suc n)) → getFrom n (forget i) ≡ i
getForget {zero} zero = refl
getForget {zero} (suc ())
getForget {suc n₁} zero = refl
getForget {suc n₁} (suc i) rewrite getForget i = refl
forget< : ∀ {n} → (i : Fin n) → forget i < n
forget< {zero} ()
forget< {suc n₁} zero = s≤s z≤n
forget< {suc n₁} (suc i) = s≤s (forget< i)
forget-mono : ∀ {n}{i j : Fin n} → i ≤F j → forget i ≤ forget j
forget-mono z≤i = z≤n
forget-mono (s≤s i≤F) = s≤s (forget-mono i≤F)
fn : Endo ℕ
fn = forget ∘ f ∘ getFrom n
return : f ≗ getFrom n ∘ fn ∘ forget
return x rewrite getForget x | getForget (f x) = refl
fn-monotone : Monotone (suc n) fn
fn-monotone {x} {y} x≤y (s≤s y≤n) = forget-mono (proper-mono (getMono x≤y y≤n))
fn-inj : IsInj (suc n) fn
fn-inj {x}{y} (s≤s sx≤sn) (s≤s sy≤sn) prf = getInj sx≤sn sy≤sn (f-inj (getFrom n x) (getFrom n y) (forgetInj prf))
fn-bounded : Bounded (suc n) fn
fn-bounded x _ = forget< (f (getFrom n x))
fn≗id : ∀ x → x < (suc n) → fn x ≡ x
fn≗id = M.is-id fn fn-monotone fn-inj fn-bounded
f≗id : f ≗ id
f≗id x rewrite return x | fn≗id (forget x) (forget< x) = getForget x
fin-view : ∀ {n} → (i : Fin (suc n)) → Fin-View i
fin-view {zero} zero = max
fin-view {zero} (suc ())
fin-view {suc n} zero = inject _
fin-view {suc n} (suc i) with fin-view i
fin-view {suc n} (suc .(fromℕ n)) | max = max
fin-view {suc n} (suc .(inject₁ i)) | inject i = inject _
absurd : {X : ★} → .⊥ → X
absurd ()
drop₁ : ∀ {n} → (i : Fin (suc n)) → .(i ≢ fromℕ n) → Fin n
drop₁ i neq with fin-view i
drop₁ {n} .(fromℕ n) neq | max = absurd (neq refl)
drop₁ .(inject₁ i) neq | inject i = i
drop₁→inject₁ : ∀ {n}(i : Fin (suc n))(j : Fin n).(p : i ≢ fromℕ n) → drop₁ i p ≡ j → i ≡ inject₁ j
drop₁→inject₁ i j p q with fin-view i
drop₁→inject₁ {n} .(fromℕ n) j p q | max = absurd (p refl)
drop₁→inject₁ .(inject₁ i) j p q | inject i = cong inject₁ q
`mono-inj→id : ∀{i}(f : Endo (`Rep i)) → Is-Inj f → Is-Mono `RC `RC f → f ≗ id
`mono-inj→id {zero} = λ f x x₁ ()
`mono-inj→id {suc i} = toNat.f≗id i
interface : Interface
interface = record
{ Ix = `Ix
; Rep = `Rep
; Syn = `Syn
; Tree = `Tree
; fromFun = `fromFun
; toFun = `toFun
; toFun∘fromFun = `toFun∘fromFun
; evalArg = `evalArg
; evalTree = `evalTree
; eval-proof = `eval-proof
; inv = `inv
; inv-proof = `inv-proof
; RC = `RC
; sort = `sort
; sort-syn = `sort-syn
; sort-proof = `sort-proof
; sort-mono = `sort-mono
; mono-inj→id = `mono-inj→id
}
count : ∀ {n} → (Fin n → ℕ) → ℕ
count {n} f = sum (tabulate f)
count-ext : ∀ {n} → (f g : Fin n → ℕ) → f ≗ g → count f ≡ count g
count-ext {zero} f g f≗g = refl
count-ext {suc n} f g f≗g rewrite f≗g zero | count-ext (f ∘ suc) (g ∘ suc) (f≗g ∘ suc) = refl
#⟨_⟩ : ∀ {n} → (Fin n → 𝟚) → ℕ
#⟨ f ⟩ = count (𝟚▹ℕ ∘ f)
#-ext : ∀ {n} → (f g : Fin n → 𝟚) → f ≗ g → #⟨ f ⟩ ≡ #⟨ g ⟩
#-ext f g f≗g = count-ext (𝟚▹ℕ ∘ f) (𝟚▹ℕ ∘ g) (cong 𝟚▹ℕ ∘ f≗g)
com-assoc : ∀ x y z → x + (y + z) ≡ y + (x + z)
com-assoc x y z rewrite
sym (ℕ°.+-assoc x y z) |
ℕ°.+-comm x y |
ℕ°.+-assoc y x z = refl
syn-pres : ∀ {n}(f : Fin n → ℕ)(S : `Syn n)
→ count f ≡ count (f ∘ `evalArg S)
syn-pres f `id = refl
syn-pres f `swap = com-assoc (f zero) (f (suc zero)) (count (λ i → f (suc (suc i))))
syn-pres f (`tail S) rewrite syn-pres (f ∘ suc) S = refl
syn-pres f (S `∘ S₁) rewrite syn-pres f S = syn-pres (f ∘ `evalArg S) S₁
count-perm : ∀ {n}(f : Fin n → ℕ)(p : Endo (Fin n)) → Is-Inj p
→ count f ≡ count (f ∘ p)
count-perm f p p-inj = trans (syn-pres f (sort-bij p)) (count-ext _ _ f∘eval≗f∘p)
where
open abs interface
f∘eval≗f∘p : f ∘ `evalArg (sort-bij p) ≗ f ∘ p
f∘eval≗f∘p x rewrite thm p p-inj x = refl
#-perm : ∀ {n}(f : Fin n → 𝟚)(p : Endo (Fin n)) → Is-Inj p
→ #⟨ f ⟩ ≡ #⟨ f ∘ p ⟩
#-perm f p p-inj = count-perm (𝟚▹ℕ ∘ f) p p-inj
test : `Syn 8
test = abs.sort-bij interface (λ x → `evalArg (`tail `swap) x)