Merge main into nightly-testing

Author: mathlib-nightly-testing[bot]

Cslib/Computability/Languages/ExampleEventuallyZero.lean

@@ -26,22 +26,22 @@ namespace Cslib.ωLanguage.Example
 
 open scoped LTS NA
 
-/-- A sequence `xs` is in `eventually_zero` iff `xs k = 0` for all large `k`. -/
+/-- A sequence `xs` is in `eventuallyZero` iff `xs k = 0` for all large `k`. -/
 @[scoped grind =]
-def eventually_zero : ωLanguage (Fin 2) :=
+def eventuallyZero : ωLanguage (Fin 2) :=
   { xs : ωSequence (Fin 2) | ∀ᶠ k in atTop, xs k = 0 }
 
-/-- `eventually_zero` is accepted by a 2-state nondeterministic Buchi automaton. -/
+/-- `eventuallyZero` is accepted by a 2-state nondeterministic Buchi automaton. -/
 @[scoped grind =]
-def eventually_zero_na : NA.Buchi (Fin 2) (Fin 2) where
+def eventuallyZeroNa : NA.Buchi (Fin 2) (Fin 2) where
   -- Once state 1 is reached, only symbol 0 is accepted and the next state is still 1
   Tr s x s' := s = 1 → x = 0 ∧ s' = 1
   start := {0}
   accept := {1}
 
-theorem eventually_zero_accepted_by_na_buchi :
-    language eventually_zero_na = eventually_zero := by
-  ext xs; unfold eventually_zero_na; constructor
+theorem eventuallyZero_accepted_by_na_buchi :
+    language eventuallyZeroNa = eventuallyZero := by
+  ext xs; unfold eventuallyZeroNa; constructor
   · rintro ⟨ss, h_run, h_acc⟩
     obtain ⟨m, h_m⟩ := Frequently.exists h_acc
     apply eventually_atTop.mpr
@@ -61,27 +61,27 @@ theorem eventually_zero_accepted_by_na_buchi :
       grind
 
 private lemma extend_by_zero (u : List (Fin 2)) :
