module WellfoundRecursion where

open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Data.Empty
open import Data.Product
open import Data.Sum
open import Data.Nat

open import DownwardLeq

-- Well-founded recursion. Most of the utilitiies are already 
-- defined in Induction.WellFounded in Standard Library.

-- Accessibility

data Acc {a : Set}(_<_ : a -> a -> Set) : a -> Set where
 acc : (x : a) -> (forall y -> y < x -> Acc _<_ y) -> Acc _<_ x

acc-elim : {a : Set} (_<_ : a -> a -> Set) {P : a -> Set} ->
  ((x : a) -> (forall y -> y < x -> Acc _<_ y) ->
                 (forall y -> y < x -> P y) -> P x) ->
     (x : a) -> Acc _<_  x -> P x
acc-elim _<_ Φ x (acc .x h) =
    Φ x h (\y y<x -> acc-elim _<_ Φ y (h y y<x)) 

acc-fold : {a : Set} (R : a -> a -> Set) {P : a -> Set} ->
    ((x : a) -> (forall y -> R y x -> P y) -> P x) ->
       (x : a) -> (accx : Acc R x) -> P x
acc-fold R {P} f x (acc .x h) = f x (\y yRx -> acc-fold R f y (h y yRx)) 

well-found : {a : Set} -> (a -> a -> Set) -> Set
well-found _<_ = forall x -> Acc _<_ x

rec-wf : {a : Set} {_<_ : a -> a -> Set} {P : a -> Set} ->
   well-found _<_ ->
      ((x : a) -> ((y : a) -> y < x -> P y) -> P x) -> 
         (x : a) -> P x
rec-wf {a}{_<_} wf f x = acc-fold _<_ f x (wf x) 

-- Example: Nat

ℕ<-wf : well-found _<′_
ℕ<-wf n = acc n (access n)
  where access : (n : ℕ) -> (m : ℕ) -> m <′ n -> Acc _<′_ m
        access zero m () 
        access (suc n) .n ≤′-refl = acc n (access n)
        access (suc n) m (≤′-step m<n) = access n m m<n 

half : ℕ -> ℕ
half = rec-wf ℕ<-wf body
  where body : (n : ℕ) -> ((m : ℕ) -> m <′ n -> ℕ) -> ℕ
        body zero rec = zero 
        body (suc zero) rec = zero
        body (suc (suc n)) rec = suc (rec n (≤′-step ≤′-refl))

-- Example: intergal division.

-- this definition does not pass the termination check.

div : ℕ -> ℕ -> ℕ
div zero n = zero
div (suc m) zero = suc m
div (suc m) (suc n) = suc (div (suc m ∸ suc n) (suc n))

-- well, I feel lazy proving this...

postulate sm-sn<sm : forall m n -> ((suc m ∸ suc n) <′ suc m)

-- terminating version of div

div-wf : ℕ -> ℕ -> ℕ
div-wf m n = rec-wf ℕ<-wf (body n) m
  where body : (n : ℕ) -> (m : ℕ) -> ((k : ℕ) -> k <′ m -> ℕ) -> ℕ
        body n zero rec = zero
        body zero (suc m) rec = suc m
        body (suc n) (suc m) rec = suc (rec (suc m ∸ suc n) (sm-sn<sm m n))

-- if you like, you may avoid the explicit fixed-point.

