Help on a List Proof

Stream: new members

[Colin ⚛️]

I need help working on a proof dealing with the injectivity of a function that inputs a list and outputs a list. An example of what I'm working on is below.

import Mathlib

open Function

def addOne (L : List Nat) :=
  match L with
  | [] => []
  | head :: tail => [head + 1] ++ addOne tail

#eval addOne [1,2,3]

example : Injective addOne := by
  dsimp only [Injective]
  rintro L₁ L₂
  sorry

I believe this is true because there exists at least one element in L1 (labelled n) that does not equate to an element in an equal position in L2 (labelled m) and will evaluate with a different output for n + 1 \= m+1 if n \= m. I don't know how to translate this logic into Lean, however.

[Johannes Tantow]

import Mathlib

open Function

def addOne (L : List Nat) :=
  match L with
  | [] => []
  | head :: tail => [head + 1] ++ addOne tail


theorem addOne_eq : addOne  = List.map (fun x => x + 1) := by
  funext L
  induction L with
  | nil => simp [addOne]
  | cons hd tl ih => simp [addOne, ih]

#eval addOne [1,2,3]

example : Injective addOne := by
  simp [addOne_eq, List.map_injective_iff, add_left_injective]