The Coq mailing list

[Nikhil Swamy <nswamy AT microsoft.com>]

> > However, I wonder if there is some more standard idiomatic way of
> > handling a situation like this. Ideally something that doesn't
> require
> > me having to pollute my definitions with this counter
> instrumentation.
> >
> 
> Well, did you try proving a lemma analogous to the one I gave, but for
> the other "stuck" case from the original proof?  If that works, it
> avoids changing the definition of the relation.

I had a lemma very similar to the one you gave. However, the analogous lemma 
for the Rel_fun case doesn't work out easily, since it must itself rely on 
transitivity. For example, you could try to show

forall P a t t1 t2 t1' t2,
         (relate P a t (typ_fun t1 t2)) -> 
         (relate P a t1' t1) ->
         (relate P a t2 t2') -> 
         (relate P a t (typ_fun t1' t2')

However, showing this requires proving that the sub-derivations that appear 
in the premises of the first derivation can be transitively composed with the 
second and third derivations.  

Anyway, thanks very much for your help. I can get away without using these 
counters in my real system. So, although I'd be interested to see if there 
was a way to do this without using counters, I am not too concerned for the 
moment. 

--Nik

> > Also, you will notice that my proof script is not very readable at
> all
> > :( I end up doing a lot of things manually, e.g, at various points
> > when I use eauto I'm left with uninstantiated existential variables,
> > so I often have to provide explicit parameters to eapply. Any tips
> for
> > how to avoid this and/or to make my proof more readable would be
> > great!

> >
> 
> At that point, you can run [Show Proof] to see where those evars came
> from.  I bet you could avoid most such problems by changing your
> relation definition, or defining another version that you prove
> equivalent.  I recommend removing the quantification over [a] values
> for
> any sub-judgments.  Instead, just require a [Fun] proof for every
> sub-judgment.  You can prove a lemma that any [NoFun] proof can be
> converted to a [Fun] proof.