Paired implication wires

Each cell has two lanes, each with an entry and an exit. Local constraints must equate all four port values. Across a gap, lane zero implies the next entry from the previous exit; lane one implies the previous exit from the next entry. These implications use separate ports. Under the local equalities, they force the representative values of consecutive cells to agree. Thus every port of a nonempty wire has the value of its first lane-zero entry.

This module uses ordinary CNF semantics. It supplies no local cell constraints or geometry. The two clauses and four literal positions per gap are counted with multiplicity, without distinctness assumptions on the port variables.

Main definitions

• Cell, Cell.Agree: two entry/exit pairs and equality of all four values.
• gapClauses, links: opposite implications across one gap and all consecutive gaps.

Main results

• eval_links_iff: under local agreement, the links equate consecutive representatives.
• agree_head, agree_head_of_ne_nil: every entry and exit has the first entry's value.
• eval_links_of_constant: constant port values satisfy every link.
• length_links, length_vars_links, length_of_mem_links: exact sizes and binary width.

References

The paired-port composition and equality argument are original.

@[reducible, inline]

abbrev Cslib.Logic.PL.CNF.PairedWire.Cell (V : Type u_2) : Type u_2

Two lanes of entry/exit variables. Lane zero's entry represents the cell's value.

def Cslib.Logic.PL.CNF.PairedWire.Cell.Agree {V : Type u_1} (cell : Cell V) (σ : V → Bool) : Prop

All four port values agree with the lane-zero entry. Local cell constraints must provide this property; the wire clauses alone do not impose it.

def Cslib.Logic.PL.CNF.PairedWire.gapClauses {V : Type u_1} (previous next : Cell V) : CNF V

Across one gap, lane zero points forward and lane one points backward.

def Cslib.Logic.PL.CNF.PairedWire.links {V : Type u_1} (cells : List (Cell V)) : CNF V

Two opposite implications across every consecutive pair of cells.

theorem Cslib.Logic.PL.CNF.PairedWire.eval_gapClauses_iff {V : Type u_1} (σ : V → Bool) (previous next : Cell V) (hp : previous.Agree σ) (hn : next.Agree σ) : eval σ (gapClauses previous next) = true ↔ σ (previous 0).fst = σ (next 0).fst

With local agreement, the two implications equate the neighboring cell values.

theorem Cslib.Logic.PL.CNF.PairedWire.eval_links_iff {V : Type u_1} (σ : V → Bool) (cells : List (Cell V)) (hcells : ∀ (c : Cell V), c ∈ cells → c.Agree σ) : eval σ (links cells) = true ↔ ∀ (p : Cell V × Cell V), p ∈ cells.consecutivePairs → σ (p.fst 0).fst = σ (p.snd 0).fst

Under local agreement in every cell, the links hold exactly when consecutive lane-zero entries agree.

@[simp]

theorem Cslib.Logic.PL.CNF.PairedWire.links_nil {V : Type u_1} : links [] = []

Empty wires have no gap clauses.

@[simp]

theorem Cslib.Logic.PL.CNF.PairedWire.links_singleton {V : Type u_1} (cell : Cell V) : links [cell] = []

A single cell has no gap clauses.

theorem Cslib.Logic.PL.CNF.PairedWire.links_cons_cons {V : Type u_1} (first next : Cell V) (rest : List (Cell V)) : links (first :: next :: rest) = gapClauses first next ++ links (next :: rest)

Remove the first gap, leaving the links of the nonempty tail.

theorem Cslib.Logic.PL.CNF.PairedWire.agree_head {V : Type u_1} (σ : V → Bool) (first : Cell V) (rest : List (Cell V)) (hcells : ∀ (c : Cell V), c ∈ first :: rest → c.Agree σ) (hlinks : eval σ (links (first :: rest)) = true) (c : Cell V) : c ∈ first :: rest → ∀ (lane : Fin 2), σ (c lane).fst = σ (first 0).fst ∧ σ (c lane).snd = σ (first 0).fst

Under local agreement and satisfied links, all entries and exits have the value of the first lane-zero entry, including for a singleton wire.

theorem Cslib.Logic.PL.CNF.PairedWire.agree_head_of_ne_nil {V : Type u_1} (σ : V → Bool) (fallback : Cell V) (cells : List (Cell V)) (hne : cells ≠ []) (hcells : ∀ (c : Cell V), c ∈ cells → c.Agree σ) (hlinks : eval σ (links cells) = true) (c : Cell V) : c ∈ cells → ∀ (lane : Fin 2), σ (c lane).fst = σ (cells.headD fallback 0).fst ∧ σ (c lane).snd = σ (cells.headD fallback 0).fst

The head-agreement rule for a list with an explicit nonemptiness hypothesis. The fallback only makes headD total and does not affect the result.

theorem Cslib.Logic.PL.CNF.PairedWire.eval_links_of_constant {V : Type u_1} (σ : V → Bool) (value : Bool) (cells : List (Cell V)) (h : ∀ (c : Cell V), c ∈ cells → ∀ (lane : Fin 2), σ (c lane).fst = value ∧ σ (c lane).snd = value) : eval σ (links cells) = true

A common value on every entry and exit satisfies all paired links.

theorem Cslib.Logic.PL.CNF.PairedWire.length_gapClauses {V : Type u_1} (previous next : Cell V) : List.length (gapClauses previous next) = 2

There are exactly two clauses per gap.

theorem Cslib.Logic.PL.CNF.PairedWire.length_of_mem_gapClauses {V : Type u_1} (previous next : Cell V) {c : Clause V} (hc : c ∈ gapClauses previous next) : List.length c = 2

Each gap clause is binary, even if some port variables coincide.

theorem Cslib.Logic.PL.CNF.PairedWire.length_vars_gapClauses {V : Type u_1} (previous next : Cell V) : (gapClauses previous next).vars.length = 4

A gap contributes four literal positions, counted with multiplicity.

theorem Cslib.Logic.PL.CNF.PairedWire.length_links_eq_gaps {V : Type u_1} (cells : List (Cell V)) : List.length (links cells) = 2 * cells.consecutivePairs.length

There are exactly two clauses for each consecutive pair of cells.

theorem Cslib.Logic.PL.CNF.PairedWire.length_links {V : Type u_1} (cells : List (Cell V)) : List.length (links cells) = 2 * (cells.length - 1)

A wire with n cells has 2 (n - 1) clauses, with truncated subtraction for n = 0.

theorem Cslib.Logic.PL.CNF.PairedWire.length_of_mem_links {V : Type u_1} (cells : List (Cell V)) {c : Clause V} (hc : c ∈ links cells) : List.length c = 2

Every clause of a paired wire has exactly two literal positions.

theorem Cslib.Logic.PL.CNF.PairedWire.width_links {V : Type u_1} (cells : List (Cell V)) (c : Clause V) : c ∈ links cells → List.length c ≤ 2

Paired links have width at most two.

theorem Cslib.Logic.PL.CNF.PairedWire.length_vars_links {V : Type u_1} (cells : List (Cell V)) : (links cells).vars.length = 4 * (cells.length - 1)

There are exactly four literal positions per gap.