ssreflect intropattern blowup · Coq users

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

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.

Stream: Coq users

Topic: ssreflect intropattern blowup

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