Built . It shows the files as they were then (ages and “working now” follow your clock).
tools/rebuild_pages.sh rebuilds the site within 5 minutes of a change; by hand: python3 -B tools/site.py.Machines / #12
1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF
How we proved it never halts
A recursive call stack whose every round costs exactly 2
The tape is runs of 1s separated by 0s, and it behaves like a recursive program's call stack. Left of the head are the pending calls; right of it is input still to come. A new call moves the next run of 1s onto the stack and costs its caller one 1. A call that is down to a single 1 ends: it and its caller leave the stack, and the caller's run goes back to the right, one 1 longer.
Every so often the stack is empty and the head is back at the left end, which reads 111 00. That 111 grows into the next round's bottom call, four 1s long, so it can pay for three calls; the number it pays for is the round's cost. The machine halts exactly when a bottom call has to pay for a fourth.
The key idea is self-similarity. A call behaves the same whatever its length, as long as it can pay. So inside a long round, a big call replays the machine's own rounds one level down, on a tape that also holds markers (lone 1s separated by even-length gaps of 0s). A replayed round costs 2, or 3 when it swallows a marker, and an exact law, proved by induction, says which from the gap lengths alone.
Why that settles it: the real run's top level has no markers (those further right only affect replayed rounds). So every top-level round costs exactly 2, the next one again starts from 111 00, and the fourth payment, the only route to the missing transition, never comes.
The Rocq proof (checked against busycoq) checks the tape moves by running them, the replay and the cost law by induction, and the 50-step opening by exact replay.
#5local proof number
876lines of Rocq
4 sto compile
6/6automatic checks
About this picture
The standard picture (bbchallenge.org's Default view): each row is the whole tape at one step, time runs downward, and the head's path draws the pattern.
bbchallenge-defaultStart blankRows steps 0 → 10,000, top to bottomWindow cells −200..199, left to rightColors 1 0 or unvisited
Claimed by someone else
We proved this machine locally, but our proof was still unsubmitted when we found it already covered upstream.
Submit completed proofs early. A local proof does not secure an upstream claim.
Upstream proof ↗ · Recorded timeline
What the timing evidence establishes
This describes upstream credit, not who first discovered the mathematics. The records do not establish adoption of our proof, first public push time, or whether an earlier submission would have secured credit.
Overview
In one sentence
Run-length counter: epochs double in time, 2 passenger marker 1s; 9 rules validated, inner invariant open
Submitted mechanism The tape is a stack of runs of 1s, 0^inf 1^a_1 0 .. 0 1^a_p <A 0 1^c_1 0^g_1 1^c_2 ... A push (R1) takes one 1 from the top run and makes the next run right of the head the new top frame; at the left edge R3 does the same without the payment, and the new frame gains a 1. When the top run is a lone 1 it finishes: R2 merges it into the run below, which moves back to the right side one cell longer. (submission/README.md, Mechanism)
- Upstream
- The blank-start machine never halts: CounterClass4.v.TM2 ↗. We also have a local proof. This upstream addition is separate from our merged submissions; adoption credit is not established. Recorded commit time: 2026-10-14T06:19:56Z. First public push time is not established.
- Rocq proof
- check_kill PASS · first Oct 10 09:25876 lines · 39 KB .v · compile 3.9 s · coqchk pass · 0 axioms · PASS Oct 10 09:25 (re-run Oct 10 11:54)· the .v file
- Automatic review
- 6 of 6 checks passtemplate: verify/CounterClass2v1.v (nearest template) · details in Proof →
- Class
- Counter Class 4ours: Counter Class 4 (sheet) · ours adds: recursive run-length counter (self-similar epochs, time doubles per epoch) · med confidence
- On the list
- not on
BB6_holdouts_663.txt(line 2 of the previous list) · historical 740 line 2
Mechanism
What to check here: the pictures show the mechanism that the rule table describes.
How it works: 3 notes
- Tape = runs of 1s. R1: pointer A moves one run right; a 1 moves from its old run to the run past the 00 gap.
- R2: A on a lone 1 merges it left and jumps 2 runs back; R3 grows the left edge. Halt needs 0^inf 1 <A: never seen.
- Epochs: short (40k+288 steps), then long (~1260*2^k): run 1 counts 2k+1 -> 1, each tick a doubling mini-epoch.
Figures for Checkpoint A
Blaze view, time runs down. Find each row where the left edge steps out, and compare the gaps between them.
bbchallenge-blazeStart blankRows Blaze time blocks of 16,384 stepsWindow cells -58..33, 1 px = 0.115 cellsColors 0 1 a cell that is 1 for part of its time block
Rows: (611 rows, each averaged), stretched to 500 px (1 px ~ 20,000 steps); epochs start near y = 32, 64, 129, 258 px · Window: 1 cell = 8.7 px
One long epoch (k = 8), time runs down. Find each step where the long left block (run 1) shrinks.
bbchallenge-blazeStart mid-run: step 320,794Rows Blaze time blocks of 512 stepsWindow cells -43..27, 1 px = 0.089 cellsColors 0 1 a cell that is 1 for part of its time block
Start: Fl(8,10) = 0∞ <A 0 13 02 117 02 119 02 1 010 1 06 1 0∞ (head at cell -42) · Rows: (629 rows, each averaged), steps 320,794..642,526 (ends at Fs(9,4)), stretched to 500 px; r1 loses cells near y = 31, 62, 125, 250, 499 px · Window: 1 cell = 11.3 px
Edge records to 1e9 (only 134 rows). Look at the two thin white lines in the black right half.
bbchallenge-defaultStart blankRows the start, then one per new leftmost or rightmost cellWindow cells -86..47, 1 px = 0.25 cellsColors 1 0 head at a new left/right edge
Rows: (134 rows, steps 0..660,597,554; no new cell from there to 1e9); not evenly spaced in time · Window: 1 cell = 4 px · Colors: right-edge rows catch the tape mid-epoch (the long white bars)
More figures (1)Fig 4: bbchallenge Default view, first 10,000 steps
For orientation: zig-zag sweeps over runs of 1s, as bbchallenge.org shows them.
bbchallenge-defaultStart blankRows 10,000 steps squeezed into 500 px rowsWindow cells -200..199, 1 px = 1 cellColors 1 0 or never visited head after a right/left move
Rows: 1 px row = 20 steps; the site blends steps 20y+9 and 20y+10
Rules (9/9 validated)exact tape rewrites the proof will formalize, each re-checked by simulation
| rule | from ⟶ to | cases | steps | checked |
|---|---|---|---|---|
| R1 pointer right | 1n+2 <A 0 1m+1 02 1x 0 ⟶ 1n+1 0 1m+1 <A 0 1x+1 02 | n,m,x>=0; x=0 covers 0^3 and 0^inf after the 00 | 3m+2x+15 | ✓60/60 |
| R2 lone 1 merges, jump back | 1j+1 0 1k+1 0 1 <A 0 ⟶ 1j+1 <A 0 1k+2 02 | j,k>=0 | k+10 | ✓60/60 |
| R2e jump to edge | 0∞ 1k+1 0 1 <A 0 ⟶ 0∞ <A 0 1k+2 02 | k>=0 | k+10 | ✓60/60 |
| R3 edge refill | 0∞ <A 0 1k+1 02 1m 0 ⟶ 0∞ 1k+2 <A 0 1m+1 02 | k,m>=0 | 3k+2m+11 | ✓60/60 |
| HALT | 03 1 <A 0 ⟶ halt | only halting route; needs a lone 1 at the far left | 4 (incl. halting transition) | ✓40/40 |
| short epoch | Fs(k,P) = 0∞ <A 0 13 02 12 02 12k 02 12k+1 0P 1 0Q 1 0∞, P+Q=2k ⟶ Fl(k,P) = 0∞ <A 0 13 02 12k+1 02 12k+3 02 1 0P 1 0Q 1 0∞ | P,Q even >=2 (k up to 200 tested) | 40k+288 | ✓24/24 |
| long epoch | Fl(k,P) ⟶ Fs(k+1,P') with P' even, 2<=P'<=2k; or D(k+1) | P' irregular in (k,P), e.g. k=11: P 2,4,6,8,10,12 -> 6,8,10,16,D,4. Macro model: every even P for k<=13 closes with no halt | ~1260*2k (+-200, depends on P) | ✓22/22 |
| degenerate D | D(k) = 0∞ <A 0 13 02 12 02 12k+2 02 12k+1 0∞ ⟶ E(k) = 0∞ <A 0 13 02 12k+3 02 12k+3 02 1 0∞ | k>=3 | 40k+312 | ✓8/8 |
| E back to family | E(k) ⟶ Fs(k+1,2) | k=3..10; the real orbit takes D at k=25 (step 4.2e10), then E, then Fs(26,2) | ~1260*2k | ✓8/8 |
Compressed historythe tape as 0∞ <A 0 13 02 12 02 12k 02 12k+1 0P 1 0Q 1 0∞ at 26 moments: where the rules are read off
0∞ <A 0 13 02 12 02 12k 02 12k+1 0P 1 0Q 1 0∞
| step | k | P | Q |
|---|---|---|---|
| 1,590 | 1 | D | D |
| 4,090 | 2 | 2 | 2 |
| 8,806 | 3 | D | D |
| 18,826 | 4 | 2 | 6 |
| 38,730 | 5 | 6 | 4 |
| 78,838 | 6 | 4 | 8 |
| 159,230 | 7 | 4 | 10 |
| 320,186 | 8 | 10 | 6 |
| 642,526 | 9 | 4 | 14 |
| 1,287,310 | 10 | 8 | 12 |
| 2,577,198 | 11 | 12 | 10 |
| 5,157,430 | 12 | 4 | 20 |
| 10,317,966 | 13 | 12 | 14 |
| 20,639,446 | 14 | 20 | 8 |
| 41,282,870 | 15 | 24 | 6 |
| 82,570,218 | 16 | 18 | 14 |
| 165,145,050 | 17 | 30 | 4 |
| 330,295,486 | 18 | 16 | 20 |
| 660,596,506 | 19 | 14 | 24 |
| 1,321,198,810 | 20 | 26 | 14 |
| 2,642,404,258 | 21 | 10 | 32 |
| 5,284,815,110 | 22 | 28 | 16 |
| 10,569,637,546 | 23 | 38 | 8 |
| 21,139,283,246 | 24 | 24 | 24 |
| 42,278,575,038 | 25 | D | D |
| 84,557,158,858 | 26 | 2 | 50 |
klast 26Plast 2Qlast 50Template comparisonCounterClass2v1.v: does not apply · the nearest solved proof, what carries over, and the transitions that differ
| 0 | 1 | |
|---|---|---|
| A | 1RB | 1LC |
| B | 1RC | 1LB |
| C | 1LD | 0RB |
| D | 0LE | 1RD |
| E | --- | 0LF |
| F | 0LA | 1LF |
- file
CounterClass2v1.v- module
- —
- machine
1RB1RD_1LC---_1LE0LD_0RE1LC_1RA1RF_1RE0LF(11 transitions apart)- diff
10/12 transitions differ (best renaming+mirror); CounterClass3v2 8/12, closest CounterClass1 machine 8/12- note
- No rules or shapes carry over: 7 of 16 CC2v1 starting shapes (SkelE/Be) halt on this machine. What does carry over is the proof skeleton: an Inductive Side type, a Good invariant and progress_nonhalt_cond.
Proof strategy & riskshow the formal proof will go · 3 risks to watch
Level 1: prove R1/R2/R2e/R3 with es plus shift rules (C> 1^n, D>, <F sweeps) and induction on run lengths. Level 2: copy the CounterClass2v1 pattern, with epoch starts Fs/Fl/D/E as an Inductive state with P existential, a Good invariant and progress_nonhalt_cond. Open: an invariant for the long epoch's right side that does not depend on P.
- ▲The inner invariant for the long epoch is not found yet. The right side is a recursive mini-counter, likely CC2v1-sized (~100 KB).
- ▲The P->P' marker map is irregular, so the proof must work for every even P, plus the degenerate D branch.
- ▲Untouched class with no Counter Class 4 precedent. The twin (6 transitions away) needs its own instance.
Stats & provenance1011 steps simulated · 176 cells · the status in full · files
- simulated
- 1011 steps
- tape
- 176 cells · 116 nonzeros
- growth
- log: span ~ 4*log2(t) (+4 cells per epoch pair, epoch time x2); 134 cells at 1e9, 176 at 1e11
- status now
- check_kill PASS, independently re-verified (status.json, 2026-10-10)
- observer's note
- Mechanism found at two levels with 9 validated rules. No sign that anyone is working on it (sheet status blank, no Discord mention). Halting does not depend on the irregular marker positions (every even P tested closes), so this is not a cryptid.
- files
- observe.json · notes.md · proof.md · how_proved.md · status.json · 1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF.v
Proof & checks
6/6 automatic checks pass
Kill 5 · Counter Class 4 · the kill file 1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF.v: 876 lines, 105 items · the package submission/
✓ 6/6 automatic checks pass · Checkpoint B: no note from Dennis yet · template (nearest template): verify/CounterClass2v1.v · 11% of our lines identical
1What is provedCheck: the string, the theorem and every check_kill line are green, and the .v on disk is the one that was checked (same sha256).
Machine
1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LFvs holdout list
Theorem
check_kill
✓ PASS
· 17/17 checks pass
· compile 3.87 s · coqchk pass
(1.3 s) · assumptions: 0
(closed)
· 2026-10-10 18:54:20 UTC
· submission/check_kill.txt
Checked .v
sha256 f867b60c1855cefb…
| ✓ | 1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF.v | f867b60c1855cefb… = checked |
| ✓ | submission/1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF.v | f867b60c1855cefb… = checked |
Status
✓Killed: never halts
updated 2026-10-10
✓ args✓ input✓ framework✓ framework_build✓ forbidden✓ structure✓ tm_text✓ theorem_text✓ coq✓ names✓ compile✓ tm_rocq✓ theorem_rocq✓ isolation✓ assumptions✓ coqchk✓ integrity
All 17 check_kill checks with their one-line results
| ✓ | args | 6x2 machine, framework module Individual62, mode nonhalt |
| ✓ | input | 39967 bytes, 876 lines, 972 sentences |
| ✓ | framework | HEAD 0940bb9cf434ba68f0c025dabfde45a219999973 == pin; no tracked changes under verify/ |
| ✓ | framework_build | 13 needed framework .vo files present and fresh, with native code no older than the .vo |
| ✓ | forbidden | none of 30 forbidden patterns occur (ground rule 1's words: anywhere; command words: outside comments and strings; comments never split a token) |
| ✓ | structure | 5 Require name(s) allowed; no top-level Variable/Context; no shadowing; Module/Section balanced |
| ✓ | tm_text | line 22: TM_from_str "1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF" == <tm> (41 bytes) |
| ✓ | theorem_text | line 831: nonhalt : ~halts tm c0 |
| ✓ | coq | coqc 8.20.1 ([local working file] |
| ✓ | names | halts, c0, TM_from_str resolved inside Individual62 |
| ✓ | compile | compiled in 3.9s with all appended checks |
| ✓ | tm_rocq | BB6Kill.Candidate.tm = BusyCoq.Individual62.TM_from_str "1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF" by eq_refl (in-file and isolated) |
| ✓ | theorem_rocq | nonhalt : ~ halts (TM_from_str "1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF") c0 with absolute names (in-file and isolated) |
| ✓ | isolation | only stock proof plugins loaded; guard/positivity/universe checking on, definitional UIP off |
| ✓ | assumptions | 0 assumption(s), all in the baseline |
| ✓ | coqchk | coqchk -norec BB6Kill.Candidate ok (1.3s); its context summary lists nothing of the file's own |
| ✓ | integrity | input sha256 and framework HEAD/cleanliness identical before and after |
2Where it came fromCheck: the template is the one you expect, and the measured reuse (tiles, the reuse figure, diff) agrees with what the README says was kept and changed (quoted).
11%of our lines identical to the template
2changed lines
663added lines (ours only)
2941template lines dropped
1 / 1 / 103items identical / adapted / new
What the package README says it reused and changed (submission/README.md line 18, Template and what changed), quoted:
No solved proof is close. proof.md §7 names CounterClass2v1.v (3,159 lines) as the nearest, but 10 of its 12 transitions differ.
- Kept: its top-level shape (
multistep_nonhalt+progress_nonhalt_condwith an index type and a predicate), and an inductive big-step relation for nested calls, as itsClosedCalldoes. - Changed: everything machine-specific is new: the run-model encoding (
lside/rside,updt),Life, the epoch rules, the marker-word combinatorics and the invariant. It imports onlyIndividual62from busycoq (noLongitudinal). The plan's small-step model and stack-simulation relation were dropped in favour ofLife(proof.md §7.1).
The file is 876 lines. The informal proof is proof.md; its §7.1 maps every section to lemma names.
Top two bars: non-blank lines after the TM string is replaced by <TM> and whitespace is collapsed. Bottom bar: our Definitions/Lemmas/… by name.
identicalchanged / adaptedours only (new)template only
Template part: whole file. Ours: lines 15–876 (header comment 1–14 left out). Line diff: Python difflib SequenceMatcher; inside a replaced block, line pairs at least 75% alike count as changed, the rest as removed + added.Template-only names: SkelE, SkelO, Pside, Bside, Aside, Pe, Po, Be, Bo, Ae, Ao, K0, K1, Side, to_side, skelE_measure, skelO_measure, side_measure, class_rank, measure, side_repeat_one_succ, K1_step, Pe_succ_step, Po_succ_step, Be_succ_step, Bo_succ_step, Ae_succ_step, Ao_succ_step, Pe_zero_step, Pe_succ_zero_step, Po_zero_step, Be_zero_step, Bo_zero_step, Ae_zero_step, Ao_zero_step, to_side_SK1_step, to_side_SPe_succ_step, to_side_SPo_succ_step, to_side_SBe_succ_step, to_side_SBo_succ_step …
Side-by-side diff: template (3029 lines) vs ours (751 lines), 3606 lines differ; runs of identical lines and long template-only runs folded
identicalequal once each TM string is <TM>changedours onlytemplate only
| template | ours | ||
|---|---|---|---|
| 1 | From BusyCoq Require Import Individual62. | 16 | From BusyCoq Require Import Individual62. |
| 2 | From BusyCoq Require Import Longitudinal. | ||
| 3 | Require Import Lia. | 17 | Require Import Lia. |
| 18 | Require Import String. | ||
| 4 | Require Import List. | 19 | Require Import List. |
| 5 | Require Import PeanoNat. | 20 | Require Import Arith. |
| 6 | Require Import String. | ||
| 7 | Require Import Wf_nat. | ||
| 8 | Import ListNotations. | ||
| 10 | Definition tm := Eval compute in (TM_from_str "1RB1RD_1LC---_1LE0LD_0RE1LC_1RA1RF_1RE0LF"). | 22 | Definition tm := Eval compute in (TM_from_str "1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF"). |
| 24 | Notation "c --> c'" := (c -[ tm ]-> c') (at level 40). | ||
| 25 | Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40). | ||
| 26 | Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40). | ||
| 12 | Open Scope list. | 28 | Open Scope list. |
| 30 | (* R1: l 1^(n+2) <A 0 1^(m+1) 0 0 1^x 0 r --> l 1^(n+1) 0 1^(m+1) <A 0 1^(x+1) 0 0 r *) | ||
| 31 | Lemma tR1 n m x l r : | ||
| 32 | l <* [1]^^(S (S n)) <{{A}} [0] *> [1]^^(S m) *> [0;0] *> [1]^^x *> [0] *> r -->+ | ||
| 33 | l <* [1]^^(S n) <* [0] <* [1]^^(S m) <{{A}} [0] *> [1]^^(S x) *> [0;0] *> r. | ||
| 34 | Proof. es. Qed. | ||
| 36 | (* R3: l 0 <A 0 1^(k+1) 0 0 1^m 0 r --> l 1^(k+2) <A 0 1^(m+1) 0 0 r *) | ||
| 37 | Lemma tR3 k m l r : | ||
| 38 | l <* [0] <{{A}} [0] *> [1]^^(S k) *> [0;0] *> [1]^^m *> [0] *> r -->+ | ||
| 39 | l <* [1]^^(S (S k)) <{{A}} [0] *> [1]^^(S m) *> [0;0] *> r. | ||
| 40 | Proof. es. Qed. | ||
| 42 | (* R2: l 0 1^(k+1) 0 1 <A 0 r --> l <A 0 1^(k+2) 0 0 r *) | ||
| 43 | Lemma tR2 k l r : | ||
| 44 | l <* [0] <* [1]^^(S k) <* [0] <* [1] <{{A}} [0] *> r -->+ | ||
| 45 | l <{{A}} [0] *> [1]^^(S (S k)) *> [0;0] *> r. | ||
| 46 | Proof. es. Qed. | ||
| 48 | Lemma tR3c k m r : | ||
| 49 | const 0 <{{A}} [0] *> [1]^^(S k) *> [0;0] *> [1]^^m *> [0] *> r -->+ | ||
| 50 | const 0 <* [1]^^(S (S k)) <{{A}} [0] *> [1]^^(S m) *> [0;0] *> r. | ||
| 51 | Proof. rewrite (const_unfold _ S0) at 1. es. Qed. | ||
| 53 | (* ---------- tape encoding of the run model ---------- *) | ||
| 54 | Fixpoint lsep (L : list nat) : side := | ||
| 55 | match L with | ||
| 56 | | [] => const 0 | ||
| 57 | | y :: L' => lsep L' <* [1]^^y <* [0] | ||
| 58 | end. | ||
| 60 | Definition lside (L : list nat) : side := | ||
| 61 | match L with | ||
| 62 | | [] => const 0 | ||
| 63 | | x :: L' => lsep L' <* [1]^^x | ||
| 64 | end. | ||
| 66 | Fixpoint rside (R : list nat) : side := | ||
| 67 | match R with | ||
| 68 | | [] => const 0 | ||
| 69 | | [c] => [1]^^c *> const 0 | ||
| 70 | | c :: g :: R' => [1]^^c *> [0]^^g *> rside R' | ||
| 71 | end. | ||
| 73 | Definition conf (L R : list nat) : Q * tape := lside L <{{A}} [0] *> rside R. | ||
| 75 | Lemma c0_1 : 0 >> const 0 = const 0. | ||
| 76 | Proof. symmetry. apply const_unfold. Qed. | ||
| 78 | Lemma lsep_eq L : lsep L = lside L <* [0]. | ||
| 79 | Proof. destruct L; cbn; [apply const_unfold | reflexivity]. Qed. | ||
| 13 | Open Scope nat_scope. | 81 | Open Scope nat_scope. |
| 15 | Ltac flia := repeat (lia || f_equal). | ||
| 83 | (* ---------- the run model ---------- *) | ||
| 17 | Ltac esc := | ||
| 84 | (* A push reads the right word h :: R': it creates a child frame of value h and | ||
| 18 | (apply BoundedConfig.segRLs_c_spec with (T:=10^3); reflexivity) || | ||
| 85 | the word right of the head becomes [updt R'] (proof.md Lemma RM). *) | ||
| 19 | (apply BoundedConfig.sideRLs_c_spec with (T:=10^3); reflexivity) || | ||
| 86 | Definition updt (R' : list nat) : option (list nat) := | ||
| 20 | (eapply sideRLs_c_spec with (T:=10^6); [vm_compute; reflexivity | st; reflexivity]). | ||
| 87 | match R' with | ||
| 22 | Fixpoint SkelE (n : nat) : side := | ||
| 88 | | [] => Some [1] | ||
| 23 | match n with | ||
| 89 | | g :: R'' => | ||
| 24 | | O => const S0 <* [S1; S1] | ||
| 90 | match g with | ||
| 25 | | S n' => | ||
| 91 | | 0 | 1 => None | ||
| 26 | SkelE n' <* [S0] <* [S1]^^(6 + 4 * n') | ||
| 92 | | 2 => match R'' with | ||
| 27 | <* [S0] <* [S1]^^(6 + 4 * n') | ||
| 93 | | [] => None | ||
| 94 | | c2 :: R3 => match R3 with | ||
| 95 | | [] => Some [S c2] | ||
| 96 | | 0 :: _ => None | ||
| 97 | | S g2 :: rest => Some (S c2 :: S (S g2) :: rest) | ||
| 98 | end | ||
| 99 | end | ||
| 100 | | S (S (S g')) => Some (1 :: S (S g') :: R'') | ||
| 101 | end | ||
| 28 | end. | 102 | end. |
| 30 | Definition SkelO (n : nat) : side := | ||
| 104 | Lemma updt_shape m R' R1 : updt R' = Some R1 -> | ||
| 31 | SkelE n <* [S0] <* [S1]^^(6 + 4 * n). | ||
| 105 | exists x r, rside (S m :: R') = [S1]^^(S m) *> [S0;S0] *> [S1]^^x *> [S0] *> r /\ | ||
| 33 | Definition Pside (i : side) (r : nat) : side := | ||
| 106 | rside R1 = [S1]^^(S x) *> [S0;S0] *> r. | ||
| 34 | i <* [S1]^^r. | ||
| 107 | Proof. | ||
| 36 | Definition Bside (i : side) (j b : nat) : side := | ||
| 108 | intros H. destruct R' as [|g R'']; cbn in H. | ||
| 37 | i <* [S1]^^(4 * j) <* [S0] <* [S1]^^b. | ||
| 109 | - inversion H; subst. exists 0, (const S0). cbn. rewrite !c0_1. split; reflexivity. | ||
| 39 | Definition Aside (i : side) (q b : nat) : side := | ||
| 110 | - destruct g as [|[|[|g']]]; try discriminate. | ||
| 40 | i <* [S0] <* [S1]^^(4 * q + 2) <* [S0] <* [S1]^^b. | ||
| 111 | + destruct R'' as [|c2 R3]; try discriminate. | ||
| 42 | Definition Pe (n r : nat) : side := Pside (SkelE n) r. | ||
| 112 | destruct R3 as [|[|g2] rest]; try discriminate; inversion H; subst. | ||
| 43 | Definition Po (n r : nat) : side := Pside (SkelO n) r. | ||
| 113 | * exists c2, (const S0). cbn. rewrite !c0_1. split; reflexivity. | ||
| 44 | Definition Be (n j b : nat) : side := Bside (SkelE n) j b. | ||
| 114 | * exists c2, ([S0]^^g2 *> rside rest). cbn. split; reflexivity. | ||
| 45 | Definition Bo (n j b : nat) : side := Bside (SkelO n) j b. | ||
| 115 | + inversion H; subst. exists 0, ([S0]^^g' *> rside R''). cbn. split; reflexivity. | ||
| 46 | Definition Ae (n q b : nat) : side := Aside (SkelE n) q b. | ||
| 116 | Qed. | ||
| 47 | Definition Ao (n q b : nat) : side := Aside (SkelO n) q b. | ||
| 118 | Lemma push_ok y h R' R1 L : updt R' = Some R1 -> 1 <= y -> 1 <= h -> | ||
| 49 | Definition K0 : side := const S0. | ||
| 119 | conf (S y :: L) (h :: R') -->+ conf (h :: y :: L) R1. | ||
| 50 | Definition K1 : side := const S0 <* [S1]. | ||
| 120 | Proof. | ||
| 52 | Opaque SkelE SkelO Pside Bside Aside Pe Po Be Bo Ae Ao K0 K1. | ||
| 121 | intros Hu Hy Hh. destruct y as [|n]; [lia|]. destruct h as [|m]; [lia|]. | ||
| 54 | Inductive Side : Type := | ||
| 122 | destruct (updt_shape m R' R1 Hu) as (x & r & E1 & E2). | ||
| 55 | | SK0 : Side | ||
| 123 | unfold conf. change (lside (S (S n) :: L)) with (lsep L <* [S1]^^(S (S n))). | ||
| 56 | | SK1 : Side | ||
| 124 | change (lside (S m :: S n :: L)) with (lsep L <* [S1]^^(S n) <* [S0] <* [S1]^^(S m)). | ||
| 57 | | SPe : nat -> nat -> Side | ||
| 125 | rewrite E1, E2. apply tR1. | ||
| 58 | | SPo : nat -> nat -> Side | ||
| 126 | Qed. | ||
| 59 | | SBe : nat -> nat -> nat -> Side | ||
| 128 | Lemma push0_ok h R' R1 : updt R' = Some R1 -> 1 <= h -> | ||
| 60 | | SBo : nat -> nat -> nat -> Side | ||
| 129 | conf [] (h :: R') -->+ conf [S h] R1. | ||
| 61 | | SAe : nat -> nat -> nat -> Side | ||
| 130 | Proof. | ||
| 62 | | SAo : nat -> nat -> nat -> Side. | ||
| 131 | intros Hu Hh. destruct h as [|m]; [lia|]. | ||
| 64 | Definition to_side (h : Side) : side := | ||
| 132 | destruct (updt_shape m R' R1 Hu) as (x & r & E1 & E2). | ||
| 65 | match h with | ||
| 133 | unfold conf. change (lside []) with (const S0). | ||
| 66 | | SK0 => K0 | ||
| 134 | change (lside [S (S m)]) with (const S0 <* [S1]^^(S (S m))). | ||
| 67 | | SK1 => K1 | ||
| 135 | rewrite E1, E2. apply tR3c. | ||
| 68 | | SPe n r => Pe n r | ||
| 136 | Qed. | ||
| 69 | | SPo n r => Po n r | ||
| 138 | Lemma pop_ok y L R : 1 <= y -> conf (1 :: y :: L) R -->+ conf L (S y :: 2 :: R). | ||
| 70 | | SBe n j b => Be n j b | ||
| 139 | Proof. | ||
| 71 | | SBo n j b => Bo n j b | ||
| 140 | intros Hy. destruct y as [|k]; [lia|]. | ||
| 72 | | SAe n q b => Ae n q b | ||
| 141 | unfold conf. change (lside (1 :: S k :: L)) with (lsep L <* [S1]^^(S k) <* [S0] <* [S1]^^1). | ||
| 73 | | SAo n q b => Ao n q b | ||
| 142 | rewrite lsep_eq. | ||
| 143 | change (rside (S (S k) :: 2 :: R)) with ([S1]^^(S (S k)) *> [S0;S0] *> rside R). | ||
| 144 | apply tR2. | ||
| 145 | Qed. | ||
| 147 | (* ---------- frame semantics ---------- *) | ||
| 148 | Inductive outcome := Fin (R : list nat) | Pop (c : nat) (R : list nat). | ||
| 150 | (* Life x R o: a frame of value x is on top with right word R. | ||
| 151 | Fin R' : it comes back on top with value 1 (it finishes; its parent is popped next); | ||
| 152 | Pop c R': it created c children, and its last child finished, which popped it; | ||
| 153 | R' is the right word after that pop (it starts with its value+1, then 2). *) | ||
| 154 | Inductive Life : nat -> list nat -> outcome -> Prop := | ||
| 155 | | L_fin R : Life 1 R (Fin R) | ||
| 156 | | L_cf y h R' R1 Rc : 1 <= y -> updt R' = Some R1 -> Life h R1 (Fin Rc) -> | ||
| 157 | Life (S y) (h :: R') (Pop 1 (S y :: 2 :: Rc)) | ||
| 158 | | L_cpf y h R' R1 c' R2 Rf : 1 <= y -> updt R' = Some R1 -> Life h R1 (Pop c' R2) -> | ||
| 159 | Life y R2 (Fin Rf) -> Life (S y) (h :: R') (Fin Rf) | ||
| 160 | | L_cpp y h R' R1 c' R2 c Rf : 1 <= y -> updt R' = Some R1 -> Life h R1 (Pop c' R2) -> | ||
| 161 | Life y R2 (Pop c Rf) -> Life (S y) (h :: R') (Pop (S c) Rf). | ||
| 163 | Lemma Life_pos x R o : Life x R o -> 1 <= x. | ||
| 164 | Proof. destruct 1; lia. Qed. | ||
| 166 | Lemma Life_tm x R o : Life x R o -> forall L, | ||
| 167 | match o with | ||
| 168 | | Fin Rf => conf (x :: L) R -->* conf (1 :: L) Rf | ||
| 169 | | Pop _ Rf => conf (x :: L) R -->+ conf L Rf | ||
| 74 | end. | 170 | end. |
| 76 | Fixpoint skelE_measure (n : nat) : nat := | ||
| 171 | Proof. | ||
| 77 | match n with | ||
| 172 | induction 1 as [R|y h R' R1 Rc Hy Hu H1 IH1|y h R' R1 c' R2 Rf Hy Hu H1 IH1 H2 IH2 | ||
| 78 | | O => 2 | ||
| 173 | |y h R' R1 c' R2 c Rf Hy Hu H1 IH1 H2 IH2]; intros L. | ||
| 79 | | S n' => skelE_measure n' + (7 + 4 * n') + (7 + 4 * n') | ||
| 174 | - apply evstep_refl. | ||
| 175 | - eapply progress_trans. { apply push_ok; eauto using Life_pos. } | ||
| 176 | eapply evstep_progress_trans. { apply (IH1 (y :: L)). } | ||
| 177 | apply pop_ok; lia. | ||
| 178 | - apply progress_evstep. eapply progress_trans. { apply push_ok; eauto using Life_pos. } | ||
| 179 | eapply progress_evstep_trans. { apply (IH1 (y :: L)). } | ||
| 180 | apply IH2. | ||
| 181 | - eapply progress_trans. { apply push_ok; eauto using Life_pos. } | ||
| 182 | eapply progress_trans. { apply (IH1 (y :: L)). } | ||
| 183 | apply IH2. | ||
| 184 | Qed. | ||
| 186 | (* ---------- epochs ---------- *) | ||
| 187 | (* Ep W c W': from Edge(W) = conf [] (3::2::W) the edge frame (value 4) creates c | ||
| 188 | children and the epoch ends at conf [] ((5-c)::2::W'). *) | ||
| 189 | Definition Ep (W : list nat) (c : nat) (W' : list nat) : Prop := | ||
| 190 | exists R0, updt (2 :: W) = Some R0 /\ Life 4 R0 (Pop c ((5 - c) :: 2 :: W')). | ||
| 192 | Lemma Ep_tm W c W' : Ep W c W' -> conf [] (3 :: 2 :: W) -->+ conf [] ((5 - c) :: 2 :: W'). | ||
| 193 | Proof. | ||
| 194 | intros (R0 & Hu & HL). | ||
| 195 | eapply progress_trans. { apply push0_ok; [exact Hu | lia]. } | ||
| 196 | exact (Life_tm _ _ _ HL []). | ||
| 197 | Qed. | ||
| 199 | Lemma Life_shape x R o : Life x R o -> forall c Rf, o = Pop c Rf -> | ||
| 200 | exists W', Rf = (x - c + 1) :: 2 :: W' /\ c + 1 <= x /\ | ||
| 201 | forall z, c + 1 <= z -> Life z R (Pop c ((z - c + 1) :: 2 :: W')). | ||
| 202 | Proof. | ||
| 203 | induction 1 as [R|y h R' R1 Rc Hy Hu H1 IH1|y h R' R1 c' R2 Rf Hy Hu H1 IH1 H2 IH2 | ||
| 204 | |y h R' R1 c' R2 c Rf Hy Hu H1 IH1 H2 IH2]; intros c0 Rf0 E; try discriminate. | ||
| 205 | - inversion E; subst. exists Rc. split; [f_equal; lia|]. split; [lia|]. | ||
| 206 | intros z Hz. destruct z as [|z]; [lia|]. | ||
| 207 | replace (S z - 1 + 1) with (S z) by lia. eapply L_cf; eauto; lia. | ||
| 208 | - inversion E; subst. destruct (IH2 c Rf0 eq_refl) as (W' & -> & Hc & Hm). | ||
| 209 | exists W'. split; [f_equal; lia|]. split; [lia|]. | ||
| 210 | intros z Hz. destruct z as [|z]; [lia|]. | ||
| 211 | replace (S z - S c + 1) with (z - c + 1) by lia. eapply L_cpp; eauto; [lia | apply Hm; lia]. | ||
| 212 | Qed. | ||
| 214 | Definition bump (o : outcome) : outcome := | ||
| 215 | match o with Fin W => Fin W | Pop c W => Pop (S c) W end. | ||
| 217 | Lemma L_cp y h R' R1 c' R2 o : 1 <= y -> updt R' = Some R1 -> Life h R1 (Pop c' R2) -> | ||
| 218 | Life y R2 o -> Life (S y) (h :: R') (bump o). | ||
| 219 | Proof. intros. destruct o; cbn; [eapply L_cpf | eapply L_cpp]; eauto. Qed. | ||
| 221 | Lemma updt_cons2 W R0 : updt (2 :: W) = Some R0 -> exists c2 W1, W = c2 :: W1. | ||
| 222 | Proof. destruct W; cbn; [discriminate | eauto]. Qed. | ||
| 224 | (* one child of a replay frame: the child runs a translated epoch (proof.md TL) *) | ||
| 225 | Lemma frame_step y z W c W' o y' z' : Ep W c W' -> 2 <= y -> c + 1 <= z -> | ||
| 226 | y' = y - 1 -> z' = z - c + 1 -> | ||
| 227 | Life y' (z' :: 2 :: W') o -> Life y (z :: 2 :: W) (bump o). | ||
| 228 | Proof. | ||
| 229 | intros (R0 & Hu & HL) Hy Hz -> -> H. | ||
| 230 | destruct (Life_shape _ _ _ HL c _ eq_refl) as (W'' & E & Hc & Hm). | ||
| 231 | injection E as E. subst W''. | ||
| 232 | destruct y as [|y]; [lia|]. | ||
| 233 | eapply L_cp; [lia | exact Hu | apply Hm; exact Hz | ]. | ||
| 234 | replace y with (S y - 1) by lia. exact H. | ||
| 235 | Qed. | ||
| 237 | (* ---------- concrete epoch rules (proof.md section 2) ---------- *) | ||
| 238 | Ltac lf := | ||
| 239 | first | ||
| 240 | [ eassumption | ||
| 241 | | apply L_fin | ||
| 242 | | eapply L_cf; [lia | reflexivity | lf] | ||
| 243 | | eapply L_cpf; [lia | reflexivity | lf | lf] | ||
| 244 | | eapply L_cpp; [lia | reflexivity | lf | lf] ]. | ||
| 246 | Ltac ep := eexists; split; [reflexivity | lf]. | ||
| 248 | Definition tail_ok (N : list nat) : Prop := N = [] \/ exists g rest, N = S (S g) :: rest. | ||
| 250 | Lemma U0 : Ep [1] 2 [2;2;1]. | ||
| 251 | Proof. ep. Qed. | ||
| 253 | Lemma U1 g rest : Ep (1 :: S (S (S (S g))) :: rest) 2 (2 :: 2 :: 1 :: S (S g) :: rest). | ||
| 254 | Proof. ep. Qed. | ||
| 256 | Lemma U2 b N : tail_ok N -> Ep (1 :: 2 :: S b :: N) 2 (S (S (S b)) :: 2 :: 1 :: N). | ||
| 257 | Proof. intros [-> | (g & rest & ->)]; ep. Qed. | ||
| 259 | Lemma ruleS a b N : tail_ok N -> | ||
| 260 | Ep (2 :: 2 :: S a :: 2 :: S b :: N) 2 (S (S a) :: 2 :: S (S (S b)) :: 2 :: 1 :: N). | ||
| 261 | Proof. intros [-> | (g & rest & ->)]; ep. Qed. | ||
| 263 | Lemma TRF a b N Rc : tail_ok N -> 2 <= a -> | ||
| 264 | Life a (S (S (S b)) :: 2 :: 1 :: N) (Fin Rc) -> Ep (a :: 2 :: S b :: N) 2 Rc. | ||
| 265 | Proof. intros [-> | (g & rest & ->)] Ha H; ep. Qed. | ||
| 267 | Lemma Xin0 a'' b'' : 1 <= a'' -> | ||
| 268 | Life 2 [2; 2; a''; 2; b''] (Pop 1 [2; 2; S a''; 2; S b'']). | ||
| 269 | Proof. intros. lf. Qed. | ||
| 271 | Lemma Xin1 a'' b'' g rest : 1 <= a'' -> | ||
| 272 | Life 2 (2 :: 2 :: a'' :: 2 :: b'' :: S g :: rest) (Pop 1 (2 :: 2 :: S a'' :: 2 :: S b'' :: S (S g) :: rest)). | ||
| 273 | Proof. intros. lf. Qed. | ||
| 275 | Lemma TRX0 a b N c a'' b'' : tail_ok N -> 2 <= a -> | ||
| 276 | Life a (S (S (S b)) :: 2 :: 1 :: N) (Pop c [2; 2; S a''; 2; S b'']) -> | ||
| 277 | Ep (a :: 2 :: S b :: N) 3 [S (S a''); 2; S (S b'')]. | ||
| 278 | Proof. intros [-> | (g & rest & ->)] Ha H; ep. Qed. | ||
| 280 | Lemma TRX1 a b N c a'' b'' g rest : tail_ok N -> 2 <= a -> | ||
| 281 | Life a (S (S (S b)) :: 2 :: 1 :: N) (Pop c (2 :: 2 :: S a'' :: 2 :: S b'' :: S g :: rest)) -> | ||
| 282 | Ep (a :: 2 :: S b :: N) 3 (S (S a'') :: 2 :: S (S b'') :: S (S g) :: rest). | ||
| 283 | Proof. intros [-> | (g' & rest' & ->)] Ha H; ep. Qed. | ||
| 285 | (* ---------- marker words, orbits, replay ---------- *) | ||
| 286 | (* A marker word is given by its absorption indices P = [I_1; ...; I_m] (proof.md section 0): | ||
| 287 | gaps g_j = I_j - I_(j-1) + 1, each followed by a lone 1. *) | ||
| 288 | Fixpoint mwf (s : nat) (P : list nat) : list nat := | ||
| 289 | match P with | ||
| 290 | | [] => [] | ||
| 291 | | p :: P' => (p - s + 1) :: 1 :: mwf p P' | ||
| 80 | end. | 292 | end. |
| 82 | Definition skelO_measure (n : nat) : nat := | ||
| 293 | Definition mw (P : list nat) : list nat := mwf 0 P. | ||
| 83 | skelE_measure n + (7 + 4 * n). | ||
| 295 | (* even gaps: each index is odd above the previous one *) | ||
| 85 | Definition side_measure (h : Side) : nat := | ||
| 296 | Fixpoint valid_from (s : nat) (P : list nat) : Prop := | ||
| 86 | match h with | 297 | match P with |
| 87 | | SK0 => 0 | ||
| 298 | | [] => True | ||
| 88 | | SK1 => 1 | ||
| 299 | | p :: P' => (exists t, p = s + 2 * t + 1) /\ valid_from p P' | ||
| 89 | | SPe n r => skelE_measure n + r | ||
| 90 | | SPo n r => skelO_measure n + r | ||
| ⋯ 2 template-only lines (template 91–92), not in ours | |||
| 93 | | SAe n q b => skelE_measure n + 4 * q + 4 + b | ||
| 94 | | SAo n q b => skelO_measure n + 4 * q + 4 + b | ||
| 95 | end. | 300 | end. |
| 97 | Definition class_rank (q : Q) (h : Side) : nat := | ||
| 301 | Definition valid (P : list nat) : Prop := valid_from 0 P. | ||
| 98 | match q, h with | ||
| 303 | Definition cnt (Q : list nat) (n : nat) : nat := length (filter (fun q => q <? n) Q). | ||
| 99 | | D, SBe _ _ _ => 3 | ||
| 304 | Definition ind (Q : list nat) (n : nat) : nat := cnt Q (S n) - cnt Q n. | ||
| 100 | | D, SBo _ _ _ => 3 | ||
| 305 | Definition cost (Q : list nat) (n : nat) : nat := 2 + ind Q n. | ||
| 101 | | C, SBe _ _ _ => 2 | ||
| 307 | Inductive Orb (Q : list nat) : nat -> list nat -> Prop := | ||
| 102 | | C, SBo _ _ _ => 2 | ||
| 308 | | O0 : Orb Q 0 (1 :: mw Q) | ||
| 103 | | F, SBe _ _ _ => 1 | ||
| 309 | | OS n W W' : Orb Q n W -> Ep W (cost Q n) W' -> Orb Q (S n) W'. | ||
| 104 | | F, SBo _ _ _ => 1 | ||
| 311 | Fixpoint bumpn (k : nat) (o : outcome) : outcome := | ||
| 105 | | F, SAe _ _ _ => 1 | ||
| 312 | match k with 0 => o | S k => bumpn k (bump o) end. | ||
| 106 | | F, SAo _ _ _ => 1 | ||
| 314 | Lemma bumpn_fin k W : bumpn k (Fin W) = Fin W. | ||
| 107 | | _, _ => 0 | ||
| 315 | Proof. induction k; cbn; auto. Qed. | ||
| 108 | end. | ||
| 317 | Lemma bumpn_pop k c W : bumpn k (Pop c W) = Pop (k + c) W. | ||
| 110 | Definition measure (q : Q) (h : Side) : nat := | ||
| 318 | Proof. revert c. induction k; intros c; cbn; [reflexivity|]. rewrite IHk. f_equal. lia. Qed. | ||
| 111 | 4 * side_measure h + class_rank q h. | ||
| 320 | Lemma cnt_0 Q : cnt Q 0 = 0. | ||
| 113 | Transparent SkelE SkelO Pside Bside Aside Pe Po Be Bo Ae Ao K0 K1. | ||
| 321 | Proof. unfold cnt. induction Q; cbn [filter length]; auto. Qed. | ||
| 115 | Lemma side_repeat_one_succ l n : | ||
| 323 | Lemma cnt_mono Q n : cnt Q n <= cnt Q (S n). | ||
| 116 | l <* [S1]^^(S n) = S1 >> (l <* [S1]^^n). | ||
| 117 | Proof. | 324 | Proof. |
| 118 | cbn [lpow]. | ||
| 325 | unfold cnt. induction Q as [|q Q IH]; cbn [filter length]; [lia|]. | ||
| 119 | reflexivity. | ||
| 326 | destruct (Nat.ltb_spec q n), (Nat.ltb_spec q (S n)); cbn [length]; lia. | ||
| 120 | Qed. | 327 | Qed. |
| 122 | Lemma K1_step : | ||
| 329 | Lemma cnt_mono' Q n m : n <= m -> cnt Q n <= cnt Q m. | ||
| 123 | K1 = S1 >> K0. | ||
| 330 | Proof. induction 1; [lia|]. pose proof (cnt_mono Q m). lia. Qed. | ||
| 332 | Lemma replay Q k Wk : Orb Q k Wk -> forall y z o, k + 1 <= y -> (k = 0 \/ k + 2 + cnt Q k <= z) -> | ||
| 333 | Life (y - k) ((z - k - cnt Q k) :: 2 :: Wk) o -> Life y (z :: 2 :: 1 :: mw Q) (bumpn k o). | ||
| 124 | Proof. | 334 | Proof. |
| 125 | unfold K1, K0. | ||
| 335 | induction 1 as [|n W W' HO IH HE]; intros y z o Hy Hz H. | ||
| 126 | reflexivity. | ||
| 336 | - cbn in *. rewrite cnt_0, !Nat.sub_0_r in H. exact H. | ||
| 337 | - cbn [bumpn]. pose proof (cnt_mono Q n) as Hm. unfold cost, ind in HE. | ||
| 338 | apply IH; [lia | right; lia | ]. | ||
| 339 | eapply frame_step; [exact HE | lia | lia | | | exact H]; lia. | ||
| 127 | Qed. | 340 | Qed. |
| 129 | Lemma Pe_succ_step n r : | ||
| 342 | Lemma mw_tail_ok Q : valid Q -> tail_ok (mw Q). | ||
| 130 | Pe n (S r) = S1 >> Pe n r. | ||
| 131 | Proof. | 343 | Proof. |
| 132 | unfold Pe, Pside. | ||
| 344 | destruct Q as [|q Q]; [left; reflexivity|]. | ||
| 133 | rewrite side_repeat_one_succ. | ||
| 345 | intros [[t Ht] _]. right. exists (q - 1), (1 :: mwf q Q). cbn. f_equal. lia. | ||
| 134 | reflexivity. | ||
| 135 | Qed. | 346 | Qed. |
| 137 | Lemma Po_succ_step n r : | ||
| 348 | Lemma ruleT a b Q W' : Orb Q (a - 1) W' -> 2 <= a -> 1 <= b -> valid Q -> | ||
| 138 | Po n (S r) = S1 >> Po n r. | ||
| 349 | a - 1 + cnt Q (a - 1) <= b -> | ||
| 350 | Ep (a :: 2 :: b :: mw Q) 2 ((b + 3 - a - cnt Q (a - 1)) :: 2 :: W'). | ||
| 139 | Proof. | 351 | Proof. |
| 140 | unfold Po, Pside. | ||
| 352 | intros HO Ha Hb HV Hc. destruct b as [|b]; [lia|]. | ||
| 141 | rewrite side_repeat_one_succ. | ||
| 353 | apply TRF; [apply mw_tail_ok; exact HV | exact Ha | ]. | ||
| 142 | reflexivity. | ||
| 354 | rewrite <- (bumpn_fin (a - 1)). | ||
| 355 | apply (replay Q (a - 1) W' HO); [lia | lia | ]. | ||
| 356 | replace (a - (a - 1)) with 1 by lia. | ||
| 357 | replace (S (S (S b)) - (a - 1) - cnt Q (a - 1)) with (S b + 3 - a - cnt Q (a - 1)) by lia. | ||
| 358 | apply L_fin. | ||
| 143 | Qed. | 359 | Qed. |
| 145 | Lemma Be_succ_step n j b : | ||
| 361 | Lemma mwf_shift s k P : mwf (s + k) (map (fun p => p + k) P) = mwf s P. | ||
| 146 | Be n j (S b) = S1 >> Be n j b. | ||
| 147 | Proof. | 362 | Proof. |
| 148 | unfold Be, Bside. | ||
| 363 | revert s. induction P as [|p P IH]; intros s; cbn; [reflexivity|]. | ||
| 149 | rewrite side_repeat_one_succ. | ||
| 364 | rewrite IH. f_equal. lia. | ||
| 150 | reflexivity. | ||
| 151 | Qed. | 365 | Qed. |
| 153 | Lemma Bo_succ_step n j b : | ||
| 367 | Lemma ruleX a b Q a'' Q'' : Orb Q (a - 2) (a'' :: 2 :: b :: mw Q'') -> 3 <= a -> 1 <= b -> | ||
| 154 | Bo n j (S b) = S1 >> Bo n j b. | ||
| 368 | 1 <= a'' -> valid Q -> valid Q'' -> b = a - 2 + cnt Q (a - 2) -> | ||
| 369 | Ep (a :: 2 :: b :: mw Q) 3 (S (S a'') :: 2 :: S (S b) :: mw (map (fun q => q + 2) Q'')). | ||
| 155 | Proof. | 370 | Proof. |
| 156 | unfold Bo, Bside. | ||
| 371 | intros HO Ha Hb Ha'' HV HV'' Hbe. destruct b as [|b0]; [lia|]. | ||
| 157 | rewrite side_repeat_one_succ. | ||
| 372 | assert (Hz : S (S (S b0)) - (a - 2) - cnt Q (a - 2) = 2) by lia. | ||
| 158 | reflexivity. | ||
| 373 | assert (Hy : a - (a - 2) = 2) by lia. | ||
| 374 | destruct Q'' as [|q Q2]. | ||
| 375 | - cbn. eapply TRX0 with (c := a - 2 + 1); [apply mw_tail_ok; exact HV | lia | ]. | ||
| 376 | rewrite <- bumpn_pop. | ||
| 377 | apply (replay Q (a - 2) _ HO); [lia | lia | ]. | ||
| 378 | rewrite Hz, Hy. apply Xin0. exact Ha''. | ||
| 379 | - change (mw (q :: Q2)) with ((q - 0 + 1) :: 1 :: mwf q Q2) in HO. | ||
| 380 | replace (q - 0 + 1) with (S q) in HO by lia. | ||
| 381 | cbn [mw mwf map]. replace (q + 2 - 0 + 1) with (S (S (S q))) by lia. | ||
| 382 | replace (q + 2) with (q + 2) by reflexivity. rewrite mwf_shift. | ||
| 383 | eapply TRX1 with (c := a - 2 + 1); [apply mw_tail_ok; exact HV | lia | ]. | ||
| 384 | rewrite <- bumpn_pop. | ||
| 385 | apply (replay Q (a - 2) _ HO); [lia | lia | ]. | ||
| 386 | rewrite Hz, Hy. apply Xin1. exact Ha''. | ||
| 159 | Qed. | 387 | Qed. |
| 161 | Lemma Ae_succ_step n q b : | ||
| 389 | (* ---------- list lemmas ---------- *) | ||
| 162 | Ae n q (S b) = S1 >> Ae n q b. | ||
| 390 | Lemma valid_gt s P : valid_from s P -> Forall (fun p => s < p) P. | ||
| 163 | Proof. | 391 | Proof. |
| 164 | unfold Ae, Aside. | ||
| 392 | revert s. induction P as [|p P IH]; intros s H; [constructor|]. | ||
| 165 | rewrite side_repeat_one_succ. | ||
| 393 | destruct H as [[t Ht] HP]. constructor; [lia|]. | ||
| 166 | reflexivity. | ||
| 394 | specialize (IH p HP). eapply Forall_impl; [|exact IH]. intros x Hx; cbn in *; lia. | ||
| 167 | Qed. | 395 | Qed. |
| 169 | Lemma Ao_succ_step n q b : | ||
| 397 | Lemma cnt_cons_lt q Q n : q < n -> cnt (q :: Q) n = S (cnt Q n). | ||
| 170 | Ao n q (S b) = S1 >> Ao n q b. | ||
| 398 | Proof. intros H. unfold cnt. cbn [filter]. rewrite (proj2 (Nat.ltb_lt q n) H). reflexivity. Qed. | ||
| 400 | Lemma cnt_cons_ge q Q n : n <= q -> cnt (q :: Q) n = cnt Q n. | ||
| 401 | Proof. intros H. unfold cnt. cbn [filter]. rewrite (proj2 (Nat.ltb_ge q n) H). reflexivity. Qed. | ||
| 403 | Lemma cnt_app X Y n : cnt (X ++ Y) n = cnt X n + cnt Y n. | ||
| 404 | Proof. unfold cnt. rewrite filter_app, length_app. reflexivity. Qed. | ||
| 406 | Lemma cnt_all_lt X n : Forall (fun q => q < n) X -> cnt X n = length X. | ||
| 171 | Proof. | 407 | Proof. |
| 172 | unfold Ao, Aside. | ||
| 408 | induction 1 as [|q X Hq HX IH]; [reflexivity|]. | ||
| 173 | rewrite side_repeat_one_succ. | ||
| 409 | rewrite cnt_cons_lt by exact Hq. cbn [length]. lia. | ||
| 174 | reflexivity. | ||
| 175 | Qed. | 410 | Qed. |
| 177 | Lemma Pe_zero_step : | ||
| 412 | Lemma cnt_all_ge X n : Forall (fun q => n <= q) X -> cnt X n = 0. | ||
| 178 | Pe 0 0 = S1 >> K1. | ||
| 179 | Proof. | 413 | Proof. |
| 180 | unfold Pe, Pside, K1, SkelE. | ||
| 414 | induction 1 as [|q X Hq HX IH]; [reflexivity|]. | ||
| 181 | reflexivity. | ||
| 415 | rewrite cnt_cons_ge by exact Hq. exact IH. | ||
| 182 | Qed. | 416 | Qed. |
| 184 | Lemma Pe_succ_zero_step n : | ||
| 418 | Lemma cnt_S_nin Q n : ~ In n Q -> cnt Q (S n) = cnt Q n. | ||
| 185 | Pe (S n) 0 = S1 >> Bo n 0 (5 + 4 * n). | ||
| 186 | Proof. | 419 | Proof. |
| 187 | unfold Pe, Pside. | ||
| 420 | induction Q as [|q Q IH]; intros H; [reflexivity|]. | ||
| 188 | cbn [SkelE]. | ||
| 421 | assert (q <> n) by (intro; apply H; left; auto). | ||
| 189 | unfold Bo, Bside, SkelO. | ||
| 422 | assert (~ In n Q) by (intro; apply H; right; auto). | ||
| 190 | replace (6 + 4 * n) with (S (5 + 4 * n)) by lia. | ||
| 423 | destruct (Nat.lt_ge_cases q n). | ||
| 191 | cbn [lpow Nat.mul]. | ||
| 424 | - rewrite !cnt_cons_lt by lia. f_equal. auto. | ||
| 192 | reflexivity. | ||
| 425 | - rewrite !cnt_cons_ge by lia. auto. | ||
| 193 | Qed. | 426 | Qed. |
| 195 | Lemma Po_zero_step n : | ||
| 428 | Lemma cnt_S_in s Q n : valid_from s Q -> In n Q -> cnt Q (S n) = S (cnt Q n). | ||
| 196 | Po n 0 = S1 >> Be n 0 (5 + 4 * n). | ||
| 197 | Proof. | 429 | Proof. |
| 198 | unfold Po, Be, Pside, Bside, SkelO. | ||
| 430 | revert s. induction Q as [|q Q IH]; intros s HV H; [destruct H|]. | ||
| 199 | replace (6 + 4 * n) with (S (5 + 4 * n)) by lia. | ||
| 431 | destruct HV as [_ HV]. pose proof (valid_gt _ _ HV) as Hg. rewrite Forall_forall in Hg. | ||
| 200 | cbn [lpow Nat.mul]. | ||
| 432 | destruct H as [<- | H]. | ||
| 201 | reflexivity. | ||
| 433 | - rewrite cnt_cons_lt by lia. rewrite cnt_cons_ge by lia. f_equal. apply cnt_S_nin. | ||
| 434 | intro Hin. specialize (Hg _ Hin). lia. | ||
| 435 | - pose proof (Hg _ H). rewrite !cnt_cons_lt by lia. f_equal. eapply IH; eauto. | ||
| 202 | Qed. | 436 | Qed. |
| 204 | Lemma Be_zero_step n j : | ||
| 438 | Lemma ind_in Q n : valid Q -> In n Q -> ind Q n = 1. | ||
| 205 | Be n j 0 = S0 >> Pe n (4 * j). | ||
| 439 | Proof. intros HV H. unfold ind. rewrite (cnt_S_in 0 Q n HV H). lia. Qed. | ||
| 441 | Lemma ind_nin Q n : ~ In n Q -> ind Q n = 0. | ||
| 442 | Proof. intros H. unfold ind. rewrite (cnt_S_nin Q n H). lia. Qed. | ||
| 444 | Lemma ind_iff P Q k k' : valid P -> valid Q -> (In k P <-> In k' Q) -> ind P k = ind Q k'. | ||
| 206 | Proof. | 445 | Proof. |
| 207 | unfold Be, Pe, Bside, Pside. | ||
| 446 | intros HP HQ E. destruct (in_dec Nat.eq_dec k P) as [H|H]. | ||
| 208 | reflexivity. | ||
| 447 | - rewrite (ind_in P k HP H), (ind_in Q k' HQ (proj1 E H)). reflexivity. | ||
| 448 | - rewrite (ind_nin P k H), (ind_nin Q k'); [reflexivity|]. intro H'. apply H, E, H'. | ||
| 209 | Qed. | 449 | Qed. |
| 211 | Lemma Bo_zero_step n j : | ||
| 451 | Lemma parity_in s P n : valid_from s P -> In n P -> exists u, n + cnt P n + s = 2 * u + 1. | ||
| 212 | Bo n j 0 = S0 >> Po n (4 * j). | ||
| 213 | Proof. | 452 | Proof. |
| 214 | unfold Bo, Po, Bside, Pside. | ||
| 453 | revert s. induction P as [|p P IH]; intros s HV H; [destruct H|]. | ||
| 215 | reflexivity. | ||
| 454 | destruct HV as [[t Ht] HV]. pose proof (valid_gt _ _ HV) as Hg. rewrite Forall_forall in Hg. | ||
| 455 | destruct H as [<- | H]. | ||
| 456 | - rewrite cnt_cons_ge by lia. rewrite cnt_all_ge. | ||
| 457 | + exists (s + t). lia. | ||
| 458 | + apply Forall_forall. intros x Hx. specialize (Hg _ Hx). lia. | ||
| 459 | - pose proof (Hg _ H). rewrite cnt_cons_lt by lia. destruct (IH p HV H) as [u Hu]. | ||
| 460 | exists (u - t). lia. | ||
| 216 | Qed. | 461 | Qed. |
| 218 | Lemma Ae_zero_step n q : | ||
| 463 | Lemma filter_lt_app X Y k : Forall (fun q => q <= k) X -> | ||
| 219 | Ae n q 0 = S0 >> Be n 0 (4 * q + 2). | ||
| 464 | filter (fun q => k <? q) (X ++ Y) = filter (fun q => k <? q) Y. | ||
| 220 | Proof. | 465 | Proof. |
| 221 | unfold Ae, Be, Aside, Bside. | ||
| 466 | intros H. rewrite filter_app. replace (filter (fun q => k <? q) X) with (@nil nat); [reflexivity|]. | ||
| 222 | reflexivity. | ||
| 467 | induction H as [|q X Hq HX IH]; cbn [filter]; [reflexivity|]. | ||
| 468 | rewrite (proj2 (Nat.ltb_ge k q) Hq). exact IH. | ||
| 223 | Qed. | 469 | Qed. |
| 225 | Lemma Ao_zero_step n q : | ||
| 471 | Lemma filter_filter_lt P k k' : k <= k' -> | ||
| 226 | Ao n q 0 = S0 >> Bo n 0 (4 * q + 2). | ||
| 472 | filter (fun p => k' <? p) (filter (fun p => k <? p) P) = filter (fun p => k' <? p) P. | ||
| 227 | Proof. | 473 | Proof. |
| 228 | unfold Ao, Bo, Aside, Bside. | ||
| 474 | intros Hk. induction P as [|p P IH]; cbn [filter]; [reflexivity|]. | ||
| 229 | reflexivity. | ||
| 475 | destruct (Nat.ltb_spec k p); cbn [filter]; destruct (Nat.ltb_spec k' p); try lia; rewrite IH; reflexivity. | ||
| 230 | Qed. | 476 | Qed. |
| 232 | Opaque SkelE SkelO Pside Bside Aside Pe Po Be Bo Ae Ao K0 K1. | ||
| 478 | Lemma filter_all P k : Forall (fun p => k < p) P -> filter (fun p => k <? p) P = P. | ||
| 234 | Lemma to_side_SK1_step : | ||
| 235 | to_side SK1 = S1 >> to_side SK0. | ||
| 236 | Proof. | 479 | Proof. |
| 237 | cbn [to_side]. | ||
| 480 | induction 1 as [|p P Hp HP IH]; cbn [filter]; [reflexivity|]. | ||
| 238 | apply K1_step. | ||
| 481 | rewrite (proj2 (Nat.ltb_lt k p) Hp). rewrite IH. reflexivity. | ||
| 239 | Qed. | 482 | Qed. |
| 241 | Lemma to_side_SPe_succ_step n r : | ||
| 484 | Lemma filter_gt P k p : In p (filter (fun p => k <? p) P) -> k < p. | ||
| 242 | to_side (SPe n (S r)) = S1 >> to_side (SPe n r). | ||
| 485 | Proof. intros Hp. apply filter_In in Hp. destruct Hp as [_ Hp]. apply Nat.ltb_lt. exact Hp. Qed. | ||
| 487 | Lemma filter_in P k p : k < p -> (In p (filter (fun p => k <? p) P) <-> In p P). | ||
| 243 | Proof. | 488 | Proof. |
| 244 | cbn [to_side]. | ||
| 489 | intros H. rewrite filter_In. split; [tauto|]. intros Hp. split; [exact Hp | apply Nat.ltb_lt; exact H]. | ||
| 245 | apply Pe_succ_step. | ||
| 246 | Qed. | 490 | Qed. |
| 248 | Lemma to_side_SPo_succ_step n r : | ||
| 492 | Lemma filter_cnt_len P n : length (filter (fun p => n <? p) P) + cnt P (S n) = length P. | ||
| 249 | to_side (SPo n (S r)) = S1 >> to_side (SPo n r). | ||
| 250 | Proof. | 493 | Proof. |
| 251 | cbn [to_side]. | ||
| 494 | induction P as [|p P IH]; [reflexivity|]. cbn [filter length]. | ||
| 252 | apply Po_succ_step. | ||
| 495 | destruct (Nat.ltb_spec n p). | ||
| 496 | - rewrite cnt_cons_ge by lia. cbn [length]. lia. | ||
| 497 | - rewrite cnt_cons_lt by lia. lia. | ||
| 253 | Qed. | 498 | Qed. |
| 255 | Lemma to_side_SBe_succ_step n j b : | ||
| 500 | (* shifted copies of index lists *) | ||
| 256 | to_side (SBe n j (S b)) = S1 >> to_side (SBe n j b). | ||
| 501 | Definition Sh (u v : nat) (Q P : list nat) : Prop := Forall2 (fun q p => q + u = p + v) Q P. | ||
| 503 | Lemma Sh_len u v Q P : Sh u v Q P -> length Q = length P. | ||
| 504 | Proof. apply Forall2_length. Qed. | ||
| 506 | Lemma Sh_eq u v u' v' Q P : Sh u v Q P -> u = u' -> v = v' -> Sh u' v' Q P. | ||
| 507 | Proof. intros H -> ->. exact H. Qed. | ||
| 509 | Lemma Sh_filter u v Q P k k' : Sh u v Q P -> k + u = k' + v -> | ||
| 510 | Sh u v (filter (fun q => k <? q) Q) (filter (fun p => k' <? p) P). | ||
| 257 | Proof. | 511 | Proof. |
| 258 | cbn [to_side]. | ||
| 512 | unfold Sh. induction 1 as [|q p Q P Hqp HQP IH]; intros Hk; cbn [filter]; [constructor|]. | ||
| 259 | apply Be_succ_step. | ||
| 513 | destruct (Nat.ltb_spec k q), (Nat.ltb_spec k' p); try lia. | ||
| 514 | - constructor; auto. | ||
| 515 | - auto. | ||
| 260 | Qed. | 516 | Qed. |
| 262 | Lemma to_side_SBo_succ_step n j b : | ||
| 518 | Lemma Sh_in u v Q P k k' : Sh u v Q P -> k + u = k' + v -> (In k Q <-> In k' P). | ||
| 263 | to_side (SBo n j (S b)) = S1 >> to_side (SBo n j b). | ||
| 264 | Proof. | 519 | Proof. |
| 265 | cbn [to_side]. | ||
| 520 | unfold Sh. induction 1 as [|q p Q P Hqp HQP IH]; intros Hk; cbn [In]; [tauto|]. | ||
| 266 | apply Bo_succ_step. | ||
| 521 | specialize (IH Hk). split; (intros [H|H]; [left; lia | right; tauto]). | ||
| 267 | Qed. | 522 | Qed. |
| 269 | Lemma to_side_SAe_succ_step n q b : | ||
| 524 | Lemma Sh_trans u1 v1 u2 v2 u v w X Y Z : Sh u1 v1 X Y -> Sh u2 v2 Y Z -> | ||
| 270 | to_side (SAe n q (S b)) = S1 >> to_side (SAe n q b). | ||
| 525 | u1 + u2 = u + w -> v1 + v2 = v + w -> Sh u v X Z. | ||
| 271 | Proof. | 526 | Proof. |
| 272 | cbn [to_side]. | ||
| 527 | unfold Sh. intros H1. revert Z. induction H1 as [|x y X Y Hxy HXY IH]; intros Z H2 E1 E2; | ||
| 273 | apply Ae_succ_step. | ||
| 528 | inversion H2; subst; constructor; [lia | auto]. | ||
| 274 | Qed. | 529 | Qed. |
| 276 | Lemma to_side_SAo_succ_step n q b : | ||
| 531 | Lemma Sh_map u v d Q P : Sh u v Q P -> Sh u (v + d) (map (fun q => q + d) Q) P. | ||
| 277 | to_side (SAo n q (S b)) = S1 >> to_side (SAo n q b). | ||
| 532 | Proof. unfold Sh. induction 1; cbn [map]; constructor; [lia | auto]. Qed. | ||
| 534 | Lemma Sh_unmap v k P : Forall (fun p => k <= p) P -> Sh (v + k) v (map (fun p => p - k) P) P. | ||
| 535 | Proof. unfold Sh. induction 1; cbn [map]; constructor; [lia | auto]. Qed. | ||
| 537 | Lemma Sh_ge u v Q P k k' : Sh u v Q P -> (forall p, In p P -> k' <= p) -> k + u <= k' + v -> | ||
| 538 | Forall (fun q => k <= q) Q. | ||
| 278 | Proof. | 539 | Proof. |
| 279 | cbn [to_side]. | ||
| 540 | unfold Sh. induction 1 as [|q p Q P Hqp HQP IH]; intros Hp Hk; constructor. | ||
| 280 | apply Ao_succ_step. | ||
| 541 | - specialize (Hp p (or_introl eq_refl)). lia. | ||
| 542 | - apply IH; [intros x Hx; apply Hp; right; exact Hx | exact Hk]. | ||
| 281 | Qed. | 543 | Qed. |
| 283 | Lemma to_side_SPe_zero_step : | ||
| 545 | Lemma valid_shift s k P : valid_from s P -> valid_from (s + k) (map (fun p => p + k) P). | ||
| 284 | to_side (SPe 0 0) = S1 >> to_side SK1. | ||
| 285 | Proof. | 546 | Proof. |
| 286 | cbn [to_side]. | ||
| 547 | revert s. induction P as [|p P IH]; intros s H; [exact I|]. | ||
| 287 | apply Pe_zero_step. | ||
| 548 | destruct H as [[t Ht] H]. cbn [map valid_from]. split; [exists t; lia | apply IH; exact H]. | ||
| 288 | Qed. | 549 | Qed. |
| 290 | Lemma to_side_SPe_succ_zero_step n : | ||
| 551 | Lemma valid_map2 s P : valid_from s P -> valid_from s (map (fun p => p + 2) P). | ||
| 291 | to_side (SPe (S n) 0) = S1 >> to_side (SBo n 0 (5 + 4 * n)). | ||
| 292 | Proof. | 552 | Proof. |
| 293 | cbn [to_side]. | ||
| 553 | destruct P as [|p P]; intros H; [exact I|]. destruct H as [[t Ht] H]. | ||
| 294 | apply Pe_succ_zero_step. | ||
| 554 | cbn [map valid_from]. split; [exists (S t); lia | apply valid_shift; exact H]. | ||
| 295 | Qed. | 555 | Qed. |
| 297 | Lemma to_side_SPo_zero_step n : | ||
| 557 | Lemma valid_cons1 Q : valid Q -> valid (1 :: map (fun q => q + 1) Q). | ||
| 298 | to_side (SPo n 0) = S1 >> to_side (SBe n 0 (5 + 4 * n)). | ||
| 558 | Proof. intros H. cbn [valid valid_from]. split; [exists 0; lia | apply (valid_shift 0 1 Q H)]. Qed. | ||
| 560 | Lemma valid_unshift s k P : valid_from (s + k) P -> valid_from s (map (fun p => p - k) P). | ||
| 299 | Proof. | 561 | Proof. |
| 300 | cbn [to_side]. | ||
| 562 | revert s. induction P as [|p P IH]; intros s H; [exact I|]. | ||
| 301 | apply Po_zero_step. | ||
| 563 | destruct H as [[t Ht] H]. cbn [map valid_from]. split; [exists t; lia|]. | ||
| 564 | apply IH. replace (p - k + k) with p by lia. exact H. | ||
| 302 | Qed. | 565 | Qed. |
| 304 | Lemma to_side_SBe_zero_step n j : | ||
| 567 | Lemma valid_app_l X Y : valid (X ++ Y) -> Forall (fun q => 1 <= q) X. | ||
| 305 | to_side (SBe n j 0) = S0 >> to_side (SPe n (4 * j)). | ||
| 306 | Proof. | 568 | Proof. |
| 307 | cbn [to_side]. | ||
| 569 | intros H. apply valid_gt in H. apply Forall_app in H. destruct H as [H _]. | ||
| 308 | apply Be_zero_step. | ||
| 570 | eapply Forall_impl; [|exact H]. intros; lia. | ||
| 309 | Qed. | 571 | Qed. |
| 311 | Lemma to_side_SBo_zero_step n j : | ||
| 573 | Lemma mwf_unshift s k P : k <= s -> Forall (fun p => k <= p) P -> | ||
| 312 | to_side (SBo n j 0) = S0 >> to_side (SPo n (4 * j)). | ||
| 574 | mwf (s - k) (map (fun p => p - k) P) = mwf s P. | ||
| 313 | Proof. | 575 | Proof. |
| 314 | cbn [to_side]. | ||
| 576 | intros Hs H. revert s Hs. induction H as [|p P Hp HP IH]; intros s Hs; cbn [map mwf]; [reflexivity|]. | ||
| 315 | apply Bo_zero_step. | ||
| 577 | rewrite (IH p Hp). f_equal. lia. | ||
| 316 | Qed. | 578 | Qed. |
| 318 | Lemma to_side_SAe_zero_step n q : | ||
| 580 | Lemma mw_cons1 Q : 2 :: 1 :: mw Q = mw (1 :: map (fun q => q + 1) Q). | ||
| 319 | to_side (SAe n q 0) = S0 >> to_side (SBe n 0 (4 * q + 2)). | ||
| 581 | Proof. unfold mw. cbn [mwf]. rewrite <- (mwf_shift 0 1 Q). reflexivity. Qed. | ||
| 583 | Lemma valid_tail_ok s P : valid_from s P -> tail_ok (mwf s P). | ||
| 320 | Proof. | 584 | Proof. |
| 321 | cbn [to_side]. | ||
| 585 | destruct P as [|p P]; [left; reflexivity|]. | ||
| 322 | apply Ae_zero_step. | ||
| 586 | intros [[t Ht] _]. right. exists (2 * t), (1 :: mwf p P). cbn [mwf]. f_equal. lia. | ||
| 323 | Qed. | 587 | Qed. |
| 325 | Lemma to_side_SAo_zero_step n q : | ||
| 589 | Lemma cnt1_valid P : valid P -> cnt P 1 = 0. | ||
| 326 | to_side (SAo n q 0) = S0 >> to_side (SBo n 0 (4 * q + 2)). | ||
| 327 | Proof. | 590 | Proof. |
| 328 | cbn [to_side]. | ||
| 591 | intros H. apply cnt_all_ge. apply valid_gt in H. eapply Forall_impl; [|exact H]. intros; cbn in *; lia. | ||
| 329 | apply Ao_zero_step. | ||
| 330 | Qed. | 592 | Qed. |
| 332 | Ltac expand_one_to_side_in_goal := | ||
| 594 | Lemma in_transfer Qi Qe P k k' u v kf : Forall (fun q => q < k) Qi -> | ||
| 333 | first | ||
| 595 | Sh u v Qe (filter (fun p => kf <? p) P) -> k + u = k' + v -> kf < k' -> | ||
| 334 | [ rewrite to_side_SK1_step | ||
| 596 | (In k (Qi ++ Qe) <-> In k' P). | ||
| 335 | | rewrite to_side_SPe_succ_step | ||
| 336 | | rewrite to_side_SPo_succ_step | ||
| ⋯ 23 template-only lines (template 337–361), not in ours | |||
| 362 | sideRLs tm h a' b' -> | ||
| 363 | sideRLs tm h a b. | ||
| 364 | Proof. | 597 | Proof. |
| 365 | intros -> -> H. | ||
| 598 | intros HQi Hsh E Hk. rewrite in_app_iff, (Sh_in _ _ _ _ k k' Hsh E), (filter_in P kf k' Hk). | ||
| 366 | exact H. | ||
| 599 | rewrite Forall_forall in HQi. | ||
| 600 | split; [intros [H|H]; [specialize (HQi _ H); lia | exact H] | intros H; right; exact H]. | ||
| 367 | Qed. | 601 | Qed. |
| 369 | Ltac unfold_to_side_one_step := | ||
| 603 | Lemma sh_compose Qi Qe Qe' P n a a' k k' : Forall (fun q => q <= k) Qi -> n <= k' -> | ||
| 370 | expand_one_to_side_in_goal. | ||
| 604 | k + (n + 3) = k' + a -> | ||
| 372 | Ltac normalize_sideRLs_ends := | ||
| 605 | Sh (k + 3) a' Qe' (filter (fun q => k <? q) (Qi ++ Qe)) -> | ||
| 373 | lazymatch goal with | ||
| 606 | Sh (n + 3) a Qe (filter (fun p => n <? p) P) -> | ||
| 374 | | |- sideRLs ?tm ?h ?a ?b => | ||
| 607 | Sh (k' + 3) a' Qe' (filter (fun p => k' <? p) P). | ||
| 375 | eapply (sideRLs_change_ends tm h a _ b _); | ||
| 376 | [ unfold_to_side_one_step; reflexivity | ||
| ⋯ 11 template-only lines (template 377–390), not in ours | |||
| 392 | Lemma sideRLs_D_Bo0_1 : | ||
| 393 | sideRLs (flip tm) [((D, []), (B, []))] (to_side (SBo 0 0 1)) (to_side (SPo 0 3)). | ||
| 394 | Proof. | 608 | Proof. |
| 395 | cbn [to_side]. | ||
| 609 | intros HQi Hn E H1 H2. rewrite (filter_lt_app _ _ _ HQi) in H1. | ||
| 396 | unfold Bo, Po, Bside, Pside, SkelO, SkelE. | ||
| 610 | pose proof (Sh_filter _ _ _ _ k k' H2 E) as H3. rewrite (filter_filter_lt P n k' Hn) in H3. | ||
| 397 | cbn. | ||
| 611 | apply (Sh_trans _ _ _ _ _ _ a _ _ _ H1 H3); lia. | ||
| 398 | esc. | ||
| 399 | Qed. | 612 | Qed. |
| 401 | Lemma sideRLs_D_Bo0_5 : | ||
| 614 | (* ---------- the orbit invariant and the absorption law (proof.md section 3) ---------- *) | ||
| 402 | sideRLs (flip tm) [((D, []), (D, []))] (to_side (SBo 0 0 5)) (to_side (SPe 1 0)). | ||
| 615 | (* Core P k a b Q: the marker tail Q of a T(a,b)/S(a,b) word splits into Qi (internal | ||
| 616 | markers within reach, plus the one being absorbed when k is in P) and Qe (the | ||
| 617 | unabsorbed original markers of P, at their exact shifted positions). *) | ||
| 618 | Definition Core (P : list nat) (k a b : nat) (Q : list nat) : Prop := | ||
| 619 | valid Q /\ 2 <= a /\ exists Qi Qe, Q = Qi ++ Qe /\ length Qi + a = b + 1 + ind P k /\ | ||
| 620 | Forall (fun q => q + 2 + ind P k <= a) Qi /\ Sh (k + 3) a Qe (filter (fun p => k <? p) P). | ||
| 622 | (* Inv(M,n), with alpha = cnt P n; T-word when n+alpha is odd, S-word when even *) | ||
| 623 | Definition Inv (P : list nat) (n : nat) (W : list nat) : Prop := | ||
| 624 | (Nat.Odd (n + cnt P n) /\ exists a Q, W = a :: 2 :: (n + cnt P n) :: mw Q /\ | ||
| 625 | Core P n a (n + cnt P n) Q) \/ | ||
| 626 | (Nat.Even (n + cnt P n) /\ exists a Q, W = 2 :: 2 :: a :: 2 :: (n + cnt P n - 1) :: mw Q /\ | ||
| 627 | Core P (S n) a (n + cnt P n - 1) Q). | ||
| 629 | Definition Claim (Lm : nat) : Prop := | ||
| 630 | forall Q k, k + length Q <= Lm -> valid Q -> exists W, Orb Q k W /\ (1 <= k -> Inv Q k W). | ||
| 632 | Lemma stepU P : valid P -> exists W', Ep (1 :: mw P) (cost P 0) W' /\ Inv P 1 W'. | ||
| 403 | Proof. | 633 | Proof. |
| 404 | cbn [to_side]. | ||
| 634 | intros HV0. assert (Hc : cost P 0 = 2). | ||
| 405 | unfold Bo, Pe, Bside, Pside, SkelO, SkelE. | ||
| 635 | { unfold cost, ind. rewrite (cnt1_valid P HV0), cnt_0. reflexivity. } | ||
| 406 | cbn. | ||
| 636 | rewrite Hc. unfold Inv. rewrite (cnt1_valid P HV0). | ||
| 407 | esc. | ||
| 637 | destruct P as [|p P']. | ||
| 638 | - exists [2;2;1]. split; [apply U0|]. left. split; [exists 0; reflexivity|]. | ||
| 639 | exists 2, (@nil nat). split; [reflexivity|]. split; [exact I|]. split; [lia|]. exists (@nil nat), (@nil nat). | ||
| 640 | split; [reflexivity|]. split; [reflexivity|]. split; constructor. | ||
| 641 | - pose proof HV0 as HV. destruct HV as [[t Ht] HV']. pose proof (valid_gt _ _ HV') as Hg. | ||
| 642 | destruct t as [|t]. | ||
| 643 | + replace p with 1 in * by lia. | ||
| 644 | exists (3 :: 2 :: 1 :: mwf 1 P'). split. | ||
| 645 | { apply (U2 0 (mwf 1 P')). apply valid_tail_ok. exact HV'. } | ||
| 646 | left. split; [exists 0; reflexivity|]. | ||
| 647 | exists 3, (map (fun p => p - 1) P'). split. | ||
| 648 | { unfold mw. rewrite <- (mwf_unshift 1 1 P'); [reflexivity | lia |]. | ||
| 649 | eapply Forall_impl; [|exact Hg]. cbn; intros; lia. } | ||
| 650 | split; [apply (valid_unshift 0 1 P' HV')|]. split; [lia|]. | ||
| 651 | exists (@nil nat), (map (fun p => p - 1) P'). split; [reflexivity|]. | ||
| 652 | rewrite (ind_in (1 :: P') 1 HV0 (or_introl eq_refl)). | ||
| 653 | split; [reflexivity|]. split; [constructor|]. | ||
| 654 | cbn [filter]. change (1 <? 1) with false. cbv iota. | ||
| 655 | rewrite (filter_all P' 1 Hg). | ||
| 656 | apply (Sh_unmap 3 1 P'). eapply Forall_impl; [|exact Hg]. cbn; intros; lia. | ||
| 657 | + exists (2 :: 2 :: 1 :: S (S (2 * t)) :: 1 :: mwf p P'). split. | ||
| 658 | { change (mw (p :: P')) with ((p - 0 + 1) :: 1 :: mwf p P'). | ||
| 659 | replace (p - 0 + 1) with (S (S (S (S (2 * t))))) by lia. apply U1. } | ||
| 660 | left. split; [exists 0; reflexivity|]. | ||
| 661 | exists 2, (map (fun q => q - 2) (p :: P')). split. | ||
| 662 | { unfold mw. cbn [map mwf]. rewrite (mwf_unshift p 2 P'); [| lia |]. | ||
| 663 | - do 4 f_equal. lia. | ||
| 664 | - eapply Forall_impl; [|exact Hg]. cbn; intros; lia. } | ||
| 665 | split. | ||
| 666 | { apply (valid_unshift 0 2 (p :: P')). cbn [valid_from]. split; [exists t; lia | exact HV']. } | ||
| 667 | split; [lia|]. | ||
| 668 | exists (@nil nat), (map (fun q => q - 2) (p :: P')). split; [reflexivity|]. | ||
| 669 | assert (Hn1 : ~ In 1 (p :: P')). | ||
| 670 | { intros [H|H]; [lia|]. rewrite Forall_forall in Hg. specialize (Hg _ H). lia. } | ||
| 671 | rewrite (ind_nin _ _ Hn1). split; [reflexivity|]. split; [constructor|]. | ||
| 672 | rewrite filter_all. | ||
| 673 | * apply (Sh_unmap 2 2 (p :: P')). constructor; [lia|]. | ||
| 674 | eapply Forall_impl; [|exact Hg]. cbn; intros; lia. | ||
| 675 | * constructor; [lia|]. eapply Forall_impl; [|exact Hg]. cbn; intros; lia. | ||
| 408 | Qed. | 676 | Qed. |
| 410 | Lemma sideRLs_E_keep_1 r : | ||
| 678 | Lemma stepS P n a Q : valid P -> 1 <= n -> Nat.Even (n + cnt P n) -> | ||
| 411 | sideRLs (flip tm) [((E, []), (F, []))] (S1 >> r) (S1 >> r). | ||
| 679 | Core P (S n) a (n + cnt P n - 1) Q -> | ||
| 680 | exists W', Ep (2 :: 2 :: a :: 2 :: (n + cnt P n - 1) :: mw Q) (cost P n) W' /\ Inv P (S n) W'. | ||
| 412 | Proof. | 681 | Proof. |
| 413 | esx. | ||
| 682 | intros HV Hn [e He] (HVQ & Ha & Qi & Qe & -> & Hlen & Hfa & Hsh). | ||
| 683 | assert (Hnin : ~ In n P). | ||
| 684 | { intro Hin. destruct (parity_in 0 P n HV Hin) as [u Hu]. lia. } | ||
| 685 | assert (HcS : cnt P (S n) = cnt P n) by (apply cnt_S_nin; exact Hnin). | ||
| 686 | assert (Hcost : cost P n = 2) by (unfold cost, ind; lia). | ||
| 687 | rewrite Hcost. | ||
| 688 | assert (Ha3 : 2 + ind P (S n) <= a). | ||
| 689 | { destruct Qi as [|q Qi']. | ||
| 690 | - cbn [length] in Hlen. lia. | ||
| 691 | - pose proof (valid_app_l _ _ HVQ) as Hq1. inversion Hq1; subst. inversion Hfa; subst. lia. } | ||
| 692 | destruct a as [|a']; [lia|]. | ||
| 693 | destruct (n + cnt P n - 1) as [|b'] eqn:Hb; [lia|]. | ||
| 694 | exists (S (S a') :: 2 :: S (S (S b')) :: 2 :: 1 :: mw (Qi ++ Qe)). split. | ||
| 695 | { apply ruleS. apply mw_tail_ok. exact HVQ. } | ||
| 696 | left. split. | ||
| 697 | { exists e. rewrite HcS. lia. } | ||
| 698 | exists (S (S a')), (1 :: map (fun q => q + 1) (Qi ++ Qe)). split. | ||
| 699 | { rewrite mw_cons1. rewrite HcS. do 3 f_equal. lia. } | ||
| 700 | split; [apply valid_cons1; exact HVQ|]. split; [lia|]. | ||
| 701 | exists (1 :: map (fun q => q + 1) Qi), (map (fun q => q + 1) Qe). | ||
| 702 | split; [rewrite map_app; reflexivity|]. | ||
| 703 | split; [cbn [length]; rewrite length_map; rewrite HcS; lia|]. | ||
| 704 | split. | ||
| 705 | { constructor; [lia|]. apply Forall_map. eapply Forall_impl; [|exact Hfa]. cbn; intros; lia. } | ||
| 706 | eapply Sh_eq; [apply Sh_map with (d := 1); exact Hsh | reflexivity | lia]. | ||
| 414 | Qed. | 707 | Qed. |
| 416 | Lemma sideRLs_F_0_to_1 r : | ||
| 709 | Lemma stepT_nabs Lm P n a Q : Claim Lm -> valid P -> 1 <= n -> n + length P <= Lm -> | ||
| 417 | sideRLs (flip tm) [((F, []), (E, []))] (S0 >> r) (S1 >> r). | ||
| 710 | Nat.Odd (n + cnt P n) -> ~ In n P -> Core P n a (n + cnt P n) Q -> | ||
| 711 | exists W', Ep (a :: 2 :: (n + cnt P n) :: mw Q) (cost P n) W' /\ Inv P (S n) W'. | ||
| 418 | Proof. | 712 | Proof. |
| 419 | esx. | ||
| 713 | intros IH HV Hn HL [e He] Hnin (HVQ & Ha & Qi & Qe & -> & Hlen & Hfa & Hsh). | ||
| 714 | assert (HcS : cnt P (S n) = cnt P n) by (apply cnt_S_nin; exact Hnin). | ||
| 715 | assert (Hi0 : ind P n = 0) by (apply ind_nin; exact Hnin). | ||
| 716 | rewrite Hi0 in Hlen, Hfa. | ||
| 717 | assert (Hcost : cost P n = 2) by (unfold cost; lia). rewrite Hcost. | ||
| 718 | assert (Hnin1 : ~ In (S n) P). | ||
| 719 | { intro Hin. destruct (parity_in 0 P (S n) HV Hin) as [u Hu]. lia. } | ||
| 720 | assert (HQe : Forall (fun q => a - 1 <= q) Qe). | ||
| 721 | { apply (Sh_ge _ _ _ _ (a - 1) (S (S n)) Hsh); [|lia]. | ||
| 722 | intros p Hp. pose proof (filter_gt _ _ _ Hp) as H1. apply filter_In in Hp. destruct Hp as [Hp _]. | ||
| 723 | assert (p <> S n) by (intros ->; contradiction). lia. } | ||
| 724 | assert (HQi : Forall (fun q => q < a - 1) Qi) by (eapply Forall_impl; [|exact Hfa]; cbn; intros; lia). | ||
| 725 | assert (HcQ : cnt (Qi ++ Qe) (a - 1) = length Qi). | ||
| 726 | { rewrite cnt_app, (cnt_all_lt _ _ HQi), (cnt_all_ge _ _ HQe). lia. } | ||
| 727 | pose proof (filter_cnt_len P n) as HlP. pose proof (Sh_len _ _ _ _ Hsh) as HlQe. | ||
| 728 | destruct (IH (Qi ++ Qe) (a - 1)) as (W1 & HO1 & HI1). | ||
| 729 | { rewrite length_app. lia. } | ||
| 730 | { exact HVQ. } | ||
| 731 | specialize (HI1 ltac:(lia)). | ||
| 732 | unfold Inv in HI1. rewrite HcQ in HI1. | ||
| 733 | destruct HI1 as [[_ (a' & Q' & -> & HC')] | [[e' He'] _]]; [| exfalso; lia]. | ||
| 734 | assert (Hb : a - 1 + length Qi = n + cnt P n) by lia. | ||
| 735 | rewrite Hb in *. | ||
| 736 | exists (2 :: 2 :: a' :: 2 :: (n + cnt P n) :: mw Q'). split. | ||
| 737 | { pose proof (ruleT a (n + cnt P n) (Qi ++ Qe) _ HO1 Ha ltac:(lia) HVQ ltac:(lia)) as HT. | ||
| 738 | rewrite HcQ in HT. replace (n + cnt P n + 3 - a - length Qi) with 2 in HT by lia. exact HT. } | ||
| 739 | right. split. | ||
| 740 | { exists (e + 1). rewrite HcS. lia. } | ||
| 741 | exists a', Q'. split. | ||
| 742 | { rewrite HcS. do 5 f_equal. lia. } | ||
| 743 | replace (S n + cnt P (S n) - 1) with (n + cnt P n) by lia. | ||
| 744 | destruct HC' as (HVQ' & Ha' & Qi' & Qe' & -> & Hlen' & Hfa' & Hsh'). | ||
| 745 | assert (Hind : ind (Qi ++ Qe) (a - 1) = ind P (S (S n))). | ||
| 746 | { apply ind_iff; [exact HVQ | exact HV | ]. | ||
| 747 | apply (in_transfer Qi Qe P (a - 1) (S (S n)) (n + 3) a n HQi Hsh); lia. } | ||
| 748 | split; [exact HVQ'|]. split; [exact Ha'|]. | ||
| 749 | exists Qi', Qe'. split; [reflexivity|]. rewrite <- Hind. split; [lia|]. split; [exact Hfa'|]. | ||
| 750 | apply (sh_compose Qi Qe Qe' P n a a' (a - 1) (S (S n))); try assumption; try lia. | ||
| 751 | eapply Forall_impl; [|exact HQi]. cbn; intros; lia. | ||
| 420 | Qed. | 752 | Qed. |
| 422 | Opaque SkelE SkelO Pside Bside Aside Pe Po Be Bo Ae Ao K0 K1. | ||
| 754 | Lemma stepT_abs Lm P n a Q : Claim Lm -> valid P -> 1 <= n -> n + length P <= Lm -> | ||
| 424 | Inductive ClosedCall : Q -> Side -> Q -> Side -> Prop := | ||
| 755 | Nat.Odd (n + cnt P n) -> In n P -> Core P n a (n + cnt P n) Q -> | ||
| 425 | | CC_C_Ao_zero n q : | ||
| 756 | exists W', Ep (a :: 2 :: (n + cnt P n) :: mw Q) (cost P n) W' /\ Inv P (S n) W'. | ||
| 426 | q <= n -> | ||
| 427 | ClosedCall C (SAo n q 0) F (SAe n q (7 + 4 * n)) | ||
| ⋯ 432 template-only lines (template 428–877), not in ours | |||
| 878 | ClosedCall q s q' s' -> | ||
| 879 | sideRLs (flip tm) [((q, []), (q', []))] (to_side s) (to_side s'). | ||
| 880 | Proof. | 757 | Proof. |
| 881 | enough | ||
| 758 | intros IH HV Hn HL [e He] Hin (HVQ & Ha & Qi & Qe & -> & Hlen & Hfa & Hsh). | ||
| 882 | (Hind : forall m q0 s0 q1 s1, | ||
| 759 | assert (HcS : cnt P (S n) = S (cnt P n)) by (apply (cnt_S_in 0); assumption). | ||
| 883 | measure q0 s0 = m -> | ||
| 760 | assert (Hi1 : ind P n = 1) by (apply ind_in; assumption). | ||
| 884 | ClosedCall q0 s0 q1 s1 -> | ||
| 761 | rewrite Hi1 in Hlen, Hfa. | ||
| 885 | sideRLs (flip tm) [((q0, []), (q1, []))] (to_side s0) (to_side s1)). | ||
| 762 | assert (Hcost : cost P n = 3) by (unfold cost; lia). rewrite Hcost. | ||
| 886 | { intro Hcall. | ||
| 763 | assert (Ha3 : 3 <= a). | ||
| 887 | eapply Hind. | ||
| 764 | { destruct Qi as [|q Qi']. | ||
| 888 | - reflexivity. | ||
| 765 | - cbn [length] in Hlen. lia. | ||
| 889 | - exact Hcall. | ||
| 766 | - pose proof (valid_app_l _ _ HVQ) as Hq1. inversion Hq1; subst. inversion Hfa; subst. lia. } | ||
| 890 | } | ||
| 767 | assert (HQe : Forall (fun q => a - 2 <= q) Qe). | ||
| 891 | intro m. | ||
| 768 | { apply (Sh_ge _ _ _ _ (a - 2) (S n) Hsh); [|lia]. | ||
| 892 | induction m as [m IH] using lt_wf_ind. | ||
| 769 | intros p Hp. apply filter_gt in Hp. lia. } | ||
| 893 | intros q0 s0 q1 s1 Hm Hcall. | ||
| 770 | assert (HQi : Forall (fun q => q < a - 2) Qi) by (eapply Forall_impl; [|exact Hfa]; cbn; intros; lia). | ||
| 894 | subst m. | ||
| 771 | assert (HcQ : cnt (Qi ++ Qe) (a - 2) = length Qi). | ||
| 895 | inversion Hcall; subst. | ||
| 772 | { rewrite cnt_app, (cnt_all_lt _ _ HQi), (cnt_all_ge _ _ HQe). lia. } | ||
| 896 | - replace (7 + 4 * n) with (S (6 + 4 * n)) by flia. | ||
| 773 | pose proof (filter_cnt_len P n) as HlP. pose proof (Sh_len _ _ _ _ Hsh) as HlQe. | ||
| 897 | normalize_split_sideRLs_concat. | ||
| 774 | destruct (IH (Qi ++ Qe) (a - 2)) as (W2 & HO2 & HI2). | ||
| 898 | { | ||
| 775 | { rewrite length_app. lia. } | ||
| 899 | eapply sideRLs_trans. | ||
| 776 | { exact HVQ. } | ||
| 900 | { eapply (IH (measure E (SBo n 0 (4 * q2 + 2)))). | ||
| 777 | specialize (HI2 ltac:(lia)). | ||
| 901 | { unfold measure, side_measure, class_rank, skelO_measure. | ||
| 778 | unfold Inv in HI2. rewrite HcQ in HI2. | ||
| 902 | cbn [skelE_measure skelO_measure]. | ||
| 779 | destruct HI2 as [[_ (a'' & Q'' & -> & HC'')] | [[e' He'] _]]; [| exfalso; lia]. | ||
| 903 | flia. } | ||
| 780 | assert (Hb : a - 2 + length Qi = n + cnt P n) by lia. | ||
| 904 | { reflexivity. } | ||
| 781 | rewrite Hb in *. | ||
| 905 | { applys_eq (CC_E_Bo n q2); flia. } } | ||
| 782 | destruct HC'' as (HVQ'' & Ha'' & Qi'' & Qe'' & -> & Hlen'' & Hfa'' & Hsh''). | ||
| 906 | destruct q2 as [| q0]. | ||
| 783 | exists (S (S a'') :: 2 :: S (S (n + cnt P n)) :: mw (map (fun q => q + 2) (Qi'' ++ Qe''))). split. | ||
| 907 | { eapply sideRLs_trans. | ||
| 784 | { apply ruleX; try assumption; lia. } | ||
| 908 | { eapply (IH (measure F (SBo n 0 2))). | ||
| 785 | left. split. | ||
| 909 | { unfold measure, side_measure, class_rank, skelO_measure. | ||
| 786 | { exists (e + 1). rewrite HcS. lia. } | ||
| 910 | cbn [skelE_measure skelO_measure]. | ||
| 787 | exists (S (S a'')), (map (fun q => q + 2) (Qi'' ++ Qe'')). split. | ||
| 911 | flia. } | ||
| 788 | { rewrite HcS. do 3 f_equal. lia. } | ||
| 912 | { reflexivity. } | ||
| 789 | replace (S n + cnt P (S n)) with (S (S (n + cnt P n))) by lia. | ||
| 913 | { apply CC_F_Bo_small2. } } | ||
| 790 | assert (Hind : ind (Qi ++ Qe) (a - 2) = ind P (S n)). | ||
| 914 | eapply (IH (measure C (SPo n 3))). | ||
| 791 | { apply ind_iff; [exact HVQ | exact HV | ]. | ||
| 915 | { unfold measure, side_measure, class_rank, skelO_measure. | ||
| 792 | apply (in_transfer Qi Qe P (a - 2) (S n) (n + 3) a n HQi Hsh); lia. } | ||
| 916 | cbn [skelE_measure skelO_measure]. | ||
| 793 | split; [apply valid_map2; exact HVQ''|]. split; [lia|]. | ||
| 917 | flia. } | ||
| 794 | exists (map (fun q => q + 2) Qi''), (map (fun q => q + 2) Qe''). split; [apply map_app|]. | ||
| 918 | { flia. } | ||
| 795 | rewrite length_map. rewrite <- Hind. split; [lia|]. split. | ||
| 919 | { applys_eq (CC_C_Po_odd n 1); flia. } } | ||
| 796 | { apply Forall_map. eapply Forall_impl; [|exact Hfa'']. cbn; intros; lia. } | ||
| 920 | { eapply sideRLs_trans. | ||
| 797 | assert (Hc : Sh (S n + 3) a'' Qe'' (filter (fun p => S n <? p) P)). | ||
| 921 | { eapply (IH (measure F (SBo n 0 (4 * q0 + 6)))). | ||
| 798 | { apply (sh_compose Qi Qe Qe'' P n a a'' (a - 2) (S n)); try assumption; try lia. | ||
| 922 | { unfold measure, side_measure, class_rank, skelO_measure. | ||
| 799 | eapply Forall_impl; [|exact HQi]. cbn; intros; lia. } | ||
| 923 | cbn [skelE_measure skelO_measure]. | ||
| 800 | eapply Sh_eq; [apply Sh_map with (d := 2); exact Hc | reflexivity | lia]. | ||
| 924 | flia. } | ||
| 925 | { flia. } | ||
| ⋯ 1459 template-only lines (template 926–2384), not in ours | |||
| 2385 | Unshelve. | ||
| 2386 | all: esc. | ||
| 2387 | Qed. | 801 | Qed. |
| 2390 | Lemma ClosedCall_progress q s q' s' : | ||
| 803 | Lemma step_lemma Lm : Claim Lm -> forall P n W, n + length P <= Lm -> valid P -> Orb P n W -> | ||
| 2391 | ClosedCall q s q' s' -> | ||
| 804 | (1 <= n -> Inv P n W) -> exists W', Ep W (cost P n) W' /\ Inv P (S n) W'. | ||
| 2392 | to_side s {{{ ((q, []), L) }}} const S0 -[ tm ]->+ | ||
| 2393 | to_side s' {{{ ((q', []), R) }}} const S0. | ||
| 2394 | Proof. | 805 | Proof. |
| 2395 | intro H. | ||
| 806 | intros IH P n W HL HV HO HI. destruct n as [|n']. | ||
| 2396 | eapply sideRLs_1L. | ||
| 807 | - inversion HO; subst. apply stepU; exact HV. | ||
| 2397 | apply ClosedCall_sideRLs. | ||
| 808 | - specialize (HI ltac:(lia)). | ||
| 2398 | exact H. | ||
| 809 | destruct HI as [[Ho (a & Q & -> & HC)] | [He (a & Q & -> & HC)]]. | ||
| 810 | + destruct (in_dec Nat.eq_dec (S n') P) as [Hin | Hnin]. | ||
| 811 | * eapply stepT_abs; eauto; lia. | ||
| 812 | * eapply stepT_nabs; eauto; lia. | ||
| 813 | + eapply stepS; eauto; lia. | ||
| 2399 | Qed. | 814 | Qed. |
| 2401 | Lemma ClosedCall_progress_any q s q' s' r : | ||
| 816 | Theorem main Lm : Claim Lm. | ||
| 2402 | ClosedCall q s q' s' -> | ||
| 2403 | to_side s {{{ ((q, []), L) }}} r -[ tm ]->+ | ||
| 2404 | to_side s' {{{ ((q', []), R) }}} r. | ||
| 2405 | Proof. | 817 | Proof. |
| 2406 | intro H. | ||
| 818 | induction Lm as [|Lm IHL]; intros Q k Hk HV. | ||
| 2407 | eapply sideRLs_1L. | ||
| 819 | - assert (k = 0) by lia. subst. exists (1 :: mw Q). split; [constructor | lia]. | ||
| 2408 | apply ClosedCall_sideRLs. | ||
| 820 | - destruct k as [|k]. | ||
| 2409 | exact H. | ||
| 821 | + exists (1 :: mw Q). split; [constructor | lia]. | ||
| 822 | + destruct (IHL Q k ltac:(lia) HV) as (W & HO & HI). | ||
| 823 | destruct (step_lemma Lm IHL Q k W ltac:(lia) HV HO HI) as (W' & HE & HI'). | ||
| 824 | exists W'. split; [econstructor; eauto | intros; exact HI']. | ||
| 2410 | Qed. | 825 | Qed. |
| 2412 | Lemma ClosedCall_evstep_any q s q' s' r : | ||
| 827 | (* ---------- top level ---------- *) | ||
| 2413 | ClosedCall q s q' s' -> | ||
| 828 | Lemma init : c0 -->* conf [] [3; 2; 1]. | ||
| 2414 | to_side s {{{ ((q, []), L) }}} r -[ tm ]->* | ||
| 829 | Proof. unfold conf, lside, rside. cbn [lpow app]. solve_init. Qed. | ||
| 2415 | to_side s' {{{ ((q', []), R) }}} r. | ||
| 831 | Lemma nonhalt: ~halts tm c0. | ||
| 2416 | Proof. | 832 | Proof. |
| 2417 | intro H. | ||
| 833 | eapply multistep_nonhalt; [apply init |]. | ||
| 2418 | apply progress_evstep. | ||
| 834 | apply (progress_nonhalt_cond tm (nat * list nat) (0, [1]) (fun i => conf [] (3 :: 2 :: snd i)) | ||
| 2419 | apply ClosedCall_progress_any. | ||
| 835 | (fun i => Orb [] (fst i) (snd i) /\ (1 <= fst i -> Inv [] (fst i) (snd i)))). | ||
| 2420 | exact H. | ||
| 836 | - intros [n W] [HO HI]. cbn [fst snd] in *. | ||
| 837 | destruct (step_lemma n (main n) [] n W ltac:(cbn; lia) I HO HI) as (W' & HE & HI'). | ||
| 838 | exists (S n, W'). cbn [fst snd]. split. | ||
| 839 | + apply Ep_tm in HE. replace (cost [] n) with 2 in HE by reflexivity. exact HE. | ||
| 840 | + split; [econstructor; eauto | intros; exact HI']. | ||
| 841 | - cbn [fst snd]. split; [exact (O0 []) | lia]. | ||
| 2421 | Qed. | 842 | Qed. |
| 2423 | Definition Bcfg (h : Side) : Q * tape := | ||
| 845 | (* | ||
| 2424 | to_side h {{{ ((B, []), R) }}} const S0. | ||
| 846 | ``` | ||
| 2426 | Lemma B_to_C h : | ||
| 847 | 1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF | ||
| 2427 | Bcfg h -[ tm ]->+ to_side h {{{ ((C, []), L) }}} (S1 >> const S0). | ||
| 849 | conf L R := 0^inf 1^a_1 0 1^a_2 0 .. 0 1^a_p <A 0 1^c_1 0^g_1 1^c_2 .. 1^c_r 0^inf | ||
| 2428 | Proof. | ||
| 850 | (L = [a_p; ..; a_1] top first, R = [c_1; g_1; c_2; ..; c_r]) | ||
| 2429 | unfold Bcfg, tm. | ||
| 851 | tR1 l 1^(n+2) <A 0 1^(m+1) 0 0 1^x 0 r -->+ l 1^(n+1) 0 1^(m+1) <A 0 1^(x+1) 0 0 r | ||
| 2430 | step1s. | ||
| 852 | tR3 l 0 <A 0 1^(k+1) 0 0 1^m 0 r -->+ l 1^(k+2) <A 0 1^(m+1) 0 0 r | ||
| 2431 | Qed. | ||
| 853 | tR2 l 0 1^(k+1) 0 1 <A 0 r -->+ l <A 0 1^(k+2) 0 0 r | ||
| 2433 | Lemma Btail_E_to_B l : | ||
| 854 | push conf (x::L) (h::R') -->+ conf (h::x-1::L) (updt R') x >= 2 (tR1) | ||
| 2434 | l {{{ ((E, []), R) }}} (S1 >> const S0) -[ tm ]->+ | ||
| 855 | push0 conf [] (h::R') -->+ conf [h+1] (updt R') (tR3) | ||
| 2435 | S1 >> S1 >> S1 >> S1 >> l {{{ ((B, []), R) }}} const S0. | ||
| 856 | pop conf (1::y::L) R -->+ conf L (y+1::2::R) y >= 1 (tR2) | ||
| 2436 | Proof. | ||
| 857 | updt [] = [1], updt [2;c] = [c+1], updt (2::c::g::R) = c+1::g+1::R, updt (g::R) = 1::g-1::R (g >= 3) | ||
| 2437 | unfold tm. | ||
| 859 | Edge W := conf [] (3::2::W); Ep W c W' : Edge W -->+ conf [] (5-c::2::W') | ||
| 2438 | step1s. | ||
| 860 | U0 Ep [1] = (2, [2;2;1]) | ||
| 2439 | Qed. | ||
| 861 | U1 Ep (1::g::rest) = (2, 2::2::1::g-2::rest) g >= 4 | ||
| 2441 | Lemma boundary_A0 l : | ||
| 862 | U2 Ep (1::2::b::N) = (2, b+2::2::1::N) b >= 1 | ||
| 2442 | l {{{ ((A, []), R) }}} const S0 -[ tm ]->+ | ||
| 863 | S Ep (2::2::a::2::b::N) = (2, a+1::2::b+2::2::1::N) a, b >= 1 | ||
| 2443 | S1 >> l {{{ ((B, []), R) }}} const S0. | ||
| 864 | T Ep (a::2::b::mw Q) = (2, b+3-a-#{q<a-1}::2::O_(a-1)(Q)) a-1+#{q<a-1} <= b | ||
| 2444 | Proof. | ||
| 865 | X Ep (a::2::b::mw Q) = (3, a''+2::2::b+2::mw (Q''+2)) O_(a-2)(Q) = a''::2::b::mw Q'', | ||
| 2445 | unfold tm. | ||
| 866 | b = a-2+#{q<a-2} | ||
| 2446 | step1s. | ||
| 867 | mw [I_1;..;I_m] = (I_1+1) 1 (I_2-I_1+1) 1 .. (marker word from its absorption indices) | ||
| 2447 | Qed. | ||
| 868 | O_0(Q) = 1::mw Q, O_(n+1)(Q) = Ep(O_n(Q)) at cost 2+[n in Q] (Orb) | ||
| 2449 | Lemma boundary_E0 l : | ||
| 869 | Inv P n: al = #{p in P | p < n}; n+al odd: O_n(P) = T(a, n+al)+mw Q, k = n | ||
| 2450 | l {{{ ((E, []), R) }}} const S0 -[ tm ]->+ | ||
| 870 | n+al even: O_n(P) = S(a, n+al-1)+mw Q, k = n+1 | ||
| 2451 | S1 >> l {{{ ((A, []), R) }}} const S0. | ||
| 871 | Q = Qi ++ Qe, |Qi| = b+1-a+[k in P], every q in Qi <= a-2-[k in P], | ||
| 2452 | Proof. | ||
| 872 | Qe = the indices of P above k, each shifted by a-k-3 | ||
| 2453 | unfold tm. | ||
| 873 | start: c0 -->* Edge [1] = Edge (O_0([])) (50 steps) | ||
| 2454 | step1s. | ||
| 874 | top: O_n([]) has no markers, so Edge (O_n([])) -->+ Edge (O_(n+1)([])) for every n | ||
| 2455 | Qed. | ||
| 875 | ``` | ||
| 2457 | Lemma boundary_F0 l : | ||
| 876 | *) | ||
| 2458 | l {{{ ((F, []), R) }}} const S0 -[ tm ]->+ | ||
| 2459 | S1 >> l {{{ ((E, []), R) }}} const S0. | ||
| ⋯ 660 template-only lines (template 2460–3157), not in ours | |||
| 3158 | + apply GoodB_start. | ||
| 3159 | Qed. | ||
3Proof outlineCheck: the new items (green) carry the argument; the names read like the proof.md rules.
105 items in 1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF.v (876 lines): 80 Lemma, 16 Definition, 5 Fixpoint, 3 Inductive, 1 Theorem. Tags against the template: identical = same name and same text once each file's own TM string is <TM> (marked "except the TM string" when that is the only difference); adapted = same name, different text; new = no item of that name in the template part.
| # | kind | name | statement (no proof body) | line | vs template |
|---|---|---|---|---|---|
| 1 | Definition | tm | Definition tm := Eval compute in (TM_from_str "1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF"). | L22 | identicalexcept the TM string |
| 2 | Lemma | tR1 | Lemma tR1 n m x l r :
l <* [1]^^(S (S n)) <{{A}} [0] *> [1]^^(S m) *> [0;0] *> [1]^^x *> [0] *> r -->+
l <* [1]^^(S n) <* [0] <* [1]^^(S m) <{{A}} [0] *> [1]^^(S x) *> [0;0] *> r. | L31 | new |
| 3 | Lemma | tR3 | Lemma tR3 k m l r :
l <* [0] <{{A}} [0] *> [1]^^(S k) *> [0;0] *> [1]^^m *> [0] *> r -->+
l <* [1]^^(S (S k)) <{{A}} [0] *> [1]^^(S m) *> [0;0] *> r. | L37 | new |
| 4 | Lemma | tR2 | Lemma tR2 k l r :
l <* [0] <* [1]^^(S k) <* [0] <* [1] <{{A}} [0] *> r -->+
l <{{A}} [0] *> [1]^^(S (S k)) *> [0;0] *> r. | L43 | new |
| 5 | Lemma | tR3c | Lemma tR3c k m r :
const 0 <{{A}} [0] *> [1]^^(S k) *> [0;0] *> [1]^^m *> [0] *> r -->+
const 0 <* [1]^^(S (S k)) <{{A}} [0] *> [1]^^(S m) *> [0;0] *> r. | L48 | new |
| 6 | Fixpoint | lsep | Fixpoint lsep (L : list nat) : side := match L with | [] => const 0 | y :: L' => lsep L' <* [1]^^y <* [0] end. | L54 | new |
| 7 | Definition | lside | Definition lside (L : list nat) : side := match L with | [] => const 0 | x :: L' => lsep L' <* [1]^^x end. | L60 | new |
| 8 | Fixpoint | rside | Fixpoint rside (R : list nat) : side := match R with | [] => const 0 | [c] => [1]^^c *> const 0 | c :: g :: R' => [1]^^c *> [0]^^g *> rside R' end. | L66 | new |
| 9 | Definition | conf | Definition conf (L R : list nat) : Q * tape := lside L <{{A}} [0] *> rside R. | L73 | new |
| 10 | Lemma | c0_1 | Lemma c0_1 : 0 >> const 0 = const 0. | L75 | new |
| 11 | Lemma | lsep_eq | Lemma lsep_eq L : lsep L = lside L <* [0]. | L78 | new |
| 12 | Definition | updt | Definition updt (R' : list nat) : option (list nat) := match R' with | [] => Some [1] | g :: R'' => match g with | 0 | 1 => None … +11 lines | L86 | new |
| 13 | Lemma | updt_shape | Lemma updt_shape m R' R1 : updt R' = Some R1 ->
exists x r, rside (S m :: R') = [S1]^^(S m) *> [S0;S0] *> [S1]^^x *> [S0] *> r /\
rside R1 = [S1]^^(S x) *> [S0;S0] *> r. | L104 | new |
| 14 | Lemma | push_ok | Lemma push_ok y h R' R1 L : updt R' = Some R1 -> 1 <= y -> 1 <= h -> conf (S y :: L) (h :: R') -->+ conf (h :: y :: L) R1. | L118 | new |
| 15 | Lemma | push0_ok | Lemma push0_ok h R' R1 : updt R' = Some R1 -> 1 <= h -> conf [] (h :: R') -->+ conf [S h] R1. | L128 | new |
| 16 | Lemma | pop_ok | Lemma pop_ok y L R : 1 <= y -> conf (1 :: y :: L) R -->+ conf L (S y :: 2 :: R). | L138 | new |
| 17 | Inductive | outcome | Inductive outcome := Fin (R : list nat) | Pop (c : nat) (R : list nat). | L148 | new |
| 18 | Inductive | Life | Inductive Life : nat -> list nat -> outcome -> Prop :=
| L_fin R : Life 1 R (Fin R)
| L_cf y h R' R1 Rc : 1 <= y -> updt R' = Some R1 -> Life h R1 (Fin Rc) ->
Life (S y) (h :: R') (Pop 1 (S y :: 2 :: Rc))
| L_cpf y h R' R1 c' R2 Rf : 1 <= y -> updt R' = Some R1 -> Life h R1 (Pop c' R2) ->
Life y R2 (Fin Rf) -> Life (S y) (h :: R') (Fin Rf)
… +2 lines | L154 | new |
| 19 | Lemma | Life_pos | Lemma Life_pos x R o : Life x R o -> 1 <= x. | L163 | new |
| 20 | Lemma | Life_tm | Lemma Life_tm x R o : Life x R o -> forall L, match o with | Fin Rf => conf (x :: L) R -->* conf (1 :: L) Rf | Pop _ Rf => conf (x :: L) R -->+ conf L Rf end. | L166 | new |
| 21 | Definition | Ep | Definition Ep (W : list nat) (c : nat) (W' : list nat) : Prop := exists R0, updt (2 :: W) = Some R0 /\ Life 4 R0 (Pop c ((5 - c) :: 2 :: W')). | L189 | new |
| 22 | Lemma | Ep_tm | Lemma Ep_tm W c W' : Ep W c W' -> conf [] (3 :: 2 :: W) -->+ conf [] ((5 - c) :: 2 :: W'). | L192 | new |
| 23 | Lemma | Life_shape | Lemma Life_shape x R o : Life x R o -> forall c Rf, o = Pop c Rf -> exists W', Rf = (x - c + 1) :: 2 :: W' /\ c + 1 <= x /\ forall z, c + 1 <= z -> Life z R (Pop c ((z - c + 1) :: 2 :: W')). | L199 | new |
| 24 | Definition | bump | Definition bump (o : outcome) : outcome := match o with Fin W => Fin W | Pop c W => Pop (S c) W end. | L214 | new |
| 25 | Lemma | L_cp | Lemma L_cp y h R' R1 c' R2 o : 1 <= y -> updt R' = Some R1 -> Life h R1 (Pop c' R2) -> Life y R2 o -> Life (S y) (h :: R') (bump o). | L217 | new |
| 26 | Lemma | updt_cons2 | Lemma updt_cons2 W R0 : updt (2 :: W) = Some R0 -> exists c2 W1, W = c2 :: W1. | L221 | new |
| 27 | Lemma | frame_step | Lemma frame_step y z W c W' o y' z' : Ep W c W' -> 2 <= y -> c + 1 <= z -> y' = y - 1 -> z' = z - c + 1 -> Life y' (z' :: 2 :: W') o -> Life y (z :: 2 :: W) (bump o). | L225 | new |
| 28 | Definition | tail_ok | Definition tail_ok (N : list nat) : Prop := N = [] \/ exists g rest, N = S (S g) :: rest. | L248 | new |
| 29 | Lemma | U0 | Lemma U0 : Ep [1] 2 [2;2;1]. | L250 | new |
| 30 | Lemma | U1 | Lemma U1 g rest : Ep (1 :: S (S (S (S g))) :: rest) 2 (2 :: 2 :: 1 :: S (S g) :: rest). | L253 | new |
| 31 | Lemma | U2 | Lemma U2 b N : tail_ok N -> Ep (1 :: 2 :: S b :: N) 2 (S (S (S b)) :: 2 :: 1 :: N). | L256 | new |
| 32 | Lemma | ruleS | Lemma ruleS a b N : tail_ok N -> Ep (2 :: 2 :: S a :: 2 :: S b :: N) 2 (S (S a) :: 2 :: S (S (S b)) :: 2 :: 1 :: N). | L259 | new |
| 33 | Lemma | TRF | Lemma TRF a b N Rc : tail_ok N -> 2 <= a -> Life a (S (S (S b)) :: 2 :: 1 :: N) (Fin Rc) -> Ep (a :: 2 :: S b :: N) 2 Rc. | L263 | new |
| 34 | Lemma | Xin0 | Lemma Xin0 a'' b'' : 1 <= a'' -> Life 2 [2; 2; a''; 2; b''] (Pop 1 [2; 2; S a''; 2; S b'']). | L267 | new |
| 35 | Lemma | Xin1 | Lemma Xin1 a'' b'' g rest : 1 <= a'' -> Life 2 (2 :: 2 :: a'' :: 2 :: b'' :: S g :: rest) (Pop 1 (2 :: 2 :: S a'' :: 2 :: S b'' :: S (S g) :: rest)). | L271 | new |
| 36 | Lemma | TRX0 | Lemma TRX0 a b N c a'' b'' : tail_ok N -> 2 <= a -> Life a (S (S (S b)) :: 2 :: 1 :: N) (Pop c [2; 2; S a''; 2; S b'']) -> Ep (a :: 2 :: S b :: N) 3 [S (S a''); 2; S (S b'')]. | L275 | new |
| 37 | Lemma | TRX1 | Lemma TRX1 a b N c a'' b'' g rest : tail_ok N -> 2 <= a -> Life a (S (S (S b)) :: 2 :: 1 :: N) (Pop c (2 :: 2 :: S a'' :: 2 :: S b'' :: S g :: rest)) -> Ep (a :: 2 :: S b :: N) 3 (S (S a'') :: 2 :: S (S b'') :: S (S g) :: rest). | L280 | new |
| 38 | Fixpoint | mwf | Fixpoint mwf (s : nat) (P : list nat) : list nat := match P with | [] => [] | p :: P' => (p - s + 1) :: 1 :: mwf p P' end. | L288 | new |
| 39 | Definition | mw | Definition mw (P : list nat) : list nat := mwf 0 P. | L293 | new |
| 40 | Fixpoint | valid_from | Fixpoint valid_from (s : nat) (P : list nat) : Prop := match P with | [] => True | p :: P' => (exists t, p = s + 2 * t + 1) /\ valid_from p P' end. | L296 | new |
| 41 | Definition | valid | Definition valid (P : list nat) : Prop := valid_from 0 P. | L301 | new |
| 42 | Definition | cnt | Definition cnt (Q : list nat) (n : nat) : nat := length (filter (fun q => q <? n) Q). | L303 | new |
| 43 | Definition | ind | Definition ind (Q : list nat) (n : nat) : nat := cnt Q (S n) - cnt Q n. | L304 | new |
| 44 | Definition | cost | Definition cost (Q : list nat) (n : nat) : nat := 2 + ind Q n. | L305 | new |
| 45 | Inductive | Orb | Inductive Orb (Q : list nat) : nat -> list nat -> Prop := | O0 : Orb Q 0 (1 :: mw Q) | OS n W W' : Orb Q n W -> Ep W (cost Q n) W' -> Orb Q (S n) W'. | L307 | new |
| 46 | Fixpoint | bumpn | Fixpoint bumpn (k : nat) (o : outcome) : outcome := match k with 0 => o | S k => bumpn k (bump o) end. | L311 | new |
| 47 | Lemma | bumpn_fin | Lemma bumpn_fin k W : bumpn k (Fin W) = Fin W. | L314 | new |
| 48 | Lemma | bumpn_pop | Lemma bumpn_pop k c W : bumpn k (Pop c W) = Pop (k + c) W. | L317 | new |
| 49 | Lemma | cnt_0 | Lemma cnt_0 Q : cnt Q 0 = 0. | L320 | new |
| 50 | Lemma | cnt_mono | Lemma cnt_mono Q n : cnt Q n <= cnt Q (S n). | L323 | new |
| 51 | Lemma | cnt_mono' | Lemma cnt_mono' Q n m : n <= m -> cnt Q n <= cnt Q m. | L329 | new |
| 52 | Lemma | replay | Lemma replay Q k Wk : Orb Q k Wk -> forall y z o, k + 1 <= y -> (k = 0 \/ k + 2 + cnt Q k <= z) -> Life (y - k) ((z - k - cnt Q k) :: 2 :: Wk) o -> Life y (z :: 2 :: 1 :: mw Q) (bumpn k o). | L332 | new |
| 53 | Lemma | mw_tail_ok | Lemma mw_tail_ok Q : valid Q -> tail_ok (mw Q). | L342 | new |
| 54 | Lemma | ruleT | Lemma ruleT a b Q W' : Orb Q (a - 1) W' -> 2 <= a -> 1 <= b -> valid Q -> a - 1 + cnt Q (a - 1) <= b -> Ep (a :: 2 :: b :: mw Q) 2 ((b + 3 - a - cnt Q (a - 1)) :: 2 :: W'). | L348 | new |
| 55 | Lemma | mwf_shift | Lemma mwf_shift s k P : mwf (s + k) (map (fun p => p + k) P) = mwf s P. | L361 | new |
| 56 | Lemma | ruleX | Lemma ruleX a b Q a'' Q'' : Orb Q (a - 2) (a'' :: 2 :: b :: mw Q'') -> 3 <= a -> 1 <= b -> 1 <= a'' -> valid Q -> valid Q'' -> b = a - 2 + cnt Q (a - 2) -> Ep (a :: 2 :: b :: mw Q) 3 (S (S a'') :: 2 :: S (S b) :: mw (map (fun q => q + 2) Q'')). | L367 | new |
| 57 | Lemma | valid_gt | Lemma valid_gt s P : valid_from s P -> Forall (fun p => s < p) P. | L390 | new |
| 58 | Lemma | cnt_cons_lt | Lemma cnt_cons_lt q Q n : q < n -> cnt (q :: Q) n = S (cnt Q n). | L397 | new |
| 59 | Lemma | cnt_cons_ge | Lemma cnt_cons_ge q Q n : n <= q -> cnt (q :: Q) n = cnt Q n. | L400 | new |
| 60 | Lemma | cnt_app | Lemma cnt_app X Y n : cnt (X ++ Y) n = cnt X n + cnt Y n. | L403 | new |
| 61 | Lemma | cnt_all_lt | Lemma cnt_all_lt X n : Forall (fun q => q < n) X -> cnt X n = length X. | L406 | new |
| 62 | Lemma | cnt_all_ge | Lemma cnt_all_ge X n : Forall (fun q => n <= q) X -> cnt X n = 0. | L412 | new |
| 63 | Lemma | cnt_S_nin | Lemma cnt_S_nin Q n : ~ In n Q -> cnt Q (S n) = cnt Q n. | L418 | new |
| 64 | Lemma | cnt_S_in | Lemma cnt_S_in s Q n : valid_from s Q -> In n Q -> cnt Q (S n) = S (cnt Q n). | L428 | new |
| 65 | Lemma | ind_in | Lemma ind_in Q n : valid Q -> In n Q -> ind Q n = 1. | L438 | new |
| 66 | Lemma | ind_nin | Lemma ind_nin Q n : ~ In n Q -> ind Q n = 0. | L441 | new |
| 67 | Lemma | ind_iff | Lemma ind_iff P Q k k' : valid P -> valid Q -> (In k P <-> In k' Q) -> ind P k = ind Q k'. | L444 | new |
| 68 | Lemma | parity_in | Lemma parity_in s P n : valid_from s P -> In n P -> exists u, n + cnt P n + s = 2 * u + 1. | L451 | new |
| 69 | Lemma | filter_lt_app | Lemma filter_lt_app X Y k : Forall (fun q => q <= k) X -> filter (fun q => k <? q) (X ++ Y) = filter (fun q => k <? q) Y. | L463 | new |
| 70 | Lemma | filter_filter_lt | Lemma filter_filter_lt P k k' : k <= k' -> filter (fun p => k' <? p) (filter (fun p => k <? p) P) = filter (fun p => k' <? p) P. | L471 | new |
| 71 | Lemma | filter_all | Lemma filter_all P k : Forall (fun p => k < p) P -> filter (fun p => k <? p) P = P. | L478 | new |
| 72 | Lemma | filter_gt | Lemma filter_gt P k p : In p (filter (fun p => k <? p) P) -> k < p. | L484 | new |
| 73 | Lemma | filter_in | Lemma filter_in P k p : k < p -> (In p (filter (fun p => k <? p) P) <-> In p P). | L487 | new |
| 74 | Lemma | filter_cnt_len | Lemma filter_cnt_len P n : length (filter (fun p => n <? p) P) + cnt P (S n) = length P. | L492 | new |
| 75 | Definition | Sh | Definition Sh (u v : nat) (Q P : list nat) : Prop := Forall2 (fun q p => q + u = p + v) Q P. | L501 | new |
| 76 | Lemma | Sh_len | Lemma Sh_len u v Q P : Sh u v Q P -> length Q = length P. | L503 | new |
| 77 | Lemma | Sh_eq | Lemma Sh_eq u v u' v' Q P : Sh u v Q P -> u = u' -> v = v' -> Sh u' v' Q P. | L506 | new |
| 78 | Lemma | Sh_filter | Lemma Sh_filter u v Q P k k' : Sh u v Q P -> k + u = k' + v -> Sh u v (filter (fun q => k <? q) Q) (filter (fun p => k' <? p) P). | L509 | new |
| 79 | Lemma | Sh_in | Lemma Sh_in u v Q P k k' : Sh u v Q P -> k + u = k' + v -> (In k Q <-> In k' P). | L518 | new |
| 80 | Lemma | Sh_trans | Lemma Sh_trans u1 v1 u2 v2 u v w X Y Z : Sh u1 v1 X Y -> Sh u2 v2 Y Z -> u1 + u2 = u + w -> v1 + v2 = v + w -> Sh u v X Z. | L524 | new |
| 81 | Lemma | Sh_map | Lemma Sh_map u v d Q P : Sh u v Q P -> Sh u (v + d) (map (fun q => q + d) Q) P. | L531 | new |
| 82 | Lemma | Sh_unmap | Lemma Sh_unmap v k P : Forall (fun p => k <= p) P -> Sh (v + k) v (map (fun p => p - k) P) P. | L534 | new |
| 83 | Lemma | Sh_ge | Lemma Sh_ge u v Q P k k' : Sh u v Q P -> (forall p, In p P -> k' <= p) -> k + u <= k' + v -> Forall (fun q => k <= q) Q. | L537 | new |
| 84 | Lemma | valid_shift | Lemma valid_shift s k P : valid_from s P -> valid_from (s + k) (map (fun p => p + k) P). | L545 | new |
| 85 | Lemma | valid_map2 | Lemma valid_map2 s P : valid_from s P -> valid_from s (map (fun p => p + 2) P). | L551 | new |
| 86 | Lemma | valid_cons1 | Lemma valid_cons1 Q : valid Q -> valid (1 :: map (fun q => q + 1) Q). | L557 | new |
| 87 | Lemma | valid_unshift | Lemma valid_unshift s k P : valid_from (s + k) P -> valid_from s (map (fun p => p - k) P). | L560 | new |
| 88 | Lemma | valid_app_l | Lemma valid_app_l X Y : valid (X ++ Y) -> Forall (fun q => 1 <= q) X. | L567 | new |
| 89 | Lemma | mwf_unshift | Lemma mwf_unshift s k P : k <= s -> Forall (fun p => k <= p) P -> mwf (s - k) (map (fun p => p - k) P) = mwf s P. | L573 | new |
| 90 | Lemma | mw_cons1 | Lemma mw_cons1 Q : 2 :: 1 :: mw Q = mw (1 :: map (fun q => q + 1) Q). | L580 | new |
| 91 | Lemma | valid_tail_ok | Lemma valid_tail_ok s P : valid_from s P -> tail_ok (mwf s P). | L583 | new |
| 92 | Lemma | cnt1_valid | Lemma cnt1_valid P : valid P -> cnt P 1 = 0. | L589 | new |
| 93 | Lemma | in_transfer | Lemma in_transfer Qi Qe P k k' u v kf : Forall (fun q => q < k) Qi -> Sh u v Qe (filter (fun p => kf <? p) P) -> k + u = k' + v -> kf < k' -> (In k (Qi ++ Qe) <-> In k' P). | L594 | new |
| 94 | Lemma | sh_compose | Lemma sh_compose Qi Qe Qe' P n a a' k k' : Forall (fun q => q <= k) Qi -> n <= k' -> k + (n + 3) = k' + a -> Sh (k + 3) a' Qe' (filter (fun q => k <? q) (Qi ++ Qe)) -> Sh (n + 3) a Qe (filter (fun p => n <? p) P) -> Sh (k' + 3) a' Qe' (filter (fun p => k' <? p) P). | L603 | new |
| 95 | Definition | Core | Definition Core (P : list nat) (k a b : nat) (Q : list nat) : Prop := valid Q /\ 2 <= a /\ exists Qi Qe, Q = Qi ++ Qe /\ length Qi + a = b + 1 + ind P k /\ Forall (fun q => q + 2 + ind P k <= a) Qi /\ Sh (k + 3) a Qe (filter (fun p => k <? p) P). | L618 | new |
| 96 | Definition | Inv | Definition Inv (P : list nat) (n : nat) (W : list nat) : Prop := (Nat.Odd (n + cnt P n) /\ exists a Q, W = a :: 2 :: (n + cnt P n) :: mw Q /\ Core P n a (n + cnt P n) Q) \/ (Nat.Even (n + cnt P n) /\ exists a Q, W = 2 :: 2 :: a :: 2 :: (n + cnt P n - 1) :: mw Q /\ Core P (S n) a (n + cnt P n - 1) Q). | L623 | new |
| 97 | Definition | Claim | Definition Claim (Lm : nat) : Prop := forall Q k, k + length Q <= Lm -> valid Q -> exists W, Orb Q k W /\ (1 <= k -> Inv Q k W). | L629 | new |
| 98 | Lemma | stepU | Lemma stepU P : valid P -> exists W', Ep (1 :: mw P) (cost P 0) W' /\ Inv P 1 W'. | L632 | new |
| 99 | Lemma | stepS | Lemma stepS P n a Q : valid P -> 1 <= n -> Nat.Even (n + cnt P n) -> Core P (S n) a (n + cnt P n - 1) Q -> exists W', Ep (2 :: 2 :: a :: 2 :: (n + cnt P n - 1) :: mw Q) (cost P n) W' /\ Inv P (S n) W'. | L678 | new |
| 100 | Lemma | stepT_nabs | Lemma stepT_nabs Lm P n a Q : Claim Lm -> valid P -> 1 <= n -> n + length P <= Lm -> Nat.Odd (n + cnt P n) -> ~ In n P -> Core P n a (n + cnt P n) Q -> exists W', Ep (a :: 2 :: (n + cnt P n) :: mw Q) (cost P n) W' /\ Inv P (S n) W'. | L709 | new |
| 101 | Lemma | stepT_abs | Lemma stepT_abs Lm P n a Q : Claim Lm -> valid P -> 1 <= n -> n + length P <= Lm -> Nat.Odd (n + cnt P n) -> In n P -> Core P n a (n + cnt P n) Q -> exists W', Ep (a :: 2 :: (n + cnt P n) :: mw Q) (cost P n) W' /\ Inv P (S n) W'. | L754 | new |
| 102 | Lemma | step_lemma | Lemma step_lemma Lm : Claim Lm -> forall P n W, n + length P <= Lm -> valid P -> Orb P n W -> (1 <= n -> Inv P n W) -> exists W', Ep W (cost P n) W' /\ Inv P (S n) W'. | L803 | new |
| 103 | Theorem | main | Theorem main Lm : Claim Lm. | L816 | new |
| 104 | Lemma | init | Lemma init : c0 -->* conf [] [3; 2; 1]. | L828 | new |
| 105 | Lemma | nonhalt | Lemma nonhalt: ~halts tm c0. | L831 | adapted |
4What a maintainer readsCheck: the rule table below is what the .v proves, and proof.md / README read cleanly for a maintainer.
- submission/proof.md · informal proof (submitted copy)
- submission/README.md · the package README
- submission/discord.md · Discord draft (not posted)
- proof.md (working copy) · differs from the submitted copy
submission/proof.md line 34: 1. TM-level rules
The --- is E0. Shift rules (each by induction on n):
CW C> 1^n 1 --> 1^n C> 1 3n steps [C1 B1 B0 per cell: 0RB, 1LB, 1RC]
DW D> 1^n --> 1^n D> n steps [D1]
FW 1^n <F --> <F 1^n n steps [F1]
Macro rules. l and r are arbitrary. All parameters are >= 0.
R1 l 1^(n+2) <A 0 1^(m+1) 0 0 1^x 0 r --> l 1^(n+1) 0 1^(m+1) <A 0 1^(x+1) 0 0 r 3m+2x+15
= A1 C1 B1 B0 C1 B0 · CW(m) · C1 B0 C0 · DW(x+2) · D0 E1 · FW(x+1) · F0
R3 0^inf <A 0 1^(k+1) 0 0 1^m 0 r --> 0^inf 1^(k+2) <A 0 1^(m+1) 0 0 r 3k+2m+11
= A0 B0 · CW(k) · C1 B0 C0 · DW(m+2) · D0 E1 · FW(m+1) · F0
R2 l 1^(j+1) 0 1^(k+1) 0 1 <A 0 r --> l 1^(j+1) <A 0 1^(k+2) 0 0 r k+10
= A1 C0 · DW(3) · D0 E1 · FW(k+2) · F0
R2e 0^inf 1^(k+1) 0 1 <A 0 r --> 0^inf <A 0 1^(k+2) 0 0 r k+10 (same transitions)
HALT 0^inf 1 <A 0 r --> A1 C0 D0, then E reads 0: halt (3 steps)
Inside R1 and R3: after C1 B0 C0 the tape reads ... 0 1^(m+1) 0 D> 1 1 1^x 0 r. DW walks over the x+2 ones, D0 writes 0 and turns, E1 erases the last 1, FW walks back, and F0 lands A on the last 1 of 1^(m+1). In the .v these are tR1, tR3 and tR2, each proved by one es, and tR3c (R3 at the left edge), proved by one const_unfold rewrite of const 0 followed by es; R2e is tR2 with l = const 0.
1.1 The run model (Lemma RM)
Every conf(L,R) in the domain moves by exactly one rule below. The result is again in the domain.
push (p = 0, or a_p >= 2): R3 if p = 0, pushing c_1+1; R1 if p >= 1, setting a_p := a_p - 1 and pushing c_1.
In both cases R becomes: g_1 = 2: [c_2+1, g_2+1, c_3, ...] (just [c_2+1] if r = 2)
g_1 >= 3: [1, g_1-1, c_2, g_2, ...] (just [1] if r = 1)
pop (a_p = 1, p >= 2): L := [a_1..a_(p-2)], R := [a_(p-1)+1, 2] + R (R2, or R2e when p = 2)
halt (a_p = 1, p = 1): HALT
Matching against §1: with g_1 = 2, R1/R3 take x = c_2, and the 0 after 1^x is the first cell of 0^g_2. With g_1 >= 3 they take x = 0, so 0 0 1^0 0 = 0^3 is the start of 0^g_1. With r = 1, the rest is 0^inf. The pop rule needs a single 0 between frames, which the domain gives. The constraints are preserved: a new first gap is g_1-1 >= 2, g_2+1 >= 2 or 2.
Frame reading. A push decrements the top frame (its payment) and creates a child frame. A frame is top only when it has just been created, or right after its child and grandchild were popped together (the grandchild finished). In both cases it then pays for one child (re)creation. When a frame is top with value 1, it finishes: it is popped together with its parent, and the parent goes back into R with value +1. The grandparent then pays to re-create the parent. HALT is a depth-1 frame that has to pay with value 1.
5FamilyCheck: related machines are killed together or have a reason to be left open.
2 machines, 2 killed, 0 not. Family links: status.json parent, same transition table with another start (tools/dashboard.py), targeting.md follow-on rows, ledger "= twin" notes. A machine string named in a .v header / proof.md / notes.md is listed but does not make a family.
| who | machine | status | relation to this kill |
|---|---|---|---|
| #12 kill 5 | 1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF | ✓Killed: never halts | this kill |
| #12b kill 6 | 1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB | ✓Killed: never halts | parent link; named in #12's proof.md; named in #12's notes.md; named in #12b's .v header; named in #12b's proof.md; named in #12b's notes.md · review · same machine as this kill? (table differs in 1 transition(s); trajectory twin; tables, pictures and numbers side by side) |
6ChecklistCheck: every ✓ is computed; the two ○ are yours to decide; an amber ! is an optional check that did not finish.
- ✓Machine string exactthe .v literal == holdout list line 2 byte for byte
- ✓Statement is
~halts tm c0parsed from the .v and confirmed by check_kill (theorem_text, theorem_rocq) - ✓No axioms beyond baseline0 assumption(s); tools/assumptions_baseline.txt allows only functional_extensionality_dep
- ✓coqchk finished (optional)coqchk pass in 1.3 s
- ✓.v hash matches the checked hash.v = checked sha256 f867b60c1855…; submission/ copy = checked sha256 f867b60c1855…
- ✓No repo-local paths in the .vcomments name no path of ours (vendor/, machines/, tools/, rocq/, scripts/, reports/, atlas/, data/, journal/, /home/); busycoq's own
verify/X.vis fine: none in the .v or the submission/ copy - ✓Public write-up is cleantools/writeup_lint.py on
submission/proof.md: 0 error(s) - ○proof.md reviewed by Dennis (Checkpoint B)no Checkpoint B note from Dennis found
- notes.md L199: `proof.md` is written, and `check_proof.py` checks every claim in it (sections A–G). status.json is now stage informal_proof, status OPEN. Checkpoint B (Dennis, non-blocking) is pending.
- notes.md L266: - No Checkpoint A or B notes from Dennis were on file when this was packaged. If he adds any, fold them into proof.md and the submission copy first.
- proof.md L6: - Status: informal proof, written 2026-10-10 (overnight, unattended), revised the same night after an independent skeptic review (six minor gaps, all closed; see the Review log at the end). Every claim below is checked b
- ○Family posted together?1 other kill(s) in the family: #12b; the Discord draft names 1 of them
Generated by tools/killreview.py at 2026-10-16 13:29 PDT in 0.1 s from the files linked above; nothing in this review is hand-written except the box “How we proved it never halts” (above), which quotes how_proved.md. Re-run: python3 -B tools/killreview.py 1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF
Files
machines/<tm>/: 14 entries · raw notes, status, scripts, images
| name | size | changed |
|---|---|---|
| notes.md ↓ | 28 KB | 2026-10-10 09:30 |
| proof.md ↓ | 39 KB | 2026-10-10 08:51 |
| how_proved.md ↓ | 1.6 KB | 2026-10-14 10:51 |
| status.json ↓ | 185 B | 2026-10-10 09:27 |
| observe.json ↓ | 11 KB | 2026-10-10 04:41 |
| deepen.json ↓ | 6.3 KB | 2026-10-10 06:52 |
| 1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF.v ↓ | 39 KB | 2026-10-10 11:50 |
| img/ | 8 items | 2026-10-10 01:56 |
| rocq/ | 8 items | 2026-10-10 09:27 |
| scripts/ | 34 items | 2026-10-10 08:51 |
| submission/ | 5 items | 2026-10-14 09:18 |
| work/ | 1 item | 2026-10-10 15:58 |
| allP_k18-25.txt ↓ | 1.7 KB | 2026-10-10 06:52 |
| check_proof.py ↓ | 39 KB | 2026-10-10 08:23 |
status.json in full
{
"tm": "1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF",
"status": "KILLED_NONHALT",
"stage": "done",
"updated": "2026-10-10",
"reason": "check_kill PASS, independently re-verified"
}