The Coq mailing list

[Sylvain Heraud <sylvain.heraud AT gmail.com>]

Hi,

The last recursive call (interleave_t t1 u) do not decrese on the first argument !

2011/7/11 <ldou AT cs.ecnu.edu.cn>

Hi,all.
I have the following codes in Coq:
========================
Require Import String Bool ListSet List Classical.
Definition Event := string.
Definition Trace := list Event.

Definition Trace_dec :forall (a b:Trace) ,{a = b} + {a <> b}.
repeat decide equality.
Defined.

Fixpoint map_prefix (e:Event) (O:set Trace) : set Trace :=
match O with
| nil => nil
| t::R => (e::t) :: (map_prefix e R)
end.

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!

----------------
===========================================================
Best regards!
 
窦亮

(Department of Computer Science, East China Normal University)

E-mail:ldou AT cs.ecnu.edu.cn   
 
===========================================================