f : Char → Char
l : List Char
⊢ (if h : atEnd { data := l ++ [] } { byteIdx := utf8Len l } = true then { data := l ++ [] }
    else
      let c := f (get { data := l ++ [] } { byteIdx := utf8Len l });
      let_fun this :=
        (_ :
          (endPos (set { data := l ++ [] } { byteIdx := utf8Len l } c)).byteIdx -
              (next (set { data := l ++ [] } { byteIdx := utf8Len l } c) { byteIdx := utf8Len l }).byteIdx <
            (endPos { data := l ++ [] }).byteIdx - { byteIdx := utf8Len l }.byteIdx);
      let s := set { data := l ++ [] } { byteIdx := utf8Len l } c;
      mapAux f (next s { byteIdx := utf8Len l }) s) =
    { data := l ++ List.map f [] }
f : Char → Char
l : List Char
⊢ mapAux f { byteIdx := utf8Len l } { data := l ++ [] } = { data := l ++ List.map f [] }
unfold mapAux
no goals
f : Char → Char
l : List Char
⊢ (if h : atEnd { data := l ++ [] } { byteIdx := utf8Len l } = true then { data := l ++ [] }
    else
      let c := f (get { data := l ++ [] } { byteIdx := utf8Len l });
      let_fun this :=
        (_ :
          (endPos (set { data := l ++ [] } { byteIdx := utf8Len l } c)).byteIdx -
              (next (set { data := l ++ [] } { byteIdx := utf8Len l } c) { byteIdx := utf8Len l }).byteIdx <
            (endPos { data := l ++ [] }).byteIdx - { byteIdx := utf8Len l }.byteIdx);
      let s := set { data := l ++ [] } { byteIdx := utf8Len l } c;
      mapAux f (next s { byteIdx := utf8Len l }) s) =
    { data := l ++ List.map f [] }
simp
f : Char → Char
l : List Char
c : Char
r : List Char
⊢ (if h : atEnd { data := l ++ c :: r } { byteIdx := utf8Len l } = true then { data := l ++ c :: r }
    else
      let c_1 := f (get { data := l ++ c :: r } { byteIdx := utf8Len l });
      let_fun this :=
        (_ :
          (endPos (set { data := l ++ c :: r } { byteIdx := utf8Len l } c_1)).byteIdx -
              (next (set { data := l ++ c :: r } { byteIdx := utf8Len l } c_1) { byteIdx := utf8Len l }).byteIdx <
            (endPos { data := l ++ c :: r }).byteIdx - { byteIdx := utf8Len l }.byteIdx);
      let s := set { data := l ++ c :: r } { byteIdx := utf8Len l } c_1;
      mapAux f (next s { byteIdx := utf8Len l }) s) =
    { data := l ++ List.map f (c :: r) }
f : Char → Char
l : List Char
c : Char
r : List Char
⊢ mapAux f { byteIdx := utf8Len l } { data := l ++ c :: r } = { data := l ++ List.map f (c :: r) }
unfold mapAux
f : Char → Char
l : List Char
c : Char
r : List Char
⊢ (let c_1 := f (get { data := l ++ c :: r } { byteIdx := utf8Len l });
    let_fun this :=
      (_ :
        (endPos (set { data := l ++ c :: r } { byteIdx := utf8Len l } c_1)).byteIdx -
            (next (set { data := l ++ c :: r } { byteIdx := utf8Len l } c_1) { byteIdx := utf8Len l }).byteIdx <
          (endPos { data := l ++ c :: r }).byteIdx - { byteIdx := utf8Len l }.byteIdx);
    let s := set { data := l ++ c :: r } { byteIdx := utf8Len l } c_1;
    mapAux f (next s { byteIdx := utf8Len l }) s) =
    { data := l ++ List.map f (c :: r) }
f : Char → Char
l : List Char
c : Char
r : List Char
⊢ (if h : atEnd { data := l ++ c :: r } { byteIdx := utf8Len l } = true then { data := l ++ c :: r }
    else
      let c_1 := f (get { data := l ++ c :: r } { byteIdx := utf8Len l });
      let_fun this :=
        (_ :
          (endPos (set { data := l ++ c :: r } { byteIdx := utf8Len l } c_1)).byteIdx -
              (next (set { data := l ++ c :: r } { byteIdx := utf8Len l } c_1) { byteIdx := utf8Len l }).byteIdx <
            (endPos { data := l ++ c :: r }).byteIdx - { byteIdx := utf8Len l }.byteIdx);
      let s := set { data := l ++ c :: r } { byteIdx := utf8Len l } c_1;
      mapAux f (next s { byteIdx := utf8Len l }) s) =
    { data := l ++ List.map f (c :: r) }
rw [dif_neg (by rw [atEnd_of_valid]; simp)]
f : Char → Char
l : List Char
c : Char
r : List Char
⊢ mapAux f { byteIdx := utf8Len l + csize (f c) } { data := l ++ f c :: r } = { data := l ++ f c :: List.map f r }
f : Char → Char
l : List Char
c : Char
r : List Char
⊢ (let c_1 := f (get { data := l ++ c :: r } { byteIdx := utf8Len l });
    let_fun this :=
      (_ :
        (endPos (set { data := l ++ c :: r } { byteIdx := utf8Len l } c_1)).byteIdx -
            (next (set { data := l ++ c :: r } { byteIdx := utf8Len l } c_1) { byteIdx := utf8Len l }).byteIdx <
          (endPos { data := l ++ c :: r }).byteIdx - { byteIdx := utf8Len l }.byteIdx);
    let s := set { data := l ++ c :: r } { byteIdx := utf8Len l } c_1;
    mapAux f (next s { byteIdx := utf8Len l }) s) =
    { data := l ++ List.map f (c :: r) }
simp [by simpa using (⟨
  set_of_valid l (c::r), get_of_valid l (c::r), next_of_valid l (f c) r⟩ : _∧_∧_)]
no goals
f : Char → Char
l : List Char
c : Char
r : List Char
⊢ mapAux f { byteIdx := utf8Len l + csize (f c) } { data := l ++ f c :: r } = { data := l ++ f c :: List.map f r }
simpa using mapAux_of_valid f (l++[f c]) r
f : Char → Char
l : List Char
c : Char
r : List Char
⊢ ¬c :: r = []
f : Char → Char
l : List Char
c : Char
r : List Char
⊢ ¬atEnd { data := l ++ c :: r } { byteIdx := utf8Len l } = true
rw [atEnd_of_valid]
no goals
f : Char → Char
l : List Char
c : Char
r : List Char
⊢ ¬c :: r = []
simp
no goals
f : Char → Char
l : List Char
c : Char
r : List Char
⊢ ?m.175154
simpa using (⟨
set_of_valid l (c::r), get_of_valid l (c::r), next_of_valid l (f c) r⟩ : _∧_∧_)