The Iris Proof Mode generates large proof terms, causing
Qed. to be very slow. Part of the issue is that the proof mode context get re-embedded in the term every time the user invokes a tactic. In fact, slight variations of the context are often embedded multiple times for each tactic application. For example, consider
Lemma tac_rename Δ Δ' i j p P Q : envs_lookup i Δ = Some (p,P) → envs_simple_replace i p (Esnoc Enil j P) Δ = Some Δ' → envs_entails Δ' Q → envs_entails Δ Q.
When this lemma is applied, both
Δ' will appear in the proof term. However, the second premise shows
Δ' is a deterministic function of
Δ, so there is no need to store
Δ' in the term. This MR removes redundant context terms like this from such lemmas. For example,
Lemma tac_rename Δ i j p P Q : envs_lookup i Δ = Some (p,P) → match envs_simple_replace i p (Esnoc Enil j P) Δ with | None => False | Some Δ' => envs_entails Δ' Q end → envs_entails Δ Q.
iRename tactic, which applies
tac_rename, will now check to see whether the
evns_simple_replace computation failed by reducing it and seeing whether the resulting goal has the form
The other change this MR currently makes is to not use the
tac_fresh lemma to update the fresh symbol counter embedded in the proof context, because each application of this tactic copies the context into the proof term, somewhat pointlessly. Instead, a special
IPM_STATE hypothesis is placed into the Coq context, which contains the fresh symbol number. This hypothesis is just modified whenever
iFresh is called. If the user clears this hypothesis from the context,
iFresh regenerates it by taking the maximum of the current anonymous hypothesis numbers in the IPM context. This means we no longer need to track the symbol counter in the IPM context itself, but I have not yet deleted it in case this
IPM_STATE hypothesis business is considered too ugly.
Preliminary benchmarks on Grafana for compiling Iris itself show that this can give speed-ups on files that use IPM heavily by about 5-10%. It would be good to do benchmarking of downstream projects that are known to have slow
End section issues.
The refactoring is not done for all
tac_ lemmas yet, because in some cases the computed
Δ' is used in complicated ways in subsequent parts of the term, and I am unsure whether the changes required will be efficient. So, I do not think it's ready for line-by-line review, rather I'm opening the MR to start the general discussion and to get people who are interested to benchmark their projects.