13. Lists, Basic properties, Monoid

18/11/22

set_option pp.structure_projections false

#check [1,2,3]

#check [tt,ff]

--#check [1,tt]
#check [[1,2],[3,4,5]]

#check [] -- empty list
-- nill  
-- LISP, first funcitonal language
#check 1::[2,3]
-- cons 

namespace mylists

-- inductive list(A : Type)
-- | nil : list
-- | cons : A → list → list


open list

local notation (name := cons)
  a :: l := cons a l

#check (1 :: 2 :: 3 :: nil)

variables {A B C : Type} -- {} make things more curly (implicet type)
open list

example : ∀ a:A, ∀ as:list A, [] ≠ a :: as :=
begin
  assume a as h,
  contradiction,
end

def tl : list A → list A
| [] := []
| (a :: as) := as

example : ∀ a b : A, ∀ as bs : list A, a :: as = b :: bs → as = bs :=
begin
  assume a b as bs eq,
  change (tl (a :: as) = bs),
  rw eq,
  refl,
end

example : ∀ a b : A, ∀ as bs : list A, a :: as = b :: bs → as = bs :=
begin
  assume a b as bs eq,
  injection eq,
end

/-
def hd : list A → A
| [] := sorry
| (a :: as) := a
-/

example : ∀ a b : A, ∀ as bs : list A, a :: as = b :: bs → a = b :=
begin
  assume a b as bs eq,
  injection eq,
  -- Challenge: Without the use of injeciton
end

#eval ([1,2,3] ++ [4,5])


def app' : list A → list A → list A 
| as [] := as
| as (b :: bs) := b :: (app' as bs)


#eval (app' [1,2,3] [4,5])

def app : list A → list A → list A
| [] as := as
| (b :: bs) as := b :: (app bs as)

#eval (app [1,2,3] [4,5])

theorem lneutr : ∀ as : list A, [] ++ as = as :=
begin
  assume as,
  dsimp[(++)],
  refl,
end

theorem rneutr : ∀ as : list A, as ++ [] = as :=
begin
  assume as,
  induction as with a as' ih,
  dsimp[(++)],
  refl,
  dsimp[(++)],
  dsimp[(++)] at ih,
  rw ih,
end

theorem assoc : ∀ as bs cs : list A, (as ++ bs) ++ cs == as ++ (bs ++ cs) :=
begin
  assume as bs cs,
  sorry,
end
  
end mylists