/machines/1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF/rocq/t2.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
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
From BusyCoq Require Import Individual62.

Require Import ZArith Lia.
Require Import String.
Require Import List.
From BusyCoq Require Import ES_v3.

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

Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40).
Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).

Definition G : list sym :=
  [0;0;1;1;0;1;1;1;1;0;1;1;0;1;1;1;1;1;1;0;1;1;0;1;1;1;1;1;0;0;1;1;0;1;1;1;1;1;0;1;1;0;0].

Definition Kr n a b c d :=
  0inf <{{F}} G *> [1] *> [1;1]^^n *> [0] *> [1;1]^^a *> [0;1;1;0] *> [1;1]^^b
    *> [0;0;0;0;0;0] *> [1] *> [1;1]^^c *> [0;1;1;0;1;1;1;1;0;0;0;0;0;0] *> [1;1]^^d
    *> [0;1;1;0;0;1;1;0;1;1;1] *> 0inf.

Ltac ES_v3.es_v3_pre ::= unfold Kr, G.

Lemma S_step n a b c d:
  Kr n (5+a) (3+b) (3+c) (1+d) -->+ Kr (24+n) (1+a) (5+b) (3+c) (3+d).
Proof.
  es' n a b c d.
Time Qed.

Lemma TE n b d:
  Kr n 2 (44+b) 17 (10+d) -->+ Kr (278+n) (1+b) 41 (35+d) 9.
Proof.
  es' n b d.
Time Qed.

Lemma TO n b c d:
  Kr n 1 (41+b) (18+c) (9+d) -->+ Kr (294+n) (14+b+c) (40+d) 17 9.
Proof.
  es' n b c d.
Time Qed.

Lemma T6 n b c d:
  Kr n 3 (41+b) (17+c) (9+d) -->+ Kr (296+n) (13+b+c) (40+d) 17 9.
Proof.
  es' n b c d.
Time Qed.

Lemma T8 n b d:
  Kr n 4 (44+b) 17 (10+d) -->+ Kr (270+n) (7+b) 43 (33+d) 9.
Proof.
  es' n b d.
Time Qed.

Lemma S_step' n a b c d:
  Kr n (5+a) (3+b) (3+c) (1+d) -->* Kr (24+n) (1+a) (5+b) (3+c) (3+d).
Proof. apply progress_evstep, S_step. Qed.

Lemma TE' n b d:
  Kr n 2 (44+b) 17 (10+d) -->* Kr (278+n) (1+b) 41 (35+d) 9.
Proof. apply progress_evstep, TE. Qed.

Lemma TO' n b c d:
  Kr n 1 (41+b) (18+c) (9+d) -->* Kr (294+n) (14+b+c) (40+d) 17 9.
Proof. apply progress_evstep, TO. Qed.

Lemma T6' n b c d:
  Kr n 3 (41+b) (17+c) (9+d) -->* Kr (296+n) (13+b+c) (40+d) 17 9.
Proof. apply progress_evstep, T6. Qed.

Lemma T8' n b d:
  Kr n 4 (44+b) 17 (10+d) -->* Kr (270+n) (7+b) 43 (33+d) 9.
Proof. apply progress_evstep, T8. Qed.

Lemma S_iter k: forall n a b c d,
  Kr n (4*k+1+a) (3+b) (3+c) (1+d) -->* Kr (24*k+n) (1+a) (2*k+3+b) (3+c) (2*k+1+d).
Proof.
  induction k; intros.
  - finish.
  - follow (S_step' n (4*k+a) b c d).
    follow (IHk (24+n) a (2+b) c (2+d)).
    finish.
Qed.

Definition Ev N X := Kr N (4*X+26) (2*X+32) 17 9.

Lemma prog_eq c1 c2 c1' c2':
  c1 -->+ c2 -> c1 = c1' -> c2 = c2' -> c1' -->+ c2'.
Proof. intros H E1 E2. subst. exact H. Qed.

Lemma DC N X:
  Ev N X -->+ Ev (48*X+716+N) (4+X).
Proof.
  unfold Ev.
  follow (S_iter (X+6) N 1 (2*X+29) 14 8).
  follow (TE' (24*(X+6)+N) (4*X) (2*X+11)).
  follow (S_iter X (278+(24*(X+6)+N)) 0 38 (2*X+43) 8).
  eapply prog_eq.
  1: apply (TO (24*X+(278+(24*(X+6)+N))) (2*X) (2*X+28) (2*X)).
  all: lia_refl.
Qed.

Fixpoint multistep_c' tm n1 n2 n3 c :=
match n1 with
| O => multistep_c tm n3 c
| S n1 =>
  match multistep_c tm n2 c with
  | Some c => multistep_c' tm n1 n2 n3 c
  | None => None
  end
end.

Lemma multistep_c'_spec tm n1 n2 n3 c c':
  multistep_c' tm n1 n2 n3 c = Some c' <-> c -[ tm ]->> (n1*n2+n3) / c'.
Proof.
  gen c c'.
  induction n1; cbn[multistep_c']; intros.
  1: apply multistep_c_spec.
  destruct (multistep_c tm n2 c) eqn:E.
  + apply multistep_c_spec in E.
    rewrite IHn1.
    replace (S n1*n2+n3) with (n2+(n1*n2+n3)) by lia.
    split; intro H.
    * eapply multistep_trans; eauto 1.
    * eapply rewind_split in H.
      destruct H as [c'0 [I1 I2]].
      multistep_deterministic.
      eauto 1.
  + split.
    1: congruence.
    replace (S n1*n2+n3) with (n2+(n1*n2+n3)) by lia.
    intro H.
    eapply rewind_split in H.
    destruct H as [c'0 [I1 I2]].
    eapply multistep_c_spec in I1.
    congruence.
Qed.

Lemma init:
  c0 -->* Kr 979 17 34 22 9.
Proof.
  eapply without_counter with (n:=4097*1000+897).
  eapply multistep_c'_spec.
  native_check_eq.
Time Qed.

Lemma opening:
  Kr 979 17 34 22 9 -->* Ev 6431 20.
Proof.
  unfold Ev.
  follow (S_iter 4 979 0 31 19 8).
  follow (TO' 1075 1 4 8).
  follow (S_iter 4 1369 2 45 14 8).
  follow (T6' 1465 15 0 8).
  follow (S_iter 6 1761 3 45 14 8).
  follow (T8' 1905 16 11).
  follow (S_iter 5 2175 2 40 41 8).
  follow (T6' 2295 12 27 10).
  follow (S_iter 12 2591 3 47 14 8).
  follow (T8' 2879 30 23).
  follow (S_iter 9 3149 0 40 53 8).
  follow (TO' 3365 20 38 18).
  follow (S_iter 17 3659 3 55 14 8).
  follow (T8' 4067 48 33).
  follow (S_iter 13 4337 2 40 63 8).
  follow (T6' 4649 28 49 26).
  follow (S_iter 22 4945 1 63 14 8).
  follow (TE' 5473 66 43).
  follow (S_iter 16 5751 2 38 75 8).
  follow (T6' 6135 32 61 32).
  finish.
Time Qed.

Lemma nonhalt: ~halts tm c0.
Proof.
  eapply multistep_nonhalt.
  1: { follow init. apply opening. }
  apply (progress_nonhalt_simple tm (nat*nat) (fun p => Ev (fst p) (snd p)) (6431,20)).
  intros [N X].
  exists (48*X+716+N, 4+X).
  apply DC.
Qed.

Print Assumptions nonhalt.