The Coq mailing list

[Eduardo Gimenez <Eduardo.Gimenez AT trusted-logic.fr>]

Dear Xingyuan,

Yes, even if the proof seems to be sound Coq's guardedness condition is no
enought smart to realize it. I didn't check the details, but I am almost sure 
that the problem comes form the fact that your proof contains a recursive 
call whose argument is not a variable that that Coq recognizes as being 
smaller than the formal argument of the function (that is, a pattern variable 
of a case on H); but a variable that is *propositionally equal* to such a 
pattern variable.  

You can avoid this problem just doing a Case instead of an Inversion, since 
Case does not perform any rewrite. Note that in this case using the tactic 
Inversion produces exactly the same effect than using  the tactic Case, since 
the instantiated argument of le is actually a general parameter of the 
predicate. Note also that there is not need for using the unrelyable tactic 
Fixpoint to show your theorem, you'd better just do a simple
induction on the first hypothesis (lt O n) and let Coq do the rest of the 
proof:

Lemma lt_O_ex : (n:nat)(lt O n)->(EX m:nat | n=(S m)).
Induction 1;EAuto.
Save.

Your sincerely,
Eduardo.


Le Tuesday 14 November 2000 16:18, vous avez ?rit :
> Hi,
> The following is a proof in which Fix and Inversion are used together:
>
> Lemma lt_O_ex : (n:nat)(lt O n)->(EX m:nat | n = (S m)).
> Fix mf 2.
> Intros.
> Inversion H.
> Show Proof.
> Exists O.
> Auto.
> Show Proof.
> Generalize (mf ? H0).
> Show Proof.
> Intros (m0, eq_m).
> Show Proof.
> Rewrite eq_m.
> Exists (S m0).
> Auto.
> Show Proof.
> Save.
>
> The final proof term is rejected by Coq for not satisfying the guarded
> condition. However, intuition told me that the recursive application of ma
> is really applied to something "smaller". My question is:
> Is it in general acceptable that the recursive function is applied to an
> arguments which are result of the Inversion command, or there should be
> some additional conditions for this?
>
> Thanks!
>
> Xingyuan Zhang