The Coq mailing list

[Andreas Abel <andreas.abel AT ifi.lmu.de>]

The problem is that you claim that interleave_t is structurally
recursive in t1, but it is not.  What decreases in each recursive call
is the sum of the lengths of the lists t1 and t2.  One quick solution is
to use nested fixpoints.

Fixpoint interleave_t (t1:Trace) {struct t1}: Trace -> set Trace :=
match t1 with
| nil  => fun t2 => t2::nil
| x::u => fix aux (t2:Trace) {struct t2} : set Trace :=
           match t2 with
           | nil => t1::nil
           | y::v => set_union Trace_dec
                (map_prefix x (interleave_t u t2))
                (map_prefix y (aux v))
           end
end.

Btw, I think you meant "v" instead of "u" in the second recursive call
below.

Cheers,
Andreas

On 7/11/11 4:18 PM, 
ldou AT cs.ecnu.edu.cn
 wrote:
> Fixpoint interleave_t (t1 t2:Trace) {struct t1}: set Trace :=
> match t1, t2 with
> | nil, _ => t2::nil
> | _, nil => t1::nil
> | x::u, y::v => set_union Trace_dec (map_prefix x (interleave_t u t2)) 
> (map_prefix y (interleave_t t1 u))
> end.
> 
> ================
> I got error for the last fixpoint:
> Recursive call to interleave_t has principal argument equal to "t1" 
> instead of u.
> Any idea to fix the problem?Thanks!

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel AT ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/