Mercurial > hg > Members > atton > agda-proofs

annotate systemF/int.agda @ 77:a2e6f61d5f2b default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add modus-ponens
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Thu, 09 Feb 2017 06:32:03 +0000
parents 4c1a6ce23f9e
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
2
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 module int where
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Relation.Binary.PropositionalEquality
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Level
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import systemF
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 -- define values
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 one : {l : Level} {U : Set l} -> Int {l} {U}
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 one = S O
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 two : {l : Level} {U : Set l} -> Int {l} {U}
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 two = S (S O)
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 three : {l : Level} {U : Set l} -> Int {l} {U}
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 three = S (S (S O))
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 four : {l : Level} {U : Set l} -> Int {l} {U}
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 four = S (S (S (S O)))
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 five : {l : Level} {U : Set l} -> Int {l} {U}
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 five = S (S (S (S (S O))))
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 six : {l : Level} {U : Set l} -> Int {l} {U}
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 six = S (S (S (S (S (S O)))))
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 seven : {l : Level} {U : Set l} -> Int {l} {U}
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 seven = S (S (S (S (S (S (S O))))))
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 eight : {l : Level} {U : Set l} -> Int {l} {U}
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 eight = S (S (S (S (S (S (S (S O)))))))
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 nine : {l : Level} {U : Set l} -> Int {l} {U}
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 nine = S (S (S (S (S (S (S (S (S O))))))))
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 ten : {l : Level} {U : Set l} -> Int {l} {U}
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 ten = S (S (S (S (S (S (S (S (S O))))))))
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 -- add
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 add : {l : Level} {U : Set l} -> Int -> Int -> Int
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 add {l} {U} a b = \(x : U) -> \(y : (U -> U)) -> a (b x y) y
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 add-r : {l : Level} {U : Set l} -> Int -> Int -> Int {{!!}} {{!!}}
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 add-r {l} {U} a b = \z -> \s -> (R (R z (\x -> \_ -> s x) a) (\x -> \_ -> s x) b)
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 lemma-same-add : {l : Level} {U : Set l} -> add ≡ add-r {_} {U}
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 lemma-same-add = refl
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 lemma-add-zero-zero : {l : Level} {U : Set l} -> add O O ≡ O {_} {U}
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 lemma-add-zero-zero = refl
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 lemma-add-one-two : {l : Level} {U : Set l} -> add one two ≡ three {_} {U}
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 lemma-add-one-two = refl
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 --lemma-add-swap : {l : Level} {U : Set l} {a b : Int} -> add a b ≡ add b a
4c1a6ce23f9e Migrate systemF from atton/agda/systemF (32:fe231950824a)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 --lemma-add-swap = refl