String-free proofterms (#172) · Issues · Iris / Iris

String-free proofterms

The goal of this is to end up in a situation where the proof terms constructed by the proof mode do NOT contain the variable names. Such names really should not end up in the proof term. @ppedrot and @janno are convinced this would give us significant speed-up. (We have a bet going here, with the threshold being 40% speedup. Let's see. ;)

@ppedrot, @janno and me recently spent some time thinking about this and I want to write this down before we forget. The basic idea is to have a version of envs_entails, say envs_entails_nameless, that takes two lists of propositions, instead of lists of pairs of strings and propositions. Now, we can change back and forth between envs_entails named_env and envs_entails_nameless nameless_env -- the two are convertible as we always have concrete lists for our environments. So before we apply any Coq tactic like apply, we always change the goal to its nameless form, and then change it back when we are done. These conversions are not actually recorded in the proof term; they only affect the type of the evar as stored in Coq, which is irrelevant at Qed time. Essentially, we use the type of the evar as per-goal mutable state to store the names in.

The main problem with this is that the coq_tactics would have to be written in nameless style, and the Ltac tactics wrapping them would have to take care of setting the right names in the subgoals they create. However, this is a problem that any solution to the issue will have -- if strings move out of the proof terms, we can't have them in Coq-level lemmas. Maybe Ltac2/Mtac could provide some other (less hacky) form of per-goal mutable state, but that wouldn't change this problem.

The goal of this is to end up in a situation where the proof terms constructed by the proof mode do NOT contain the variable names.  Such names really should not end up in the proof term. @ppedrot and @janno are convinced this would give us significant speed-up.  (We have a bet going here, with the threshold being 40% speedup. Let's see. ;)

@ppedrot, @janno and me recently spent some time thinking about this and I want to write this down before we forget. The basic idea is to have a version of `envs_entails`, say `envs_entails_nameless`, that takes two lists of propositions, instead of lists of pairs of strings and propositions. Now, we can `change` back and forth between `envs_entails named_env` and `envs_entails_nameless nameless_env` -- the two are convertible as we always have concrete lists for our environments. So before we apply any Coq tactic like `apply`, we always `change` the goal to its nameless form, and then `change` it back when we are done. These conversions are not actually recorded in the proof term; they only affect the type of the evar as stored in Coq, which is irrelevant at `Qed` time. Essentially, we use the type of the evar as per-goal mutable state to store the names in.

The main problem with this is that the `coq_tactics` would have to be written in nameless style, and the Ltac tactics wrapping them would have to take care of setting the right names in the subgoals they create. However, this is a problem that any solution to the issue will have -- if strings move out of the proof terms, we can't have them in Coq-level lemmas. Maybe Ltac2/Mtac could provide some other (less hacky) form of per-goal mutable state, but that wouldn't change this problem.