[Agda] Induction when the argument is wrapped in a constructor?

[Nils Anders Danielsson]

On Fri, Mar 21, 2008 at 3:30 PM, Shin-Cheng Mu <scm at iis.sinica.edu.tw> wrote:

>    unfoldT↓ : {a : Set}(B : ℕ -> Set){n : ℕ} ->
>        (f : forall {i} -> B (suc i) -> ⊤ ⊎ a ⊎ (B i × B i)) ->
>          B n -> Tree a

>    data Split (a : Set): ℕ -> Set where
>      Sp : (xs : [ a ]) -> (bnd : ℕ) ->
>            length xs ≤ bnd -> Split a bnd

>    split↓ : forall {a i} ->
>      Split a (suc i) -> ⊤ ⊎ a ⊎ (Split a i × Split a i)
>
>  So far so good, except that it is now split↓ that fails
>  the termination check. The definition of split↓ is horrifying [...]

I think that the problem you have is, basically, that the structures
of the input and the decreasing measure do not match very well. One
alternative approach is to allow the indices to decrease arbitrarily
and use well-founded recursion:

  open import Logic.Induction.Nat

  data Split (P : Set -> ℕ -> Set) (a : Set) : ℕ -> Set where
    nul : Split P a 0
    tip : a -> Split P a 1
    bin : forall {n l r} -> l <′ 2 + n -> r <′ 2 + n ->
          P a l -> P a r -> Split P a (2 + n)

  unfold : forall {a} (P : Set -> ℕ -> Set) ->
           (forall {i} -> P a i -> Split P a i) ->
           forall {n} -> P a n -> Tree a
  unfold {a} P f {n} p = <-rec Pred helper n p
    where
    Pred = \n -> P a n -> Tree a

    helper : forall n -> <-Rec Pred n -> Pred n
    helper n             rec p with f p
    helper zero          rec p | nul               = Nul
    helper (suc zero)    rec p | tip x             = Tip x
    helper (suc (suc n)) rec p | bin le₁ le₂ p₁ p₂ =
      Bin (rec _ le₁ p₁) (rec _ le₂ p₂)

Then you can easily define split:

  split : forall {a n} -> Vec a n -> Split Vec a n
  split []           = nul
  split (x ∷ [])     = tip x
  split (y ∷ z ∷ xs) with split xs
  ... | nul               = bin ≤′-refl ≤′-refl           (y ∷ [])     (z ∷ [])
  ... | tip x             = bin ≤′-refl (≤′-step ≤′-refl) (y ∷ x ∷ []) (z ∷ [])
  ... | bin le₁ le₂ ys zs = bin le₁'    le₂'              (y ∷ ys)     (z ∷ zs)
    where
    le₁' = ≤′-step (s≤′s le₁)
    le₂' = ≤′-step (s≤′s le₂)

Note that this definition is rather inefficient, since the recursion
parameter "rec" above traverses the proofs. Perhaps one could hope
for the compiler to optimise away this inefficiency, though.

You could also have a look at "Why Dependent Types Matter", which
shows how you can do merge sort in a structurally recursive way. The
program developed in that paper does not use an unfold, though, so it
may not be very helpful to you.

I have attached a complete development, including fold and merge sort,
which works with Agda's current libraries.

-- 
/NAD
-------------- next part --------------
A non-text attachment was scrubbed...
Name: MergeSort.agda
Type: application/octet-stream
Size: 2768 bytes
Desc: not available
Url : https://lists.chalmers.se/mailman/private/agda/attachments/20080326/b852044f/MergeSort.obj