WIP: Make proof mode terms more compact

Closed Joseph Tassarotti requested to merge ci/joe/compact_ipm into master

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

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 Δ and Δ' 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, tac_rename becomes:

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.

The 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 False.

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 Qed. and 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.

Merge request reports