Merge pull request #52 from jessealama/type-class-improvements

Author: jessealama

Urm/Basic.lean

@@ -215,6 +215,11 @@ theorem init_state (inputs : List ℕ) : (init inputs).state = State.fromInputs
 theorem ext {c₁ c₂ : Config} (hpc : c₁.pc = c₂.pc) (hstate : c₁.state = c₂.state) : c₁ = c₂ := by
   cases c₁; cases c₂; simp only at hpc hstate; simp [hpc, hstate]
 
+instance : Inhabited Config := ⟨init []⟩
+
+instance : Repr Config where
+  reprPrec c _ := s!"Config(pc={c.pc})"
+
 end Config
 
 end Urm

Urm/Composition/Construction.lean

@@ -15,31 +15,51 @@ open Program
 def gPhase (base n : ℕ) (pG : Program) (i : ℕ) : Program :=
   (clearRegisters base).concat ((copyRegisterRange (base + 1) 0 n).concat (pG.concat [Instr.T 0 (base + n + 1 + i)]))
 
+/-- Helper to map gPhase over a list of indices. -/
+def gPhaseList (n base : ℕ) (pGs : Fin m → Program) (indices : List (Fin m)) : List Program :=
+  indices.map (fun i => gPhase base n (pGs i) i.val)
+
 def allGPhases (m n base : ℕ) (pGs : Fin m → Program) : Program :=
-  (List.finRange m).foldl (fun acc i => acc.concat (gPhase base n (pGs i) i.val)) []
+  (gPhaseList n base pGs (List.finRange m)).prod
 
 def allGPhases_prefix (m n base : ℕ) (pGs : Fin m → Program) (i : ℕ) : Program :=
-  (List.finRange m).take i |>.foldl (fun acc j => acc.concat (gPhase base n (pGs j) j.val)) []
+  (gPhaseList n base pGs ((List.finRange m).take i)).prod
 
 def allGPhases_suffix (m n base : ℕ) (pGs : Fin m → Program) (i : ℕ) : Program :=
-  (List.finRange m).drop i |>.foldl (fun acc j => acc.concat (gPhase base n (pGs j) j.val)) []
-
-theorem foldl_concat_eq_acc_concat {α : Type*} (f : α → Program) (l : List α) (acc : Program) :
-    l.foldl (fun a x => a.concat (f x)) acc = acc.concat (l.foldl (fun a x => a.concat (f x)) []) := by
-  induction l generalizing acc with
-  | nil => simp only [List.foldl_nil, concat_nil_right]
-  | cons x xs ih => simp only [List.foldl_cons, concat_nil_left]; rw [ih (acc.concat (f x)), ih (f x), concat_assoc]
+  (gPhaseList n base pGs ((List.finRange m).drop i)).prod
 
 theorem allGPhases_split (m n base : ℕ) (pGs : Fin m → Program) (i : ℕ) (_hi : i ≤ m) :
     allGPhases m n base pGs = (allGPhases_prefix m n base pGs i).concat (allGPhases_suffix m n base pGs i) := by
-  simp only [allGPhases, allGPhases_prefix, allGPhases_suffix]
-  conv_lhs => rw [(List.take_append_drop i (List.finRange m)).symm]
-  simp only [List.foldl_append]
-  exact foldl_concat_eq_acc_concat (fun j => gPhase base n (pGs j) j.val) _ _
+  simp only [allGPhases, allGPhases_prefix, allGPhases_suffix, gPhaseList]
+  rw [show (List.finRange m).map (fun i => gPhase base n (pGs i) i.val) =
+      ((List.finRange m).take i).map (fun i => gPhase base n (pGs i) i.val) ++
+      ((List.finRange m).drop i).map (fun i => gPhase base n (pGs i) i.val) by
+    rw [← List.map_append, List.take_append_drop]]
+  rw [List.prod_append]
+  rfl
 
 theorem allGPhases_prefix_full (m n base : ℕ) (pGs : Fin m → Program) :
     allGPhases_prefix m n base pGs m = allGPhases m n base pGs := by
