Replace the two-bank machine with a K-bank ring, prove its reproduction in Rocq, and revise the paper
a9ea017 | (* The netlist of ternary threshold units computes the ring machine: every orbit of the network on | |
| encoded states is the encoding of an orbit of the machine. *) | |
| From Stdlib Require Import List Bool Arith ZArith Lia. | |
| Import ListNotations. | |
| From TH Require Import TwoHead Net Gates Phys PhysWF PhysSem. | |
| (* the network iterated on its state bits *) | |
| Fixpoint netiter (al K S0 L n : nat) (x : list bool) : list bool := | |
| match n with | |
| | O => x | |
| | S m => netiter al K S0 L m (netstep (nst al K S0 L) (phys_units al K S0 L) (phys_next al K S0 L) x) | |
| end. | |
| Lemma itern_fits : forall al K S0 L n s, 4 <= al -> 2 <= K -> 1 <= S0 -> 1 <= L -> | |
| fits al K S0 L s -> fits al K S0 L (itern al K S0 L n s). | |
| Proof. | |
| intros al K S0 L n. induction n as [|n IH]; intros s Hal HK HS HL Hs; [exact Hs|]. | |
| cbn [itern]. apply IH; try assumption. apply step_fits; assumption. | |
| Qed. | |
| (* From every state of the machine with a window of 2^al cells, al >= 4, K >= 2 banks of S0 >= 1 slots | |
| and K tapes of L >= 1 cells, the network started from the encoded state holds after n steps the | |
| encoding of the state the machine reaches in n steps. *) | |
| Theorem network_orbit : forall al K S0 L n s, 4 <= al -> 2 <= K -> 1 <= S0 -> 1 <= L -> fits al K S0 L s -> | |
| netiter al K S0 L n (encode al K S0 L s) = encode al K S0 L (itern al K S0 L n s). | |
| Proof. | |
| intros al K S0 L n. induction n as [|n IH]; intros s Hal HK HS HL Hs; [reflexivity|]. | |
| cbn [netiter itern]. rewrite (netlist_step al K S0 L s Hal HK HS HL Hs). | |
| apply IH; try assumption. apply step_fits; assumption. | |
| Qed. | |