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.

added 1 commit

• c4de1014 - Update tac_forall_specialize to not embed the context twice.

Compare with previous version

@jung or @robbertkrebbers could you please add a branch to lambda-rust to time against this? I do not have push rights there.

I think this is great. No time to do a proper review yet, but already some comment based on the text in the MR. Looking at:

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.

Couldn't we even avoid the first premise by letting envs_simple_replace return the old hypothesis named i. Then the tactic would be something like:

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 (P', p', Δ') => P' = P ∧ p' = p ∧ envs_entails Δ' Q
  end →
  envs_entails Δ Q.

Of course, using Ltac we still need to establish P somehow, but this way we could avoid the envs_lookup i Δ = Some (p,P) in the proof term.

That said, I'm not actually sure if this helps, the ∧ will also store the whole context in its implicit argument again.

could you please add a branch to lambda-rust to time against this? I do not have push rights there.

I just added you as a developer, so you should have push rights (to unprotected branches) now.

but this way we could avoid the envs_lookup i Δ = Some (p,P) in the proof term.

You still have it in the lemma though? Did you forget to complete the edit?

Whether this helps or not, I guess, depends on whether the proof term for this equality is eq_refl (envs_lookup i Δ), which is big, or eq_refl (Some (p,P)), which is much smaller. I think we do "compute and then reflexivity", so I suspect it is the latter -- so removing this probably doesn't help too much. I guess.

Looks like we got some numbers for lambda-rust, and we have a 10% speedup for the entire development and 15% for the lifetime logic in particular. That's awesome!

I really love the part about avoiding Δ'. However, I am less of a fan of the IPM_STATE thing. I assume this is some kind of forgetful function so it can be changed to any desired state? What kind of trace does this leave in the proof term? And do you have an idea how much of the win is due to this, vs. the Δ change?

At the moment, IPM_STATE: positive -> Type is an inductive which has a single constructor state_dummy. So, to bump the counter I apply a lemma called ipm_state_incr to the current IPM_STATE hypothesis in the context that sends state_dummy p to state_dummy (succ p). In the proof term, that amounts to a let-binding that applies this ipm_state_incr to the previous counter hypothesis. I don't think I can do a change trick directly with this encoding, because I don't think you can change something in the Coq context.

I can do another benchmark where I revert this to see how much it helps.

However, in mattermost you suggested that we could continue to use a counter embedded in the enviroment/goal somewhere, and use change to modify that. This depends on making envs_entails sealing interact with this so that indeed the terms would be convertible.

I don't think I can do a change trick directly with this encoding, because I don't think you can change something in the Coq context.

Uh, what? That'd be a strange limitation. I assumed there would be change in... but indeed the documentation does not mention such a facility. Wow. I'll ask on the Coq forums.

in mattermost you suggested that we could continue to use a counter embedded in the enviroment/goal somewhere, and use change to modify that. This depends on making envs_entails sealing interact with this so that indeed the terms would be convertible.

Yes, that would be a more invasive change (every tactic and pattern requires adjustment), but it would keep the context clean.

Actually, change in works. It's just not documented very well.

I think this idea is great. To make progress on this MR, how about the following:

1. Delegate improving the performance of iFresh to another MR. The approach that we wish to take is not yet clear.
2. Adapt this MR so that all tactics will be written in a style using match so as to avoid the double Δs.

I think the second point is pretty uncontroversial since a.) it maintains backwards compatibility b.) it gives a clear performance improvement c.) it's rather elegant. So once this MR adapts all tactics, it should be pretty much a no-brainer to merge.

Sure, sounds good to me. I will pick this up in a week or so, after the SOSP deadline.

Excellent, good luck with SOSP.

added 56 commits

• c4de1014...a9031f7f - 45 commits from branch master
• 6bc7eb79 - Delete extra copies of context from terms for some proof mode tactics.
• a4a2e903 - Avoid using tac_fresh by storing the counter value in the Coq context...
• 261c0ae5 - Fix list_reverse.ref
• 5057681c - Properly fix the .ref files for 8.8.x
• 57e607da - Convert more tac_ lemmas to not duplicate the context.
• 5f63357f - Convert remaining tac_ lemmas to not duplicate context (where straightforward)
• d8ea1bbb - Regenerate the 'IPM_STATE' counter hypothesis if the user clears it.
• 06451bb9 - Convert tac_frame to not duplicate contexts.
• d670b34b - Try to make the iFrame change faster.
• 6be00876 - Another attempt to improve tac_frame.
• 3ea7253d - Update tac_forall_specialize to not embed the context twice.

Compare with previous version

added 1 commit

• 8682b057 - Convert tac_assumption.

Compare with previous version

added 1 commit

• bd6590cb - Convert additional tactics to shrink proof term.

Compare with previous version

added 1 commit

• 3679862e - Convert remaining simple tactics.

Compare with previous version

added 1 commit

• 8085936e - Convert tac_specialize.

Compare with previous version

added 3 commits

• 560c093b - Convert tac_specialize_assert.
• 67fe3bd6 - Convert tac_specialize frame.
• f1a4c243 - Convert remaining tac_specialize_* lemmas.

Compare with previous version

added 1 commit

• 027488d8 - Try to improve performance of converted tac_specialize_*

Compare with previous version

Just curious, what's esplit doing and why is it useful here?

For some of the tactics, the converted form changes a series of implications into a large conjunction. I observed that "split" fail sometimes when there were some unresolved typeclass instances, and so tried "esplit", which worked. But I don't understand fully why split was failing.

It may be good to figure out a small example where this happens. It may be a Coq bug.