Mercurial > hg > Members > atton > agda-proofs

annotate moggi/moggi.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 36c9175d9adb
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
3
36c9175d9adb Migrate moggi from atton/agda/moggi (0:530373ccbcee)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 module moggi where
36c9175d9adb Migrate moggi from atton/agda/moggi (0:530373ccbcee)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
36c9175d9adb Migrate moggi from atton/agda/moggi (0:530373ccbcee)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3
36c9175d9adb Migrate moggi from atton/agda/moggi (0:530373ccbcee)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 postulate A : Set
36c9175d9adb Migrate moggi from atton/agda/moggi (0:530373ccbcee)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 postulate A1 : Set
36c9175d9adb Migrate moggi from atton/agda/moggi (0:530373ccbcee)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 postulate A2 : Set
36c9175d9adb Migrate moggi from atton/agda/moggi (0:530373ccbcee)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
36c9175d9adb Migrate moggi from atton/agda/moggi (0:530373ccbcee)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 postulate x : A
36c9175d9adb Migrate moggi from atton/agda/moggi (0:530373ccbcee)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 postulate e1 : A1
36c9175d9adb Migrate moggi from atton/agda/moggi (0:530373ccbcee)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 --postulate f : A1 -> A2
36c9175d9adb Migrate moggi from atton/agda/moggi (0:530373ccbcee)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
36c9175d9adb Migrate moggi from atton/agda/moggi (0:530373ccbcee)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 data _==_ : {A : Set} -> A -> A -> Set where
36c9175d9adb Migrate moggi from atton/agda/moggi (0:530373ccbcee)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 refl : {x : A} -> x == x
36c9175d9adb Migrate moggi from atton/agda/moggi (0:530373ccbcee)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 sym : {x y : A} -> x == y -> y == x
36c9175d9adb Migrate moggi from atton/agda/moggi (0:530373ccbcee)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 trans : {x y z : A} -> x == y -> y == z -> x == z
36c9175d9adb Migrate moggi from atton/agda/moggi (0:530373ccbcee)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 congr : {x y : A1} -> (f : A1 -> A2) -> x == y ->
36c9175d9adb Migrate moggi from atton/agda/moggi (0:530373ccbcee)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 f x == f y
36c9175d9adb Migrate moggi from atton/agda/moggi (0:530373ccbcee)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18
36c9175d9adb Migrate moggi from atton/agda/moggi (0:530373ccbcee)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 record Term (A : Set) : Set where
36c9175d9adb Migrate moggi from atton/agda/moggi (0:530373ccbcee)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 field
36c9175d9adb Migrate moggi from atton/agda/moggi (0:530373ccbcee)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 type : A
36c9175d9adb Migrate moggi from atton/agda/moggi (0:530373ccbcee)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 var : A -> (A -> A)
36c9175d9adb Migrate moggi from atton/agda/moggi (0:530373ccbcee)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 f : A1 -> A2
36c9175d9adb Migrate moggi from atton/agda/moggi (0:530373ccbcee)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 eq : (g1 : A1 -> A2) -> (g2 : A1 -> A2) -> g1 == g2
36c9175d9adb Migrate moggi from atton/agda/moggi (0:530373ccbcee)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25