The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

Hi,
"intuition" does silly things with the "max_list" variable that ends to make 
an unauthorized definition (for silly reason).
Add "clear max_list; " before "intuition" and things will go smoothly.

All the best,
Pierre B.

Le 26 sept. 2013 à 16:03, Rodrigo Ribeiro 
<rodrigogribeiro AT gmail.com>
 a écrit :

> Hello to all!
> 
> I'm having some trobules in understand an error message given by Coq in a 
> rather simple definition using refine tactic. The complete code is:
> 
> Require Import List Omega Arith_base.
> 
> Definition max_list : forall (l : list nat), {n | forall n', In n' l -> n > 
> n'}.
>   refine (fix max_list (l : list nat) : {n | forall n', In n' l -> n > n'} 
> :=
>             match l with
>               | nil => exist _ 0 _
>               | x :: l' => 
>                 match max_list l' with
>                   exist x' _ =>
>                     match le_gt_dec x x' with
>                       | left _ => exist _ (S x') _
>                       | right _ => exist _ (S x) _
>                     end
>                 end
>             end) ; simpl in * ; intuition ; 
>                    try (match goal with
>                           | [H : context[In _ _ -> _],
>                              H1 : In _ _ |- _] => apply H in H1 ; try omega
>                         end).
> Defined.
> 
> When I try to process the "Defined." command, Coq gives me the error: 
> "Recursive definition of max_list is ill-formed.". Can someone explain to 
> me why this is happening?
> 
> Thanks!
> 
> Rodrigo
>