The Coq mailing list

[David Delahaye <delahaye AT jurancon.inria.fr>]

    Hi Dimitri,

    Here is a trick to deal with your example:

Require Export PolyList.

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

Definition merge:= Fix aux {aux/1: (list AB)-> (list AB) -> (list AB) :=
[l1,l2:(list AB)]
Cases l1 l2 of
|(cons a t1)(cons a t2) => (cons a (cons a (aux t1 t2)))
|(cons b t1)(cons a t2) => (cons a (aux t1 (cons b t2)))
|(cons a t1)(cons b t2) => (cons a (aux t1 l2))
|(cons b t1)(cons b t2) => (app (aux t1 t2)(cons b (cons b (nil AB))))
| _          _          => (app l1 l2)
end}.

Definition l0:=(cons a (cons b (cons a (nil AB)))).
Definition l1:=(cons b (cons a (cons a (nil AB)))).
Definition res:=Eval Compute in (merge l0 l1).

Coq < Print res.
res = 
(cons a (cons a (cons a (cons a (cons b (cons b (nil AB)))))))
     : (list AB)

    The Fix construction is used to precise that the recursion is done only on
the first argument and not on the two lists. Here, the "trick" is in the
second rule where you can decrease the first argument by putting the "b" in 
the
second argument. It's a kind of hack which gives the expected result. It works
here but may be your real example is more complicated...

    Regards.

    David.

===============================================================================
David Delahaye                                 <Email>: 
David.Delahaye AT inria.fr
<Laboratory>: The Coq Project                                  <Domain>: 
Proofs
<Adress>: INRIA-Rocquencourt Domaine de Voluceau BP105 78153 Le Chesnay Cedex
          FRANCE
<Tel>: (33)-(0)1 39 63 57 53
<Fax>: (33)-(0)1 39 63 56 84
<Url>: http://pauillac.inria.fr/~delahaye
===============================================================================

[If you have time to waste, you can have a look on my proof that 2 = 1. We 
know
 that, for -1 < x <= 1:

   ln(1 + x) = x - 1/2(x^2) + 1/3(x^3) - 1/4(x^4) + ...

 Let x = 1:

   ln(2) = 1 - 1/2 + 1/3 - 1/4 + 1/5 - 1/6 + 1/7 - 1/8 + 1/9 - ...

 Let multiply the two members by 2:

   2ln(2) = 2 - 2/2 + 2/3 - 2/4 + 2/5 - 2/6 + 2/7 - 2/8 + 2/9 - ...
   2ln(2) = 2 - 1 + 2/3 - 1/2 + 2/5 - 1/3 + 2/7 - 1/4 + 2/9 - ...

 Let sum the terms with the same denominator:

   2ln(2) = 1 - 1/2 + 1/3 - 1/4 + 1/5 - 1/6 + 1/7 - ...
   2ln(2) = ln(2)

 Finally, 2 = 1.]