Add chain_concat_sf variant for standard form programs

Add Steps.chain_concat_sf that derives pc equality from IsStandardForm,
eliminating explicit pc proofs at call sites where the first program
is standard form.

Refactor call sites in:
- Preservation.lean: 3 sites use chain_concat_sf
- Halting.lean: Most sites use chain_concat_sf, 2 remain with chain_concat
- Correctness.lean: Mixed approach based on downstream pc requirements

Author: jessealama

Urm/Composition/Correctness.lean

@@ -109,7 +109,7 @@ theorem comp_general_halts_imp_gi_dom
       have hn_le_base : n ≤ base + 1 := by have := compositionBase_ge_n_sub_one m n pF pGs; omega
       have hsSave_value : sSave.read (base + 1 + r) = inputs ⟨r, hr_lt_n⟩ := by
         rw [hsSave_eq]; exact saveInputs_state base n hn_le_base inputs r hr_lt_n
-      have hSavePrefixChain := Steps.chain_concat hSave_steps (by simp) rfl hPrefix_steps hPrefix_halted
+      have hSavePrefixChain := Steps.chain_concat_sf hSaveInputs_sf hSave_steps hSave_halted' hPrefix_steps hPrefix_halted
       have hPrefix_state_match : cPrefix.state = sSavePrefix := by
         simp only [hsSavePrefix_eq hSavePrefix_halts, ← Steps.halts_unique hSavePrefixChain.1 hSavePrefixChain.2 hSavePrefix_halts.choose_spec.1 hSavePrefix_halts.choose_spec.2]
       have hPrefix_preserves := allGPhases_prefix_preserves_saved_inputs m n base pGs hGs_sf hpGs_max hn_le_base
@@ -251,23 +251,22 @@ theorem comp_general_dom_imp_halts
   have hGPhases_pc : cGPhases.pc = gPhases.length :=
     hGPhases_sf.pc_eq_length_of_halted hGPhases_steps (Nat.zero_le _) hGPhases_halted
   let sGPhases := cGPhases.state
+  have hpc_eq : cGPhases.pc + saveInputs.length = (saveInputs.concat gPhases).length := by
+    simp only [Program.concat_length, hGPhases_pc]; omega
   have hResults : ∀ j : ℕ, (hj : j < m) → sGPhases.read (base + n + 1 + j) = results ⟨j, hj⟩ := fun j hj => by
     have hSaveGPhases_halted' : ∃ c : Config,
         Steps (saveInputs.concat gPhases) ⟨0, State.fromInputs (List.ofFn inputs)⟩ c ∧
         c.isHalted (saveInputs.concat gPhases) ∧ c.state = cGPhases.state :=
-      ⟨⟨(saveInputs.concat gPhases).length, sGPhases⟩,
-       by convert hSaveGPhases_steps using 2; simp [Program.concat_length, hGPhases_pc, add_comm],
-       by simp, rfl⟩
+      ⟨⟨(saveInputs.concat gPhases).length, sGPhases⟩, hpc_eq ▸ hSaveGPhases_steps, by simp, rfl⟩
     exact allGPhases_saves_result (pF := pF) hGs_sf hGs_spec inputs hGs_dom ⟨j, hj⟩ _ hSaveGPhases_halted'
   have hpF_max : pF.maxRegister ≤ base := compositionBase_ge_pF_max m n pF pGs
   have hm_le_base : m ≤ base + 1 := compositionBase_ge_m m n pF pGs
   obtain ⟨cFinal, hFinal_steps, hFinal_halted⟩ :=
     finalPhase_halts_from_results hF_sf hpF_max hm_le_base hF_halts sGPhases hResults
   have hSaveGPhases_steps' : Steps (saveInputs.concat gPhases) ⟨0, State.fromInputs (List.ofFn inputs)⟩
