File size: 6,986 Bytes
6c3fe2a | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 | \section{Proofs of Properties} \label{app:proof}
\subsection{Soundness of FPS}\label{app:proof:soundness_fps}
\noindent\textbf{Theorem.}\ \textit{FPS is \textbf{sound}: for any problem $P$ and direct answer $\hat a$ resulted from FPS, $P(\hat a)$ holds.}
\begin{proof} The Lean 4 proof state of FPS initializes as:
\begin{lstlisting}[frame=single,mathescape]
case $h$
$(v_1 : T_1) \dots (v_n : T_n)$
$(h_1 : \phi_1) \cdots (h_p : \phi_p)$
$\vdash (\psi_1 \wedge \dots \wedge \psi_q)[a \mapsto ?a]$
case $a$
$(v_1 : T_1) \dots (v_n : T_n)$
$(h_1 : \phi_1) \cdots (h_p : \phi_p)$
$\vdash T_a$
\end{lstlisting}
Therefore, upon finishing the proof, we can extract from the Lean 4 kernel:
\begin{itemize}
\item A term $\hat{a} : T_a$ filling the metavariable $?a$ from the initial goal \texttt{case} $a$
\item A proof term $h$ from the initial goal \texttt{case} $h$.
\end{itemize}
Since $?a$ is filled by $\hat a$, $h$ is actually a proof of $(\forall_{i=1}^n (v_i : T_i), \forall_{i=1}^p (h_i : \phi_i), (\wedge_{i=1}^q \psi_i))[a \mapsto \hat{a}]$, i.e. $P(\hat a)$.
Therefore, $P(\hat a)$ holds by the proof term $h$.
\end{proof}
\subsection{Expressivenss of D-FPS for Find-All Problems}\label{app:proof:expressiveness_dfps}
\noindent\textbf{Theorem.}\ \textit{Regarding find-all problems, the expressiveness of D-FPS is at least as strong as that of FPS.}
\begin{proof}
We construct an injection from an arbitrary find-all FPS problem to D-FPS while preserving semantics.
Suppose the FPS problem consists of $(V, (a : T_a), \Phi, \Psi)$ and the ground-truth answer is $\bar a$. We have
$$\forall_{i=1}^n (v_i : T_i), \forall_{i=1}^p (h_i : \phi_i), (\wedge_{i=1}^q \psi_i)[a\mapsto \bar a]$$
Therefore, the following assertion holds.
\begin{equation}\label{eq:sufficienty}
\forall_{i=1}^n (v_i : T_i), \forall_{i=1}^p (h_i : \phi_i), \forall (a : T_a), (a = \bar a) \rightarrow (\wedge_{i=1}^q \psi_i)
\end{equation}
Since it is a find-all problem, $\bar a$ is the only answer (for find-unique-one problems) or the complete collection of all valid answers (for multiple-answer problems). The following assertion holds.
\begin{equation}\label{eq:necessity}
\forall_{i=1}^n (v_i : T_i), \forall_{i=1}^p (h_i : \phi_i), \forall (a : T_a), (\wedge_{i=1}^q \psi_i) \rightarrow (a = \bar a)
\end{equation}
Therefore, composing Prop.~\ref{eq:sufficienty} and Prop.~\ref{eq:necessity}, the following proposition holds:
$$\forall_{i=1}^n (v_i : T_i), \forall_{i=1}^p (h_i : \phi_i), \forall (a : T_a), (\wedge_{i=1}^q \psi_i) \leftrightarrow (a = \bar a)$$
i.e.
$$
\forall_{i=1}^n (v_i : T_i), \forall (a : T_a), \forall_{i=1}^p (h_i : \phi_i), ((\wedge_{i=1}^q \psi_i) \leftrightarrow A)[A \mapsto a=\bar a]
$$
which corresponds to the D-FPS problem $(V\cup\{(a : T_a)\}, (A : \texttt{Prop}), \Phi, \{\bigwedge_{i=1}^q\psi_i \leftrightarrow A\})$ with ground-truth answer $\bar A = (a = \bar a)$.
\end{proof}
Specifically, a multiple-answer problem with ground-truth answer $\bar a$ formulated in FPS as
$(V, (a : \texttt{Set}\ T_x), \Phi, \{a = \{x : T_x | \bigwedge_{i=1}^q \psi_i\}\})$
or
$(V \cup \{(x : T_x)\}, (a : \texttt{Set}\ T_x), \Phi, \{\bigwedge_{i=1}^q \psi_i \leftrightarrow x\in a\})$
can be mapped into D-FPS as
$(V \cup \{(x : T_x)\}, (A : \texttt{Prop}), \Phi, \{\bigwedge_{i=1}^q \psi_i \leftrightarrow A\})$
with ground-truth answer $\bar A := x \in \bar a$ (neither $a$ nor $x$ occurs free in $\Phi$).
\subsection{Completeness of D-FPS for Find-All Problems}\label{app:proof:completeness_dfps}
\noindent\textbf{Theorem.}\ \textit{D-FPS is \textbf{complete}: for any find-all problem with ground-truth $\bar A$, for any direct answer $\hat A$ resulted from D-FPS, the following proposition holds: $$\forall_{i=1}^n (v_i : T_i), \forall_{i=1}^p (h_i : \phi_i), \bar A \rightarrow \hat A$$}
\begin{proof}
Suppose the D-FPS problem consists of $(V, (A : \texttt{Prop}), \Phi, \{\psi \leftrightarrow A\})$ and the Lean 4 proof state is initializes as:
\begin{lstlisting}[frame=single,mathescape]
case $h^{\rightarrow}$ -- Forward Solving
$(v_1 : T_1) \dots (v_n : T_n)$
$(h_1 : \phi_1) \cdots (h_p : \phi_p)$
$(h^\prime : \psi)$
$\vdash ?A$
case $h^{\leftarrow}$ -- Backward Provinng
$(v_1 : T_1) \dots (v_n : T_n)$
$(h_1 : \phi_1) \cdots (h_p : \phi_p)$
$(h_a :\ ?A)$
$\vdash \psi$
case $A$ -- Hole of the answer
$(v_1 : T_1) \dots (v_n : T_n)$
$(h_1 : \phi_1) \cdots (h_p : \phi_p)$
$\vdash \texttt{Prop}$
\end{lstlisting}
Therefore, upon finishing forward-solving, we can extract from the Lean 4 kernel:
\begin{itemize}
\item A term $\hat{A} : \texttt{Prop}$ filling the metavariable $?A$ from the initial goal \texttt{case} $A$
\item A proof term $h^{\rightarrow}$ from the initial goal \texttt{case} $h^{\rightarrow}$.
\end{itemize}
Since $?A$ is filled by $\hat A$, $h^{\rightarrow}$ is actually a proof of
$$\forall_{i=1}^n (v_i : T_i), \forall_{i=1}^p (h_i : \phi_i), \forall (h^\prime : \psi), \hat A$$
The ground-truth $\bar A$ satisfies
$$\forall_{i=1}^n (v_i : T_i), \forall_{i=1}^p (h_i : \phi_i), (\psi \leftrightarrow \bar A)$$
Therefore, we have
$$\forall_{i=1}^n (v_i : T_i), \forall_{i=1}^p (h_i : \phi_i), \forall (h^\prime : \bar A), \hat A$$
i.e.,
$$\forall_{i=1}^n (v_i : T_i), \forall_{i=1}^p (h_i : \phi_i), \bar A \rightarrow \hat A$$
\end{proof}
\subsection{Soundness of D-FPS for Find-All Problems}\label{app:proof:soundness_dfps}
\noindent\textbf{Theorem.}\ \textit{D-FPS is \textbf{sound}: for any find-all problem with ground-truth $\bar A$, for any direct answer $\hat A$ resulted from D-FPS, if the backward-proving is finished, the following proposition holds: $$\forall_{i=1}^n (v_i : T_i), \forall_{i=1}^p (h_i : \phi_i), \hat A \rightarrow \bar A$$}
\begin{proof}
Upon finishing backward-proving, apart from $\hat{A}$, we can extract a proof term $h^{\leftarrow}$ from the initial goal \texttt{case} $h^{\leftarrow}$.
Since $?A$ is filled by $\hat A$, $h^{\leftarrow}$ is actually a proof of
$$\forall_{i=1}^n (v_i : T_i), \forall_{i=1}^p (h_i : \phi_i), (\forall (h_a : ?A), \psi)[?A \mapsto \hat A]$$
i.e.,
$$\forall_{i=1}^n (v_i : T_i), \forall_{i=1}^p (h_i : \phi_i), \forall (h_a : \hat A), \psi$$
The ground-truth $\bar A$ satisfies
$$\forall_{i=1}^n (v_i : T_i), \forall_{i=1}^p (h_i : \phi_i), (\psi \leftrightarrow \bar A)$$
Therefore, we have
$$\forall_{i=1}^n (v_i : T_i), \forall_{i=1}^p (h_i : \phi_i), \forall (h_a : \hat A), \bar A$$
i.e.,
$$\forall_{i=1}^n (v_i : T_i), \forall_{i=1}^p (h_i : \phi_i), \hat A \rightarrow \bar A$$
\end{proof}
Notably, for find-unique-one problems (only one valid answer exists) with queriable $a$, if it is expressed in D-FPS as in Appendix~\ref{app:proof:expressiveness_dfps} and concludes a direct answer of the form $\hat A = (a = \hat a)$, a backward proof is not required anymore (completeness implies soundness). Because of the uniqueness of $\bar a$ and Assumption~\ref{ass:satisfiable}, the valid answer term $\hat a$ must be the unique one.
|