source/appendix.proofs.tex

\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.