changeset 27:7b0f2025112b

Define Add on Int
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 28 Apr 2014 11:30:09 +0900
parents 852798763d56
children 02926d953ef7
files int.agda systemF.agda
diffstat 2 files changed, 60 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/int.agda	Mon Apr 28 11:30:09 2014 +0900
@@ -0,0 +1,58 @@
+module int where
+
+open import Relation.Binary.PropositionalEquality
+open import Level
+open import systemF
+
+-- define values
+
+one : {l : Level} {U : Set l} -> Int {l} {U}
+one = S O
+
+two : {l : Level} {U : Set l} -> Int {l} {U}
+two = S (S O)
+
+three : {l : Level} {U : Set l} -> Int {l} {U}
+three = S (S (S O))
+
+four : {l : Level} {U : Set l} -> Int {l} {U}
+four = S (S (S (S O)))
+
+five : {l : Level} {U : Set l} -> Int {l} {U}
+five = S (S (S (S (S O))))
+
+six : {l : Level} {U : Set l} -> Int {l} {U}
+six =  S (S (S (S (S (S O)))))
+
+seven : {l : Level} {U : Set l} -> Int {l} {U}
+seven = S (S (S (S (S (S (S O))))))
+
+eight : {l : Level} {U : Set l} -> Int {l} {U}
+eight = S (S (S (S (S (S (S (S O)))))))
+
+nine : {l : Level} {U : Set l} -> Int {l} {U}
+nine = S (S (S (S (S (S (S (S (S O))))))))
+
+ten : {l : Level} {U : Set l} -> Int {l} {U}
+ten = S (S (S (S (S (S (S (S (S O))))))))
+
+
+-- add
+
+add : {l : Level} {U : Set l} -> Int -> Int -> Int
+add {l} {U} a b = \(x : U) -> \(y : (U -> U)) -> a (b x y) y
+
+add-r : {l : Level} {U : Set l} -> Int -> Int -> Int
+add-r {l} {U} a b = R a (\x -> \n -> S x) b
+
+lemma-same-add : {l : Level} {U : Set l} -> add ≡ add-r {l} {U}
+lemma-same-add = refl
+
+lemma-add-zero-zero : {l : Level} {U : Set l} -> add O O ≡ O {_} {U}
+lemma-add-zero-zero = refl
+
+lemma-add-one-two : {l : Level} {U : Set l} -> add one two ≡ three {_} {U}
+lemma-add-one-two = refl
+
+--lemma-add-swap : {l : Level} {U : Set l} {a b : Int}  -> add a b ≡ add b a
+--lemma-add-swap = refl
--- a/systemF.agda	Tue Apr 22 11:11:50 2014 +0900
+++ b/systemF.agda	Mon Apr 28 11:30:09 2014 +0900
@@ -213,3 +213,5 @@
 
 lemma-tree-it-collect : {l : Level} {U W : Set l} {w : W} {h : (U -> W) -> W} {f : U -> Tree U} -> (TreeIt w h (collect f)) ≡ (h (\(x : U) -> TreeIt w h (f x)))
 lemma-tree-it-collect = refl
+
+