module Finite where

open import Equality
open import Logic
open import LogicalFacts
open import Naturals
open import JK-Monads
open import Finite-JK-Shifts


data smaller :   Set where
  fzero : {n : }  smaller(succ n)
  fsucc : {n : }  smaller n  smaller(succ n)


embed : {n : }  smaller n  
embed {O} ()
embed {succ n} fzero = O
embed {succ n} (fsucc i) = succ(embed i)


restriction : {m : } {X : Set}  (  X)  smaller m  X
restriction f = f  embed


coerce : {n : }  smaller n  smaller(succ n)
coerce {O} ()
coerce {succ n} (fzero) = fzero 
coerce {succ n} (fsucc i) = fsucc(coerce i)


-- In summary, embed i ≡ embed (coerce i).

embed-coerce-lemma : {n : }  {i : smaller n}  

   embed {n} i  embed {succ n} (coerce {n} i)

embed-coerce-lemma {O} {()}
embed-coerce-lemma {succ n} {fzero} = reflexivity
embed-coerce-lemma {succ n} {fsucc i} = lemma₄
  where induction-hypothesis : embed {n} i  embed {succ n} (coerce {n} i)
        induction-hypothesis = embed-coerce-lemma {n} {i}

        lemma₀ : embed {succ n} (fsucc i)  succ(embed {n} i)
        lemma₀ = reflexivity

        lemma₁ : succ(embed {n} i)  succ(embed{succ n} (coerce {n} i))
        lemma₁ = compositionality succ induction-hypothesis

        lemma₂ : embed {succ n} (fsucc i)  succ(embed{succ n} (coerce {n} i))
        lemma₂ = transitivity lemma₀ lemma₁

        lemma₃ :   succ(embed{succ n} (coerce {n} i)) 
                  embed{succ(succ n)} (coerce {succ n} (fsucc i))
        lemma₃ = reflexivity

        lemma₄ :   embed {succ n} (fsucc i) 
                  embed{succ(succ n)} (coerce {succ n} (fsucc i))
        lemma₄ = transitivity lemma₂ lemma₃


fmin : (m : )    smaller(succ m)

fmin O n = fzero
fmin (succ m)  0 = fzero
fmin (succ m) (succ n) = fsucc(fmin m n)



-- The following mimicks the definition of the infinite shifts
-- (in the modules Naturals.agda and J-Shift-Selection.agda):


fhead : {m : } {A : smaller(succ m)  Ω}  
-----
       (∀(n : smaller(succ m))  A n)  A fzero

fhead α = α fzero


ftail : {m : } {A : smaller(succ m)  Ω}  
-----
       (∀(n : smaller(succ m))  A n)  ∀(n : smaller m)  A(fsucc n)

ftail α n = α(fsucc n)



fcons : {m : } {A : smaller(succ m)  Ω}  
-----
       A fzero  (∀(n : smaller m)  A(fsucc n))  ∀(n : smaller(succ m))  A n

fcons (∧-intro a α) fzero = a
fcons (∧-intro a α) (fsucc n) = α n


fK-∧-shift' : {R : Ω} {m : } {A : smaller(succ m)  Ω}  
----------
             K(A fzero)  K(∀(n : smaller m)  A(fsucc n))  
             K(∀(n : smaller(succ m))  A n)

fK-∧-shift' {R} = (K-functor {R} fcons)  K-∧-shift


fK-∀-shift : {m : } {R : Ω} {A : smaller m  Ω}  
----------
             (∀(n : smaller m)  K {R} (A n))  
       K {R} (∀(n : smaller m)  A n) 

fK-∀-shift  {O} φs = λ p  p λ()
fK-∀-shift {succ m}  φs = 
 fK-∧-shift' (∧-intro (fhead φs) (fK-∀-shift (ftail φs)))


-- This is used for Berger's modified bar recursion.


override : {X :   Set}  {m : }  

 (s : (i : smaller m)  X(embed i))  
 ((n : )  X n)  ((n : )  X n) 

override {X} {m} s α n = less-cases {X} m n s (α n)
 where
  less-cases : {X :   Set}  (m n : )  
   (s : (i : smaller m)  X(embed i))  X n  X n

  less-cases 0 n s a = a
  less-cases (succ m) 0 s a = s fzero
  less-cases {X} (succ m) (succ n) s a 
   = less-cases  n  X(succ n)} m n (ftail s) a


append : {X :   Set}  {m : } 
 ((i : smaller m)  X(embed i))  X m  (i : smaller(succ m))  X(embed i)

append {X} {0} s x fzero = x
append {X} {0} s x (fsucc ())
append {X} {succ m} s x fzero = s fzero
append {X} {succ m} s x (fsucc i) 
 = append  n  X(succ n)} {m} (ftail s) x i