-      ⟨(saveInputs.concat gPhases).length, sGPhases⟩ := by
-    convert hSaveGPhases_steps using 2; simp only [Program.concat_length, hGPhases_pc]; omega
-  have ⟨hTotal_steps, hTotal_halted⟩ := Steps.chain_concat hSaveGPhases_steps' (by simp)
-    rfl hFinal_steps hFinal_halted
+      ⟨(saveInputs.concat gPhases).length, sGPhases⟩ := hpc_eq ▸ hSaveGPhases_steps
+  have hSaveGPhases_halted' : (⟨(saveInputs.concat gPhases).length, sGPhases⟩ : Config).isHalted (saveInputs.concat gPhases) := by simp
+  have ⟨hTotal_steps, hTotal_halted⟩ := Steps.chain_concat hSaveGPhases_steps' hSaveGPhases_halted' rfl hFinal_steps hFinal_halted
   rw [hH_eq, ← concat_assoc]; exact ⟨_, hTotal_steps, hTotal_halted⟩
 
 /-- The result of the composition equals the composed function value. -/
@@ -314,6 +313,8 @@ theorem comp_general_result
   have hn_le_base : n ≤ base + 1 := compositionBase_ge_n m n pF pGs
   have hGi_halts : ∀ i, Halts (pGs i) (List.ofFn inputs) := fun i => (hGs_spec i inputs).1.mpr (hGs_dom i)
   have hGPhases_sf := allGPhases_isStandardForm (n := n) (base := base) hGs_sf
+  have hSaveInputs_sf := saveInputs_isStandardForm base n
+  have hSaveGPhases_sf := hSaveInputs_sf.concat hGPhases_sf
   have hSave_sl := copyRegisterRange_isStraightLine 0 (base + 1) n
   obtain ⟨cSave, hSave_steps, hSave_halted, hSave_pc'⟩ := straightLine_halts_from_state hSave_sl (State.fromInputs (List.ofFn inputs))
   have hNoOverlap' : 0 + n ≤ base + 1 := by simp; exact compositionBase_ge_n m n pF pGs
@@ -332,6 +333,8 @@ theorem comp_general_result
   have hGPhases_pc : cGPhases.pc = gPhases.length :=
     hGPhases_sf.pc_eq_length_of_halted hGPhases_steps (Nat.zero_le _) hGPhases_halted
   let sGPhases := cGPhases.state
+  have hpc_eq : cGPhases.pc + saveInputs.length = (saveInputs.concat gPhases).length := by
+    simp only [Program.concat_length, hGPhases_pc]; omega
   have hResults : ∀ j : ℕ, (hj : j < m) → sGPhases.read (base + n + 1 + j) = results ⟨j, hj⟩ := fun j hj => by
     have hSaveGPhases_halted' : ∃ c : Config,
         Steps (saveInputs.concat gPhases) ⟨0, State.fromInputs (List.ofFn inputs)⟩ c ∧
@@ -377,9 +380,9 @@ theorem comp_general_result
   have ⟨hTransferF_steps, hTransferF_halted⟩ := Steps.chain_concat hTransfer_steps hTransfer_halted rfl epF.steps epF.halted
   have ⟨hClearTransferF_steps, hClearTransferF_halted⟩ := Steps.chain_concat hClear_steps hClear_halted hClear_pc hTransferF_steps hTransferF_halted
   have hSaveGPhases_steps' : Steps (saveInputs.concat gPhases) ⟨0, State.fromInputs (List.ofFn inputs)⟩
-      ⟨(saveInputs.concat gPhases).length, sGPhases⟩ := by
-    convert hSaveGPhases_steps using 2; simp only [Program.concat_length, hGPhases_pc]; omega
-  have ⟨hTotal_steps, hTotal_halted⟩ := Steps.chain_concat hSaveGPhases_steps' (by simp) rfl hClearTransferF_steps hClearTransferF_halted
+      ⟨(saveInputs.concat gPhases).length, sGPhases⟩ := hpc_eq ▸ hSaveGPhases_steps
+  have hSaveGPhases_halted' : (⟨(saveInputs.concat gPhases).length, sGPhases⟩ : Config).isHalted (saveInputs.concat gPhases) := by simp
+  have ⟨hTotal_steps, hTotal_halted⟩ := Steps.chain_concat hSaveGPhases_steps' hSaveGPhases_halted' rfl hClearTransferF_steps hClearTransferF_halted
   rw [hH_eq, ← concat_assoc] at hH_steps hH_halted
   let cH_built : Config := ⟨(saveInputs.concat gPhases).length + final.length + epF.config.pc - pF.length, epF.config.state⟩
   have hcH_built_halted : cH_built.isHalted ((saveInputs.concat gPhases).concat final) := by

