Replace the two-bank machine with a K-bank ring, prove its reproduction in Rocq, and revise the paper
a9ea017 | (* Self-reproduction of the organism in the ring of K banks. In every generation the organism builds | |
| itself into the next bank and copies its description onto the next tape, and the next bank takes | |
| over. The copies accumulate until every bank holds one; from then on the whole state of the machine | |
| repeats every K generations. *) | |
| From Stdlib Require Import List Bool Arith ZArith Lia. | |
| Import ListNotations. | |
| From TH Require Import TwoHead Net Abstract Indep Spec Organism PassCheck PassLemma Decoder Run Complete | |
| PhysMain. | |
| Lemma rho_enc : rho = enc organism. | |
| Proof. reflexivity. Qed. | |
| Lemma length_rho : length rho = 26 * G. | |
| Proof. rewrite rho_enc, length_enc. reflexivity. Qed. | |
| Lemma translate_desc : translate desc = Some rho. | |
| Proof. exact (describe_complete rho G length_rho). Qed. | |
| Lemma length_desc_4 : 4 <= length desc. | |
| Proof. exact (translate_aux_long _ _ _ translate_desc). Qed. | |
| (* Universal construction from the code of descriptions: every image of n records that fits the bank | |
| is built from describe X. *) | |
| Theorem builds_every_image : forall K S0 L X n tail s zc c3 c2 c1 c0 m, | |
| 2 <= K -> G <= S0 -> length X = 26 * n -> n <= S0 -> length (describe X) <= L -> zc <= 31 -> | |
| fits 6 K S0 L s -> bq (nth (kap s) (banks s) bank0) = enc organism ++ repeat false ((S0 - G) * 26) -> | |
| bs (nth (kap s) (banks s) bank0) = 0 -> | |
| (forall i, relevant i = true -> wget (win s) i = wget (wcfg (mkC PI zc c3 c2 c1 c0 m)) i) -> | |
| td (nth (kap s) (tapes s) tape0) = describe X ++ tail -> | |
| let s' := itern 6 K S0 L ((30 * n + 4 + length (describe X)) * S0 + G) s in | |
| kap s' = succ_mod K (kap s) | |
| /\ nth (succ_mod K (kap s)) (banks s') bank0 = mkB (X ++ repeat false ((S0 - n) * 26)) 0 0 | |
| /\ nth (succ_mod K (kap s)) (tapes s') tape0 = mkT (describe X ++ repeat false (L - length (describe X))) 0. | |
| Proof. | |
| intros K S0 L X n tail s zc c3 c2 c1 c0 m HK HS HX Hn HL Hz Hf Hact Hslot Hw HR. | |
| pose proof (translate_aux_long _ _ _ (describe_complete X n HX)) as Hd4. | |
| destruct (universal_construction K S0 L HK HS ltac:(lia) (describe X) X tail s zc c3 c2 c1 c0 m | |
| (describe_complete X n HX) ltac:(lia) HL Hz Hf Hact Hslot Hw HR) as (nrec & Hr & U). | |
| assert (nrec = n) by lia. subst nrec. cbv zeta in U |- *. | |
| destruct U as (_ & Hk & HI & HC & _). | |
| refine (conj Hk (conj _ HC)). rewrite HI. do 3 f_equal. lia. | |
| Qed. | |
| Section Ring. | |
| Variables (K S0 L : nat). | |
| Hypotheses (HK : 2 <= K) (HS : G <= S0) (HL : length desc <= L). | |
| Lemma HL1 : 1 <= L. | |
| Proof. pose proof length_desc_4. lia. Qed. | |
| Lemma HS1' : 1 <= S0. | |
| Proof. pose proof length_organism. lia. Qed. | |
| (* the active bank's contents, the read tape's, the configuration of phase I, and a generation *) | |
| Definition img : list bool := enc organism ++ repeat false ((S0 - G) * 26). | |
| Definition dz : list bool := desc ++ repeat false (L - length desc). | |
| Definition cfs : cfg := mkC PI 1 true true true true false. | |
| Definition T : nat := (30 * G + 4 + length desc) * S0 + G. | |
| (* a state from which a generation starts: the organism active from slot 0, its description on the | |
| read tape followed by blank cells, the decoder in phase I *) | |
| Definition start (s : st) : Prop := | |
| fits 6 K S0 L s /\ bq (nth (kap s) (banks s) bank0) = img /\ bs (nth (kap s) (banks s) bank0) = 0 | |
| /\ (forall i, relevant i = true -> wget (win s) i = wget (wcfg cfs) i) | |
| /\ td (nth (kap s) (tapes s) tape0) = dz. | |
| (* the decoder's state at the hand-over pass, the same in every generation *) | |
| Definition tH : dst := dsteps (S0 * 26) L (30 * G + 4 + length desc - 1) | |
| (mkD (mkC PC 3 true true true true false) (mkT dz 0) (mkT (repeat false (S0 * 26)) 0) (mkT (repeat false L) 0)). | |
| Definition wH (i : nat) : bool := | |
| wget (aw (aiter G organism (start_ast (wcfg (dc tH)) (tget (dR tH)) (tget (dA tH)) (tget (dK tH))))) i. | |
| Lemma img_eq : rho ++ repeat false (S0 * 26 - length rho) = img. | |
| Proof. unfold img. rewrite <- rho_enc, length_rho. do 2 f_equal. lia. Qed. | |
| (* one generation *) | |
| Lemma gen : forall s, start s -> | |
| let s' := itern 6 K S0 L T s in | |
| start s' /\ kap s' = succ_mod K (kap s) | |
| /\ nth (succ_mod K (kap s)) (banks s') bank0 = mkB img 0 0 | |
| /\ nth (succ_mod K (kap s)) (tapes s') tape0 = mkT dz 0 | |
| /\ nth (kap s) (banks s') bank0 = mkB img (G mod S0) (bj (nth (kap s) (banks s) bank0)) | |
| /\ nth (kap s) (tapes s') tape0 = mkT dz (length desc mod L) | |
| /\ (forall x, x < K -> x <> kap s -> x <> succ_mod K (kap s) -> | |
| nth x (banks s') bank0 = nth x (banks s) bank0 /\ nth x (tapes s') tape0 = nth x (tapes s) tape0) | |
| /\ (forall i, fixedcell i -> wget (win s') i = wget (win s) i) | |
| /\ (forall i, 4 <= i -> istmp i = false \/ In i (map ao_of organism) -> wget (win s') i = wH i). | |
| Proof. | |
| intros s (Hf & Hq & Hb & Hw & Hd) s'. | |
| assert (Hr : length rho <= S0 * 26) by (rewrite length_rho; lia). | |
| destruct (universal_construction K S0 L HK HS HL1 desc rho (repeat false (L - length desc)) s 1 | |
| true true true true false translate_desc Hr HL ltac:(lia) Hf Hq Hb Hw Hd) as (n1 & Hn1 & U). | |
| destruct (uc_window K S0 L HK HS HL1 desc rho (repeat false (L - length desc)) s 1 | |
| true true true true false translate_desc Hr HL ltac:(lia) Hf Hq Hb Hw Hd) as (n2 & Hn2 & V). | |
| rewrite length_rho in Hn1, Hn2. assert (n1 = G) by lia. assert (n2 = G) by lia. subst n1 n2. | |
| cbv zeta in U, V. | |
| change (itern 6 K S0 L ((30 * G + 4 + length desc) * S0 + G) s) with s' in U, V. | |
| destruct U as (Hf' & Hk' & HI' & HC' & HA' & HR' & Hw' & Ho'). | |
| destruct V as (Hfx & Hdet). | |
| rewrite img_eq in HI'. rewrite Hq in HA'. | |
| refine (conj _ (conj Hk' (conj HI' (conj HC' (conj HA' (conj HR' (conj Ho' (conj Hfx _)))))))). | |
| - unfold start. rewrite Hk', HI', HC'. cbn [bq bs td]. | |
| exact (conj Hf' (conj eq_refl (conj eq_refl (conj Hw' eq_refl)))). | |
| - intros i H4 Hi. exact (Hdet i H4 Hi). | |
| Qed. | |
| (* ---- generations since a bank was active ------------------------------------------------------- *) | |
| Definition age (k x : nat) : nat := if x <=? k then k - x else k + K - x. | |
| Lemma age_zero : forall k x, k < K -> x < K -> age k x = 0 -> x = k. | |
| Proof. intros k x Hk Hx. unfold age. destruct (Nat.leb_spec x k); lia. Qed. | |
| Lemma age_self : forall k, age k k = 0. | |
| Proof. intro k. unfold age. rewrite Nat.leb_refl. lia. Qed. | |
| Lemma age_lt : forall k x, k < K -> x < K -> age k x < K. | |
| Proof. intros k x Hk Hx. unfold age. destruct (Nat.leb_spec x k); lia. Qed. | |
| Lemma age_succ : forall k x, k < K -> x < K -> | |
| age (succ_mod K k) x = if Nat.eqb x (succ_mod K k) then 0 else S (age k x). | |
| Proof. | |
| intros k x Hk Hx. unfold age, succ_mod. | |
| destruct (Nat.eqb_spec (S k) K) as [E|E]. | |
| - destruct (Nat.eqb_spec x 0) as [->|E0]; [reflexivity|]. | |
| destruct (Nat.leb_spec x 0), (Nat.leb_spec x k); lia. | |
| - destruct (Nat.eqb_spec x (S k)) as [->|E1]; [rewrite Nat.leb_refl; lia|]. | |
| destruct (Nat.leb_spec x (S k)), (Nat.leb_spec x k); lia. | |
| Qed. | |
| Lemma succ_mod_plus : forall k0 g, succ_mod K ((k0 + g) mod K) = (k0 + S g) mod K. | |
| Proof. intros k0 g. rewrite succ_mod_mod by lia. f_equal. lia. Qed. | |
| (* ---- the state after g generations --------------------------------------------------------------- *) | |
| (* After g >= 1 generations from x0: a start state again; the bank active for the last time a | |
| generations ago holds the organism, at slot G mod S0 if a > 0, and the tape read then its | |
| description; the banks and tapes not yet reached are those of x0; the cells no step writes are those | |
| of x0 and every other cell from 4 on is the same in every generation. *) | |
| Definition after (x0 : st) (g : nat) (s : st) : Prop := | |
| start s /\ kap s = (kap x0 + g) mod K | |
| /\ (forall i, fixedcell i -> wget (win s) i = wget (win x0) i) | |
| /\ (forall i, 4 <= i -> istmp i = false \/ In i (map ao_of organism) -> wget (win s) i = wH i) | |
| /\ (forall x, x < K -> | |
| (age (kap s) x = 0 -> nth x (banks s) bank0 = mkB img 0 0 /\ nth x (tapes s) tape0 = mkT dz 0) | |
| /\ (0 < age (kap s) x < g -> nth x (banks s) bank0 = mkB img (G mod S0) 0 | |
| /\ nth x (tapes s) tape0 = mkT dz (length desc mod L)) | |
| /\ (age (kap s) x = g -> nth x (banks s) bank0 = mkB img (G mod S0) (bj (nth (kap x0) (banks x0) bank0)) | |
| /\ nth x (tapes s) tape0 = mkT dz (length desc mod L)) | |
| /\ (g < age (kap s) x -> nth x (banks s) bank0 = nth x (banks x0) bank0 | |
| /\ nth x (tapes s) tape0 = nth x (tapes x0) tape0)). | |
| Lemma kap_lt : forall s, start s -> kap s < K. | |
| Proof. intros s ((_ & H & _) & _). exact H. Qed. | |
| Lemma after_1 : forall x0, start x0 -> after x0 1 (itern 6 K S0 L T x0). | |
| Proof. | |
| intros x0 Hs. | |
| destruct (gen x0 Hs) as (Hs' & Hk & HI & HC & HA & HR & Ho & Hfx & Hdet). | |
| pose proof (kap_lt x0 Hs) as Hk0. | |
| set (s1 := itern 6 K S0 L T x0) in *. | |
| refine (conj Hs' (conj _ (conj Hfx (conj Hdet _)))). | |
| - rewrite Hk, <- (Nat.mod_small (kap x0) K Hk0) at 1. rewrite succ_mod_mod by lia. f_equal. lia. | |
| - intros x Hx. rewrite Hk, (age_succ (kap x0) x Hk0 Hx). | |
| destruct (Nat.eqb_spec x (succ_mod K (kap x0))) as [->|E1]. | |
| + refine (conj (fun _ => conj HI HC) (conj _ (conj _ _))); intros; lia. | |
| + destruct (Nat.eq_dec x (kap x0)) as [->|E0]. | |
| * rewrite age_self. refine (conj _ (conj _ (conj (fun _ => conj HA HR) _))); intros; lia. | |
| * pose proof (Ho x Hx E0 E1) as [B Tp]. | |
| assert (age (kap x0) x <> 0) by (intro Z; apply E0; exact (age_zero _ _ Hk0 Hx Z)). | |
| refine (conj _ (conj _ (conj _ (fun _ => conj B Tp)))); intros; lia. | |
| Qed. | |
| Lemma after_S : forall x0 g s, 1 <= g -> after x0 g s -> after x0 (S g) (itern 6 K S0 L T s). | |
| Proof. | |
| intros x0 g s Hg (Hs & Hkap & Hfx0 & Hdet0 & Hb0). | |
| destruct (gen s Hs) as (Hs' & Hk & HI & HC & HA & HR & Ho & Hfx & Hdet). | |
| pose proof (kap_lt s Hs) as Hks. | |
| refine (conj Hs' (conj _ (conj _ (conj Hdet _)))). | |
| - rewrite Hk, Hkap. apply succ_mod_plus. | |
| - intros i Hi. rewrite (Hfx i Hi). exact (Hfx0 i Hi). | |
| - intros x Hx. rewrite Hk, (age_succ (kap s) x Hks Hx). | |
| destruct (Hb0 (kap s) Hks) as (Hact & _). rewrite age_self in Hact. destruct (Hact eq_refl) as [Bk Tk]. | |
| destruct (Nat.eqb_spec x (succ_mod K (kap s))) as [->|E1]. | |
| + refine (conj (fun _ => conj HI HC) (conj _ (conj _ _))); intros; lia. | |
| + destruct (Nat.eq_dec x (kap s)) as [->|E0]. | |
| * rewrite age_self. rewrite Bk in HA. cbn [bj] in HA. | |
| refine (conj _ (conj (fun _ => conj HA HR) (conj _ _))); intros; lia. | |
| * pose proof (Ho x Hx E0 E1) as [B Tp]. rewrite B, Tp. | |
| assert (Ha : age (kap s) x <> 0) by (intro Z; apply E0; exact (age_zero _ _ Hks Hx Z)). | |
| destruct (Hb0 x Hx) as (_ & Hmid & Heq & Hgt). | |
| refine (conj _ (conj _ (conj _ _))); intros; [lia | apply Hmid; lia | apply Heq; lia | apply Hgt; lia]. | |
| Qed. | |
| Theorem reproduces : forall x0, start x0 -> forall g, 1 <= g -> after x0 g (itern 6 K S0 L (g * T) x0). | |
| Proof. | |
| intros x0 Hs g Hg. induction g as [|g IH]; [lia|]. | |
| destruct (Nat.eq_dec g 0) as [->|E]. | |
| - replace (1 * T) with T by lia. exact (after_1 x0 Hs). | |
| - replace (S g * T) with (g * T + T) by lia. rewrite itern_add. | |
| apply after_S; [lia | apply IH; lia]. | |
| Qed. | |
| (* After g >= 1 generations, every bank active within the last g generations, and the one active now, | |
| holds the organism, and its tape the description: min(g + 1, K) copies. *) | |
| Corollary copies : forall x0, start x0 -> forall g x, 1 <= g -> x < K -> | |
| age (kap (itern 6 K S0 L (g * T) x0)) x <= g -> | |
| bq (nth x (banks (itern 6 K S0 L (g * T) x0)) bank0) = img | |
| /\ td (nth x (tapes (itern 6 K S0 L (g * T) x0)) tape0) = dz. | |
| Proof. | |
| intros x0 Hs g x Hg Hx Ha. | |
| destruct (reproduces x0 Hs g Hg) as (_ & _ & _ & _ & Hb). destruct (Hb x Hx) as (H0 & Hmid & Heq & _). | |
| destruct (Nat.eq_dec (age (kap (itern 6 K S0 L (g * T) x0)) x) 0) as [Z|Z]; | |
| [destruct (H0 Z) as [B Tp] | | |
| destruct (Nat.eq_dec (age (kap (itern 6 K S0 L (g * T) x0)) x) g) as [Q|Q]; | |
| [destruct (Heq Q) as [B Tp] | destruct (Hmid ltac:(lia)) as [B Tp]]]; | |
| rewrite B, Tp; split; reflexivity. | |
| Qed. | |
| (* the window after every generation *) | |
| Lemma window_eq : forall w w', length w = 64 -> length w' = 64 -> | |
| (forall i, fixedcell i -> wget w i = wget w' i) -> | |
| (forall i, 4 <= i -> istmp i = false \/ In i (map ao_of organism) -> wget w i = wget w' i) -> w = w'. | |
| Proof. | |
| intros w w' Hl Hl' Hf Hd. apply (nth_ext w w' false false); [congruence|]. | |
| intros i Hi. change (wget w i = wget w' i). | |
| destruct (Nat.lt_ge_cases i AR) as [H|H]; [apply Hf; left; exact H|]. | |
| destruct (Nat.leb_spec 27 i) as [H27|H27]. | |
| - destruct (in_dec Nat.eq_dec i (map ao_of organism)) as [Hin|Hin]. | |
| + apply Hd; [unfold AR in H; lia | right; exact Hin]. | |
| + apply Hf. right. split; assumption. | |
| - apply Hd; [unfold AR in H; lia | left; unfold istmp; apply Nat.leb_gt; lia]. | |
| Qed. | |
| (* From the K-th generation on, the whole state of the machine repeats every K generations. *) | |
| Theorem periodic : forall x0, start x0 -> forall g, K <= g -> | |
| itern 6 K S0 L ((g + K) * T) x0 = itern 6 K S0 L (g * T) x0. | |
| Proof. | |
| intros x0 Hs g Hg. | |
| destruct (reproduces x0 Hs g ltac:(lia)) as (Hs1 & Hk1 & Hf1 & Hd1 & Hb1). | |
| destruct (reproduces x0 Hs (g + K) ltac:(lia)) as (Hs2 & Hk2 & Hf2 & Hd2 & Hb2). | |
| set (s1 := itern 6 K S0 L (g * T) x0) in *. set (s2 := itern 6 K S0 L ((g + K) * T) x0) in *. | |
| assert (Hk : kap s2 = kap s1). | |
| { rewrite Hk1, Hk2. replace (kap x0 + (g + K)) with (kap x0 + g + 1 * K) by lia. apply Nat.Div0.mod_add. } | |
| destruct Hs1 as ((Hw1 & Hkl1 & HB1 & HT1 & _) & _). destruct Hs2 as ((Hw2 & Hkl2 & HB2 & HT2 & _) & _). | |
| assert (Hwin : win s2 = win s1). | |
| { apply window_eq; [exact Hw2 | exact Hw1 | |]. | |
| - intros i Hi. rewrite (Hf2 i Hi), (Hf1 i Hi). reflexivity. | |
| - intros i H4 Hi. rewrite (Hd2 i H4 Hi), (Hd1 i H4 Hi). reflexivity. } | |
| assert (Hnth : forall x, x < K -> nth x (banks s2) bank0 = nth x (banks s1) bank0 | |
| /\ nth x (tapes s2) tape0 = nth x (tapes s1) tape0). | |
| { intros x Hx. pose proof (age_lt (kap s1) x Hkl1 Hx) as Ha. | |
| destruct (Hb1 x Hx) as (A0 & A1 & _). destruct (Hb2 x Hx) as (B0 & B1 & _). rewrite Hk in B0, B1. | |
| destruct (Nat.eq_dec (age (kap s1) x) 0) as [Z|Z]. | |
| - destruct (A0 Z) as [P Q]. destruct (B0 Z) as [P' Q']. split; congruence. | |
| - destruct (A1 ltac:(lia)) as [P Q]. destruct (B1 ltac:(lia)) as [P' Q']. split; congruence. } | |
| destruct s1 as [w1 k1 b1 t1], s2 as [w2 k2 b2 t2]. cbn [win kap banks tapes] in *. | |
| rewrite Hwin, Hk. f_equal. | |
| - apply (nth_ext b2 b1 bank0 bank0); [congruence|]. intros x Hx. rewrite HB2 in Hx. exact (proj1 (Hnth x Hx)). | |
| - apply (nth_ext t2 t1 tape0 tape0); [congruence|]. intros x Hx. rewrite HT2 in Hx. exact (proj2 (Hnth x Hx)). | |
| Qed. | |
| End Ring. | |