/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/rocq-scratch/probe_segments_2.v · raw
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
(* PROBE ONLY (formalization prep, 2026-10-10). Not a proof of #2.
   Checks that busycoq's segment automation (esx / esc / wal) proves the
   low-level facts that change when A1 = 0RF instead of TM7's 0RC.
   Header and notations copied from vendor/busycoq/verify/SOMDCv6.v (TM7). *)
From BusyCoq Require Import Individual62 Longitudinal DivModCases.
Require Import ZifyNat Lia.
Require Import ZArith.
Require Import String.
Require Import List.

Ltac esc :=
  (apply BoundedConfig.segRLs_c_spec with (T:=10^3); reflexivity) ||
  (apply BoundedConfig.sideRLs_c_spec with (T:=10^3); reflexivity) ||
  (eapply sideRLs_c_spec with (T:=10^6); [vm_compute; reflexivity | st; reflexivity]).

Definition tm := Eval compute in (TM_from_str "1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---").

Notation ld := [1;1;0].
Notation d0 := [0;0;0].
Notation d1 := [1;0;0].
Notation w1ld := [1;1;1;0]. (* the stray 1 of h1 mode, then an L *)
Notation hR := (B,@nil Sym).
Notation hR' := (D,[1]).
Notation hL := (C,@nil Sym).
Notation h := [(hR,hL)].
Notation h' := [(hR',hL)].

Ltac wal :=
  eapply segRLs_wall''; esx.

Open Scope nat.

(* The +1 pass is an ordinary h-visit (enter as B, leave as C) on the aligned side. *)
Lemma probe_inc_d0: segRLs tm h [] d0 d1.
Proof. esx. Qed.

Lemma probe_inc_d1: segRLs tm h h d1 d0.
Proof. esx. Qed.

Lemma probe_inc_ld: segRLs tm h h ld ld.
Proof. esx. Qed.

Lemma probe_inc_nil: sideRLs tm h 0inf (d1 *> 0inf).
Proof. esc. Qed.

(* Eater (D with a 1 on its left) enters an L: TM7 emits h' then h to the
   right; ours first emits one extra h (the +1 pass), then the same. *)
Lemma probe_hx_ld_1: segRLs tm h' (h ++ h' ++ h) ld ld.
Proof. esx. Qed.

Lemma probe_hx_ld k: segRLs tm (h' ++ h^^k) (h ++ h' ++ h^^(1+k)) ld ld.
Proof.
  rewrite lpow_add.
  change (h ++ h' ++ h^^1 ++ h^^k) with ((h ++ h' ++ h^^1) ++ h^^k).
  eapply segRLs_trans; [esx | wal].
Qed.

(* Drain pass (B, with the stray 1 of h1 mode in front) enters an L. *)
Lemma probe_h1_ld_1: segRLs tm h (h ++ h' ++ h) w1ld ld.
Proof. esx. Qed.

Lemma probe_h1_ld k: segRLs tm (h^^1 ++ h^^k) (h ++ h' ++ h^^(1+k)) w1ld ld.
Proof.
  rewrite lpow_add.
  change (h ++ h' ++ h^^1 ++ h^^k) with ((h ++ h' ++ h^^1) ++ h^^k).
  eapply segRLs_trans; [esx | wal].
Qed.