TwistedMaxAcc.agda

{-# OPTIONS --without-K --safe #-}

module TwistedMaxAcc where

open import Data.Nat using (ℕ ; zero ; suc ; _>_ ; _≤_ ; _≤″_ ; less-than-or-equal ; _≰_ ; _>?_ ; _≤?_ ; _+_)
open import Data.Nat.Properties using (≤-reflexive ; ≤-antisym ; ≮⇒≥ ; >⇒≢ ; ≤⇒≤″ ; m≤m+n ; +-suc ; +-comm)
open import Data.Empty using (⊥-elim ; ⊥)
open import Relation.Nullary using (Dec ; yes ; no)
open import Relation.Binary.PropositionalEquality.Core using (refl ; _≡_ ; subst ; sym)

≤step : ∀ {m n} → m ≤ n → m ≤ suc n
≤step _≤_.z≤n       = _≤_.z≤n
≤step (_≤_.s≤s m≤n) = _≤_.s≤s (≤step m≤n)

{-
f : ℕ → ℕ → ℕ
f k n with  k ≤? n
... | yes p = n
... | no ¬p = f k (f k (suc n))
-}

mutual
  -- call graph
  data Acc : ℕ → ℕ → Set where
    ALEQ : ∀ {k n} → k ≤ n → Acc k n
    AGT  : ∀ {k n} →
              k > n →
              (A[k,n+1] : Acc k (suc n)) →
              Acc k (f′ k (suc n) A[k,n+1]) →
          --------------------------------------
              Acc k n

  f′ : (k : ℕ) → (n : ℕ) → Acc k n → ℕ
  f′ k n (ALEQ k≤n) = n
  f′ k n (AGT k>n A[k,n+1] A[k,f⟨k,n+1⟩]) = f′ k (f′ k (suc n) A[k,n+1]) A[k,f⟨k,n+1⟩]

lemma-0 : ∀ {k n} → n ≤ k → (acc : Acc k n) → f′ k n acc ≡ k
lemma-0 n≤k (ALEQ k≤n) = ≤-antisym n≤k k≤n
lemma-0 n≤k (AGT k>n A[k,n+1] A[k,f⟨k,n+1⟩])
  rewrite lemma-0 k>n A[k,n+1]                      --  f′ k n+1 A[k,n+1] ≡ k by lemma-0 with k n+1
  with A[k,f⟨k,n+1⟩]
... | ALEQ k≤f⟨k,n+1⟩ = refl
... | AGT k>f⟨k,n+1⟩ _ _ = ⊥-elim (>⇒≢ k>f⟨k,n+1⟩ refl)

acc-refl : ∀ {k} → Acc k k
acc-refl = ALEQ (≤-reflexive refl)

make-acc-ind : ∀ d n → Acc (d + n) n
make-acc-ind zero n = acc-refl
make-acc-ind (suc d) n =
  AGT 1+d+n>n A[1+d+n,1+n] (subst (Acc (1 + d + n)) (sym f′⟨1+d+n,1+n⟩≡1+d+n) A[1+d+n,1+d+n])
  where 1+d+n>n             = subst (λ x → suc x > n) (+-comm n d) (m≤m+n (suc n) d)
        A[1+d+n,1+n]        = subst (λ x → Acc x (suc n)) (+-suc d n) (make-acc-ind d (suc n))
        f′⟨1+d+n,1+n⟩≡1+d+n  = lemma-0 1+d+n>n A[1+d+n,1+n]
        A[1+d+n,1+d+n]      = acc-refl {1 + d + n}

make-acc : ∀ k n → Acc k n
make-acc k n with k >? n
... | no  k≯n = ALEQ (≮⇒≥ k≯n)
... | yes k>n with ≤⇒≤″ k>n
... | less-than-or-equal {d′} refl = subst (λ x → Acc (suc x) n) (+-comm d′ n) (make-acc-ind (suc d′) n)

f : ℕ → ℕ → ℕ
f k n = f′ k n (make-acc k n)