Terminating decision on a tree

Tree.agda

open import Agda.Builtin.Nat renaming (Nat to ℕ)

open import List
open import Decidable

data _≤_ : ℕ → ℕ → Set where
  0≤n    : ∀{n} → zero ≤ n
  sn≤sm : ∀{n m} → n ≤ m → (suc n) ≤ (suc m)

_≤?_ : (n m : ℕ) → Dec (n ≤ m)
zero ≤? zero = yes 0≤n
zero ≤? suc m = yes 0≤n
suc n ≤? zero = no (λ ())
suc n ≤? suc m with n ≤? m
...            | yes n≤m = yes (sn≤sm n≤m)
...            | no ¬n≤m = no φ
                           where φ : _
                                 φ (sn≤sm n≤m) = ¬n≤m n≤m

data Tree : Set where
  leaf : ℕ → Tree
  stem : ℕ → List (Tree) → Tree

data ∣_∣≤_ : Tree → ℕ → Set where
  leaf : ∀{n m}    → n ≤ m → ∣ leaf n ∣≤ m
  stem : ∀{n m ts} → n ≤ m → All (∣_∣≤ m) ts → ∣ stem n ts ∣≤ m


-- A tempting strategy is to recurse the case for (stem n ts) by checking the
-- result of (all (∣_∣≤ m) ts), but this does not pass termination checking

module Naive where
  {-# TERMINATING #-}
  ∣_∣≤?_ : (t : Tree) → (n : ℕ) → Dec (∣ t ∣≤ n)
  ∣ leaf n    ∣≤? m with n ≤? m
  ...               | yes 0≤n = yes (leaf 0≤n)
  ...               | yes (sn≤sm n≤m) = yes (leaf (sn≤sm n≤m))
  ...               | no ¬n≤m = no φ
                                where φ : _
                                      φ (leaf n≤m) = ¬n≤m n≤m
  ∣ stem n ts ∣≤? m with n ≤? m
  ...               | no ¬n≤m = no φ
                                where φ : _
                                      φ (stem n≤m _) = ¬n≤m n≤m
  ...               | yes n≤m with all (∣_∣≤? m) ts -- Agda: Does this terminate?
  ...                                   | yes [] = yes (stem n≤m [])
  ...                                   | yes (x ∷ xs) = yes (stem n≤m (x ∷ xs))
  ...                         | no ¬All = no φ
                                          where φ : _
                                                φ (stem _ pf) = ¬All pf

-- Instead, we cut off the left branch of the tree, to create a structurally
-- smaller case

∣_∣≤?_ : (t : Tree) → (n : ℕ) → Dec (∣ t ∣≤ n)
∣ leaf n          ∣≤? m with n ≤? m
...                     | yes 0≤n = yes (leaf 0≤n)
...                     | yes (sn≤sm n≤m) = yes (leaf (sn≤sm n≤m))
...                     | no ¬n≤m = no φ
                                    where φ : _
                                          φ (leaf n≤m) = ¬n≤m n≤m
∣ stem n []       ∣≤? m with n ≤? m
...                     | yes 0≤n = yes (stem 0≤n [])
...                     | yes (sn≤sm n≤m) = yes (stem (sn≤sm n≤m) [])
...                     | no ¬n≤m = no φ
                                    where φ : _
                                          φ (stem n≤m _) = ¬n≤m n≤m
∣ stem n (t ∷ ts) ∣≤? m with ∣ t ∣≤? m
...                     | no ¬∣t∣≤m = no φ
                                      where φ : _
                                            φ (stem _ (∣t∣≤m ∷ _)) = ¬∣t∣≤m ∣t∣≤m
...                     | yes ∣t∣≤m with ∣ stem n ts ∣≤? m
...                                 | no ¬rst = no φ
                                                where φ : _
                                                      φ (stem n≤m (_ ∷ rst)) = ¬rst (stem n≤m rst)
...                                 | yes (stem n≤m rst) = yes (stem n≤m (∣t∣≤m ∷ rst))