Stream: Coq users

Topic: ssreflect intropattern blowup

Andrej Dudenhefner (Jun 30 2021 at 10:56):

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?

Christian Doczkal (Jun 30 2021 at 11:17):

Summoning @Enrico Tassi who might know. I'm curious too.

Janno (Jun 30 2021 at 11:17):

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.)

Enrico Tassi (Jun 30 2021 at 11:57):

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.

Andrej Dudenhefner (Jun 30 2021 at 12:10):

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).

Christian Doczkal (Jun 30 2021 at 12:11):

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.

Enrico Tassi (Jun 30 2021 at 12:28):

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"...

Andrej Dudenhefner (Jun 30 2021 at 12:54):

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 *)
``````

Andrej Dudenhefner (Jun 30 2021 at 12:55):

(Also I'm not sure how to measure Qed time. The timings given are only for the tactics.)

Andrej Dudenhefner (Jun 30 2021 at 12:58):

*Just counting seconds, the `Qed` time for larger iteration numbers also differs by more than a factor of 2.

Janno (Jun 30 2021 at 12:59):

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.

Janno (Jun 30 2021 at 13:02):

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.

Andrej Dudenhefner (Jun 30 2021 at 13:02):

Thanks @Janno `Time Qed.`: `fast` 1000 iterations: 5.018 secs; `slow` 500 iterations: 8.272 secs.

Andrej Dudenhefner (Jun 30 2021 at 13:04):

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.

Janno (Jun 30 2021 at 13:05):

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.
``````

Janno (Jun 30 2021 at 17:47):

@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.

Enrico Tassi (Jun 30 2021 at 17:53):

Thanks for the heads up and the test case, I'll open an issue

Enrico Tassi (Jun 30 2021 at 17:56):

https://github.com/coq/coq/issues/14584

Last updated: Jun 17 2024 at 22:01 UTC