module tactics where

open  import  Ataca.Tactics
open  import  Relation.Binary.PropositionalEquality
open ≡-Reasoning
                                                  
open import Level


postulate a : Set
postulate b : Set
postulate c : Set


infixr 40 _::_
data  List {a} (A : Set a) : Set a where
   [] : List A
   _::_ : A → List A → List A


infixl 30 _++_
-- _++_ : {a : Level } → {A : Set a} → List A → List A → List A
_++_ : ∀ {a} {A : Set a} → List A → List A → List A
[]        ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)


l1 = a :: []
l2 = a :: b :: a :: c ::  []

l3 = l1 ++ l2

test1 : {a : Level} → {A : Set a } → List {a} A
test1 = []

list-id-l : { A : Set } → { x : List A} →  [] ++ x ≡ x
list-id-l = refl

list-id-r : { A : Set } → ( x : List A ) →  x ++ [] ≡ x
list-id-r [] =   refl
list-id-r (x :: xs) =  cong ( _::_ x ) ( list-id-r xs )


-- listAssoc : { A : Set } → { a b c : List A} →  ( ( a ++ b ) ++ c ) ≡ ( a ++ ( b ++ c ) )
-- listAssoc   = eq-reflection

list-assoc : {A : Set } → ( xs ys zs : List A ) →
     ( ( xs ++ ys ) ++ zs ) ≡ ( xs ++ ( ys ++ zs ) )
list-assoc  [] ys zs = refl
list-assoc  (x :: xs)  ys zs = cong  ( _::_ x ) ( list-assoc xs ys zs )