Mercurial > hg > Members > atton > delta_monad

annotate agda/list.agda @ 31:33b386de3f56

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Proof list-associative
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Sat, 18 Oct 2014 13:38:29 +0900
parents 5ba82f107a95
children 743c05b98dad
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
25
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 module list where
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Relation.Binary.PropositionalEquality
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open ≡-Reasoning
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 infixr 40 _::_
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 data List (A : Set) : Set where
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 [] : List A
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 _::_ : A -> List A -> List A
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 infixl 30 _++_
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 _++_ : {A : Set} -> List A -> List A -> List A
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 [] ++ ys = ys
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 (x :: xs) ++ ys = x :: (xs ++ ys)
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16
26
5ba82f107a95 Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 25
diff changeset
17 [[_]] : {A : Set} -> A -> List A
5ba82f107a95 Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 25
diff changeset
18 [[ x ]] = x :: []
5ba82f107a95 Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 25
diff changeset
19
25
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 empty-append : {A : Set} -> (xs : List A) -> xs ++ [] ≡ [] ++ xs
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 empty-append [] = refl
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 empty-append (x :: xs) = begin
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 x :: (xs ++ [])
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 ≡⟨ cong (_::_ x) (empty-append xs) ⟩
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 x :: xs
31
33b386de3f56 Proof list-associative
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 26
diff changeset
27 ∎
33b386de3f56 Proof list-associative
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 26
diff changeset
28
33b386de3f56 Proof list-associative
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 26
diff changeset
29
33b386de3f56 Proof list-associative
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 26
diff changeset
30 list-associative : {A : Set} -> (a b c : List A) -> (a ++ (b ++ c)) ≡ ((a ++ b) ++ c)
33b386de3f56 Proof list-associative
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 26
diff changeset
31 list-associative [] b c = refl
33b386de3f56 Proof list-associative
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 26
diff changeset
32 list-associative (x :: a) b c = cong (_::_ x) (list-associative a b c)