Compared to "standard" intropatterns the
ssreflect intropatterns result in larger terms. This could lead to longer
Qed time. Here an example:
Lemma test : (False \/ (True /\ False)) -> False. Proof. intros [H0|[H1 H2]]; assumption. Qed. Print test. (* fun H : False \/ True /\ False => match H with | or_introl H0 => H0 | or_intror (conj _ H2) => H2 end *) Require Import ssreflect. Lemma test_ssr : (False \/ (True /\ False)) -> False. Proof. move=> [H0|[H1 H2]]; assumption. Qed. Print test_ssr. (* fun __top_assumption_ : False \/ True /\ False => (fun (_evar_0_ : forall a : False, (fun _ : False \/ True /\ False => False) (or_introl a)) (_evar_0_0 : forall b : True /\ False, (fun _ : False \/ True /\ False => False) (or_intror b)) => match __top_assumption_ as o return ((fun _ : False \/ True /\ False => False) o) with | or_introl x => _evar_0_ x | or_intror x => _evar_0_0 x end) (fun H0 : False => H0) (fun __top_assumption_0 : True /\ False => (fun _evar_0_ : forall (a : True) (b : False), (fun _ : True /\ False => False) (conj a b) => match __top_assumption_0 as a return ((fun _ : True /\ False => False) a) with | conj x x0 => _evar_0_ x x0 end) (fun (_ : True) (H2 : False) => H2)) *)
Is this by design? Should this be reported as an issue and possibly improved upon?
Summoning @Enrico Tassi who might know. I'm curious too.
I have also wondered about this. I much prefer ssreflect proofs but whenever I use tactics to build transparent terms I tend to use vanilla coq tactics to avoid the blowup. (Also for better readability of the term.)
I know where this comes from, there is a routine which takes a term with holes and abstracts the holes out with lambdas (see the _evar_n_ thing). Then when you chain tactics you don't beta-reduce the proof.
To my knowledge this is not a source of slow Qed (for the type checker a variable of the right type is better than a term of the right type). Did you measure a slowdown, or it is a speculation?
I recall having added explicit beta steps for tactics which produce "transparent" steps, eg
have @H (wrt to
have H). I can add more if it helps Qed.
If you care about the readibility of the proof term, you should use no tactic at all IMO. It's like hoping a compiler generates readable assembly, an objective which is orthogonal, if not opposite, to its main purpose.
I will try to measure whether the slow Qed is because of large terms. (I just saw huge terms constantly repeating subgoals as an output of a larger automation procedure).
I agree with everything you (Enrico) said except for the last part, because I have a use-case similar to the one of @Janno : Sometimes writing a (dependently typed) term is annoying/tricky to write by hand. In those cases I like to write it using tactics followed by some post-processing. So the less noise there is is, the less post-processing is required. Admittedly, this has nothing to do with proof checking time.
Unless I'm mistaken, the blow up we see here can be solved by
eval lazy in (or even
lazy beta). But maybe you mean "manual post-processing"...
Here a pathological example (that is quite close to actual code). More than twice the time for less than half the iterations.
This emphasizes that for automation standard Coq could be a faster choice. I still use
ssreflect for coherence.
Require Import List. Lemma neq_0_1 : 0 = 1 -> False. Proof. easy. Qed. Set Ltac Profiling. Reset Ltac Profile. Lemma fast : In 1 (repeat 0 500) -> False. Proof. intros H. do 500 (destruct H as [H|H]; [apply (neq_0_1 H)|]). exact H. Qed. Show Ltac Profile. (* 500 iterations; total time: 0.578s *) Reset Ltac Profile. Lemma slow : In 1 (repeat 0 200) -> False. Proof. do 200 (move=> [/neq_0_1|]; [exact id|]). exact id. Qed. Show Ltac Profile. (* 200 iterations; total time: 1.281s *)
(Also I'm not sure how to measure Qed time. The timings given are only for the tactics.)
*Just counting seconds, the
Qed time for larger iteration numbers also differs by more than a factor of 2.
You can use
Time Qed. It doesn't track universe minimization so be aware that the timings will be only be comparable if both proofs have similar universes and constraints.
A useful trick to perform multiple measurements is to use
Fail Fail Time Qed. which allows backtracking over just that statement instead of going back to the beginning of the proof.
fast 1000 iterations: 5.018 secs;
slow 500 iterations: 8.272 secs.
To be clear: I am ok with the more powerful
ssreflect tactics taking more time to construct a term. I wish that the constructed term would
Qed as fast as standard Coq.
I am getting similar results, I think. For 500 iterations in both proofs I get 1.4s versus 8.4s. Admittedly my machine is quite busy but the timings seem stable. I have also changed the ssreflect version to be a bit closer to the vanilla coq one:
intros H. do 500 (case: H => [/neq_0_1 H|H]; [exact H|]). exact H.
@Enrico Tassi pinging you just in case you missed the last bits of discussion above. There does indeed seem to be a measurable difference in Qed times.
Thanks for the heads up and the test case, I'll open an issue
Last updated: Feb 08 2023 at 23:03 UTC