-  simp only [allGPhases_prefix, allGPhases]; congr 1; simp
+  simp only [allGPhases_prefix, allGPhases, gPhaseList]; congr 1; simp
+
+/-- Decompose suffix when start < m: first gPhase followed by remaining suffix. -/
+theorem allGPhases_suffix_cons {m n base : ℕ} (pGs : Fin m → Program) (start : ℕ) (hstart : start < m) :
+    allGPhases_suffix m n base pGs start =
+      (gPhase base n (pGs ⟨start, hstart⟩) start).concat (allGPhases_suffix m n base pGs (start + 1)) := by
+  simp only [allGPhases_suffix, gPhaseList]
+  rw [List.drop_eq_getElem_cons (by simp; exact hstart), List.map_cons, List.prod_cons]
+  simp only [List.getElem_finRange]
+  rfl
+
+/-- Decompose prefix when taking one more: previous prefix followed by the next gPhase. -/
+theorem allGPhases_prefix_succ {m n base : ℕ} (pGs : Fin m → Program) (i : ℕ) (hi : i < m) :
+    allGPhases_prefix m n base pGs (i + 1) =
+      (allGPhases_prefix m n base pGs i).concat (gPhase base n (pGs ⟨i, hi⟩) i) := by
+  simp only [allGPhases_prefix, gPhaseList]
+  rw [List.take_succ_eq_append_getElem (by simp; exact hi : i < (List.finRange m).length)]
+  rw [List.map_append, List.map_singleton, List.prod_append, List.prod_singleton]
+  simp only [List.getElem_finRange]
+  rfl
 
 def finalPhase (m n base : ℕ) (pF : Program) : Program :=
   (clearRegisters base).concat ((transferResultsToInputs (base + n + 1) m).concat pF)

Urm/Composition/Correctness.lean

@@ -61,13 +61,8 @@ theorem comp_general_halts_imp_gi_dom
   obtain ⟨sSavePrefix, _, hsSavePrefix_eq, cSuffix, hSuffix_steps, hSuffix_halted⟩ :=
     Halts.suffix_of_concat_sf hSaveGPhases_halts hSavePrefix_sf
   have hSuffix_i_eq : allGPhases_suffix m n base pGs i.val =
-      (gPhase base n (pGs i) i.val).concat (allGPhases_suffix m n base pGs (i.val + 1)) := by
-    simp only [allGPhases_suffix]
-    rw [show (List.finRange m).drop i.val = i :: (List.finRange m).drop (i.val + 1) from by
-          rw [List.drop_eq_getElem_cons]; · congr 1; simp only [List.finRange, List.getElem_ofFn]
-          · simp only [List.length_finRange]; exact i.isLt,
-        List.foldl_cons, concat_nil_left]
-    exact foldl_concat_eq_acc_concat _ _ _
+      (gPhase base n (pGs i) i.val).concat (allGPhases_suffix m n base pGs (i.val + 1)) :=
+    allGPhases_suffix_cons pGs i.val i.isLt
   rw [hSuffix_i_eq] at hSuffix_steps hSuffix_halted
   obtain ⟨_, hGPhase_i_steps, hGPhase_i_halted⟩ :=
     prefix_of_concat_from_zero hSuffix_steps hSuffix_halted hGPhase_i_sf

Urm/Composition/Halting.lean