-    u ++ω const 0 ∈ eventually_zero := by
+    u ++ω const 0 ∈ eventuallyZero := by
   apply eventually_atTop.mpr
   use u.length
   grind [get_append_right']
 
 private lemma extend_by_one (u : List (Fin 2)) :
-    ∃ v, 1 ∈ v ∧ u ++ v ++ω const 0 ∈ eventually_zero := by
+    ∃ v, 1 ∈ v ∧ u ++ v ++ω const 0 ∈ eventuallyZero := by
   use [1]
   grind [extend_by_zero]
 
-private lemma extend_by_hyp {l : Language (Fin 2)} (h : l↗ω = eventually_zero)
+private lemma extend_by_hyp {l : Language (Fin 2)} (h : l↗ω = eventuallyZero)
     (u : List (Fin 2)) : ∃ v, 1 ∈ v ∧ u ++ v ∈ l := by
   obtain ⟨v, _, h_pfx⟩ := extend_by_one u
   rw [← h] at h_pfx
   have := frequently_atTop.mp h_pfx (u ++ v).length
   grind [extract_append_zero_right]
 
-private noncomputable def oneSegs {l : Language (Fin 2)} (h : l↗ω = eventually_zero) (n : ℕ) :=
+private noncomputable def oneSegs {l : Language (Fin 2)} (h : l↗ω = eventuallyZero) (n : ℕ) :=
   Classical.choose <| extend_by_hyp h (List.ofFn (fun k : Fin n ↦ oneSegs h k)).flatten
 
-private lemma oneSegs_lemma {l : Language (Fin 2)} (h : l↗ω = eventually_zero) (n : ℕ) :
+private lemma oneSegs_lemma {l : Language (Fin 2)} (h : l↗ω = eventuallyZero) (n : ℕ) :
     1 ∈ oneSegs h n ∧ (List.ofFn (fun k : Fin (n + 1) ↦ oneSegs h k)).flatten ∈ l := by
   let P u v := 1 ∈ v ∧ u ++ v ∈ l
   have : P ((List.ofFn (fun k : Fin n ↦ oneSegs h k)).flatten) (oneSegs h n) := by
@@ -92,13 +92,13 @@ private lemma oneSegs_lemma {l : Language (Fin 2)} (h : l↗ω = eventually_zero
   rw [List.ofFn_succ_last]
   simpa
 
-theorem eventually_zero_not_omegaLim :
-    ¬ ∃ l : Language (Fin 2), l↗ω = eventually_zero := by
+theorem eventuallyZero_not_omegaLim :
+    ¬ ∃ l : Language (Fin 2), l↗ω = eventuallyZero := by
   rintro ⟨l, h⟩
   let ls := ωSequence.mk (oneSegs h)
   have h_segs := oneSegs_lemma h
   have h_pos : ∀ k, (ls k).length > 0 := by grind
-  have h_ev : ls.flatten ∈ eventually_zero := by
+  have h_ev : ls.flatten ∈ eventuallyZero := by
     rw [← h, mem_omegaLim, frequently_iff_strictMono]
     use (fun k ↦ ls.cumLen (k + 1))
     constructor

Cslib/Computability/Languages/OmegaRegularLanguage.lean

@@ -61,11 +61,11 @@ where the automaton is not even required to be finite-state. -/
 theorem IsRegular.not_da_buchi :
   ∃ (Symbol : Type) (p : ωLanguage Symbol), p.IsRegular ∧
     ¬ ∃ (State : Type) (da : DA.Buchi State Symbol), language da = p := by
-  refine ⟨Fin 2, Example.eventually_zero, ?_, ?_⟩
-  · use Fin 2, inferInstance, Example.eventually_zero_na,
-      Example.eventually_zero_accepted_by_na_buchi
+  refine ⟨Fin 2, Example.eventuallyZero, ?_, ?_⟩
+  · use Fin 2, inferInstance, Example.eventuallyZeroNa,
+      Example.eventuallyZero_accepted_by_na_buchi
   · rintro ⟨State, ⟨da, acc⟩, _⟩
-    have := Example.eventually_zero_not_omegaLim
+    have := Example.eventuallyZero_not_omegaLim
     grind [DA.buchi_eq_finAcc_omegaLim]
 
 /-- The ω-limit of a regular language is ω-regular. -/

Cslib/Computability/Machines/SingleTapeTuring/Basic.lean

@@ -160,27 +160,27 @@ def haltCfg (tm : SingleTapeTM Symbol) (s : List Symbol) : tm.Cfg := ⟨none, Bi
 /--
 The space used by a configuration is the space used by its tape.
 -/
-def Cfg.space_used (tm : SingleTapeTM Symbol) (cfg : tm.Cfg) : ℕ := cfg.BiTape.space_used
+def Cfg.spaceUsed (tm : SingleTapeTM Symbol) (cfg : tm.Cfg) : ℕ := cfg.BiTape.spaceUsed
 
 @[scoped grind =]
-lemma Cfg.space_used_initCfg (tm : SingleTapeTM Symbol) (s : List Symbol) :
-    (tm.initCfg s).space_used = max 1 s.length := BiTape.space_used_mk₁ s
+lemma Cfg.spaceUsed_initCfg (tm : SingleTapeTM Symbol) (s : List Symbol) :
+    (tm.initCfg s).spaceUsed = max 1 s.length := BiTape.spaceUsed_mk₁ s
 
 @[scoped grind =]
-lemma Cfg.space_used_haltCfg (tm : SingleTapeTM Symbol) (s : List Symbol) :
-    (tm.haltCfg s).space_used = max 1 s.length := BiTape.space_used_mk₁ s
+lemma Cfg.spaceUsed_haltCfg (tm : SingleTapeTM Symbol) (s : List Symbol) :
+    (tm.haltCfg s).spaceUsed = max 1 s.length := BiTape.spaceUsed_mk₁ s
 
-lemma Cfg.space_used_step {tm : SingleTapeTM Symbol} (cfg cfg' : tm.Cfg)
-    (hstep : tm.step cfg = some cfg') : cfg'.space_used ≤ cfg.space_used + 1 := by
+lemma Cfg.spaceUsed_step {tm : SingleTapeTM Symbol} (cfg cfg' : tm.Cfg)
+    (hstep : tm.step cfg = some cfg') : cfg'.spaceUsed ≤ cfg.spaceUsed + 1 := by
   obtain ⟨_ | q, tape⟩ := cfg
   · simp [step] at hstep
   · simp only [step] at hstep
     generalize hM : tm.tr q tape.head = result at hstep
     obtain ⟨⟨wr, dir⟩, q''⟩ := result
     cases hstep; cases dir with
-    | none => simp [Cfg.space_used, BiTape.optionMove, BiTape.space_used_write, hM]
-    | some d => simpa [Cfg.space_used, BiTape.optionMove, BiTape.space_used_write, hM] using
-        BiTape.space_used_move (tape.write wr) d
+    | none => simp [Cfg.spaceUsed, BiTape.optionMove, BiTape.spaceUsed_write, hM]
+    | some d => simpa [Cfg.spaceUsed, BiTape.optionMove, BiTape.spaceUsed_write, hM] using
+        BiTape.spaceUsed_move (tape.write wr) d
 
 end Cfg
 
@@ -215,8 +215,8 @@ lemma output_length_le_input_length_add_time (tm : SingleTapeTM Symbol) (l l' :
     (h : tm.OutputsWithinTime l l' t) :
     l'.length ≤ max 1 l.length + t := by
   obtain ⟨steps, hsteps_le, hevals⟩ := h
-  grind [hevals.apply_le_apply_add (Cfg.space_used tm)
-      fun a b hstep ↦ Cfg.space_used_step a b (Option.mem_def.mp hstep)]
+  grind [hevals.apply_le_apply_add (Cfg.spaceUsed tm)
+      fun a b hstep ↦ Cfg.spaceUsed_step a b (Option.mem_def.mp hstep)]
 
 section Computers
 
@@ -392,15 +392,15 @@ structure TimeComputable (f : List Symbol → List Symbol) where
   /-- the underlying bundled SingleTapeTM -/
   tm : SingleTapeTM Symbol
   /-- a bound on runtime -/
-  time_bound : ℕ → ℕ
-  /-- proof this machine outputs `f` in at most `time_bound(input.length)` steps -/
-  outputsFunInTime (a) : tm.OutputsWithinTime a (f a) (time_bound a.length)
+  timeBound : ℕ → ℕ
+  /-- proof this machine outputs `f` in at most `timeBound(input.length)` steps -/
+  outputsFunInTime (a) : tm.OutputsWithinTime a (f a) (timeBound a.length)
 
 
 /-- The identity map on Symbol is computable in constant time. -/
 def TimeComputable.id : TimeComputable (Symbol := Symbol) id where
   tm := idComputer
-  time_bound _ := 1
+  timeBound _ := 1
   outputsFunInTime _ := ⟨1, le_rfl, RelatesInSteps.single rfl⟩
 
 /--
@@ -419,36 +419,36 @@ then the time bound for the second machine still holds for that shorter input to
 -/
 def TimeComputable.comp {f g : List Symbol → List Symbol}
     (hf : TimeComputable f) (hg : TimeComputable g)
-    (h_mono : Monotone hg.time_bound) :
+    (h_mono : Monotone hg.timeBound) :
     (TimeComputable (g ∘ f)) where
   tm := compComputer hf.tm hg.tm
   -- perhaps it would be good to track the blow up separately?
-  time_bound l := (hf.time_bound l) + hg.time_bound (max 1 l + hf.time_bound l)
+  timeBound l := (hf.timeBound l) + hg.timeBound (max 1 l + hf.timeBound l)
   outputsFunInTime a := by
     have hf_outputsFun := hf.outputsFunInTime a
     have hg_outputsFun := hg.outputsFunInTime (f a)
     simp only [OutputsWithinTime, initCfg, compComputer_q₀_eq, Function.comp_apply,
       haltCfg] at hg_outputsFun hf_outputsFun ⊢
-    -- The computer reduces a to f a in time hf.time_bound a.length
+    -- The computer reduces a to f a in time hf.timeBound a.length
     have h_a_reducesTo_f_a :
         RelatesWithinSteps (compComputer hf.tm hg.tm).TransitionRelation
           (initialCfg hf.tm hg.tm a)
           (intermediateCfg hf.tm hg.tm (f a))
-          (hf.time_bound a.length) :=
+          (hf.timeBound a.length) :=
       comp_left_relatesWithinSteps hf.tm hg.tm a (f a)
-        (hf.time_bound a.length) hf_outputsFun
-    -- The computer reduces f a to g (f a) in time hg.time_bound (f a).length
+        (hf.timeBound a.length) hf_outputsFun
+    -- The computer reduces f a to g (f a) in time hg.timeBound (f a).length
     have h_f_a_reducesTo_g_f_a :
         RelatesWithinSteps (compComputer hf.tm hg.tm).TransitionRelation
           (intermediateCfg hf.tm hg.tm (f a))
           (finalCfg hf.tm hg.tm (g (f a)))
-          (hg.time_bound (f a).length) :=
+          (hg.timeBound (f a).length) :=
       comp_right_relatesWithinSteps hf.tm hg.tm (f a) (g (f a))
-        (hg.time_bound (f a).length) hg_outputsFun
+        (hg.timeBound (f a).length) hg_outputsFun
     -- Therefore, the computer reduces a to g (f a) in the sum of those times.
     have h_a_reducesTo_g_f_a := RelatesWithinSteps.trans h_a_reducesTo_f_a h_f_a_reducesTo_g_f_a
     apply RelatesWithinSteps.of_le h_a_reducesTo_g_f_a
-    refine Nat.add_le_add_left ?_ (hf.time_bound a.length)
+    refine Nat.add_le_add_left ?_ (hf.timeBound a.length)
     · apply h_mono
       -- Use the lemma about output length being bounded by input length + time
       exact output_length_le_input_length_add_time hf.tm _ _ _ (hf.outputsFunInTime a)
@@ -478,7 +478,7 @@ structure PolyTimeComputable (f : List Symbol → List Symbol) extends TimeCompu
   /-- a polynomial time bound -/
   poly : Polynomial ℕ
   /-- proof that this machine outputs `f` in at most `time(input.length)` steps -/
-  bounds : ∀ n, time_bound n ≤ poly.eval n
+  bounds : ∀ n, timeBound n ≤ poly.eval n
 
 /-- A proof that the identity map on Symbol is computable in polytime. -/
 noncomputable def PolyTimeComputable.id : PolyTimeComputable (Symbol := Symbol) id where
@@ -493,7 +493,7 @@ A proof that the composition of two polytime computable functions is polytime co
 -/
 noncomputable def PolyTimeComputable.comp {f g : List Symbol → List Symbol}
     (hf : PolyTimeComputable f) (hg : PolyTimeComputable g)
-    (h_mono : Monotone hg.time_bound) :
+    (h_mono : Monotone hg.timeBound) :
     PolyTimeComputable (g ∘ f) where
   toTimeComputable := TimeComputable.comp hf.toTimeComputable hg.toTimeComputable h_mono
   poly := hf.poly + hg.poly.comp (1 + X + hf.poly)

Cslib/Computability/URM/StraightLine.lean

@@ -20,7 +20,7 @@ they always halt exactly at their length.
 ## Main results
 
 - `straight_line_halts`: straight-line programs always halt
-- `straightLine_finalState`: final state after running a straight-line program
+- `straightLinefinalState`: final state after running a straight-line program
 -/
 
 @[expose] public section
@@ -100,27 +100,27 @@ theorem straight_line_halts {p : Program} (hsl : p.IsStraightLine) (inputs : Lis
 
 /-- The halting state for a straight-line program starting from registers r.
 Wraps Classical.choose to hide it from the API. -/
-noncomputable def straightLine_finalState {p : Program}
+noncomputable def straightLinefinalState {p : Program}
     (hsl : p.IsStraightLine) (r : Regs) : State :=
   Classical.choose (straight_line_halts_from_regs hsl r)
 
-/-- Specification: the state from straightLine_finalState satisfies Steps, isHalted,
+/-- Specification: the state from straightLinefinalState satisfies Steps, isHalted,
 and has pc = p.length. -/
-theorem straightLine_finalState_spec {p : Program} (hsl : p.IsStraightLine) (r : Regs) :
-    let s := straightLine_finalState hsl r
+theorem straightLinefinalState_spec {p : Program} (hsl : p.IsStraightLine) (r : Regs) :
+    let s := straightLinefinalState hsl r
     Steps p ⟨0, r⟩ s ∧ s.isHalted p ∧ s.pc = p.length :=
   Classical.choose_spec (straight_line_halts_from_regs hsl r)
 
 /-- The final registers after running a straight-line program from given starting registers. -/
-noncomputable def straightLine_finalRegs {p : Program} (hsl : p.IsStraightLine) (r : Regs) : Regs :=
-  (straightLine_finalState hsl r).regs
+noncomputable def straightLineFinalRegs {p : Program} (hsl : p.IsStraightLine) (r : Regs) : Regs :=
+  (straightLinefinalState hsl r).regs
 
-/-- For a straight-line program, s.regs equals straightLine_finalRegs if halted from r. -/
-theorem straightLine_finalRegs_eq_of_halted {p : Program} (hsl : p.IsStraightLine)
+/-- For a straight-line program, s.regs equals straightLineFinalRegs if halted from r. -/
+theorem straightLineFinalRegs_eq_of_halted {p : Program} (hsl : p.IsStraightLine)
     (r : Regs) (s : State) (hsteps : Steps p ⟨0, r⟩ s) (hhalted : s.isHalted p) :
-    s.regs = straightLine_finalRegs hsl r :=
-  Steps.eq_of_halts hsteps hhalted (straightLine_finalState_spec hsl r).1
-    (straightLine_finalState_spec hsl r).2.1 ▸ rfl
+    s.regs = straightLineFinalRegs hsl r :=
+  Steps.eq_of_halts hsteps hhalted (straightLinefinalState_spec hsl r).1
+    (straightLinefinalState_spec hsl r).2.1 ▸ rfl
 
 /-- In a straight-line program, we can characterize the state at any intermediate pc.
 This gives us the state after executing instructions 0..pc-1. -/

Cslib/Foundations/Data/BiTape.lean

@@ -33,7 +33,7 @@ will not collide.
 * `BiTape`: A tape with a head symbol and left/right contents stored as `StackTape`
 * `BiTape.move`: Move the tape head left or right
 * `BiTape.write`: Write a symbol at the current head position
-* `BiTape.space_used`: The space used by the tape
+* `BiTape.spaceUsed`: The space used by the tape
 -/
 
 @[expose] public section
@@ -76,28 +76,28 @@ with the head under the first element of the list if it exists.
 def mk₁ (l : List Symbol) : BiTape Symbol :=
   match l with
   | [] => ∅
-  | h :: t => { head := some h, left := ∅, right := StackTape.map_some t }
+  | h :: t => { head := some h, left := ∅, right := StackTape.mapSome t }
 
 section Move
 
 /--
 Move the head left by shifting the left StackTape under the head.
 -/
-def move_left (t : BiTape Symbol) : BiTape Symbol :=
+def moveLeft (t : BiTape Symbol) : BiTape Symbol :=
   ⟨t.left.head, t.left.tail, StackTape.cons t.head t.right⟩
 
 /--
 Move the head right by shifting the right StackTape under the head.
 -/
-def move_right (t : BiTape Symbol) : BiTape Symbol :=
+def moveRight (t : BiTape Symbol) : BiTape Symbol :=
   ⟨t.right.head, StackTape.cons t.head t.left, t.right.tail⟩
 
 /--
 Move the head to the left or right, shifting the tape underneath it.
 -/
 def move (t : BiTape Symbol) : Dir → BiTape Symbol
-  | .left => t.move_left
-  | .right => t.move_right
+  | .left => t.moveLeft
+  | .right => t.moveRight
 
 /--
 Optionally perform a `move`, or do nothing if `none`.
@@ -107,12 +107,12 @@ def optionMove : BiTape Symbol → Option Dir → BiTape Symbol
   | t, some d => t.move d
 
 @[simp]
-lemma move_left_move_right (t : BiTape Symbol) : t.move_left.move_right = t := by
-  simp [move_right, move_left]
+lemma moveLeft_moveRight (t : BiTape Symbol) : t.moveLeft.moveRight = t := by
+  simp [moveRight, moveLeft]
 
 @[simp]
-lemma move_right_move_left (t : BiTape Symbol) : t.move_right.move_left = t := by
-  simp [move_left, move_right]
+lemma moveRight_moveLeft (t : BiTape Symbol) : t.moveRight.moveLeft = t := by
+  simp [moveLeft, moveRight]
 
 end Move
 
@@ -126,22 +126,22 @@ The space used by a `BiTape` is the number of symbols
 between and including the head, and leftmost and rightmost non-blank symbols on the `BiTape`.
 -/
 @[scoped grind]
-def space_used (t : BiTape Symbol) : ℕ := 1 + t.left.length + t.right.length
+def spaceUsed (t : BiTape Symbol) : ℕ := 1 + t.left.length + t.right.length
 
 @[simp, grind =]
-lemma space_used_write (t : BiTape Symbol) (a : Option Symbol) :
-    (t.write a).space_used = t.space_used := by rfl
+lemma spaceUsed_write (t : BiTape Symbol) (a : Option Symbol) :
+    (t.write a).spaceUsed = t.spaceUsed := by rfl
 
-lemma space_used_mk₁ (l : List Symbol) :
-    (mk₁ l).space_used = max 1 l.length := by
+lemma spaceUsed_mk₁ (l : List Symbol) :
+    (mk₁ l).spaceUsed = max 1 l.length := by
   cases l with
-  | nil => simp [mk₁, space_used, nil, StackTape.length_nil]
-  | cons h t => simp [mk₁, space_used, StackTape.length_nil, StackTape.length_map_some]; omega
+  | nil => simp [mk₁, spaceUsed, nil, StackTape.length_nil]
+  | cons h t => simp [mk₁, spaceUsed, StackTape.length_nil, StackTape.length_mapSome]; omega
 
-lemma space_used_move (t : BiTape Symbol) (d : Dir) :
-    (t.move d).space_used ≤ t.space_used + 1 := by
-  cases d <;> grind [move_left, move_right, move,
-    space_used, StackTape.length_tail_le, StackTape.length_cons_le]
+lemma spaceUsed_move (t : BiTape Symbol) (d : Dir) :
+    (t.move d).spaceUsed ≤ t.spaceUsed + 1 := by
+  cases d <;> grind [moveLeft, moveRight, move,
+    spaceUsed, StackTape.length_tail_le, StackTape.length_cons_le]
 
 end BiTape
 

Cslib/Foundations/Data/HasFresh.lean

@@ -44,7 +44,7 @@ instance HasFresh.to_infinite (α : Type u) [HasFresh α] : Infinite α := by
 
 /-- All infinite types have an associated (at least noncomputable) fresh function.
 This, in conjunction with `HasFresh.to_infinite`, characterizes `HasFresh`. -/
-noncomputable instance HasFresh.of_infinite (α : Type u) [Infinite α] : HasFresh α where
+noncomputable instance (α : Type u) [Infinite α] : HasFresh α where
   fresh s := Infinite.exists_notMem_finset s |>.choose
   fresh_notMem s := by grind