Some community members have expressed skepticism about what might be lost in reducing everything to a problem-oriented programming model like that of “The View From the Left”. For example, a large part of typical tactic scripts in Rocq amounts to procedurally generalising goals and calling eliminators, and this is indeed well-handled by the Mc Bride—McKinna model; on the other hand, there are many other useful pieces of tactical reasoning like apply f or eapply f that aren’t discussed in that paper. If we built a system in which you could not easily backchain through a lemma, it would indeed be a pretty unrewarding system to use.
The particular case of backchaining through lemmas can, however, be addressed within a very small extension of the Mc Bride–McKinna model. For this, we will need what might be referred to as the “view from the right”. There is an analogy to be had here:
- Mc Bride and McKinna defined a general notion of “elimination operator”, and devised a pattern matching notation for it.
- We seem to need to define a general notion of “introduction operator”, and then devise a co-pattern matching notation for it.
In Epigram, we can think of the ability to return a value (written \Rightarrow \mathit {val}) as the beginning of a “view from the right”, which is just lacking any kind of right-handed decomposition. Our goal is to add this decomposition.
Consider the case of showing that a particular sum \sum _{x:\mathbf {1}}x=() is a proposition, using a lemma about the closure of propositions under internal sums. Here is our initial proof state as it might appear in our editor:
\begin {aligned}
&\mathsf {example} : \mathsf {isProp}~\textstyle \sum _{x:\mathbf {1}}x=()
\\
&\mathsf {example}~\color {gray}[?\colon \mathsf {isProp}~\textstyle \sum _{x:\mathbf {1}}x=()]
\end {aligned}
Next, we use the backchaining introduction operator, which generalises the usual “return” / \Rightarrow co-gadget of Epigram to allow for subgoals.
\begin {aligned}
&\mathsf {example} : \mathsf {isProp}~\textstyle \sum _{x:\mathbf {1}}x=()
\\
&\mathsf {example} \Rightarrow \mathsf {sumIsProp}
\\
&\mathsf {example}.\mathsf {baseIsProp}~\color {gray}[?\colon \mathsf {isProp}~\mathbf {1}]
\\
&\mathsf {example}.\mathsf {famIsProp}~\color {gray}[?\colon (x:\mathbf {1}) \to \mathsf {isProp}~(x=\mathbf {1})]
\end {aligned}
Note that with records, we can easily arrange for the subgoals of to have more human-readable names than \pi _1,\pi _2, as we’ve done above. The first goal is easy to solve using another lemma; that lemma has no subgoals, so that branch is finished off like so:
\begin {aligned}
&\mathsf {example} : \mathsf {isProp}~\textstyle \sum _{x:\mathbf {1}}x=()
\\
&\mathsf {example} \Rightarrow \mathsf {sumIsProp}
\\
&\mathsf {example}.\mathsf {baseIsProp}\Rightarrow \mathsf {unitIsProp}
\\
&\mathsf {example}.\mathsf {famIsProp}~\color {gray}[?\colon (x:\mathbf {1}) \to \mathsf {isProp}~(x=\mathbf {1})]
\end {aligned}
In the second branch, we can abstract the variable.
\begin {aligned}
&\mathsf {example} : \mathsf {isProp}~\textstyle \sum _{x:\mathbf {1}}x=()
\\
&\mathsf {example} \Rightarrow \mathsf {sumIsProp}
\\
&\mathsf {example}.\mathsf {baseIsProp}\Rightarrow \mathsf {unitIsProp}
\\
&\mathsf {example}.\mathsf {famIsProp}~x~\color {gray}[?\colon \mathsf {isProp}~(x=\mathbf {1})]
\end {aligned}
Next, we backchain through yet another lemma, namely that propositions are sets.
\begin {aligned}
&\mathsf {example} : \mathsf {isProp}~\textstyle \sum _{x:\mathbf {1}}x=()
\\
&\mathsf {example} \Rightarrow \mathsf {sumIsProp}
\\
&\mathsf {example}.\mathsf {baseIsProp}\Rightarrow \mathsf {unitIsProp}
\\
&\mathsf {example}.\mathsf {famIsProp}~x~\Rightarrow \mathsf {propsAreSets}\\
&\mathsf {example}.\mathsf {famIsProp}~x~\color {gray}[?\colon \mathsf {isProp}~\mathbf {1}]
\end {aligned}
Finally, we finish up the problem with a lemma that has no subgoals.
\begin {aligned}
&\mathsf {example} : \mathsf {isProp}~\textstyle \sum _{x:\mathbf {1}}x=()
\\
&\mathsf {example} \Rightarrow \mathsf {sumIsProp}
\\
&\mathsf {example}.\mathsf {baseIsProp}\Rightarrow \mathsf {unitIsProp}
\\
&\mathsf {example}.\mathsf {famIsProp}~x\Rightarrow \mathsf {propsAreSets}\\
&\mathsf {example}.\mathsf {famIsProp}~x\Rightarrow \mathsf {unitIsProp}
\end {aligned}
Personally, I find the above to strike a good balance between readability and writeability while maintaining the very important procedural aspect of how mathematicians write proofs; it is an extremely small generalisation of the Mc Bride–McKinna model.
We can workshop the notation and improve it, but I think the underlying idea here is viable. For those who think “But that is exactly what we already had with tactics”, that is actually my entire point: I don’t want to get rid of procedural tactical reasoning, but I do want to find a way to incorporate it into a problem-oriented notation that mostly documents itself in connection with editor facilities to see the proof state at a given step.
I won’t say that this solves all problems, but I hope it gives some impression of the methodology by which we will tackle procedural reasoning.