7
$\begingroup$

I have been looking into various proof assistants, and came across the method of proof by reflection in Coq, which (from what I understand) allows one to verify a program provides the correct "answer" (in boolean form) as to the truth value of a proposition, and then use the result of that program as proof instead of the explicit proof term, which may be excessively long (the example in the linked article is proof of evenness of a large natural number).

This reminds me of a technique seen in the Homotopy Type Theory book described as the "encode-decode" method. This method performs a similar feat, by proving that a given type family (which is interpreted as a predicate) is equal to another type family whose values are all either $\boldsymbol{1}$ or $\boldsymbol{0}$, allowing simple computation of otherwise lengthy proofs (in particular, computing the (dis-)equality of two natural numbers in section 2.13).

In the case of proving evenness (as in the linked proof reflection article) it seems to me we can do the same with the encode-decode method. We define our $\mathrm{code} : \mathbb{N} \to U$ by:

$$ \begin{eqnarray} \mathrm{code} (0) &=& \boldsymbol{1} \\ \mathrm{code} (1) &=& \boldsymbol{0} \\ \mathrm{code} (S(S(m)) &=& \mathrm{code}(m) \end{eqnarray} $$

For the direction $\mathrm{code} (n) \to \mathrm{isEven}(n)$ we define a function $\mathrm{decode} : \prod_{n : \mathbb{N}} \mathrm{code} (n) \to \mathrm{isEven}(n)$ by induction as follows:

$$ \begin{eqnarray} f(0, r) &=& \mathrm{Even}_0 \\ f(1, r) &=& \mathrm{ind}_\boldsymbol{0}(\mathrm{isEven}(1))(r) \\ f(S(S(m), r) &=& \mathrm{Even}_{SS}(m,\, f(m,r)) \end{eqnarray} $$

For the reverse, we define $\mathrm{encode} : \prod_{n : \mathbb{N}} \mathrm{isEven}(n) \to \mathrm{code}(n)$ as composition of two functions $h : \prod_{n : \mathbb{N}} \mathrm{isEven}(n) \to (n \% 2 = 0)$ and $k : \prod_{n : \mathbb{N}} (n \% 2 = 0) \to \mathrm{code}(n)$:

$$ \begin{eqnarray} h(n, Even_0) &=& \mathrm{refl}_0 \\ h(n, \mathrm{Even}_{SS}(m,q)) &=& h(m,q) \end{eqnarray} $$

$$ \begin{eqnarray} k(0, r) &=& * \\ k(1, r) &=& (p : \neg(1 = 0))(r) \\ k(S(S(m)), r) &=& k(m, r) \end{eqnarray} $$

Since $\mathrm{isEven}(n)$ and $\mathrm{code}(n)$ are mere propositions for all $n : \mathbb{N}$, this proves $\mathrm{isEven} = \mathrm{code}$

My question is: When dealing with proof-irrelevant propositions (i.e. mere propositions in HoTT), is one of these faculties more powerful than the other?

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.