Read-back: PvsNP.encodeCNF_injective

The statement. The declaration asserts that the map $\mathrm{encodeCNF}$ (defined below) from "CNF formulas" to finite bit-strings is injective; explicitly, for all $F_1, F_2$ of the type called CNF,

$$\mathrm{encodeCNF}(F_1) = \mathrm{encodeCNF}(F_2) \;\Longrightarrow\; F_1 = F_2 .$$

There are no other hypotheses, no typeclass assumptions and no further quantified variables. The equalities on both sides are equalities of finite lists: two lists are equal exactly when they have the same length and agree entry-by-entry in order. The theorem is stated with the proof omitted (a placeholder), so what is recorded is the claim itself.

What the objects are. Every notion below is a bare list type with no side conditions.

• A bit-string ($\mathrm{Str}$) is a finite list of Booleans $b \in \{\mathsf{false}, \mathsf{true}\}$; below I write $0$ for $\mathsf{false}$ and $1$ for $\mathsf{true}$.
• A literal is an ordered pair $(s, v)$ with $s \in \{0,1\}$ a Boolean (a "sign" flag) and $v \in \mathbb{N} = \{0,1,2,\dots\}$ a natural number (a "variable index"). Every such pair is a literal; in particular $v = 0$ is allowed, and both signs are allowed for every $v$.
• A clause is a finite list of literals $[\ell_1, \dots, \ell_m]$, $m \ge 0$. The empty clause is allowed; literals may repeat; order matters (the lists $[\ell_1,\ell_2]$ and $[\ell_2,\ell_1]$ are different clauses).
• A CNF formula is a finite list of clauses $[c_1, \dots, c_k]$, $k \ge 0$. The empty formula is allowed; clauses may repeat; order matters. Nothing ties the variable indices to any bound, and nothing requires clauses to be non-empty or literals to be distinct.

Consequently the conclusion $F_1 = F_2$ means: $F_1$ and $F_2$ have the same number of clauses, the $i$-th clauses have the same number of literals for every $i$, and the $j$-th literal of the $i$-th clause has the same sign flag and the same variable index in both.

The binary digits of a natural number. For $v \in \mathbb{N}$, $\mathrm{bits}(v)$ denotes the (Mathlib) list of binary digits of $v$, least significant digit first, with no trailing zeros (i.e. no leading zeros in ordinary positional notation). It is determined by

$$\mathrm{bits}(0) = [\,] \ (\text{the empty list}), \qquad \mathrm{bits}(2n+1) = 1 :: \mathrm{bits}(n), \qquad \mathrm{bits}(2n) = 0 :: \mathrm{bits}(n)\ \ (n \ne 0),$$

where $b :: L$ means the list $L$ with $b$ prepended. Thus $\mathrm{bits}(1) = [1]$, $\mathrm{bits}(2) = [0,1]$, $\mathrm{bits}(5) = [1,0,1]$, $\mathrm{bits}(6) = [0,1,1]$; the list has length $\lfloor \log_2 v \rfloor + 1$ for $v \ge 1$, and length $0$ for $v = 0$. In particular $v = 0$ is the only number whose digit list is empty, and the last entry of $\mathrm{bits}(v)$ is $1$ whenever $v \ge 1$.

The encoding of a literal. For a literal $(s, v)$, form the Boolean list $s :: \mathrm{bits}(v) = [s, d_0, d_1, \dots, d_{r-1}]$ (the sign flag followed by the digits of $v$, $r = |\mathrm{bits}(v)|$). Replace each entry $b$ of this list by the two-bit block $[0, b]$ and concatenate, then append the two-bit block $[1, 0]$:

$$\mathrm{encodeLiteral}(s, v) \;=\; [0, s,\; 0, d_0,\; 0, d_1,\; \dots,\; 0, d_{r-1},\; 1, 0] .$$

This string has length $2(r+1) + 2 = 2r + 4$. Examples: $\mathrm{encodeLiteral}(1, 0) = [0,1,1,0]$; $\mathrm{encodeLiteral}(0, 0) = [0,0,1,0]$; $\mathrm{encodeLiteral}(1, 2) = [0,1,\,0,0,\,0,1,\,1,0]$.

The encoding of a clause. For a clause $c = [\ell_1, \dots, \ell_m]$, concatenate the encodings of its literals in order and append the two-bit block $[1, 1]$:

$$\mathrm{encodeClause}(c) \;=\; \mathrm{encodeLiteral}(\ell_1) \,\Vert\, \cdots \,\Vert\, \mathrm{encodeLiteral}(\ell_m) \,\Vert\, [1, 1],$$

where $\Vert$ is list concatenation. The empty clause encodes to $[1,1]$.

The encoding of a formula. For a formula $F = [c_1, \dots, c_k]$, concatenate the encodings of its clauses in order, with no terminator or header:

$$\mathrm{encodeCNF}(F) \;=\; \mathrm{encodeClause}(c_1) \,\Vert\, \cdots \,\Vert\, \mathrm{encodeClause}(c_k) .$$

The empty formula encodes to the empty bit-string. Every encoded string has even length, and, read in consecutive two-bit blocks, each block is $[0, b]$ (a payload bit $b$, either the sign flag or a digit of a variable index), $[1, 0]$ (end of a literal) or $[1, 1]$ (end of a clause).

Summary of the claim in these terms. For any two finite lists of finite lists of pairs (Boolean, natural number) $F_1$ and $F_2$, if the bit-strings obtained by the above three-level concatenation coincide as lists, then $F_1$ and $F_2$ coincide as lists of lists of pairs. Equivalently, distinct formulas (distinct in number of clauses, order of clauses, multiplicity or order of literals within a clause, or sign flag or index of any literal) always have distinct encodings.