Commit c4038e68 authored by Michael Sammler's avatar Michael Sammler
Browse files

add causes for slow Qed

parent 188c6e0c
......@@ -2,7 +2,6 @@
This repository contain a collection of interesting tricks and facts about Coq that were useful during the development of Iris.
- [simpl.v](theories/simpl.v): `simpl` and similar reduction insert casts even if they do not change the goal which can slow down Qed.
- [slow_qed.v](theories/slow_qed.v) Causes for slow Qed times
- TODO: How to use custom typeclass databases
- TODO: How to iterate over all solutions for typeclass search
- TODO: Causes for slow Qed times
......@@ -7,4 +7,4 @@
-Q theories tricks
theories/simpl.v
\ No newline at end of file
theories/slow_qed.v
\ No newline at end of file
(** [simpl] and other reduction tactics inserts casts in the goal even
if they don't change the goal. This can lead to a slower Coq. To avoid
this behaviour, one can use [try progress simpl] instead of [simpl].
See also the discussion at
https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs.20.26.20plugin.20devs/topic/exact_no_check.2C.20repeated.20casts.20in.20proof.20terms
and https://github.com/coq/coq/pull/15104 *)
Goal 1 = 1.
Set Printing All.
Show Proof.
(** => ?Goal *)
simpl.
Show Proof.
(** => (?Goal : @eq nat (S O) (S O))
Notice the cast. *)
Undo.
Show Proof.
(** => ?Goal *)
try progress simpl.
Show Proof.
(** => ?Goal.
Notice that there is no cast *)
Abort.
(** This file documents some known causes for slow Qed times. *)
(** 1. Qed can be slow because the generated proof term is large.
Consider for example the following: *)
Goal 2000 = 1 + 1999. (** Large unary numbers. *)
Time do 100 (etransitivity; [reflexivity|]).
(** => Finished transaction in 0.949 secs (0.949u,0.s) (successful) *)
(** Uncomment the following to see that 2000 is repeated very often
in the proof term and thus makes it very large. *)
(* Set Printing Implicit. Show Proof. *)
(** => (@eq_trans nat 2000 2000 (1 + 1999) (@eq_refl nat 2000)
(@eq_trans nat 2000 2000 (1 + 1999) (@eq_refl nat 2000) ...))*)
reflexivity.
(** This Qed is now quite slow. *)
Time Qed.
(** => Finished transaction in 1.036 secs (1.036u,0.s) (successful) *)
(** In theory, Coq realize that large parts of the previous proof term
are shared (e.g. 2000 repeats very often) and use this to gain
efficiency. But in practice, this is difficult and Coq does not
exploit the sharing. (Concretely, Coq tries to do hash-consing but it
cannot be use for type-checking for some reason).
Thus, we have to help Coq to realize that there is sharing by
introducing let-bindings: *)
Goal 2000 = 1 + 1999.
(** Introduce let bindings for the large numbers. *)
pose (x := 2000).
pose (y := 1999).
change_no_check (x = 1 + y).
(** Now the following is a lot faster: *)
Time do 100 (etransitivity; [reflexivity|]).
(** => Finished transaction in 0.042 secs (0.042u,0.s) (successful) *)
(** The proof term explicitly shares the large numbers via the let-bindings for x and y *)
(* Set Printing Implicit. Show Proof. *)
(** => let x := 2000 in
let y := 1999 in
@eq_trans nat x x (1 + y) (@eq_refl nat x)
(@eq_trans nat x x (1 + y) (@eq_refl nat x) ...) *)
reflexivity.
(** Qed now is a lot faster: *)
Time Qed.
(** => Finished transaction in 0.013 secs (0.013u,0.s) (successful) *)
(** 2. Another reason for slow Qed can be that [simpl] and other
reduction tactics inserts casts in the goal even if they don't change
the goal. To avoid this behaviour, one
can use [try progress simpl] instead of [simpl].
See also the discussion at
https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs.20.26.20plugin.20devs/topic/exact_no_check.2C.20repeated.20casts.20in.20proof.20terms
and https://github.com/coq/coq/pull/15104 *)
Goal 1 = 1.
Set Printing All.
Show Proof.
(** => ?Goal *)
(** No cast *)
simpl.
Show Proof.
(** => (?Goal : @eq nat (S O) (S O)) *)
(** Notice the cast. *)
Undo.
Show Proof.
(** => ?Goal *)
try progress simpl.
Show Proof.
(** => ?Goal. *)
(** Notice that there is no cast *)
Abort.
(** 3. Another common reason for slow Qed can be the use of reduction
tactics like [simpl] that are not part of the kernel. Concretely, when
using [simpl], the kernel only seen the Goal before and after [simpl]
and has to figure out itself how to get from one to the other.
To avoid this, it is recommended to use vm_compute for complicated
simplifications (as vm_compute is part of the kernel and leaves a
special cast to tell the kernel that it should use vm_compute).
Also using [Strategy] can help guide the kernel. *)
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment