Skip to content

Commit c6877bf

Browse files
int-y1int-y1
committed
Prove BB(3,3) id 642 doesn't halt
1 parent ce2f22e commit c6877bf

File tree

2 files changed

+189
-1
lines changed

2 files changed

+189
-1
lines changed

‎verify/BB33_642.v‎

Lines changed: 188 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,188 @@
1+
(** * Unofficial holdout ID 642 1RB2LB---_1RC2RB1LC_0LA0RB1LB *)
2+
3+
From BusyCoq Require Import Individual33.
4+
From Coq Require Import PeanoNat Decidable.
5+
From Coq Require Import Lia.
6+
Set Default Goal Selector "!".
7+
8+
Definition tm : TM := fun '(q, s) =>
9+
match q, s with
10+
| A, 0 => Some (1, R, B) | A, 1 => Some (2, L, B) | A, 2 => None
11+
| B, 0 => Some (1, R, C) | B, 1 => Some (2, R, B) | B, 2 => Some (1, L, C)
12+
| C, 0 => Some (0, L, A) | C, 1 => Some (0, R, B) | C, 2 => Some (1, L, B)
13+
end.
14+
15+
Notation "c --> c'" := (c -[ tm ]-> c') (at level 40).
16+
Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40).
17+
Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).
18+
19+
Lemma merge_1 : forall (r : side) (n : nat) (s1 : sym),
20+
[s1]^^n *> s1 >> r = [s1]^^(S n) *> r.
21+
Proof.
22+
intros. rewrite lpow_S, Str_app_assoc, <- lpow_shift'. trivial.
23+
Qed.
24+
25+
(* B> 1^t => 2^t B> *)
26+
Lemma r1_l2 : forall (t : nat) (l r : side),
27+
l {{B}}> [1]^^t *> r -->*
28+
l <* [2]^^t {{B}}> r.
29+
Proof.
30+
induction t. { execute. }
31+
intros. rewrite <- merge_1. follow IHt. execute.
32+
Qed.
33+
34+
(* 2^(2t) <B => <B 1^(2t) *)
35+
Lemma l22_b_r11 : forall (t : nat) (l r : side),
36+
l <* [2]^^(t*2) <{{B}} r -->*
37+
l <{{B}} [1]^^(t*2) *> r.
38+
Proof.
39+
induction t. { execute. }
40+
intros. replace (S t * 2) with (S (S (t*2))) by trivial.
41+
rewrite <- merge_1. rewrite <- merge_1. follow IHt. execute.
42+
Qed.
43+
44+
(* 2^(2t) <C => <C 1^(2t) *)
45+
Lemma l22_c_r11 : forall (t : nat) (l r : side),
46+
l <* [2]^^(t*2) <{{C}} r -->*
47+
l <{{C}} [1]^^(t*2) *> r.
48+
Proof.
49+
induction t. { execute. }
50+
intros. replace (S t * 2) with (S (S (t*2))) by trivial.
51+
rewrite <- merge_1. rewrite <- merge_1. follow IHt. execute.
52+
Qed.
53+
54+
(* 1 C> 1^(2t+3) 0^∞ => 2221 C> 0 1^(2t+1) 0^∞ *)
55+
Lemma l1r111_l2221r01 : forall (t : nat) (l : side),
56+
l << 1 {{C}}> [1]^^(t*2+3) *> const 0 -->*
57+
l << 2 << 2 << 2 << 1 {{C}}> 0 >> [1]^^(t*2+1) *> const 0.
58+
Proof.
59+
intros. replace (t*2+3) with (S ((t+1)*2)) by lia. execute.
60+
follow r1_l2. execute.
61+
follow l22_b_r11. replace ((t+1)*2) with (2+t*2) by lia. execute.
62+
follow r1_l2. rewrite merge_1. execute.
63+
follow l22_b_r11. rewrite merge_1. execute. rewrite merge_1.
64+
follow r1_l2. rewrite <- merge_1. execute.
65+
follow l22_b_r11. execute.
66+
follow r1_l2. execute.
67+
follow l22_c_r11. rewrite merge_1. finish.
68+
Qed.
69+
70+
(* C> 1^(2s+2) 0 1^(2t+3) 0^∞ => 11 C> 1^(2s+4) 0 1^(2t+1) 0^∞ *)
71+
Lemma r110111_step : forall (s t : nat) (l : side),
72+
l {{C}}> [1]^^(s*2+2) *> 0 >> [1]^^(t*2+3) *> const 0 -->*
73+
l << 1 << 1 {{C}}> [1]^^(s*2+4) *> 0 >> [1]^^(t*2+1) *> const 0.
74+
Proof.
75+
intros. replace (s*2+2) with (S (s*2+1)) by trivial. set (t*2+3). set (t*2+1). execute.
76+
follow r1_l2. execute.
77+
follow l1r111_l2221r01. set (t*2+1). execute.
78+
follow l22_c_r11. execute.
79+
follow r1_l2. execute.
80+
follow l22_b_r11. execute.
81+
Qed.
82+
83+
(* C> 1^(2s+2) 0 1^(2t+1) 0^∞ => 1^(2t) C> 0 1^(2s+2t+5) 0^∞ *)
84+
Lemma r110111_finish : forall (t s : nat) (l : side),
85+
l {{C}}> [1]^^(s*2+2) *> 0 >> [1]^^(t*2+1) *> const 0 -->*
86+
l <* [1]^^(t*2) {{C}}> 0 >> [1]^^(s*2+t*2+5) *> const 0.
87+
Proof.
88+
induction t.
89+
{ intros. replace (s*2+2) with (S (s*2+1)) by trivial. execute.
90+
follow r1_l2. execute.
91+
follow l22_b_r11. repeat rewrite merge_1. execute. }
92+
intros. replace (S t * 2 + 1) with (t * 2 + 3) by lia.
93+
follow r110111_step. replace (s * 2 + 4) with ((S s)*2+2) by lia.
94+
follow IHt. repeat rewrite merge_1. finish.
95+
Qed.
96+
97+
(* 11 2^(2s) 1 C> 0 1^(2t+3) 0^∞ => 2^(2s+6) 1 C> 0 1^(2t+1) 0^∞ *)
98+
Lemma l11221r0111_step : forall (s t : nat) (l : side),
99+
l << 1 << 1 <* [2]^^(s*2) << 1 {{C}}> 0 >> [1]^^(t*2+3) *> const 0 -->*
100+
l <* [2]^^(s*2+6) << 1 {{C}}> 0 >> [1]^^(t*2+1) *> const 0.
101+
Proof.
102+
intros. set (t*2+3). set (t*2+1). execute.
103+
follow l22_b_r11. execute.
104+
follow r1_l2. execute.
105+
follow l22_c_r11. execute.
106+
follow r1_l2. execute.
107+
follow l1r111_l2221r01. repeat rewrite merge_1. finish.
108+
Qed.
109+
110+
(* 1^(2s+1) C> 0 1^(2s+2t+1) 0^∞ => 2^(6s) 1 C> 0 1^(2t+1) 0^∞ *)
111+
Lemma l11221r0111_finish : forall (s t : nat) (l : side),
112+
l <* [1]^^(s*2+1) {{C}}> 0 >> [1]^^(s*2+t*2+1) *> const 0 -->*
113+
l <* [2]^^(s*6) << 1 {{C}}> 0 >> [1]^^(t*2+1) *> const 0.
114+
Proof.
115+
induction s. { trivial. }
116+
intros. replace (S s * 2 + 1) with (S (S (s*2+1))) by lia. do 2 rewrite <- merge_1.
117+
replace (S s * 2 + t * 2 + 1) with (s * 2 + (S t) * 2 + 1) by lia.
118+
follow IHs. replace (s*6) with (s*3*2) by lia. replace (S t * 2 + 1) with (t*2+3) by lia.
119+
follow l11221r0111_step. finish.
120+
Qed.
121+
122+
(* 1 C> 1^(2s+2) 0 1^(2t+1) 0^∞ => 2^(6t) 1 C> 0 1^(2s+5) 0^∞ *)
123+
Lemma l1r110111_step : forall (s t : nat) (l : side),
124+
l << 1 {{C}}> [1]^^(s*2+2) *> 0 >> [1]^^(t*2+1) *> const 0 -->*
125+
l <* [2]^^(t*6) << 1 {{C}}> 0 >> [1]^^(s*2+5) *> const 0.
126+
Proof.
127+
intros.
128+
follow r110111_finish. rewrite merge_1. replace (S (t * 2)) with (t*2+1) by lia.
129+
replace (s*2+t*2+5) with (t*2+(s+2)*2+1) by lia.
130+
follow l11221r0111_finish. finish.
131+
Qed.
132+
133+
(* 0^∞ 1 C> 1^(2s+2) 0 1^(2t+3) 0^∞ => 0^∞ 11 C> 1^(6t+6) 0 1^(2s+5) 0^∞
134+
Note: "0^∞ 1 C> 1^(2s+2) 0 1 0^∞" doesn't follow the pattern. *)
135+
Lemma l1_l11 : forall (s t : nat),
136+
const 0 << 1 {{C}}> [1]^^(s*2+2) *> 0 >> [1]^^(t*2+3) *> const 0 -->*
137+
const 0 << 1 << 1 {{C}}> [1]^^(t*6+6) *> 0 >> [1]^^(s*2+5) *> const 0.
138+
Proof.
139+
intros. replace (t*2+3) with ((t+1)*2+1) by lia.
140+
follow l1r110111_step. execute. replace ((t+1)*6) with ((1+t*3+2)*2) by lia.
141+
follow l22_b_r11. execute.
142+
follow r1_l2. execute.
143+
follow l22_c_r11. replace ((t*3+2)*2) with (4+t*6) by lia. repeat rewrite merge_1. execute.
144+
Qed.
145+
146+
(* 0^∞ 11 C> 1^(2s+2) 0 1^(2t+1) 0^∞ => 0^∞ 1 C> 1^(6t+2) 0 1^(2s+5) 0^∞ *)
147+
Lemma l11_l1 : forall (s t : nat),
148+
const 0 << 1 << 1 {{C}}> [1]^^(s*2+2) *> 0 >> [1]^^(t*2+1) *> const 0 -->+
149+
const 0 << 1 {{C}}> [1]^^(t*6+2) *> 0 >> [1]^^(s*2+5) *> const 0.
150+
Proof.
151+
intros.
152+
follow l1r110111_step. set (s*2+5). execute. replace (t*6) with (t*3*2) by lia.
153+
follow l22_b_r11. execute.
154+
follow r1_l2. execute.
155+
follow l22_c_r11. repeat rewrite merge_1. execute.
156+
Qed.
157+
158+
(* 0^∞ 11 C> 1^(2s+2) 0 1^(2t+1) 0^∞ => 0^∞ 11 C> 1^(6s+12) 0 1^(6t+5) 0^∞ *)
159+
Lemma l11_next : forall (s t : nat),
160+
const 0 << 1 << 1 {{C}}> [1]^^(s*2+2) *> 0 >> [1]^^(t*2+1) *> const 0 -->+
161+
const 0 << 1 << 1 {{C}}> [1]^^(s*6+12) *> 0 >> [1]^^(t*6+5) *> const 0.
162+
Proof.
163+
intros.
164+
(* "follow l11_l1." doesn't work *)
165+
eapply progress_evstep_trans. { apply l11_l1. }
166+
replace (t*6+2) with (t*3*2+2) by lia. replace (s*2+5) with ((s+1)*2+3) by lia.
167+
follow l1_l11. finish.
168+
Qed.
169+
170+
(* D(s, t) = 0^∞ 11 C> 1^(2s+2) 0 1^(2t+1) 0^∞ *)
171+
Definition D s t : Q * tape :=
172+
const 0 << 1 << 1 {{C}}> [1]^^(s*2+2) *> 0 >> [1]^^(t*2+1) *> const 0.
173+
174+
(* D(s, t) => D(3s+5, 3t+2). This is l11_next rewritten in terms of D. *)
175+
Lemma D_next : forall (s t : nat),
176+
D s t -->+ D (s*3+5) (t*3+2).
177+
Proof.
178+
intros. unfold D.
179+
(* "follow l11_next." doesn't work *)
180+
eapply progress_evstep_trans. { apply l11_next. } finish.
181+
Qed.
182+
183+
Theorem nonhalt : ~ halts tm c0.
184+
Proof.
185+
apply multistep_nonhalt with (D 0 0). { execute. }
186+
apply progress_nonhalt_simple with (C := fun '(s, t) => D s t) (i0 := (0%nat, 0%nat)).
187+
intros [s t]. exists (s*3+5, t*3+2). apply D_next.
188+
Qed.

‎verify/Makefile‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ ALLVFILES := LibTactics.v Helper.v Pigeonhole.v TM.v Compute.v Flip.v Permute.v
44
Cyclers.v TranslatedCyclers.v BackwardsReasoning.v Bouncers.v Individual.v \
55
BB52.v Individual52.v FixedBin.v ShiftOverflow.v ShiftOverflowBins.v Skelet15.v Skelet26.v Skelet33.v Skelet34.v Skelet35.v \
66
Skelet10.v Skelet17.v Skelet1.v Finned.v Finned1.v Finned2.v Finned3.v Finned4.v Finned5.v Extraction.v \
7-
BB33.v Individual33.v BB33_494.v
7+
BB33.v Individual33.v BB33_494.v BB33_642.v
88

99
all: check verify skelet1
1010

0 commit comments

Comments
 (0)