The Coq mailing list

[Laurent Thery <Laurent.Thery AT sophia.inria.fr>]

Hi Dimitri,

a slightly more general solution than David's one  is to
split your function in two:
  one that is recursive on the first argurment 
  and one that is recursive on the second argument.

like this Coq will accept the recursion.

Following David's example, here is a possible code

aux1 is the function that is recursive on the first argument
aux2 is the function that is recursive on the second one.

-------------------------------

Require Import PolyList.
Section a.
Variable A:Set.
Variable test:A -> A ->bool.

Definition merge :=
   Fix aux1 {
    aux1/1: (list A) -> (list A) ->(list A) := 
    [l1, l2:(list A)]
      Cases l1 l2 of
        (cons a t1) (cons b t2) =>
            Cases (test a b) of
              true => (cons a (aux1t1 (cons b t2)))
            | false =>
               (Fix aux2 {aux2/1: (list A) -> (list A) :=
                  [l3:(list A)]
                    Cases l3 of
                      (cons c t3) =>
                         Cases (test a c) of
                           true => (cons a (aux1 t1 (cons c l3)))
                         | false =>(cons c (aux2 t3))
                         end
                    | nil => (cons a t1)
                    end
                }
               (cons b t2))
             end
        | nil _ => l2
        | _ nil => l1
        end
   }.
End a.

Mutual Inductive AB: Set :=
     a: AB
    | b: AB .

Definition test :=
   [x, y:AB]
      Cases x y of
          a _ => true
         | _ _ => false
      end.

Eval Compute in (merge ? test (cons b (cons a (nil ?))) (cons a (nil ?))).

----------------------------



--Laurent