\begin{code}
module Chi where
open import Data.Nat as Nat
open import Data.Nat.Properties
open import Data.Bool hiding (_≟_;_∨_)
open import Data.Empty
open import Function
open import Data.Sum hiding (map) renaming (_⊎_ to _∨_)
open import Data.Product renaming (Σ to Σₓ;map to mapₓ)
open import Relation.Nullary
open import Relation.Nullary.Decidable hiding (map)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as PropEq renaming ([_] to [_]ᵢ)
open import Data.List hiding (any) renaming (length to length')
open import Data.List.Properties
open import Data.List.Any as Any hiding (map)
open import Data.List.Any.Membership
open import Data.List.Any.Properties
open Any.Membership-≡ renaming (_∈_ to _∈[]_;_∉_ to _∉[]_)
open import Algebra.Structures
open import Relation.Binary
n+0≡n = IsCommutativeMonoid.identityˡ (IsCommutativeSemiring.*-isCommutativeMonoid isCommutativeSemiring)
+-comm = IsCommutativeMonoid.comm (IsCommutativeSemiring.+-isCommutativeMonoid isCommutativeSemiring)
total = IsTotalOrder.total (IsDecTotalOrder.isTotalOrder (DecTotalOrder.isDecTotalOrder decTotalOrder))
V = ℕ
f<s : (x : V)(xs : List V) → x ∈[] xs → ((y : V) → y < x → y ∈[] xs) → (y : V) → y < (suc x) → y ∈[] xs
f<s x xs x∈xs f< y sucy≤sucx with ≤⇒≤′ sucy≤sucx
f<s x xs x∈xs f< .x _ | ≤′-refl = x∈xs
f<s x xs x∈xs f< y _ | ≤′-step sucy<'sucx = f< y (≤′⇒≤ sucy<'sucx)
χaux : (n m k : V) → n + m ≡ k → (xs : List V) → ((y : V) → y < n → y ∈[] xs) →
∃ (λ v → (v ∉[] xs ∨ v ≡ k) × ((y : V) → y < v → y ∈[] xs))
χaux x 0 k x+0≡k _ f< with trans (sym (n+0≡n x)) x+0≡k
χaux x 0 .x x+0≡k _ f< | refl
= x , inj₂ refl , f<
χaux x (suc n) k x+Sn≡k xs f<
with any (_≟_ x) xs
... | no x∉xs = x , inj₁ x∉xs , f<
... | yes x∈xs = χaux (suc x) n k (trans (cong suc (+-comm x n)) (trans (+-comm (suc n) x) x+Sn≡k)) xs (f<s x xs x∈xs f<)
y<0⇒y∈xs : (xs : List V)(y : V) → y < 0 → y ∈[] xs
y<0⇒y∈xs xs y ()
\end{code}
\begin{code}
χ' : List V → V
\end{code}
\begin{code}
χ' xs = proj₁ (χaux 0 (length' xs) (length' xs) refl xs (y<0⇒y∈xs xs))
sucn≡sucm→n≡m : {n m : ℕ} → suc n ≡ suc m → n ≡ m
sucn≡sucm→n≡m refl = refl
predn≡m→n≡sucm : {n m : ℕ} → n > 0 → pred n ≡ m → n ≡ suc m
predn≡m→n≡sucm {suc n} {m} (s≤s _) n≡m = cong suc n≡m
x∈xs→|xs|>0 : {n : ℕ}{x : ℕ}{xs : List ℕ} → x ∈[] xs → n ≡ length' xs → n > 0
x∈xs→|xs|>0 .{suc (length' xs)} {x} {y ∷ xs} (here px) refl = s≤s z≤n
x∈xs→|xs|>0 .{suc (length' xs)} {x} {y ∷ xs} (there x∈xs) refl = s≤s z≤n
del : (n : ℕ)(x : ℕ)(xs : List ℕ) → n ≡ length' xs → x ∈[] xs → Σₓ (List ℕ) (λ ys → pred n ≡ length' ys)
del .0 x [] refl ()
del 0 _ (x ∷ xs) () _
del (suc n) .x (x ∷ xs) n+1≡|xxs| (here refl)
= xs , sucn≡sucm→n≡m n+1≡|xxs|
del (suc n) x (y ∷ xs) n+1≡|yxs| (there x∈xs)
= y ∷ proj₁ (del n x xs n≡|xs| x∈xs) ,
predn≡m→n≡sucm (x∈xs→|xs|>0 x∈xs n≡|xs|) (proj₂ (del n x xs n≡|xs| x∈xs))
where n≡|xs| = sucn≡sucm→n≡m n+1≡|yxs|
<→≢ : {n m : ℕ} → n < m → n ≢ m
<→≢ (s≤s n<m) refl = ⊥-elim (aux n<m)
where
aux : {n : ℕ} → suc n ≤ n → ⊥
aux (s≤s sucn≤n) = aux sucn≤n
del∈ : (x : ℕ)(xs : List ℕ) → (x∈xs : x ∈[] xs) → (y : ℕ) → y < x → y ∈[] xs → y ∈[] (proj₁ (del (length' xs) x xs refl x∈xs))
del∈ x [] () y y<x y∈xs
del∈ x (.x ∷ xs) (here refl) .x x<x (here refl) = ⊥-elim ((<→≢ x<x) refl)
del∈ x (.x ∷ xs) (here refl) y y<x (there y∈xs) = y∈xs
del∈ x (.y ∷ xs) (there x∈xs) y y<x (here refl) = here refl
del∈ x (z ∷ xs) (there x∈xs) y y<x (there y∈xs) = there (del∈ x xs x∈xs y y<x y∈xs)
palomar-aux : (n : ℕ)(xs : List V) → ((y : V) → y ≤ n → y ∈[] xs) → n ≡ length' xs → ⊥
palomar-aux .0 [] f refl with f 0 z≤n
... | ()
palomar-aux 0 (x ∷ xs) f ()
palomar-aux (suc n) (x ∷ xs) f sucn≡suc|xs| with any (_≟_ (length' (x ∷ xs))) (x ∷ xs)
palomar-aux (suc n) (x ∷ xs) f sucn≡suc|xs|
| no |x∷xs|∉x∷xs = ⊥-elim (|x∷xs|∉x∷xs (f (suc (length' xs)) (subst₂ _≤_ refl (sym sucn≡suc|xs|) (n≤m+n 0 (suc (length' xs))))))
palomar-aux (suc n) (x ∷ xs) f sucn≡suc|xs|
| yes |x∷xs|∈x∷xs
with proj₁ (del (length' (x ∷ xs)) (length' (x ∷ xs)) (x ∷ xs) refl |x∷xs|∈x∷xs) |
proj₂ (del (length' (x ∷ xs)) (length' (x ∷ xs)) (x ∷ xs) refl |x∷xs|∈x∷xs) |
del∈ (length' (x ∷ xs)) (x ∷ xs) |x∷xs|∈x∷xs
palomar-aux (suc n) (x ∷ xs) f sucn≡suc|xs|
| yes |x∷xs|∈x∷xs | ys | |xs|≡|ys| | f2
= palomar-aux n ys fys (trans (sucn≡sucm→n≡m sucn≡suc|xs|) |xs|≡|ys|)
where
fys : (y : V) → y ≤ n → y ∈[] ys
fys y y≤n = f2 y (s≤s (subst₂ _≤_ refl (sucn≡sucm→n≡m sucn≡suc|xs|) y≤n)) (f y (≤-step y≤n))
palomar : (n : V)(xs : List V) → ((y : V) → y < n → y ∈[] xs) → n ≡ length' xs → n ∉[] xs
palomar .(length' xs) xs f refl |xs|∈xs = palomar-aux (length' xs) xs (faux (length' xs) xs |xs|∈xs f refl) refl
where
faux : (n : ℕ)(xs : List ℕ) → length' xs ∈[] xs → ((y : V) → y < n → y ∈[] xs) → n ≡ length' xs → (y : ℕ) → y ≤ length' xs → y ∈[] xs
faux .(length' xs) xs |xs|∈xs f refl y y≤|xs| with ≤⇒≤′ y≤|xs|
faux .0 [] |xs|∈xs f refl .0 y≤|xs|
| ≤′-refl = |xs|∈xs
faux .(suc (length' xs)) (x ∷ xs) |xs|∈xs f refl .(suc (length' xs)) y≤|xs|+1
| ≤′-refl = |xs|∈xs
faux .(suc (length' xs)) (x ∷ xs) |xs|∈xs f refl .0 z≤n
| ≤′-step _ = f 0 (s≤s z≤n)
faux .(suc (length' xs)) (x ∷ xs) |xs|∈xs f refl (suc y) (s≤s a)
| ≤′-step b = f (suc y) (s≤s (≤′⇒≤ b))
lemmaχaux∉ : (xs : List V) → proj₁ (χaux 0 (length' xs) (length' xs) refl xs (y<0⇒y∈xs xs)) ∉[] xs
lemmaχaux∉ xs with χaux 0 (length' xs) (length' xs) refl xs (y<0⇒y∈xs xs)
... | v , inj₁ v∉xs , _ = v∉xs
... | .((length' xs)) , inj₂ refl , f = palomar (length' xs) xs f refl
≤→<∨≡ : (n m : ℕ) → n ≤ m → n < m ∨ m ≡ n
≤→<∨≡ .0 0 z≤n = inj₂ refl
≤→<∨≡ .0 (suc n) z≤n = inj₁ (s≤s z≤n)
≤→<∨≡ .(suc n) .(suc m) (s≤s {n} {m} n≤m) with ≤→<∨≡ n m n≤m
... | inj₁ n<m = inj₁ (s≤s n<m)
≤→<∨≡ .(suc n) .(suc n) (s≤s {n} {.n} n≤n)
| inj₂ refl = inj₂ refl
<≡ : (n m : ℕ) → n < m ∨ m < n ∨ n ≡ m
<≡ n m with total n m
... | inj₂ m≤n = inj₂ (≤→<∨≡ m n m≤n)
... | inj₁ n≤m with ≤→<∨≡ n m n≤m
... | inj₁ n<m = inj₁ n<m
... | inj₂ n≡m = inj₂ (inj₂ (sym n≡m))
lemmaχaux⊆ : (xs ys : List V) → xs ⊆ ys → ys ⊆ xs →
proj₁ (χaux 0 (length' xs) (length' xs) refl xs (y<0⇒y∈xs xs)) ≡ proj₁ (χaux 0 (length' ys) (length' ys) refl ys (y<0⇒y∈xs ys))
lemmaχaux⊆ xs ys xs⊆ys ys⊆xs
with
proj₁ (χaux 0 (length' xs) (length' xs) refl xs (y<0⇒y∈xs xs)) |
proj₂ (χaux 0 (length' xs) (length' xs) refl xs (y<0⇒y∈xs xs)) |
lemmaχaux∉ xs |
proj₁ (χaux 0 (length' ys) (length' ys) refl ys (y<0⇒y∈xs ys)) |
proj₂ (χaux 0 (length' ys) (length' ys) refl ys (y<0⇒y∈xs ys)) |
lemmaχaux∉ ys
... | x | _ , fx | x∉xs | y | _ , fy | y∉ys
with <≡ x y
... | inj₁ x<y = ⊥-elim (x∉xs (ys⊆xs (fy x x<y)))
... | inj₂ (inj₁ y<x) = ⊥-elim (y∉ys (xs⊆ys (fx y y<x)))
... | inj₂ (inj₂ x≡y) = x≡y
\end{code}