view agda/list.agda @ 129:d57c88171f38

Prove assciation-law for DeltaM on (S O)
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 03 Feb 2015 12:42:28 +0900
parents 743c05b98dad
children
line wrap: on
line source

module list where

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

infixr 40 _::_
data  List {l : Level} (A : Set l) : (Set l)where
   [] : List A
   _::_ : A -> List A -> List A


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

[[_]] : {l : Level} {A : Set l} -> A -> List A
[[ x ]] = x :: []


empty-append : {l : Level} {A : Set l} -> (xs : List A) -> xs ++ [] ≡ [] ++ xs
empty-append [] = refl
empty-append (x :: xs) = begin
    x :: (xs ++ [])
  ≡⟨ cong (_::_ x) (empty-append xs) ⟩
    x :: xs



list-associative : {l : Level} {A : Set l} -> (a b c : List A) -> (a ++ (b ++ c)) ≡ ((a ++ b) ++ c)
list-associative [] b c = refl
list-associative (x :: a) b c = cong (_::_ x) (list-associative a b c)