Urm/Composition/Halting.lean

@@ -34,9 +34,9 @@ theorem gPhase_halts_from_saved_inputs {base n : ℕ} {pG : Program} {i : ℕ} {
       simp [State.fromInputs, State.read, hr_n]
   let epG := Halts.executeFromAgreeingState hpG_halts hpG_sf hagree
   let eT := executeSingleTransfer 0 (base + n + 1 + i) epG.config.state
-  have ⟨hPGT_steps, hPGT_halted⟩ := Steps.chain_concat epG.steps epG.halted epG.pc_eq eT.steps eT.halted
-  have ⟨hCopyPGT_steps, hCopyPGT_halted⟩ := Steps.chain_concat hCopy_steps hCopy_halted hCopy_pc hPGT_steps hPGT_halted
-  have ⟨hGPhase_steps, hGPhase_halted⟩ := Steps.chain_concat hClear_steps hClear_halted hClear_pc hCopyPGT_steps hCopyPGT_halted
+  have ⟨hPGT_steps, hPGT_halted⟩ := Steps.chain_concat_sf hpG_sf epG.steps epG.halted eT.steps eT.halted
+  have ⟨hCopyPGT_steps, hCopyPGT_halted⟩ := Steps.chain_concat_sf (copyRegisterRange_isStandardForm (base + 1) 0 n) hCopy_steps hCopy_halted hPGT_steps hPGT_halted
+  have ⟨hGPhase_steps, hGPhase_halted⟩ := Steps.chain_concat_sf (clearRegisters_isStandardForm base) hClear_steps hClear_halted hCopyPGT_steps hCopyPGT_halted
   exact ⟨_, hGPhase_steps, hGPhase_halted⟩
 
 theorem gPhase_writes_result {base n : ℕ} {pG : Program} {j : ℕ} {inputs : Fin n → ℕ}
@@ -75,9 +75,9 @@ theorem gPhase_writes_result {base n : ℕ} {pG : Program} {j : ℕ} {inputs : F
   have hT_result : cT.state.read (base + n + 1 + j) = sPG.read 0 := by
     let tr := executeSingleTransfer 0 (base + n + 1 + j) sPG
     simp only [Steps.halts_unique hT_steps hT_halted tr.steps tr.halted, tr.dst_eq]
-  have hPGT := Steps.chain_concat hPG_steps (by simp) rfl hT_steps hT_halted
-  have hCopyPGT := Steps.chain_concat hCopy_steps (by simp) rfl hPGT_steps hPGT_halted
-  have hClearRest := Steps.chain_concat hClear_steps (by simp) rfl hRest_steps hRest_halted
+  have hPGT := Steps.chain_concat_sf hpG_sf hPG_steps (by simp) hT_steps hT_halted
+  have hCopyPGT := Steps.chain_concat_sf (copyRegisterRange_isStandardForm (base + 1) 0 n) hCopy_steps (by simp) hPGT_steps hPGT_halted
+  have hClearRest := Steps.chain_concat_sf (clearRegisters_isStandardForm base) hClear_steps (by simp) hRest_steps hRest_halted
   simp only [Steps.halts_unique hsteps hhalted hClearRest.1 hClearRest.2,
       Steps.halts_unique hRest_steps hRest_halted hCopyPGT.1 hCopyPGT.2,
       Steps.halts_unique hPGT_steps hPGT_halted hPGT.1 hPGT.2, hT_result, hR0_after_pG]
@@ -100,15 +100,14 @@ theorem allGPhases_halts_from_saved_inputs {m n base : ℕ} {pGs : Fin m → Pro
     obtain ⟨cPrefix, hPrefix_steps, hPrefix_halted⟩ := ih (fun i => hpGs_sf i.castSucc)
       (fun i => hpGs_max i.castSucc) (fun i => hpGs_halts i.castSucc)
     have hPrefix_sf := allGPhases_isStandardForm (n := n) (base := base) (fun i => hpGs_sf i.castSucc)
-    have hPrefix_pc := hPrefix_sf.pc_eq_length_of_halted hPrefix_steps (Nat.zero_le _) hPrefix_halted
     have hSaved_after_prefix : ∀ j : ℕ, (hj : j < n) → cPrefix.state.read (base + 1 + j) = inputs ⟨j, hj⟩ := fun j hj =>
       allGPhases_prefix_preserves_saved_inputs m' n base pGs' (fun i => hpGs_sf i.castSucc) (fun i => hpGs_max i.castSucc) hn_le_base
         m' (Nat.le_refl m') s cPrefix.state cPrefix
         (allGPhases_prefix_full m' n base pGs' ▸ hPrefix_steps) (allGPhases_prefix_full m' n base pGs' ▸ hPrefix_halted) rfl
         (base + 1 + j) (by omega) (by omega) ▸ hSaved j hj
     obtain ⟨cLast, hLast_steps, hLast_halted⟩ := gPhase_halts_from_saved_inputs (i := m')
       (hpGs_sf (Fin.last m')) (hpGs_max (Fin.last m')) hn_le_base (hpGs_halts (Fin.last m')) cPrefix.state hSaved_after_prefix
-    have ⟨hTotal_steps, hTotal_halted⟩ := Steps.chain_concat hPrefix_steps hPrefix_halted hPrefix_pc hLast_steps hLast_halted
+    have ⟨hTotal_steps, hTotal_halted⟩ := Steps.chain_concat_sf hPrefix_sf hPrefix_steps hPrefix_halted hLast_steps hLast_halted
     exact ⟨_, hTotal_steps, hTotal_halted⟩
 
 theorem finalPhase_halts_from_results {m n base : ℕ} {pF : Program} {results : Fin m → ℕ}
@@ -140,8 +139,8 @@ theorem finalPhase_halts_from_results {m n base : ℕ} {pF : Program} {results :
     · rw [hTransfer_preserves r (by omega), hClear_zeros r (by omega : r ≤ base)]
       simp [State.fromInputs, State.read, hr_m]
   let epF := Halts.executeFromAgreeingState hpF_halts hpF_sf hagree
-  have ⟨hTransferF_steps, hTransferF_halted⟩ := Steps.chain_concat hTransfer_steps hTransfer_halted rfl epF.steps epF.halted
-  have ⟨hFinal_steps, hFinal_halted⟩ := Steps.chain_concat hClear_steps hClear_halted hClear_pc hTransferF_steps hTransferF_halted
+  have ⟨hTransferF_steps, hTransferF_halted⟩ := Steps.chain_concat_sf (transferResultsToInputs_isStandardForm (base + n + 1) m) hTransfer_steps hTransfer_halted epF.steps epF.halted
+  have ⟨hFinal_steps, hFinal_halted⟩ := Steps.chain_concat_sf (clearRegisters_isStandardForm base) hClear_steps hClear_halted hTransferF_steps hTransferF_halted
   exact ⟨_, hFinal_steps, hFinal_halted⟩
 
 theorem allGPhases_suffix_preserves_earlier_results {m n base : ℕ} {pGs : Fin m → Program}
@@ -172,7 +171,7 @@ theorem allGPhases_suffix_preserves_earlier_results {m n base : ℕ} {pGs : Fin
         (hpGs_sf _) (hpGs_max _) hn_le_base (by omega) s sFirst ⟨_, sFirst⟩ hFirst_steps (by simp) rfl
       have hRest_preserves := allGPhases_suffix_preserves_earlier_results hpGs_sf hpGs_max hn_le_base
         (start + 1) k (by omega) sFirst cRest hRest_steps hRest_halted
-      have hChain := Steps.chain_concat hFirst_steps (by simp) rfl hRest_steps hRest_halted
+      have hChain := Steps.chain_concat_sf (gPhase_isStandardForm (hpGs_sf ⟨start, hEmpty⟩)) hFirst_steps (by simp) hRest_steps hRest_halted
       simp only [Steps.halts_unique hsteps hhalted hChain.1 hChain.2, hRest_preserves, hFirst_preserves]
 termination_by m - start
 decreasing_by simp_wf; omega
@@ -249,7 +248,7 @@ theorem allGPhases_saves_result {m n : ℕ} [NeZero m] {pF : Program} {pGs : Fin
       conv at hPrefix_steps => rw [hsSave'_eq]
       have hPrefix_steps' : Steps (allGPhases_prefix m n base pGs i.val) ⟨0, cSave.state⟩ cPrefix :=
         hSave_state_sSave ▸ hPrefix_steps
-      have hPrefixChain := Steps.chain_concat hSave_steps' hSave_halted' hSave_pc' hPrefix_steps' hPrefix_halted
+      have hPrefixChain := Steps.chain_concat_sf (copyRegisterRange_isStandardForm 0 (base + 1) n) hSave_steps' hSave_halted' hPrefix_steps' hPrefix_halted
       have hcPrefix_state : cPrefix.state = sSavePrefixI :=
         (congrArg Config.state (Steps.halts_unique hSavePrefixI_steps (by simp) hPrefixChain.1 hPrefixChain.2)).symm
       rw [← hcPrefix_state, allGPhases_prefix_preserves_saved_inputs m n base pGs hGs_sf hpGs_max hn_le_base

Urm/Composition/Helpers.lean

@@ -45,6 +45,15 @@ theorem Steps.chain_concat {p1 p2 : Program} {s : State} {c1 c2 : Config}
   rw [hstart_eq] at h2'
   exact ⟨h1'.trans h2', by simp only [Config.isHalted, Program.concat_length] at h2_halted ⊢; omega⟩
 
+/-- Chain two programs where p1 is standard form: derives pc equality from halted. -/
+theorem Steps.chain_concat_sf {p1 p2 : Program} {s : State} {c1 c2 : Config}
+    (h1_sf : p1.IsStandardForm)
+    (h1_steps : Steps p1 ⟨0, s⟩ c1) (h1_halted : c1.isHalted p1)
+    (h2_steps : Steps p2 ⟨0, c1.state⟩ c2) (h2_halted : c2.isHalted p2) :
+    Steps (p1.concat p2) ⟨0, s⟩ ⟨c2.pc + p1.length, c2.state⟩ ∧
+    (⟨c2.pc + p1.length, c2.state⟩ : Config).isHalted (p1.concat p2) :=
+  chain_concat h1_steps h1_halted (h1_sf.pc_eq_length_of_halted h1_steps (Nat.zero_le _) h1_halted) h2_steps h2_halted
+
 /-! ## Agreeing State Execution -/
 
 /-- Bundle for an execution from an agreeing state. -/

Urm/Composition/Preservation.lean

@@ -109,9 +109,9 @@ private theorem gPhase_preserves_register_aux (base n : ℕ) (pG : Program) (j :
   let tr := executeSingleTransfer 0 (base + n + 1 + j) sPG
   have hT_preserves : cT.state.read r = sPG.read r := by
     simp only [Steps.halts_unique hT_steps hT_halted tr.steps tr.halted]; exact tr.preserved r (by omega)
-  have hPGT := Steps.chain_concat hPG_steps (by simp) rfl hT_steps hT_halted
-  have hRest' := Steps.chain_concat hCopy_steps (by simp) rfl hPGT_steps hPGT_halted
-  have hGPhase := Steps.chain_concat hClear_steps (by simp) rfl hRest_steps hRest_halted
+  have hPGT := Steps.chain_concat_sf hpG_sf hPG_steps (by simp) hT_steps hT_halted
+  have hRest' := Steps.chain_concat_sf (copyRegisterRange_isStandardForm (base + 1) 0 n) hCopy_steps (by simp) hPGT_steps hPGT_halted
+  have hGPhase := Steps.chain_concat_sf (clearRegisters_isStandardForm base) hClear_steps (by simp) hRest_steps hRest_halted
   simp only [← hstate_eq, Steps.halts_unique hsteps hhalted hGPhase.1 hGPhase.2,
     Steps.halts_unique hRest_steps hRest_halted hRest'.1 hRest'.2,
     Steps.halts_unique hPGT_steps hPGT_halted hPGT.1 hPGT.2,