The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 03/20/2016 12:52 AM, Jason Gross wrote:
> Hi,
> I just ran into a tactic that's 20x slower in 8.4 than in 8.4
> <https://coq.inria.fr/bugs/show_bug.cgi?id=4630>.  Basically the tactic is:
>     match goal with
>       | [ |- appcontext[?e] ]
>         => not is_var e;
>            not is_evar e;
>            match type of e with
>              | _ <= _ => idtac
>            end;
>            generalize e
>     end
> where not is a tactical of my own devising that does the obvious thing.
>
> Is there a better way to do this?  One that doesn't require doing stuff with
> every single subterm of the goal type?
>
> Thanks,
> Jason

I have a similar tactic that wants to examine only subterms of a 
specific type.  The unfortunate thing is that context does not accept 
type casts - or actually, it does, but does nothing with them.  Because 
it would be nice to be able to do this instead "context[?e : _ <= _]".

I found that rewriting the tactic to avoid using context and instead do 
recursive descent speeds things up - but this is only worth doing if the 
goal is limited syntactically somewhat - like without binders, or at 
least without matches.

However, maybe one can use universes to limit the search?  Assuming that 
"_ <= _" is in Prop, then one can recurse over the goal using set to 
pull out one context at a time (set would replace it with a var), which 
is then examined recursively, but only if it is itself a Prop or 
something that can contain a Prop (not a Set). Hopefully, the slowdown 
comes from contexts that cannot contain Props.

-- Jonathan