Disjoint index intervals of compiled clause blocks

Local positive auxiliary names carry an index in their original signed clause block. Adding the preceding signed-block lengths gives disjoint intervals for distinct original clauses.

Main results

• PositiveExactOne.blockOffset_mono, PositiveExactOne.blockOffset_succ.
• PositiveExactOne.blockOffset_range_injective: a global index identifies its block and slot.
• PositiveExactOneCompile.signedOffset_range_injective: the actual compiler specialization.

References

These are original list-index identities for the explicit compiler.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.blockOffset_mono {V : Type u_1} (bs : List (CNF V)) {i j : ℕ} (hij : i ≤ j) : blockOffset bs i ≤ blockOffset bs j

Prefix lengths are monotone, without requiring the blocks to be nonempty.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.blockOffset_succ {V : Type u_1} (bs : List (CNF V)) {i : ℕ} (hi : i < bs.length) : blockOffset bs (i + 1) = blockOffset bs i + List.length bs[i]

Passing an existing block adds exactly its number of signed clauses.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.blockOffset_range_injective {V : Type u_1} (bs : List (CNF V)) {i j a b : ℕ} (hi : i < bs.length) (hj : j < bs.length) (ha : a < List.length bs[i]) (hb : b < List.length bs[j]) (he : blockOffset bs i + a = blockOffset bs j + b) : i = j ∧ a = b

Local index ranges of different blocks are disjoint. No positive-length assumption on unrelated blocks is needed.

theorem Cslib.Logic.PL.CNF.PositiveExactOneCompile.signedOffset_range_injective {V : Type u_1} (φ : CNF V) {i j a b : ℕ} (hi : i < List.length φ) (hj : j < List.length φ) (ha : a < List.length (FromSAT.clause i φ[i])) (hb : b < List.length (FromSAT.clause j φ[j])) (he : signedOffset φ i + a = signedOffset φ j + b) : i = j ∧ a = b

In the actual compiler, a positive auxiliary's global signed-clause position uniquely identifies its original clause block and local signed-clause position.