Theorem: elfToString_roundtrip (One.lean)

State before:
elf : List ℤ
⊢ stringToElf (elfToString elf) = elf
Tactic:
if h:elf = [] then
  simp only [h]
else
  unfold stringToElf elfToString
  rw [List.splitOn_intercalate, List.filter_eq_self.2, List.map_map]
  . unfold Function.comp
    simp only [String.toIntΔ_inv_IntreprΔ, List.map_id'']
  . simp only [List.mem_map', ne_eq, decide_not, Bool.not_eq_true', decide_eq_false_iff_not, forall_exists_index,
      and_imp, forall_apply_eq_imp_iff₂, Int.reprΔ_ne_nil, not_false_iff, implies_true, forall_const]
  . simp only [List.mem_map', forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
    intro a _
    apply Int.not_newline_mem_reprΔ
  . simp only [ne_eq, List.map_eq_nil, h, not_false_iff]
State after:
no goals

State before:
elf : List ℤ
h : elf = []
⊢ stringToElf (elfToString elf) = elf
Tactic:
simp only [h]
State after:
no goals

State before:
elf : List ℤ
h : ¬elf = []
⊢ stringToElf (elfToString elf) = elf
Tactic:
unfold stringToElf elfToString
State after:
elf : List ℤ
h : ¬elf = []
⊢ List.map String.toIntΔ
      (List.filter (fun x => decide (x ≠ []))
        (List.splitOn (Char.ofNat 10) (List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)))) =
    elf

State before:
elf : List ℤ
h : ¬elf = []
⊢ List.map String.toIntΔ
      (List.filter (fun x => decide (x ≠ []))
        (List.splitOn (Char.ofNat 10) (List.intercalate [Char.ofNat 10] (List.map Int.reprΔ elf)))) =
    elf
Tactic:
rw [List.splitOn_intercalate, List.filter_eq_self.2, List.map_map]
State after:
elf : List ℤ
h : ¬elf = []
⊢ List.map (String.toIntΔ ∘ Int.reprΔ) elf = elf

elf : List ℤ
h : ¬elf = []
⊢ ∀ (a : List Char), a ∈ List.map Int.reprΔ elf → decide (a ≠ []) = true

case hx
elf : List ℤ
h : ¬elf = []
⊢ ∀ (l : List Char), l ∈ List.map Int.reprΔ elf → ¬Char.ofNat 10 ∈ l

case hls
elf : List ℤ
h : ¬elf = []
⊢ List.map Int.reprΔ elf ≠ []

State before:
elf : List ℤ
h : ¬elf = []
⊢ List.map (String.toIntΔ ∘ Int.reprΔ) elf = elf

elf : List ℤ
h : ¬elf = []
⊢ ∀ (a : List Char), a ∈ List.map Int.reprΔ elf → decide (a ≠ []) = true

case hx
elf : List ℤ
h : ¬elf = []
⊢ ∀ (l : List Char), l ∈ List.map Int.reprΔ elf → ¬Char.ofNat 10 ∈ l

case hls
elf : List ℤ
h : ¬elf = []
⊢ List.map Int.reprΔ elf ≠ []
Tactic:
. unfold Function.comp
  simp only [String.toIntΔ_inv_IntreprΔ, List.map_id'']
State after:
elf : List ℤ
h : ¬elf = []
⊢ ∀ (a : List Char), a ∈ List.map Int.reprΔ elf → decide (a ≠ []) = true

case hx
elf : List ℤ
h : ¬elf = []
⊢ ∀ (l : List Char), l ∈ List.map Int.reprΔ elf → ¬Char.ofNat 10 ∈ l

case hls
elf : List ℤ
h : ¬elf = []
⊢ List.map Int.reprΔ elf ≠ []

State before:
elf : List ℤ
h : ¬elf = []
⊢ ∀ (a : List Char), a ∈ List.map Int.reprΔ elf → decide (a ≠ []) = true

case hx
elf : List ℤ
h : ¬elf = []
⊢ ∀ (l : List Char), l ∈ List.map Int.reprΔ elf → ¬Char.ofNat 10 ∈ l

case hls
elf : List ℤ
h : ¬elf = []
⊢ List.map Int.reprΔ elf ≠ []
Tactic:
. simp only [List.mem_map', ne_eq, decide_not, Bool.not_eq_true', decide_eq_false_iff_not, forall_exists_index,
    and_imp, forall_apply_eq_imp_iff₂, Int.reprΔ_ne_nil, not_false_iff, implies_true, forall_const]
State after:
case hx
elf : List ℤ
h : ¬elf = []
⊢ ∀ (l : List Char), l ∈ List.map Int.reprΔ elf → ¬Char.ofNat 10 ∈ l

case hls
elf : List ℤ
h : ¬elf = []
⊢ List.map Int.reprΔ elf ≠ []

State before:
case hx
elf : List ℤ
h : ¬elf = []
⊢ ∀ (l : List Char), l ∈ List.map Int.reprΔ elf → ¬Char.ofNat 10 ∈ l

case hls
elf : List ℤ
h : ¬elf = []
⊢ List.map Int.reprΔ elf ≠ []
Tactic:
. simp only [List.mem_map', forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
  intro a _
  apply Int.not_newline_mem_reprΔ
State after:
case hls
elf : List ℤ
h : ¬elf = []
⊢ List.map Int.reprΔ elf ≠ []

State before:
case hls
elf : List ℤ
h : ¬elf = []
⊢ List.map Int.reprΔ elf ≠ []
Tactic:
. simp only [ne_eq, List.map_eq_nil, h, not_false_iff]
State after:
no goals