The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT cnam.fr>]

Le Thu, 8 Nov 2007 12:24:16 +0000, Edsko de Vries 
<devriese AT cs.tcd.ie>
a écrit:
>   Lemma merge_comm : forall l1 l2,
>     merge (l1, l2) = merge (l2, l1).
> 
> (With the "symmetric" merge, this will hold even if the lists aren't 
> sorted).
> However, I get stuck when I try to prove this using functional induction:
> 
>   Proof.
>     intros l1 l2.  
>     functional induction (merge (l1, l2)).
>     functional induction (merge (l2, l1)).
>     reflexivity.

Hi

You should not use functional induction with non variable arguments
(as with "induction"). 

Here is an example of use of functional induction.

Lemma merge_nil : forall x l2,
  x= (nil,l2) -> merge x = l2.
  intros x.
  functional induction (merge x);auto;intros.
  inversion H;subst;trivial.
  inversion H;subst;trivial.
  inversion H;subst;trivial.
  inversion H.
  inversion H;subst;trivial.
  inversion H;subst;trivial.
Qed.


Cheers,
Pierre Courtieu