The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

I just ran some performance tests where proofs that started with the 
tactic sequence "simple inversion H; intros; subst" instead use the 
tactic sequence "inversion H; subst".  Nothing else about these proofs 
was altered - just this first line.  Still, the impact on just the Qed 
times at the end of the proofs was very large:


simple inversion vs. inversion (all times in seconds)
3.234                 120.656
0.846                 28.994
0.908                 30.288
117.987               1061


Obviously, inversion does more than simple inversion - but in those 
cases where its attempts to do more don't pan out, there is still 
considerable impact on the resulting proof term, and one pays for that 
at Qed time.  In the proofs I tested, the subgoals resulting from 
"inversion H;subst" vs. "simple inversion H;intros;subst" were identical 
up to the order of hypothesis, hence no simplifications that inversion 
attempted impacted the proof, even though the impact on the proof term 
was dramatic.

-- Jonathan