-----Description----- 
This task requires writing a Lean 4 method that replaces every occurrence of a specified character within a string with a new character. The output should be a new string that maintains the same length as the input string, with all instances of the designated character replaced by the given substitute, and all other characters preserved unchanged.

-----Input-----
The input consists of:
s: A string in which the replacement will occur.
oldChar: The character within the string that needs to be replaced.
newChar: The character that will substitute for every occurrence of oldChar.

-----Output-----
The output is a string that meets the following:
- It has the same length as the input string.
- All occurrences of oldChar in the input string are replaced with newChar.
- All characters other than oldChar remain unchanged.

-----Note-----
There are no preconditions; the method will always work. It is assumed that the input string is valid and non-null.
Difficulty: basic

Lean 4 solution:
-- !benchmark @start import type=solution

-- !benchmark @end import

-- !benchmark @start solution_aux

-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

-- !benchmark @end precond_aux

@[reducible, simp]
def replaceChars_precond (s : String) (oldChar : Char) (newChar : Char) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def replaceChars (s : String) (oldChar : Char) (newChar : Char) (h_precond : replaceChars_precond (s) (oldChar) (newChar)) : String :=
  -- !benchmark @start code
  let cs := s.toList
  let cs' := cs.map (fun c => if c = oldChar then newChar else c)
  String.mk cs'
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def replaceChars_postcond (s : String) (oldChar : Char) (newChar : Char) (result: String) (h_precond : replaceChars_precond (s) (oldChar) (newChar)) :=
  -- !benchmark @start postcond
  let cs := s.toList
  let cs' := result.toList
  result.length = s.length ∧
  (∀ i, i < cs.length →
    (cs[i]! = oldChar → cs'[i]! = newChar) ∧
    (cs[i]! ≠ oldChar → cs'[i]! = cs[i]!))
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem replaceChars_spec_satisfied (s: String) (oldChar: Char) (newChar: Char) (h_precond : replaceChars_precond (s) (oldChar) (newChar)) :
    replaceChars_postcond (s) (oldChar) (newChar) (replaceChars (s) (oldChar) (newChar) h_precond) h_precond := by
  -- !benchmark @start proof
  -- Unfold the definitions of replaceChars and replaceChars_postcond
  unfold replaceChars replaceChars_postcond
  -- Split the goal into two parts
  constructor
  · -- First part: length is preserved
    simp [String.length]
  · -- Second part: character replacement specification
    simp_all
  -- !benchmark @end proof


Tests:
input: s: hello, world!
oldChar: ,
newChar: ;
s: a,b.c
oldChar: ,
newChar: :
s: hello, world!
oldChar: o
newChar: O
oldChar: x
newChar: y
s: test
oldChar: x
newChar: y
s: unchanged
oldChar: u
newChar: u
s: aaa
oldChar: a
newChar: b
expected: hello; world!
a:b.c
hellO, wOrld!
test
unchanged
bbb
unexpected: hello, world!
hello world!
hello;world!
a,b.c
a;b.c
ab:c
hello, world!
hellO, world!
hello, wOrld!
 
abc
testy
tset
yxest
nchanged
unchanged!
unchangEd
aaa
abb
bba

Inputs rejected by the precondition: