Why can't Coq define a mutually inductive append of parametrized even/odd lists?

user_1601580 0
Viewed 45

I am following Chlipala's book with Coq and I tried to extend his mutually inductive definition of appending even/odd lists but I get a recursion error by Coq:

Module mutual_induct.

  Inductive even_list (T: Set) : Set :=
  | ENil
  | ECons (t: T) (ol: odd_list T)
  with odd_list (T: Set) : Set :=
  | OCons (t: T) (el: even_list T).

  Compute ENil.

  Fixpoint elength {T: Set} (el: even_list T) : nat :=
    match el with
    | ENil _ => 0
    | ECons _ _ ol => 1 + olength ol
    end
      
  with olength {T: Set} (ol: odd_list T) : nat :=
    match ol with
    | OCons _ _ el => 1 + elength el
    end
  .

  Fixpoint eapp {T: Set} (el1 el2: even_list T) : even_list T :=
    match el1 with
    | ENil _ => el2
    | ECons _ t' ol' => ECons T t' (oapp ol' el2)
    end
  with oapp {T: Set} (ol: odd_list T) (el: even_list T) : odd_list T :=
    match ol with
    | OCons _ t' el' => OCons T t' (eapp el el')
    end
  .     
           
End Mutual_induct.

got error:

Error: Cannot guess decreasing argument of fix.

Obviously I am just learning Coq and I suppose that is why he didn't try to do it that way to not distract the reader from a weird bug... but I want to have it parametrized. How do I fix this and why is Coq complaining? (I understand intuitively it can't guess something is decreasing but from my perspective nothing seems obviously wron).

coq
1 Answers

A recursive definition in Coq is well formed only when the recursive calls are performed on subterms of the principal argument of the function. The problem with oapp is that the recursive call is performed on the other argument el (oapp el el'), which was probably a typo. Here is a corrected version:

Module mutual_induct.

  Inductive even_list (T: Set) : Set :=
  | ENil
  | ECons (t: T) (ol: odd_list T)
  with odd_list (T: Set) : Set :=
  | OCons (t: T) (el: even_list T).

  Compute ENil.

  Fixpoint elength {T: Set} (el: even_list T) : nat :=
    match el with
    | ENil _ => 0
    | ECons _ _ ol => 1 + olength ol
    end

  with olength {T: Set} (ol: odd_list T) : nat :=
    match ol with
    | OCons _ _ el => 1 + elength el
    end
  .

  Fixpoint eapp {T: Set} (el1 el2: even_list T) : even_list T :=
    match el1 with
    | ENil _ => el2
    | ECons _ t' ol' => ECons T t' (oapp ol' el2)
    end
  with oapp {T: Set} (ol: odd_list T) (el: even_list T) : odd_list T :=
    match ol with
    | OCons _ t' el' => OCons T t' (eapp el' el)
    end
  .

End mutual_induct.
user_16337700
Related