t-n.agda

open import Data.Fin hiding (_<_; _≤_; _+_)
open import Data.Nat
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Decidable
open import Data.Nat.Properties.Simple
ℕ- : (a b : ℕ) → a ≥ b → ℕ
ℕ- a .0 z≤n = a
ℕ- (suc m) (suc n) (s≤s p) = ℕ- m n p


ℕ-0 : ∀ (n : ℕ) → (p : 0 ≤ n) → ℕ- n 0 p ≡ n
ℕ-0 n z≤n = refl

aux : ∀ i n → (p : i < n) → i + suc (ℕ- n (suc i) p) ≡ n
aux zero zero ()
aux zero (suc n) (s≤s p) = cong suc (ℕ-0 n p)
aux (suc i) zero ()
aux (suc i) (suc n) (s≤s p) = cong suc (aux i n p)

≤-refl : ∀ {a} → a ≤ a
≤-refl {zero} = z≤n
≤-refl {suc a} = s≤s (≤-refl {a})


≤-trans : ∀ {a b c} → a ≤ b → b ≤ c → a ≤ c
≤-trans z≤n z≤n = z≤n
≤-trans z≤n (s≤s p2) = z≤n
≤-trans (s≤s p1) (s≤s p2) = s≤s (≤-trans p1 p2)

≤-weakening : (a b c : ℕ) -> a ≤ b → a ≤ b + c
≤-weakening .0 zero zero z≤n = z≤n
≤-weakening .0 zero (suc c) z≤n = z≤n
≤-weakening .0 (suc b) c z≤n = z≤n
≤-weakening (suc m) (suc n) c (s≤s p) = s≤s (≤-weakening m n c p)


a+suc-b==suc-a+b : (a b : ℕ) → a + (suc b) ≡ suc (a + b)
a+suc-b==suc-a+b zero zero = refl
a+suc-b==suc-a+b (suc x) zero = cong suc (a+suc-b==suc-a+b x zero)
a+suc-b==suc-a+b zero (suc y) = refl
a+suc-b==suc-a+b (suc x) (suc y) = cong suc (a+suc-b==suc-a+b x (suc y))


t : ∀ (i n : ℕ) → (p : i < n) → Fin n
t i n p = subst Fin (aux i n p)
  ((# (ℕ- n (1 + i) p)) {_} {fromWitness (≤-trans
                                            (≤-weakening (suc (ℕ- n (suc i) p)) (suc (ℕ- n (suc i) p)) i
                                             ≤-refl)
                                            (subst (λ x → suc x ≤ i + suc (ℕ- n (suc i) p)) (+-comm i (ℕ- n (suc i) p))
                                              (subst (λ x → x ≤ i + suc (ℕ- n (suc i) p))
                                                (a+suc-b==suc-a+b i (ℕ- n (suc i) p)) ≤-refl)))}) 

t-n-≡-zero : ∀ (n : ℕ) → t n (suc n) ≤-refl ≡ zero
t-n-≡-zero n = {!!}