@@ -85,15 +85,21 @@ theorem allGPhases_halts_from_saved_inputs {m n base : ℕ} {pGs : Fin m → Pro
     (hSaved : ∀ j : ℕ, (hj : j < n) → s.read (base + 1 + j) = inputs ⟨j, hj⟩) :
     ∃ c, Steps (allGPhases m n base pGs) ⟨0, s⟩ c ∧ c.isHalted (allGPhases m n base pGs) := by
   induction m with
-  | zero => simp only [allGPhases, List.finRange_zero, List.foldl_nil]
-            exact ⟨⟨0, s⟩, Relation.ReflTransGen.refl, by simp⟩
+  | zero =>
+    have hAllGPhases_zero : allGPhases 0 n base pGs = [] := by
+      simp only [allGPhases, gPhaseList, List.finRange_zero, List.map_nil, List.prod_nil]; rfl
+    simp only [hAllGPhases_zero]
+    exact ⟨⟨0, s⟩, Relation.ReflTransGen.refl, by simp⟩
   | succ m' ih =>
-    simp only [allGPhases]
-    rw [List.finRange_succ_last, List.foldl_append, List.foldl_map, List.foldl_cons, List.foldl_nil]
     let pGs' : Fin m' → Program := fun i => pGs i.castSucc
-    have hPrefix_eq : List.foldl (fun x y => Program.concat x (gPhase base n (pGs y.castSucc) ↑y.castSucc))
-        [] (List.finRange m') = allGPhases m' n base pGs' := rfl
-    rw [hPrefix_eq]
+    have hAllGPhases_succ : allGPhases (m' + 1) n base pGs =
+        (allGPhases m' n base pGs').concat (gPhase base n (pGs (Fin.last m')) m') := by
+      simp only [allGPhases, gPhaseList]
+      rw [List.finRange_succ_last, List.map_append, List.map_singleton, List.prod_append, List.prod_singleton]
+      show (Program.concat _ _) = (Program.concat _ _)
+      simp only [List.map_map, Fin.val_last, Function.comp_def]
+      rfl
+    rw [hAllGPhases_succ]
     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)
@@ -144,20 +150,23 @@ theorem allGPhases_suffix_preserves_earlier_results {m n base : ℕ} {pGs : Fin
     (hhalted : c'.isHalted (allGPhases_suffix m n base pGs start)) :
     c'.state.read (base + n + 1 + k) = s.read (base + n + 1 + k) := by
   match m with
-  | 0 => simp only [allGPhases_suffix, List.finRange_zero, List.drop_nil, List.foldl_nil] at hsteps hhalted
-         rw [Steps.halts_unique hsteps hhalted Relation.ReflTransGen.refl (by simp)]
+  | 0 =>
+    have hSuffix_zero : allGPhases_suffix 0 n base pGs start = [] := by
+      simp only [allGPhases_suffix, gPhaseList, List.finRange_zero, List.drop_nil, List.map_nil, List.prod_nil]; rfl
+    simp only [hSuffix_zero] at hsteps hhalted
+    rw [Steps.halts_unique hsteps hhalted Relation.ReflTransGen.refl (by simp)]
   | Nat.succ m' =>
     by_cases hEmpty : start ≥ m' + 1
     · have hSuffix_empty : allGPhases_suffix (m' + 1) n base pGs start = [] := by
-        simp only [allGPhases_suffix]; rw [List.drop_eq_nil_of_le (by simp; omega)]; rfl
+        simp only [allGPhases_suffix, gPhaseList]
+        rw [List.drop_eq_nil_of_le (by simp; omega)]
+        rfl
       rw [hSuffix_empty] at hsteps hhalted
       rw [Steps.halts_unique hsteps hhalted Relation.ReflTransGen.refl (by simp)]
     · push_neg at hEmpty
       have hSuffix_decomp : allGPhases_suffix (m' + 1) n base pGs start =
-          (gPhase base n (pGs ⟨start, hEmpty⟩) start).concat (allGPhases_suffix (m' + 1) n base pGs (start + 1)) := by
-        simp only [allGPhases_suffix]
-        rw [List.drop_eq_getElem_cons (by simp; exact hEmpty), List.foldl_cons, foldl_concat_eq_acc_concat]
-        simp only [concat_nil_left, List.getElem_finRange]; congr 2
+          (gPhase base n (pGs ⟨start, hEmpty⟩) start).concat (allGPhases_suffix (m' + 1) n base pGs (start + 1)) :=
+        allGPhases_suffix_cons pGs start hEmpty
       rw [hSuffix_decomp] at hsteps hhalted
       let dFirst := decompose_concat hsteps hhalted (gPhase_isStandardForm (hpGs_sf ⟨start, hEmpty⟩))
       obtain ⟨cRest, hRest_steps, hRest_halted⟩ := dFirst.halts_right
@@ -198,11 +207,8 @@ theorem allGPhases_saves_result {m n : ℕ} [NeZero m] {pF : Program} {pGs : Fin
   obtain ⟨sSavePrefix, hSavePrefix_steps, cSuffix, hSuffix_steps, hSuffix_halted⟩ :=
     suffix_of_concat_from_zero hsteps hhalted hSavePrefix_sf
   have hPrefixDecomp : allGPhases_prefix m n base pGs (i.val + 1) =
-      (allGPhases_prefix m n base pGs i.val).concat (gPhase base n (pGs i) i.val) := by
-    simp only [allGPhases_prefix]
-    rw [List.take_succ_eq_append_getElem (by simp : i.val < (List.finRange m).length),
-        List.foldl_append, List.foldl_cons, List.foldl_nil, foldl_concat_eq_acc_concat]
-    simp only [List.getElem_finRange]; congr 1
+      (allGPhases_prefix m n base pGs i.val).concat (gPhase base n (pGs i) i.val) :=
+    allGPhases_prefix_succ pGs i.val i.isLt
   have hSavePrefixI_sf := hSave_sf.concat (allGPhases_prefix_isStandardForm (n := n) (base := base) hGs_sf i.val)
   have hSavePrefix_eq : saveInputs.concat (allGPhases_prefix m n base pGs (i.val + 1)) =
       (saveInputs.concat (allGPhases_prefix m n base pGs i.val)).concat (gPhase base n (pGs i) i.val) := by
@@ -229,7 +235,9 @@ theorem allGPhases_saves_result {m n : ℕ} [NeZero m] {pF : Program} {pGs : Fin
   have hSaved_i : ∀ k : ℕ, (hk : k < n) → sSavePrefixI.read (base + 1 + k) = inputs ⟨k, hk⟩ := by
     intro k hk
     by_cases hi_zero : i.val = 0
-    · simp only [hi_zero, allGPhases_prefix, List.take_zero, List.foldl_nil, concat_nil_right] at hSavePrefixI_steps
+    · have hPrefix_zero : allGPhases_prefix m n base pGs 0 = [] := by
+        simp only [allGPhases_prefix, gPhaseList, List.take_zero, List.map_nil, List.prod_nil]; rfl
+      simp only [hi_zero, hPrefix_zero, concat_nil_right] at hSavePrefixI_steps
       rw [show sSavePrefixI = cSave.state from
             congrArg Config.state (Steps.halts_unique hSavePrefixI_steps (by simp) hSave_steps' hSave_halted'),
           hSave_state_sSave, hAfterSave k hk]

Urm/Composition/Preservation.lean

@@ -137,18 +137,16 @@ theorem allGPhases_prefix_preserves_saved_inputs (m n base : ℕ) (pGs : Fin m 
   intro r hr_lo hr_hi
   induction k generalizing s s' c' with
   | zero =>
-    simp only [allGPhases_prefix, List.take_zero, List.foldl_nil] at hsteps hhalted
+    have hPrefix_zero : allGPhases_prefix m n base pGs 0 = [] := by
+      simp only [allGPhases_prefix, gPhaseList, List.take_zero, List.map_nil, List.prod_nil]; rfl
+    simp only [hPrefix_zero] at hsteps hhalted
     simp only [← hstate_eq, Steps.halts_unique hsteps hhalted (.refl _) (by simp)]
   | succ k' ih =>
     have hk'_lt : k' < m := Nat.lt_of_succ_le hk
     let k'_fin : Fin m := ⟨k', hk'_lt⟩
-    have htake_eq : (List.finRange m).take (k' + 1) = (List.finRange m).take k' ++ [k'_fin] := by
-      rw [List.take_add_one, getElem?_pos (List.finRange m) k' (by simp [hk'_lt]), Option.toList_some]
-      simp only [List.finRange, List.getElem_ofFn, k'_fin]
     have hPrefix_succ_eq : allGPhases_prefix m n base pGs (k' + 1) =
-        (allGPhases_prefix m n base pGs k').concat (gPhase base n (pGs k'_fin) k') := by
-      simp only [allGPhases_prefix]
-      rw [htake_eq, List.foldl_append, List.foldl_cons, List.foldl_nil]
+        (allGPhases_prefix m n base pGs k').concat (gPhase base n (pGs k'_fin) k') :=
+      allGPhases_prefix_succ pGs k' hk'_lt
     rw [hPrefix_succ_eq] at hsteps hhalted
     obtain ⟨sMid, hMid_steps, ⟨cGPhase, hGPhase_steps, hGPhase_halted⟩⟩ :=
       suffix_of_concat_from_zero hsteps hhalted (allGPhases_prefix_isStandardForm hpGs_sf k')

Urm/Composition/StandardForm.lean

@@ -24,18 +24,23 @@ theorem gPhase_isStandardForm {base n : ℕ} {pG : Program} {i : ℕ} (hG : pG.I
     ((copyRegisterRange_isStandardForm (base + 1) 0 n).concat
     (hG.concat (single_T_isStandardForm 0 (base + n + 1 + i))))
 
-private theorem foldl_preserves_isStandardForm {α : Type*} (l : List α) (f : Program → α → Program)
-    (hf : ∀ acc a, acc.IsStandardForm → (f acc a).IsStandardForm) (acc : Program) (hacc : acc.IsStandardForm) :
-    (l.foldl f acc).IsStandardForm := by
-  induction l generalizing acc with
-  | nil => exact hacc
-  | cons x xs ih => simp only [List.foldl_cons]; exact ih (f acc x) (hf acc x hacc)
+private theorem prod_preserves_isStandardForm (l : List Program)
+    (hl : ∀ p ∈ l, p.IsStandardForm) : l.prod.IsStandardForm := by
+  induction l with
+  | nil => exact straightLine_isStandardForm rfl
+  | cons x xs ih =>
+    rw [List.prod_cons]
+    show (x.concat xs.prod).IsStandardForm
+    exact Program.IsStandardForm.concat (hl x List.mem_cons_self)
+      (ih (fun p hp => hl p (List.mem_cons_of_mem x hp)))
 
 theorem allGPhases_isStandardForm {m n base : ℕ} {pGs : Fin m → Program}
     (hGs : ∀ i, (pGs i).IsStandardForm) : (allGPhases m n base pGs).IsStandardForm := by
-  simp only [allGPhases]
-  exact foldl_preserves_isStandardForm _ _ (fun acc i hacc => hacc.concat (gPhase_isStandardForm (hGs i)))
-    [] (straightLine_isStandardForm rfl)
+  unfold allGPhases gPhaseList
+  exact prod_preserves_isStandardForm _ (fun p hp => by
+    simp only [List.mem_map] at hp
+    obtain ⟨i, _, rfl⟩ := hp
+    exact gPhase_isStandardForm (hGs i))
 
 theorem finalPhase_isStandardForm {m n base : ℕ} {pF : Program} (hF : pF.IsStandardForm) :
     (finalPhase m n base pF).IsStandardForm := by
@@ -52,15 +57,19 @@ theorem composeGeneral_isStandardForm {m n : ℕ} {pF : Program} {pGs : Fin m 
 
 theorem allGPhases_prefix_isStandardForm {m n base : ℕ} {pGs : Fin m → Program}
     (hGs : ∀ i, (pGs i).IsStandardForm) (k : ℕ) : (allGPhases_prefix m n base pGs k).IsStandardForm := by
-  simp only [allGPhases_prefix]
-  exact foldl_preserves_isStandardForm _ _ (fun acc j hacc => hacc.concat (gPhase_isStandardForm (hGs j)))
-    [] (straightLine_isStandardForm rfl)
+  unfold allGPhases_prefix gPhaseList
+  exact prod_preserves_isStandardForm _ (fun p hp => by
+    simp only [List.mem_map] at hp
+    obtain ⟨i, _, rfl⟩ := hp
+    exact gPhase_isStandardForm (hGs i))
 
 theorem allGPhases_suffix_isStandardForm {m n base : ℕ} {pGs : Fin m → Program}
     (hGs : ∀ i, (pGs i).IsStandardForm) (k : ℕ) : (allGPhases_suffix m n base pGs k).IsStandardForm := by
-  simp only [allGPhases_suffix]
-  exact foldl_preserves_isStandardForm _ _ (fun acc j hacc => hacc.concat (gPhase_isStandardForm (hGs j)))
-    [] (straightLine_isStandardForm rfl)
+  unfold allGPhases_suffix gPhaseList
+  exact prod_preserves_isStandardForm _ (fun p hp => by
+    simp only [List.mem_map] at hp
+    obtain ⟨i, _, rfl⟩ := hp
+    exact gPhase_isStandardForm (hGs i))
 
 theorem saveInputs_isStandardForm (base n : ℕ) : (copyRegisterRange 0 (base + 1) n).IsStandardForm :=
   copyRegisterRange_isStandardForm 0 (base + 1) n

Urm/Concat.lean

@@ -6,6 +6,7 @@ Authors: Jesse Alama
 
 import Urm.Execution
 import Urm.StraightLine
+import Mathlib.Algebra.Group.Defs
 
 /-! # Program Concatenation
 
@@ -82,6 +83,22 @@ theorem concat_assoc (p1 p2 p3 : Program) :
   | T m n => simp [Instr.shiftJumps]
   | J m n q => simp [Instr.shiftJumps]; omega
 
+/-- Program concatenation forms a semigroup.
+Note: This uses `concat` (which shifts jumps), not raw list append. -/
+instance : Semigroup Program where
+  mul := concat
+  mul_assoc := concat_assoc
+
+/-- Program concatenation forms a monoid with empty program as identity. -/
+instance : Monoid Program where
+  one := []
+  one_mul := concat_nil_left
+  mul_one := concat_nil_right
+
+/-- Relates `.concat` to `*` for algebraic automation.
+Use with `simp only [concat_eq_mul, mul_assoc]` to leverage Monoid associativity. -/
+theorem concat_eq_mul (p q : Program) : p.concat q = p * q := rfl
+
 /-- Get instruction from concatenated program in the first part. -/
 theorem getInstr_concat_left {p1 p2 : Program} (i : ℕ) (hi : i < p1.length) :
     (p1.concat p2).getInstr i = p1.getInstr i := by