Add straight-line composition lemmas for cleaner proofs

Add is_straight_line_append, is_straight_line_cons, is_straight_line_singleton,
and Instr.*_is_non_jumping lemmas to StraightLine.lean. These provide reusable
building blocks for proving composite programs are straight-line.

Update Preservation.lean files in Minimization and PrimitiveRecursion to use
the new composition lemmas, making the proof structure more explicit.

Author: jessealama

Urm/Minimization/Preservation.lean

@@ -46,10 +46,10 @@ private theorem loop_prologue_no_write_high (r : ℕ) (hr : minimization_base n
 /-- Setup phase is a straight-line program. -/
 theorem setup_phase_is_straight_line :
     (setup_phase n pF).is_straight_line = true := by
-  simp only [setup_phase, Program.is_straight_line, List.all_append, List.all_cons, List.all_nil,
-    Bool.and_true, Bool.and_eq_true]
-  refine ⟨copy_register_range_is_straight_line 0 (savedInputsStart n pF) n, ?_, rfl⟩
-  simp [Instr.is_non_jumping]
+  simp only [setup_phase]
+  exact is_straight_line_append (copy_register_range_is_straight_line _ _ _)
+    (is_straight_line_cons (Instr.Z_is_non_jumping _)
+      (is_straight_line_singleton (Instr.Z_is_non_jumping _)))
 
 /-- After setup phase, saved inputs contain original inputs. -/
 theorem setup_phase_saves_inputs (inputs : Fin n → ℕ)
@@ -161,10 +161,10 @@ theorem setup_phase_zero_reg_zero
 /-- Loop prologue is a straight-line program. -/
 theorem loop_prologue_is_straight_line :
     (loop_prologue n pF).is_straight_line = true := by
-  simp only [loop_prologue, Program.is_straight_line, List.all_append, List.all_cons, List.all_nil,
-    Bool.and_true, Bool.and_eq_true]
-  exact ⟨⟨clear_registers_is_straight_line (minimization_base n pF),
-           copy_register_range_is_straight_line (savedInputsStart n pF) 0 n⟩, rfl⟩
+  simp only [loop_prologue]
+  apply is_straight_line_append _ (is_straight_line_singleton (Instr.T_is_non_jumping _ _))
+  exact is_straight_line_append (clear_registers_is_straight_line _)
+    (copy_register_range_is_straight_line _ _ _)
 
 /-- After loop prologue, R[0..n-1] contain saved inputs. -/
 theorem loop_prologue_restores_inputs

Urm/PrimitiveRecursion/Preservation.lean

@@ -67,25 +67,26 @@ private theorem pr_loop_prologue_no_write_high (n : ℕ) (pF pG : Program) (r :
 /-- Setup phase is a straight-line program. -/
 theorem pr_setup_phase_is_straight_line (n : ℕ) (pF pG : Program) :
     (pr_setup_phase n pF pG).is_straight_line = true := by
-  simp only [pr_setup_phase, Program.is_straight_line, List.all_append, List.all_cons, List.all_nil,
-    Bool.and_true, Bool.and_eq_true]
-  refine ⟨copy_register_range_is_straight_line 0 (pr_saved_inputs_start n pF pG) (n + 1), ?_, rfl⟩
-  simp [Instr.is_non_jumping]
+  simp only [pr_setup_phase]
+  exact is_straight_line_append (copy_register_range_is_straight_line _ _ _)
+    (is_straight_line_cons (Instr.Z_is_non_jumping _)
+      (is_straight_line_singleton (Instr.Z_is_non_jumping _)))
 
 /-- Base case prologue is a straight-line program. -/
 theorem pr_base_case_prologue_is_straight_line (n : ℕ) (pF pG : Program) :
     (pr_base_case_prologue n pF pG).is_straight_line = true := by
-  simp only [pr_base_case_prologue, Program.is_straight_line, List.all_append, Bool.and_eq_true]
-  exact ⟨clear_registers_is_straight_line (primitive_recursion_base n pF pG),
-         copy_register_range_is_straight_line (pr_saved_inputs_start n pF pG) 0 n⟩
+  simp only [pr_base_case_prologue]
+  exact is_straight_line_append (clear_registers_is_straight_line _)
+    (copy_register_range_is_straight_line _ _ _)
 
 /-- Loop prologue is a straight-line program. -/
 theorem pr_loop_prologue_is_straight_line (n : ℕ) (pF pG : Program) :
     (pr_loop_prologue n pF pG).is_straight_line = true := by
-  simp only [pr_loop_prologue, Program.is_straight_line, List.all_append, Bool.and_eq_true]
-  refine ⟨⟨clear_registers_is_straight_line (primitive_recursion_base n pF pG),
-          copy_register_range_is_straight_line (pr_saved_inputs_start n pF pG) 0 n⟩, ?_⟩
-  simp only [List.all_cons, List.all_nil, Instr.is_non_jumping, Bool.and_self]
+  simp only [pr_loop_prologue]
+  apply is_straight_line_append _ (is_straight_line_cons (Instr.T_is_non_jumping _ _)
+    (is_straight_line_singleton (Instr.T_is_non_jumping _ _)))
+  exact is_straight_line_append (clear_registers_is_straight_line _)
+    (copy_register_range_is_straight_line _ _ _)
 
 /-! ## Setup Phase Invariants -/
 

Urm/StraightLine.lean

@@ -286,6 +286,40 @@ theorem clear_registers_from_preserves (start count : ℕ) (s : State) (r : ℕ)
   simp only [Instr.writes_to, ne_eq, Option.some.injEq]
   omega
 
+/-! ## Straight-Line Program Composition
+
+Lemmas for proving composite programs are straight-line.
+These simplify proofs in Preservation.lean files across closures. -/
+
+/-- Append preserves straight-line property. -/
+theorem is_straight_line_append {p q : Program}
+    (hp : p.is_straight_line = true) (hq : q.is_straight_line = true) :
+    (p ++ q).is_straight_line = true := by
+  simp only [Program.is_straight_line, List.all_append] at hp hq ⊢
+  rw [hp, hq]; rfl
+
+/-- Cons of non-jumping instruction preserves straight-line. -/
+theorem is_straight_line_cons {instr : Instr} {p : Program}
+    (hinstr : instr.is_non_jumping = true) (hp : p.is_straight_line = true) :
+    Program.is_straight_line (instr :: p) = true := by
+  simp only [Program.is_straight_line, List.all_cons] at hp ⊢
+  rw [hinstr, hp]; rfl
+
+/-- Singleton non-jumping instruction is straight-line. -/
+theorem is_straight_line_singleton {instr : Instr}
+    (h : instr.is_non_jumping = true) :
+    Program.is_straight_line [instr] = true := by
+  simp only [Program.is_straight_line, List.all_cons, List.all_nil, h, Bool.and_self]
+
+/-- Z instruction is non-jumping. -/
+@[simp] theorem Instr.Z_is_non_jumping (n : ℕ) : (Instr.Z n).is_non_jumping = true := rfl
+
+/-- S instruction is non-jumping. -/
+@[simp] theorem Instr.S_is_non_jumping (n : ℕ) : (Instr.S n).is_non_jumping = true := rfl
+
+/-- T instruction is non-jumping. -/
+@[simp] theorem Instr.T_is_non_jumping (m n : ℕ) : (Instr.T m n).is_non_jumping = true := rfl
+
 /-! ## clear_registers and copy_register_range
 
 These are straight-line program building blocks used by both Composition and Minimization. -/