List.lean

@[simp]
def take : List Nat -> Nat -> List Nat 
| [], _ => [] 
| _ , 0 => [] 
| h :: t, (Nat.succ n) => h :: take t n 

@[simp]
def drop : List Nat -> Nat -> List Nat 
| [], _ => []
| hs, 0 => hs 
| _ :: t, (Nat.succ n) => drop t n


theorem take_drop_preserve_list : 
  ∀ (ls : List Nat) (n : Nat), take ls n ++ drop ls n = ls := by 
  intro ls
  induction ls with 
  | nil => simp
  | cons lsh lstl IHl => 
    intro n
    cases n with 
    | zero => simp 
    | succ n => 
      simp 
      exact (IHl n) 

inductive is_prefix : List Nat -> List Nat -> Prop 
| base_case (l : List Nat) : is_prefix [] l 
| ind_case (x : Nat) (m l : List Nat ) : 
  is_prefix m l -> is_prefix (x :: m) (x :: l)

theorem take_computes_is_prefix : 
  ∀ (ls : List Nat) (n : Nat) , is_prefix (take ls n) ls := by 
  intro ls
  induction ls with 
  | nil => 
    intro n 
    simp 
    apply is_prefix.base_case 
  | cons lshd lstl IHl =>
    intro n
    cases n with 
    | zero => 
      simp 
      apply is_prefix.base_case 
    | succ n =>
      simp
      apply is_prefix.ind_case
      apply IHl 
  
inductive is_postfix : List Nat -> List Nat -> Prop 
| base_case (l : List Nat) : is_postfix l l 
| ind_case (x : Nat) (m l : List Nat) : 
  is_postfix m l -> is_postfix m (x :: l)


theorem drop_computes_is_postfix : 
  ∀ (ls : List Nat) (n : Nat) , is_postfix (drop ls n) ls := by
  intro ls
  induction ls with 
  | nil => 
    intro n 
    simp 
    apply is_postfix.base_case 
  | cons lshd lstl IHl =>
    intro n
    cases n with 
    | zero => 
      simp 
      apply is_postfix.base_case 
    | succ n =>
      simp 
      apply is_postfix.ind_case
      apply IHl 


/-

-/
inductive step_comp : List Nat -> List Nat -> List Nat -> Prop 
| base_case (l : List Nat) : step_comp [] l l
| ind_case (x : Nat) (l m r : List Nat) : 
  step_comp l m r -> step_comp (x :: l) m (x :: r)


theorem take_drop_step_comp : 
  ∀ (ls : List Nat) (n : Nat) , step_comp (take ls n) (drop ls n) ls := by
  intro ls 
  induction ls with 
  | nil => 
    intro n
    simp 
    apply step_comp.base_case
  | cons lshd lstl ih =>
    intro n
    cases n with 
    | zero =>
      simp
      apply step_comp.base_case 
    | succ n => 
      simp 
      apply step_comp.ind_case
      apply ih