The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

My guess, without trying anything, is that omega or intuition make use of [max_list] (and end up applying it to something other than l').  Try inserting a [clear max_list] between [refine] and [simpl in *].  Does that fix it?

-Jason

On Thursday, September 26, 2013, Rodrigo Ribeiro wrote:

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