div-wf' : forall m -> ℕ -> Acc _<′_ m -> ℕ
div-wf' zero n _ = zero
div-wf' (suc m) zero _ = suc m
div-wf' (suc m) (suc n) (acc .(suc m) h) = 
   suc (div-wf' (suc m ∸ suc n) (suc n) (h (suc m ∸ suc n) (sm-sn<sm m n)))

-- an ordering for downward induction.

_<_≤_ : ℕ -> ℕ -> ℕ -> Set
m < n ≤ k = (m <′′ n) × (n ≤′′ k)

◁ : ℕ -> ℕ -> ℕ -> Set
(◁ k) m n = n < m ≤ k

◁-access : forall k m n -> (m <′′ k) -> (m < n ≤ k) -> Acc (◁ k) n
◁-access .(suc m) m .(suc m) ≤′′-refl (≤′′-refl , 1+m≤1+m) = 
  acc (suc m) (\y 1+m<y∧y≤1+m -> ⊥-elim (¬[m<n∧n≤m] 1+m<y∧y≤1+m)) 
◁-access k m .(suc m) (≤′′-step 1+m<k) (≤′′-refl , 1+m≤k) = 
  acc (suc m) (\y -> ◁-access k (suc m) y 1+m<k) 
◁-access .(suc m) m n ≤′′-refl (≤′′-step 1+m<n , n≤1+m) = 
  acc n (⊥-elim (m<n⇒¬n≤m 1+m<n n≤1+m)) 
◁-access k m n (≤′′-step 1+m<k) (≤′′-step 1+m<n , n≤k) = 
  ◁-access k (suc m) n 1+m<k (1+m<n , n≤k)

ℕ◁-wf : forall k -> well-found (◁ k)
ℕ◁-wf k m = acc m access 
  where access : forall n -> (m <′′ n × n ≤′′ k)  -> Acc (◁ k) n
        access n (m<n , n≤k) = 
         ◁-access k m n (≤′′-trans m<n n≤k) (m<n , n≤k) 

-- McCarthian Maximum.

P : ℕ -> ℕ -> Set
P k n = Σ ℕ (\fn -> n ≤′′ k -> fn ≡ k)

f : (k : ℕ) -> (n : ℕ) -> P k n  
f k = rec-wf (ℕ◁-wf k) body
 where 
  body : (i : ℕ) -> ((j : ℕ) -> i < j ≤ k -> P k j) -> P k i
  body n rec with (k ≤′′? n)
  ... | inj₁ k≤n = (n , \n≤k -> ≤′′-antisym n≤k k≤n) 
  ... | inj₂ n<k with rec (1 + n) (≤′′-refl , n<k)
  ...       | (m , 1+n≤k⇒m≡k) with 1+n≤k⇒m≡k n<k 
  ...         | m≡k with rec m (≡-subst (\i -> n <′′ i) (≡-sym m≡k) n<k ,
                                ≡-subst (\i -> m ≤′′ i) m≡k ≤′′-refl)
  ...           | (h , m≤k⇒h≡k) = 
                    (h , \_ -> m≤k⇒h≡k (≡-subst (\i -> m ≤′′ i) m≡k ≤′′-refl))
 

-- Building new accessibility from old.

-- relations

ℙ : Set -> Set1
ℙ A = A -> Set

singleton : {A : Set} -> A -> ℙ A
singleton a = \b -> a ≡ b

_←_ : Set -> Set -> Set1
B ← A = A -> B -> Set

_º : {A B : Set} -> B ← A -> A ← B
(r º) b a = r a b

infixr 8 _·_ 
infixr 9 _○_

_·_ : {A B : Set} -> (B ← A) -> ℙ A -> ℙ B
(R · s) b = ∃ (\a -> (s a × R a b))

_○_ : {A B C : Set} -> C ← B -> B ← A -> C ← A
(R ○ S) a = R · (S a)

infixr 2 _⊆_ _⊇_

_⊆_ : {A : Set} -> ℙ A -> ℙ A -> Set
r ⊆ s = forall a -> r a -> s a

_⊇_ : {A : Set} -> ℙ A -> ℙ A -> Set
r ⊇ s = s ⊆ r

infixr 6 _⊑_ _⊒_ 

_⊑_ : {A B : Set} -> (B ← A) -> (B ← A) -> Set
R ⊑ S = forall a -> R a ⊆ S a

_⊒_ : {A B : Set} -> (B ← A) -> (B ← A) -> Set
R ⊒ S = S ⊑ R

fun : {A B : Set} -> (A -> B) -> (B ← A)
fun f a = singleton (f a)

acc-⊑ : {a : Set}{_≪_ _<_ : a -> a -> Set} ->
    _≪_ ⊑ _<_ -> (x : a) -> Acc _<_ x -> Acc _≪_ x
acc-⊑ {a}{_≪_} ≪⊑< x (acc .x h) = acc x access  
  where access : (y : a) -> (y ≪ x) -> Acc _≪_ y
        access y y≪x = acc-⊑ ≪⊑< y (h y (≪⊑< y x y≪x)) 

acc-fRfº : {a b : Set}{R : a -> a -> Set}{f : a -> b} ->
   (x : a) -> Acc (fun f ○ R ○ ((fun f) º)) (f x) -> Acc R x
acc-fRfº {a}{b}{R}{f} x (acc ._ h) = acc x access 
  where access : (y : a) -> R y x -> Acc R y
        access y xRy = 
         acc-fRfº y (h (f y) (x , ((y , (≡-refl , xRy)) , ≡-refl))) 

-- transitive closure

data _⁺ {a : Set}(R : a -> a -> Set) : a -> a -> Set where
  ⁺-base : forall {x y} -> R x y -> (R ⁺) x y
  ⁺-step : forall {x z} -> Σ a (\y -> R y z × (R ⁺) x y) -> (R ⁺) x z 

acc-tc : {a : Set}{R : a -> a -> Set} -> 
      (x : a) -> Acc R x -> Acc (R ⁺) x
acc-tc {a}{R} x ac = acc x (access x ac)
  where access : (x : a) -> Acc R x -> (y : a) -> (R ⁺) y x -> Acc (R ⁺) y
        access x (acc .x h) y (⁺-base yRx) = acc-tc y (h y yRx)  
        access x (acc .x h) y (⁺-step (z , (zRx , yR⁺z))) = 
         access z (h z zRx) y yR⁺z 



{-- Expanding the definition, we get:

  rec_wf {a}{_<_} wf f x with wf x
  ...  | (acc .x h) = f x (\y y<x -> acc_rec _<_ (\z _ -> f z) y (h y y<x))

preferable:
  rec_wf {a}{_<_} wf f x =  f x (\y y<x -> rec_wf wf f y)

x₁ x₂ x₃ .
 --}
} wf f x =  f x (\y y<x -> rec_wf wf f y)

x₁ x₂ x₃ .
 --}