# WIP: Make proof mode terms more compact

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.