wip

GoldbachTm/Tm31/Prime.lean

@@ -272,21 +272,48 @@ induction rb with intros i lb l r g p
 -- r1 : count of 1 on the right
 theorem lemma_23 (i r1: ℕ) (l r : List Γ)
 (g :
-nth_cfg i = some ⟨⟨0, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate r1 Γ.one ++ List.cons Γ.zero r)⟩⟩)
-(p : Nat.Prime r1) :
-∃ j, nth_cfg (i+j) = some ⟨⟨22, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate r1 Γ.one ++ List.cons Γ.zero r)⟩⟩ :=
+nth_cfg i = some ⟨⟨0, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (Γ.zero :: l), Turing.ListBlank.mk (List.replicate r1 Γ.one ++ List.cons Γ.zero r)⟩⟩)
+(p : Nat.Prime (r1+1)) :
+∃ j, nth_cfg (i+j) = some ⟨⟨22, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate (r1+1) Γ.one ++ List.cons Γ.zero r)⟩⟩ :=
 match h : r1 with
 | Nat.zero => by subst r1
                  exfalso
-                 apply Nat.not_prime_zero p
-| Nat.succ Nat.zero => by subst r1
-                          exfalso
-                          apply Nat.not_prime_one p
+                 apply Nat.not_prime_one p
+| Nat.succ Nat.zero => by
+  subst r1
+  forward g g i
+  forward g g (1+i)
+  forward g g (2+i)
+  forward g g (3+i)
+  forward g g (4+i)
+  use 5
+  ring_nf at *
+  simp [g]
 | Nat.succ (Nat.succ Nat.zero) => by
   subst r1
   forward g g i
   forward g g (1+i)
   forward g g (2+i)
-  sorry
-| Nat.succ (Nat.succ (Nat.succ Nat.zero)) => sorry
-| Nat.succ (Nat.succ (Nat.succ (Nat.succ r1))) => sorry
+  forward g g (3+i)
+  forward g g (4+i)
+  forward g g (5+i)
+  forward g g (6+i)
+  use 7
+  ring_nf at *
+  simp [g]
+| Nat.succ (Nat.succ (Nat.succ r1)) => by
+  forward g g i
+  forward g g (1+i)
+  forward g g (2+i)
+  forward g g (3+i)
+  forward g g (4+i)
+  forward g g (5+i)
+  forward g g (6+i)
+  forward g g (7+i)
+  forward g g (8+i)
+  forward g g (9+i)
+  forward g g (10+i)
+  forward g g (11+i)
+  forward g g (12+i)
+  forward g g (13+i)
+  all_goals sorry