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

[Shin-Cheng Mu]

On Thu, 20 Mar 2008 14:25:34, Nils Anders Danielsson wrote:
> On Thu, Mar 20, 2008 at 8:43 AM, Ulf Norell <ulfn at cs.chalmers.se>  
> wrote:
>>
>> I suppose you could try to unwrap. Maybe something like
>>
>> data Wrap : List N -> N -> Set where
>>  W : forall {xs} bnd -> Wrap xs bnd
>>
>> f : forall {i} -> (xs : [ N ]) -> Wrap xs i -> N
>> f {i} [] _ = []
>> f {i} (x :: xs) (W .i) with lemma i
>> ... | j with f {j} xs (W j)
>> ...     | _ = 0
> Shin-Cheng, if you can describe your original problem in more detail,
> then we can try to find a slightly nicer solution.

Yes. I am interested in designing an unfold (for trees) for
cases that are known to terminate. For example, consider this
datatype for binary trees:

  data Tree (a : Set) : Set where
     Nul : Tree a
     Tip : a -> Tree a
     Bin : Tree a -> Tree a -> Tree a

We can write a function split having type:

   split : {a : Set} -> [ a ] -> ⊤ ⊎ a ⊎ ([ a ] × [ a ])

that splits a list into two halfs of roughly the same lengths
when the size is big enough (definition given below). When
split is repeatedly called in an unfold, we span a tree that
is roughly balanced.

An unfold defined in the way we'd do in a common functional
language, which may have this type:

   unfoldT : {a b : Set} ->
      (f : b -> ⊤ ⊎ a ⊎ (b × b)) -> b-> Tree a

does not (and shall not) pass the termination check. I could
switch to co-inductive Trees, but I would like to be able to
feed the constructed tree to a fold. For example, folding
the tree constructed by "unfoldT split" with "foldT merge"
gives me mergesort. So I'd like to stick with inductive types
and with the typical program construction approach providing a
separate proof that the unfolding phase terminates.

One possibility is to have unfoldT take some extra arguments
representing a bound on the seed. The unfold, having many
arguments, looks quite complicated,

When I talked about it with Nils Anders, he suggested wrapping
this bound information in the type of the seed (B). A possible
candidate of unfold may look like this:

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

whose definition (given below) is reasonably clean. Here n
is some bound on the seed B. The type of f ensures that the
bound strictly decreases with every call to f. The definition
of unfoldT↓ pattern matches on n, which makes the termination
check happy.

We can then define a datatye Split:

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

which maintains that the length of xs is bounded by bnd,
and make the type of split↓ be:

   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
but basically looks like this:

   split↓ {a}{i} (Sp [] .(suc i) _) = ... -- base case 1
   split↓ {a}{i} (Sp (x ∷ []) .(suc i) _) = ... -- base case 2
   split↓ {a}{i} (Sp (x ∷ (y ∷ xs)) .(suc i) #x∷y∷xs≤1+i)
      with lemma1 {a}{x}{y}{xs}{i} #x∷y∷xs≤1+i
   ... | exists {witness = j} (#y∷xs≤1+j , 1+j≡i)
        ..  -- calls split↓ {a}{j} (Sp (y ∷ xs) ...)

The function f I gave in my previous email was a simplified
version of split↓. As Ulf pointed out, this is due to the
call to lemma1.

I can probably separate the list xs and proof about its
length, which would kind of defeat the original purpose of
coupling xs with its bound.

Any suggestions?

PS.

split : {a : Set} -> [ a ] -> ⊤ ⊎ a ⊎ ([ a ] × [ a ])
split [] = inj₁ tt
split (a ∷ []) = inj₂ (inj₁ a)
split (a ∷ x) with split x
... | inj₁ _ = inj₂ (inj₁ a)
... | inj₂ (inj₁ b) = inj₂ (inj₂ (b ∷ [] , a ∷ []))
... | inj₂ (inj₂ (y , z)) = inj₂ (inj₂ (z , a ∷ y))


unfoldT↓ : {a : Set}(B : ℕ -> Set){n : ℕ} ->
     (f : forall {i} -> B (suc i) -> ⊤ ⊎ a ⊎ (B i × B i)) ->
      B n -> Tree a
unfoldT↓ B {0} f b = Nul
unfoldT↓ B {suc i} f b with f b
... | inj₁ _ = Nul
... | inj₂ (inj₁ a) = Tip a
... | inj₂ (inj₂ (b₁ , b₂)) =
         Bin (unfoldT↓ B {i} f b₁) (unfoldT↓ B {i} f b₂)


-- split↓ is more complicated than I would hope.
-- many lemmas are omitted.

split↓ : forall {a i} -> Split a (suc i) -> ⊤ ⊎ a ⊎ (Split a i  
× Split a i)
split↓ {a}{i} (Sp [] .(suc i) _) = inj₁ tt
split↓ {a}{i} (Sp (x ∷ []) .(suc i) _) = inj₂ (inj₁ x)
split↓ {a}{i} (Sp (x ∷ (y ∷ xs)) .(suc i) #x∷y∷xs≤1+i)
    with lemma1 {a}{x}{y}{xs}{i} #x∷y∷xs≤1+i
... | exists {witness = j} (#y∷xs≤1+j , 1+j≡i)
        with split↓ {a}{j} (Sp (y ∷ xs) (suc j) #y∷xs≤1+j)
... | (inj₁ _) = inj₂ (inj₁ x)    -- impossible!
... | (inj₂ (inj₁ z)) =
          inj₂ (inj₂ (Sp (z ∷ []) i 1≤i , Sp (x ∷ []) i  
1≤i))
      where 1≤i : 1 ≤ i
            1≤i = ≡-subst (\k -> 1 ≤ k) 1+j≡i (1≤1+k {j})
... | (inj₂ (inj₂ (Sp ys .j #ys≤j , Sp zs .j #zs≤j))) =
        inj₂ (inj₂ (Sp zs i (≤-trans #zs≤j j≤i) , Sp (x ∷  
ys) i 1+#ys≤i))
      where j≤i : j ≤ i
            j≤i = ≡-subst (\m -> j ≤ m) 1+j≡i (k≤1+k {j})
            1+#ys≤i : 1 + length ys ≤ i
            1+#ys≤i = ≡-subst (\k -> 1 + length ys ≤ k) 1+j≡i  
(s≤s #ys≤j)