/machines/1RB0LD_0RC1RA_1LD1RC_1LE0RF_---1LA_1LF0LA/LocalSweep.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
68
69
70
71
72
73
74
75
76
77
78
(** Conditional ordered run transformations for
    1RB0LD_0RC1RA_1LD1RC_1LE0RF_---1LA_1LF0LA.
    No invariant for the blank initial configuration is asserted.
    AI assistance: GPT-6 Astra (OpenAI). *)

From BusyCoq Require Import Individual62.
From AstraLocal Require Import LocalRules.
Require Import Lia List.
Open Scope list.

Lemma A_triples l r n :
  l <* [1;1;1]^^n <{{A}} r -->* l <{{A}} [0;1;1]^^n *> r.
Proof.
  shift_rule. intros. apply progress_evstep, A_111.
Qed.

Lemma run_residue_zero l r q :
  l <* [0] <* [1;1;1]^^(S q) <{{A}} r -->+
  l <* <[1;0] {{C}}> [1;1] *> [0;1;1]^^q *> r.
Proof. follow A_triples. es. Qed.

Lemma run_residue_one_safe l r q :
  l <* <[1;0;1] <* [1;1;1]^^q <{{A}} r -->+
  l <{{A}} [1;1;0] *> [0;1;1]^^q *> r.
Proof. follow A_triples. apply A_101. Qed.

Lemma run_residue_one_terminal l r q :
  l <* <[0;0;1] <* [1;1;1]^^q <{{A}} r -->+
  l {{E}}> [0;1;0] *> [0;1;1]^^q *> r.
Proof. follow A_triples. es. Qed.

Lemma run_residue_one_halt l r q :
  halts tm (l <* <[0;0;1] <* [1;1;1]^^q <{{A}} r).
Proof.
  eapply halts_evstep.
  - apply halted_halts with (c := l {{E}}> [0;1;0] *> [0;1;1]^^q *> r).
    reflexivity.
  - apply progress_evstep, run_residue_one_terminal.
Qed.

Lemma run_residue_two l r q z :
  l <* [1] <* [0]^^z <* [1;1] <* [1;1;1]^^q <{{A}} r -->+
  l <{{A}} [0] *> [1]^^(z+2) *> [0;1;1]^^q *> r.
Proof. follow A_triples. apply A_zero_run. Qed.

Inductive scan_word : list sym -> Prop :=
| scan_nil : scan_word []
| scan_one w : scan_word w -> scan_word (1 :: w)
| scan_one_zero w : scan_word w -> scan_word (1 :: 0 :: w).

Lemma C_token_10 l r :
  l {{C}}> [1;0] *> r -->+ l <* <[1;0] {{C}}> r.
Proof. es. Qed.

Lemma C_token_scan w (H : scan_word w) l r :
  l {{C}}> w *> r -->* l <* (rev w) {{C}}> r.
Proof.
  revert l r. induction H; intros l r.
  - es.
  - cbn [rev]. rewrite Str_app_assoc.
    follow100 C_1. apply IHscan_word.
  - cbn [rev]. rewrite !Str_app_assoc.
    follow100 C_token_10. apply IHscan_word.
Qed.

Lemma C_first_double_zero w (H : scan_word w) l r :
  l {{C}}> w *> [1;0;0] *> r -->+
  l <* (rev w) <{{A}} [1;1;1] *> r.
Proof.
  follow (C_token_scan w H).
  es.
Qed.

Print Assumptions run_residue_zero.
Print Assumptions run_residue_one_safe.
Print Assumptions run_residue_one_halt.
Print Assumptions run_residue_two.
Print Assumptions C_first_double_zero.