mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-10-26 08:09:22 +03:00
Merge branch 'master' of github.com:uwu-tech/kind
This commit is contained in:
commit
eb3b3ee5d5
@ -3,4 +3,14 @@ Bits.concat(a: Bits, b: Bits): Bits
|
||||
e: b,
|
||||
o: Bits.o(Bits.concat(a.pred, b)),
|
||||
i: Bits.i(Bits.concat(a.pred, b))
|
||||
}
|
||||
}
|
||||
|
||||
Bits.concat.tail(a: Bits, b: Bits): Bits
|
||||
case a {
|
||||
e: b,
|
||||
o: Bits.concat.tail(a.pred, Bits.o(b))
|
||||
i: Bits.concat.tail(a.pred, Bits.i(b))
|
||||
}
|
||||
|
||||
Bits.concat.go(a : Bits, b : Bits) : Bits
|
||||
Bits.concat.tail(Bits.reverse(a), b)
|
||||
|
65
base/Bits/hex_tail.kind
Normal file
65
base/Bits/hex_tail.kind
Normal file
@ -0,0 +1,65 @@
|
||||
Bits.hex_tail.encode(x: Bits): String
|
||||
String.reverse(Bits.hex_tail.encode.go(x, ""))
|
||||
|
||||
Bits.hex_tail.encode.go(x: Bits, str: String): String
|
||||
case x {
|
||||
e: str
|
||||
o: case x.pred as x {
|
||||
e: Bits.hex_tail.encode.go(x.pred, "0" | str)
|
||||
o: case x.pred as x {
|
||||
e: Bits.hex_tail.encode.go(x.pred, "0" | str)
|
||||
o: case x.pred as x {
|
||||
e: Bits.hex_tail.encode.go(x.pred, "0" | str)
|
||||
o: Bits.hex_tail.encode.go(x.pred, "0" | str)
|
||||
i: Bits.hex_tail.encode.go(x.pred, "8" | str)
|
||||
}
|
||||
i: case x.pred as x {
|
||||
e: "4" | str
|
||||
o: Bits.hex_tail.encode.go(x.pred, "4" | str)
|
||||
i: Bits.hex_tail.encode.go(x.pred, "c" | str)
|
||||
}
|
||||
}
|
||||
i: case x.pred as x {
|
||||
e: "2" | str
|
||||
o: case x.pred as x {
|
||||
e: "2" | str
|
||||
o: Bits.hex_tail.encode.go(x.pred, "2" | str)
|
||||
i: Bits.hex_tail.encode.go(x.pred, "a" | str)
|
||||
}
|
||||
i: case x.pred as x {
|
||||
e: "6" | str
|
||||
o: Bits.hex_tail.encode.go(x.pred, "6" | str)
|
||||
i: Bits.hex_tail.encode.go(x.pred, "e" | str)
|
||||
}
|
||||
}
|
||||
}
|
||||
i: case x.pred as x {
|
||||
e: "1" | str
|
||||
o: case x.pred as x {
|
||||
e: "1" | str
|
||||
o: case x.pred as x {
|
||||
e: "1" | str
|
||||
o: Bits.hex_tail.encode.go(x.pred, "1" | str)
|
||||
i: Bits.hex_tail.encode.go(x.pred, "9" | str)
|
||||
}
|
||||
i: case x.pred as x {
|
||||
e: "5" |str
|
||||
o: Bits.hex_tail.encode.go(x.pred, "5" | str)
|
||||
i: Bits.hex_tail.encode.go(x.pred, "d" | str)
|
||||
}
|
||||
}
|
||||
i: case x.pred as x {
|
||||
e: "3" | str
|
||||
o: case x.pred as x {
|
||||
e: "3" | str
|
||||
o: Bits.hex_tail.encode.go(x.pred, "3" | str)
|
||||
i: Bits.hex_tail.encode.go(x.pred, "b" | str)
|
||||
}
|
||||
i: case x.pred as x {
|
||||
e: "7" | str
|
||||
o: Bits.hex_tail.encode.go(x.pred, "7" | str)
|
||||
i: Bits.hex_tail.encode.go(x.pred, "f" | str)
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
2
base/Bits/pad_right.kind
Normal file
2
base/Bits/pad_right.kind
Normal file
@ -0,0 +1,2 @@
|
||||
Bits.pad_right(size: Nat, bit: Bool, bits: Bits): Bits
|
||||
Bits.concat(bits, Bits.repeat(Nat.sub(size, Bits.length(bits)), bit))
|
@ -1,4 +0,0 @@
|
||||
// A Bytes
|
||||
// valid byte range (i.e. between 0 and 255 inclusive)
|
||||
Bytes: Type
|
||||
String
|
@ -1,4 +0,0 @@
|
||||
// Convert a hexstring to a Uint8Array
|
||||
Bytes.arrayify(value: String): Buffer8
|
||||
let {_,buf} = Buffer8.from_hex(String.to_hex(value))
|
||||
buf
|
@ -1,2 +0,0 @@
|
||||
Bytes.drop(n: Nat, b: Bytes): Bytes
|
||||
String.drop(n, b)
|
@ -1,6 +0,0 @@
|
||||
Bytes.from_nat(num: Nat): String
|
||||
let hex = Nat.to_string_base(16, num)
|
||||
if Nat.eql((String.length(hex) % 2), 0)
|
||||
then "0x" | hex
|
||||
else "0x0" | hex
|
||||
|
@ -1,2 +0,0 @@
|
||||
Bytes.from_string(s: String): Bytes
|
||||
"0x"|String.to_hex(s)
|
@ -1,2 +0,0 @@
|
||||
Bytes.length(b: Bytes): Nat
|
||||
(String.length(b) - 2) / 2
|
@ -1,7 +0,0 @@
|
||||
// Bytes.pad(len: Nat, hex: String): String
|
||||
// if Nat.eql(String.length(hex), (len*2)+2)
|
||||
// then hex
|
||||
// else Bytes.pad(len, "0x" | "0" | String.slice(0, 2, hex))
|
||||
|
||||
Bytes.pad_left(len: Nat, hex: String): String
|
||||
"0x" | String.pad_left(len, String.to_char("0"), hex)
|
@ -1,2 +0,0 @@
|
||||
Bytes.pad_right(len: Nat, hex: String): String
|
||||
String.pad_right(len, String.to_char("0"), hex)
|
@ -1,93 +0,0 @@
|
||||
// 28 Sep 21
|
||||
// Author: Maisa Milena
|
||||
// FIXME:
|
||||
// - parse characters using 3 and 4 bytes
|
||||
// - deal with parse error
|
||||
// Hint: check the test cases in Bytes/test/parse_string.kind
|
||||
// and add more tests
|
||||
|
||||
// IMPORTANT: do not use these functions yet. Still WIP
|
||||
|
||||
// Decode a UTF8 data into a String
|
||||
Bytes.parse_string(b: Bytes): String
|
||||
Bytes.parse_string.aux(b, "")
|
||||
|
||||
Bytes.parse_string.take_bytes_pair(b: Bytes): Pair(Bytes, Maybe(Bytes))
|
||||
let fst = Bytes.take(2, b)
|
||||
let snd = String.drop(2, Bytes.take(4, b))
|
||||
if String.is_empty(snd)
|
||||
then {fst, Maybe.none!}
|
||||
else {fst, Maybe.some!(snd)}
|
||||
|
||||
Bytes.parse_string.aux(b: Bytes, s: String): String
|
||||
// Auxiliary
|
||||
let concat_s = (a: String) s | a
|
||||
let b_tail = String.drop(2, b)
|
||||
|
||||
let {fst, snd} = Bytes.parse_string.take_bytes_pair(b)
|
||||
case snd {
|
||||
none: s
|
||||
some:
|
||||
let snd = snd.value
|
||||
let snd = Bytes.to_nat(snd)
|
||||
let fst = Bytes.to_nat(fst)
|
||||
|
||||
let fst = Nat.to_u16(fst)
|
||||
let snd = Nat.to_u16(snd)
|
||||
|
||||
let control_num = 999#16
|
||||
let s_temp =
|
||||
if U16.gtn(snd, 127) then
|
||||
case Bytes.parse_string.gtn_one_byte(fst, snd) as res {
|
||||
none: control_num // got parsing error or help parsing symbols. Confusing, I know
|
||||
some: res.value
|
||||
}
|
||||
else
|
||||
snd
|
||||
|
||||
if U16.ltn(s_temp, 0xffff) then
|
||||
// log("c ltn 0xffff: " | U16.show(s_temp))
|
||||
let parsed =
|
||||
if U16.eql(s_temp, control_num)
|
||||
then "" // Couldn't parse byte, but may be not and error (like for some symbols)
|
||||
else Char.to_string(s_temp)
|
||||
// log(" parsed value: " | parsed)
|
||||
Bytes.parse_string.aux(b_tail, concat_s(parsed)) // String.fromCharCode(c)
|
||||
else if U16.lte(s_temp, 0x10ffff) then// c <= 0x10ffff
|
||||
let aux = U16.sub(s_temp, 0x10000)
|
||||
let a = Char.to_string(U16.or(U16.shr(s_temp, 10), 0xd800)) // String.fromCharCode(c >> 10 | 0xd800)
|
||||
let b = Char.to_string(U16.or(U16.and(s_temp, 0x3FF), 0xdc00)) // String.fromCharCode(c & 0x3FF | 0xdc00)
|
||||
let parsed = a | b
|
||||
// log("c ltn 0x10ffff: " | parsed)
|
||||
Bytes.parse_string.aux(b_tail, concat_s(parsed))
|
||||
else ""
|
||||
}
|
||||
|
||||
// Auxiliar to parse chunks bigger than 1 byte
|
||||
Bytes.parse_string.gtn_one_byte(c: U16, fst: U16): Maybe(U16)
|
||||
let two_bytes = Bool.and(U16.gtn(c, 191), U16.ltn(c, 224)) // (c > 191 && c < 224)
|
||||
let three_bytes = Bool.and(U16.gtn(c, 223), U16.ltn(c, 240)) // (c > 223 && c < 240)
|
||||
let four_bytes = Bool.and(U16.gtn(c, 239), U16.ltn(c, 248)) // (c > 239 && c < 248)
|
||||
if two_bytes then
|
||||
let l = U16.shl(U16.and(c, 31), 6) // (c & 31) << 6
|
||||
let r = U16.and(fst, 63) // bytes[i++] & 63
|
||||
let res = U16.or(l, r)
|
||||
Maybe.some!(res) // l | r
|
||||
else if three_bytes then
|
||||
let l = U16.shl(U16.and(c, 15), 12) // (c & 15) << 12
|
||||
let m = U16.shl(U16.and(fst, 63), 6) // (bytes[i++] & 63) << 6
|
||||
let r = U16.and(fst, 63) // bytes[i++] & 63
|
||||
let res = U16.or(l, U16.or(m, r))
|
||||
Maybe.some!(res) // l | m | r;
|
||||
else if four_bytes then
|
||||
let l = U16.shl(U16.and(c, 7), 18) // (c & 7) << 18
|
||||
let m0 = U16.shl(U16.and(fst, 63), 12) // (bytes[i++] & 63) << 12
|
||||
let m1 = U16.shl(U16.and(fst, 63), 6) // (bytes[i++] & 63) << 6
|
||||
let r = U16.and(fst, 63) // bytes[i++] & 63
|
||||
let res = U16.or(U16.or(l, m0), U16.or(m1, r))
|
||||
Maybe.some!(res) // l | m0 | m1 | r
|
||||
else Maybe.none! // UTF-8 decode: unknown multibyte or auxiliary to parse symbols
|
||||
|
||||
// Reference:
|
||||
// - https://gist.github.com/pascaldekloe/62546103a1576803dade9269ccf76330
|
||||
// -
|
@ -1,7 +0,0 @@
|
||||
// https://github.com/MaiaVictor/eth-lib/blob/da0971f5b09964d9c8449975fa87933f0c9fef35/lib/bytes.js#L19
|
||||
Bytes.reverse(hex: String): String
|
||||
let rev = "0x"
|
||||
let len = ((String.length(hex) - 2) / 2)
|
||||
for i from 0 to len with rev:
|
||||
String.concat(rev, String.slice((len-i)*2, ((len-i)+1)*2, hex))
|
||||
rev
|
@ -1,2 +0,0 @@
|
||||
Bytes.slice(i: Nat, j: Nat, bs: Bytes): Bytes
|
||||
"0x" | String.slice((i*2)+2, ((j*2)+2), bs)
|
@ -1,3 +0,0 @@
|
||||
// Take the first 'n' characters from 'b'
|
||||
Bytes.take(n: Nat, b: Bytes): Bytes
|
||||
String.take(n, b)
|
@ -1,18 +0,0 @@
|
||||
Bytes.test.all: _
|
||||
TestSuite.many("Bytes",
|
||||
[
|
||||
Bytes.test.from_nat
|
||||
Bytes.test.length
|
||||
Bytes.test.slice
|
||||
Bytes.test.to_nat
|
||||
Bytes.test.from_string
|
||||
Bytes.test.parse_string
|
||||
]
|
||||
)
|
||||
|
||||
// Print all tests
|
||||
Bytes.test.all.show: _
|
||||
log(TestSuite.show(Bytes.test.all, 0))
|
||||
0
|
||||
|
||||
|
@ -1,29 +0,0 @@
|
||||
Bytes.test.from_nat.0: TestSuite
|
||||
let test = Bytes.from_nat(0);
|
||||
let got = test
|
||||
let exp = "0x00"
|
||||
let name = "0"
|
||||
TestSuite.show.log_string(name, test, exp, got)
|
||||
|
||||
Bytes.test.from_nat.1: TestSuite
|
||||
let test = Bytes.from_nat(100);
|
||||
let got = test
|
||||
let exp = "0x64"
|
||||
let name = "1"
|
||||
TestSuite.show.log_string(name, test, exp, got)
|
||||
|
||||
Bytes.test.from_nat.2: TestSuite
|
||||
let test = Bytes.from_nat(50);
|
||||
let got = test
|
||||
let exp = "0x32"
|
||||
let name = "2"
|
||||
TestSuite.show.log_string(name, test, exp, got)
|
||||
|
||||
Bytes.test.from_nat: TestSuite
|
||||
TestSuite.many("from_nat", [
|
||||
Bytes.test.from_nat.0
|
||||
Bytes.test.from_nat.1
|
||||
Bytes.test.from_nat.2
|
||||
])
|
||||
|
||||
|
@ -1,53 +0,0 @@
|
||||
Bytes.test.from_string.0: TestSuite
|
||||
let test = "some_random_string"
|
||||
let got = Bytes.from_string(test)
|
||||
let exp = "0x736f6d655f72616e646f6d5f737472696e67"
|
||||
let name = "0"
|
||||
TestSuite.show.log_string(name, test, exp, got)
|
||||
|
||||
Bytes.test.from_string.1: TestSuite
|
||||
let test = ""
|
||||
let got = Bytes.from_string(test)
|
||||
let exp = "0x"
|
||||
let name = "1"
|
||||
TestSuite.show.log_string(name, test, exp, got)
|
||||
|
||||
Bytes.test.from_string.2: TestSuite
|
||||
let test = "¢"
|
||||
let got = Bytes.from_string(test)
|
||||
let exp = "0xc2a2"
|
||||
let name = "2"
|
||||
TestSuite.show.log_string(name, test, exp, got)
|
||||
|
||||
Bytes.test.from_string.3: TestSuite
|
||||
let test = "ह€"
|
||||
let got = Bytes.from_string(test)
|
||||
let exp = "0xe0a4b9e282ac"
|
||||
let name = "3"
|
||||
TestSuite.show.log_string(name, test, exp, got)
|
||||
|
||||
Bytes.test.from_string.4: TestSuite
|
||||
let test = "𐍈"
|
||||
let got = Bytes.from_string(test)
|
||||
let exp = "0xf0908d88"
|
||||
let name = "4"
|
||||
TestSuite.show.log_string(name, test, exp, got)
|
||||
|
||||
Bytes.test.from_string.5: TestSuite
|
||||
let test = "0123456789"
|
||||
let got = Bytes.from_string(test)
|
||||
let exp = "0x30313233343536373839"
|
||||
let name = "5"
|
||||
TestSuite.show.log_string(name, test, exp, got)
|
||||
|
||||
Bytes.test.from_string: TestSuite
|
||||
TestSuite.many("from_string", [
|
||||
Bytes.test.from_string.0
|
||||
Bytes.test.from_string.1
|
||||
Bytes.test.from_string.2
|
||||
Bytes.test.from_string.3
|
||||
Bytes.test.from_string.4
|
||||
Bytes.test.from_string.5
|
||||
])
|
||||
|
||||
|
@ -1,44 +0,0 @@
|
||||
Bytes.test.length.0: TestSuite
|
||||
let test = "0x883bb7da0342d870"
|
||||
let got = Nat.show(Bytes.length(test))
|
||||
let exp = "8"
|
||||
let name = "0"
|
||||
TestSuite.show.log_string(name, test, exp, got)
|
||||
|
||||
Bytes.test.length.1: TestSuite
|
||||
let test = "0x"
|
||||
let got = Nat.show(Bytes.length(test))
|
||||
let exp = "0"
|
||||
let name = "1"
|
||||
TestSuite.show.log_string(name, test, exp, got)
|
||||
|
||||
Bytes.test.length.2: TestSuite
|
||||
let test = "0xbeeca47320461d05ba928962339e46cef56a2f6dd11d9eea0d1fc0c4f2c762f25512959f243d108081c6a665e9e12c90f27db5741612787114f96f85c8ee5f0b0d30f1d8be4329705ca1dbaf500fd525542e02a11381f85717a1599031cb6898e11c6485823ea228b491440c404687696140ec70735a773a101f824aa25039ad2c15759a4e1ba0a546eec1ed12a5816aa7caa1abd7830837b9bdf46c86a7eec9b1424e6ef0329ebfec45317397a2021941d2a5825df14c32a729eb67fb5f39cf3fee8a86e7a5463ab347159cd3af7d3a4fd7eb4f5a643be150b6549e714f5e4f4f7fc53e817bbbe0b2b62a3ad0edbd924040cd796c2ab9a9bde214af841a8de4e4b976985fcff30605764e523edadc68130fdd97fcc93908ea3e323406574ff7fcf6c198e032417b7f0d5de4e8b4185ce00d8a16fe1039bbfbeecd2e67bbc88086ee96a849ee11f27ee17838be9f8ff3b1057050a862fc9d1f126e4f3507611f1800eca8f7502ee5083473d07a4729370080397656bab631788418f775e1de1f17653f5efe5945482ec1b7e50ca8990fd7284795f6d9ef54676a3bd0e814b742b064a9535f6068fd66944a68526962b0d472c74f01d0c02256318e82bbe18346a7009fdab34b1e4fc198ae70ba000d86a221f3508fbc22d286d1b277c23274bc065b37a51de314a0c6b5e78ca594f0336d83b8bbafcf27824bdee3e017c7ff7f03499d84dca28b4a11937e11f17a102683d6bd4e40c877681bf9f4e18fabbb6b816d392f07e5dc06e8375c112560abe34c093052748a06119a3bb14ee4ce765d787c02b83897cb47bf84fcc818078fcbf8c282ca3cc8a081f5264d9a31e226d518e43eaade939cb111ec5f3e3f84cdca5d8586ee1cfd96710f3c665ee77d399d38b504626f33b2384e8f50d86e8a1ea262adaa5f10d0d4a1f676ae4dfef0c72ddbb868f7c99634e6305fb93744a1b8814b6b7ac3bd988ccc446017b11028241e1b167a0fc7ae792ee158cf137f91379418be714522200aa2e6623de8bd6f26763c99a29ce4a27d2ae7699ca16f8b61f80117b89d9e536dc9bdf49e1526ffe5f8075c3f7a2949d3a6b6f2a276dd15f80236e847fc61307dc8a1947a2d965f5d3516d579b0a38d2c5a28656a069317b40939553d7a4df44561a18312e31c64b42b8449060de8daedbfd16288316cc11b7aaf921ca4b7fd9662ef35bc927338b6957665233cafed398f6a23fae50ec076ddf90fb83a7bf1e875447dc2ad0e42282ff253ef5ce9ff6fba07bad731c2e35ef9a8a61a896e1f79cc31e48cb013eb77919373a5fbed9533a50cdb0fa4fa131d3b3dc34c870cfeab5a260a7af57eb97a4b331f08e789906143107e61e71d847f343516d674c936c942e65f6f5edb9f1b8e2f0818f355e4c8b9"
|
||||
let got = Nat.show(Bytes.length(test))
|
||||
let exp = "1000"
|
||||
let name = "2"
|
||||
TestSuite.show.log_string(name, "long string", exp, got)
|
||||
|
||||
Bytes.test.length.3: TestSuite
|
||||
let test = "0x2ebd18326908ff"
|
||||
let got = Nat.show(Bytes.length(test))
|
||||
let exp = "7"
|
||||
let name = "3"
|
||||
TestSuite.show.log_string(name, test, exp, got)
|
||||
|
||||
Bytes.test.length.4: TestSuite
|
||||
let test = "0x0000000001"
|
||||
let got = Nat.show(Bytes.length(test))
|
||||
let exp = "5"
|
||||
let name = "4"
|
||||
TestSuite.show.log_string(name, test, exp, got)
|
||||
|
||||
Bytes.test.length: TestSuite
|
||||
TestSuite.many("length", [
|
||||
Bytes.test.length.0
|
||||
Bytes.test.length.1
|
||||
Bytes.test.length.2
|
||||
Bytes.test.length.3
|
||||
Bytes.test.length.4
|
||||
])
|
||||
|
@ -1,64 +0,0 @@
|
||||
Bytes.test.parse_string.0: TestSuite
|
||||
let test = "0x"
|
||||
let got = Bytes.parse_string(test)
|
||||
let exp = ""
|
||||
let name = "0"
|
||||
TestSuite.show.log_string(name, test, exp, got)
|
||||
|
||||
Bytes.test.parse_string.1: TestSuite
|
||||
let test = "0x30313233343536373839"
|
||||
let got = Bytes.parse_string(test)
|
||||
let exp = "0123456789"
|
||||
let name = "1"
|
||||
TestSuite.show.log_string(name, test, exp, got)
|
||||
|
||||
// 2 bytes
|
||||
Bytes.test.parse_string.2: TestSuite
|
||||
let test = "0xc2a2"
|
||||
let got = Bytes.parse_string(test)
|
||||
let exp = "¢"
|
||||
let name = "2"
|
||||
TestSuite.show.log_string(name, test, exp, got)
|
||||
|
||||
// 3 bytes
|
||||
Bytes.test.parse_string.3: TestSuite
|
||||
let test = "0xe282ac"
|
||||
let got = Bytes.parse_string(test)
|
||||
let exp = "€"
|
||||
let name = "3"
|
||||
TestSuite.show.log_string(name, test, exp, got)
|
||||
|
||||
// 4 bytes
|
||||
Bytes.test.parse_string.4: TestSuite
|
||||
let test = "0xf0908d88"
|
||||
let got = Bytes.parse_string(test)
|
||||
let exp = "𐍈"
|
||||
let name = "4"
|
||||
TestSuite.show.log_string(name, test, exp, got)
|
||||
|
||||
// Unable to parse
|
||||
Bytes.test.parse_string.5: TestSuite
|
||||
let test = "0x708e08"
|
||||
let got = Bytes.parse_string(test)
|
||||
let exp = ""
|
||||
let name = "5"
|
||||
TestSuite.show.log_string(name, test, exp, got)
|
||||
|
||||
// String
|
||||
Bytes.test.parse_string.6: TestSuite
|
||||
let test = "0x736f6d655f72616e646f6d5f737472696e67"
|
||||
let got = Bytes.parse_string(test)
|
||||
let exp = "some_random_string"
|
||||
let name = "6"
|
||||
TestSuite.show.log_string(name, test, exp, got)
|
||||
|
||||
Bytes.test.parse_string: TestSuite
|
||||
TestSuite.many("parse_string", [
|
||||
Bytes.test.parse_string.0
|
||||
Bytes.test.parse_string.1
|
||||
Bytes.test.parse_string.2
|
||||
Bytes.test.parse_string.3
|
||||
Bytes.test.parse_string.4
|
||||
Bytes.test.parse_string.5
|
||||
Bytes.test.parse_string.6
|
||||
])
|
@ -1,43 +0,0 @@
|
||||
Bytes.test.slice.0: TestSuite
|
||||
let test = "0x4cf5fc74dff02752"
|
||||
let got = Bytes.slice(0, 2, test)
|
||||
let exp = "0x4cf5"
|
||||
let name = "0"
|
||||
TestSuite.show.log_string(name, test, exp, got)
|
||||
|
||||
Bytes.test.slice.1: TestSuite
|
||||
let test = "0x4cf5fc74dff02752"
|
||||
let got = Bytes.slice(0, 0, test)
|
||||
let exp = "0x"
|
||||
let name = "1"
|
||||
TestSuite.show.log_string(name, test, exp, got)
|
||||
|
||||
Bytes.test.slice.2: TestSuite
|
||||
let test = "0x4cf5fc74dff02752"
|
||||
let got = Bytes.slice(2, 0, test)
|
||||
let exp = "0x"
|
||||
let name = "2"
|
||||
TestSuite.show.log_string(name, test, exp, got)
|
||||
|
||||
Bytes.test.slice.3: TestSuite
|
||||
let test = "0x"
|
||||
let got = Bytes.slice(0, 2, test)
|
||||
let exp = "0x"
|
||||
let name = "3"
|
||||
TestSuite.show.log_string(name, test, exp, got)
|
||||
|
||||
Bytes.test.slice.4: TestSuite
|
||||
let test = "0x2384c637e6c83e"
|
||||
let got = Bytes.slice(6, 9, test)
|
||||
let exp = "0x3e"
|
||||
let name = "4"
|
||||
TestSuite.show.log_string(name, test, exp, got)
|
||||
|
||||
Bytes.test.slice: TestSuite
|
||||
TestSuite.many("slice", [
|
||||
Bytes.test.slice.0
|
||||
Bytes.test.slice.1
|
||||
Bytes.test.slice.2
|
||||
Bytes.test.slice.3
|
||||
Bytes.test.slice.4
|
||||
])
|
@ -1,29 +0,0 @@
|
||||
Bytes.test.to_nat.0: TestSuite
|
||||
let test = "30"
|
||||
let got = Nat.show(Bytes.to_nat(test))
|
||||
let exp = "48"
|
||||
let name = "0"
|
||||
TestSuite.show.log_string(name, test, exp, got)
|
||||
|
||||
Bytes.test.to_nat.1: TestSuite
|
||||
let test = "5f"
|
||||
let got = Nat.show(Bytes.to_nat(test))
|
||||
let exp = "101"
|
||||
let name = "1"
|
||||
TestSuite.show.log_string(name, test, exp, got)
|
||||
|
||||
Bytes.test.to_nat.2: TestSuite
|
||||
let test = ""
|
||||
let got = Nat.show(Bytes.to_nat(test))
|
||||
let exp = ""
|
||||
let name = "2"
|
||||
TestSuite.show.log_string(name, test, exp, got)
|
||||
|
||||
Bytes.test.to_nat: TestSuite
|
||||
TestSuite.many("to_nat", [
|
||||
Bytes.test.to_nat.0
|
||||
Bytes.test.to_nat.1
|
||||
Bytes.test.to_nat.2
|
||||
// Bytes.test.to_nat.3
|
||||
// Bytes.test.to_nat.4
|
||||
])
|
@ -1,3 +0,0 @@
|
||||
Bytes.to_nat(b: Bytes): Nat
|
||||
Nat.hex.decode(String.reverse(b))
|
||||
|
@ -1,2 +0,0 @@
|
||||
BytesLike: Type
|
||||
Either<Bytes, String>
|
5
base/Either3.kind
Normal file
5
base/Either3.kind
Normal file
@ -0,0 +1,5 @@
|
||||
type Either3 <A: Type, B: Type, C: Type> {
|
||||
fst(value: A)
|
||||
snd(value: B)
|
||||
trd(value: C)
|
||||
}
|
@ -1,9 +1,10 @@
|
||||
|
||||
|
||||
Ether.RLP.proof.pad_bytes(bits : Bits) : Bits
|
||||
let size = Bits.length(bits)
|
||||
Bits.trim(((8 * ((size + 7) / 8)) - size) + size, bits)
|
||||
|
||||
|
||||
Ether.RLP.proof.pad_8bits(bits : Bits) : Bits
|
||||
let size = Bits.length(bits)
|
||||
Bits.trim(8, bits)
|
||||
|
||||
Bits.size.rec(x : Bits, n : Nat) :
|
||||
Nat.succ(Bits.length.go(x, n)) == Bits.length.go(x, Nat.succ(n))
|
||||
@ -58,16 +59,20 @@ Ether.RLP.proof.mul_injective(x : Nat, y : Nat, n : Nat, H : Nat.mul(Nat.succ(n)
|
||||
case x with H {
|
||||
succ : case y with H {
|
||||
succ :
|
||||
|
||||
let H = H :: rewrite Y in Y == _ with Nat.mul.succ_right(Nat.succ(n), x.pred)
|
||||
let H = H :: rewrite Y in _ == Y with Nat.mul.succ_right(Nat.succ(n), y.pred)
|
||||
let inj_add = Ether.RLP.proof.add_injective(Nat.mul(Nat.succ(n), x.pred), Nat.mul(Nat.succ(n), y.pred), n, H)
|
||||
let H = Ether.RLP.proof.mul_injective(x.pred, y.pred, n, inj_add)
|
||||
Equal.apply!!!!(Nat.succ, H)
|
||||
zero :
|
||||
let H = H :: rewrite Y in _ == Y with Nat.mul.comm(Nat.succ(n), 0)
|
||||
let H4 = Nat.succ_neq_zero!(H)
|
||||
Empty.absurd!(H4)
|
||||
}!
|
||||
zero : case y with H {
|
||||
succ :
|
||||
let H2 = refl :: 0 == Nat.mul(Nat.succ(n),0)
|
||||
let H = H :: rewrite Y in Y == _ with Nat.mul.comm(Nat.succ(n), 0)
|
||||
let H4 = Nat.succ_neq_zero!(mirror(H))
|
||||
Empty.absurd!(H4)
|
||||
zero :
|
||||
@ -168,9 +173,9 @@ Ether.RLP.proof.encode.bytes(tree : Ether.RLP.Tree) : Bits
|
||||
let bytes_size = Ether.Bits.get_bytes_size(tree.value)
|
||||
// let u16_char = Bits.trim(4, tree.value)
|
||||
if (bytes_size =? 1) && Bits.ltn(tree.value, Ether.RLP.Constants.bits_128) then
|
||||
tree.value
|
||||
Ether.RLP.proof.pad_bytes(tree.value)
|
||||
else
|
||||
Bits.concat.go(Ether.RPL.proof.encode_length(bytes_size, 128), tree.value)
|
||||
Bits.concat.go(Ether.RPL.proof.encode_length(bytes_size, 128), Ether.RLP.proof.pad_bytes(tree.value))
|
||||
list :
|
||||
let bytes = Bits.e
|
||||
for item in tree.value with bytes :
|
||||
@ -182,13 +187,13 @@ Ether.RLP.proof.encode.bytes(tree : Ether.RLP.Tree) : Bits
|
||||
Ether.RPL.proof.encode_length(value : Nat, offSet : Nat) : Bits
|
||||
switch(Nat.ltn(value)) {
|
||||
56 :
|
||||
Nat.to_bits(value + offSet)
|
||||
Ether.RLP.proof.pad_8bits(Nat.to_bits(value + offSet))
|
||||
} default
|
||||
let binary_encoding = Ether.RPL.proof.encode.binary(value)
|
||||
let binary_encoding = Ether.RLP.proof.pad_8bits(Ether.RPL.proof.encode.binary(value))
|
||||
let len = Ether.Bits.get_bytes_size(binary_encoding)
|
||||
|
||||
let len = Ether.RLP.proof.pad_8bits(Nat.to_bits(len + offSet + 55))
|
||||
//log(Bits.show(Nat.to_bits(len + offSet + 55)) | " " | Bits.show(Bits.concat.go(Nat.to_bits(len + offSet + 55), binary_encoding)))
|
||||
Bits.concat.go(Nat.to_bits(len + offSet + 55), binary_encoding)
|
||||
Bits.concat.go(len, binary_encoding)
|
||||
|
||||
Ether.RPL.proof.encode.binary(value : Nat) : Bits
|
||||
if (value =? 0) then
|
||||
@ -207,28 +212,41 @@ Ether.RLP.proof.encode.read.binary(value : Bits) : Nat
|
||||
else
|
||||
Ether.RLP.proof.encode.read.binary(rest) + (decode * 256)
|
||||
|
||||
Ether.RLP.proof.encode.read(bits : Bits) : String
|
||||
let {byte_prefix, rest} = Bits.break(8, bits)
|
||||
log(Bits.show(byte_prefix))
|
||||
Ether.RLP.proof.decode.list(value : Bits) : Pair<String, Bits>
|
||||
if (Bits.eql(value, Bits.e)) then
|
||||
{"" value}
|
||||
else
|
||||
let {tree, rest} = Ether.RLP.proof.encode.read(value)
|
||||
let {trees, rest} = Ether.RLP.proof.decode.list(rest)
|
||||
{tree | trees, rest}
|
||||
|
||||
"0x" | switch (Bits.ltn(byte_prefix)) {
|
||||
Ether.RLP.proof.encode.read(bits : Bits) : Pair<String, Bits>
|
||||
let {byte_prefix, rest} = Bits.break(8, bits)
|
||||
switch (Bits.ltn(byte_prefix)) {
|
||||
Ether.RLP.Constants.bits_128 :
|
||||
String.reverse(Bits.hex.encode(bits)) // between (0, 127)
|
||||
{String.reverse(Bits.hex.encode(bits)), rest} // between (0, 127)
|
||||
Ether.RLP.Constants.bits_184 :
|
||||
let content_length = (Bits.to_nat(byte_prefix) - 128) * 8
|
||||
let {prefix, rest} = Bits.break(content_length, rest)
|
||||
String.reverse(Bits.hex.encode(byte_prefix)) | String.reverse(Bits.hex.encode(prefix))
|
||||
{String.reverse(Bits.hex.encode(byte_prefix)) | String.reverse(Bits.hex.encode(prefix)), rest}
|
||||
Ether.RLP.Constants.bits_192 :
|
||||
let content_length = (Bits.to_nat(byte_prefix) - 183) * 8
|
||||
let {head, rest} = Bits.break(content_length, rest)
|
||||
let length = Ether.RLP.proof.encode.read.binary(head)
|
||||
log("teste : " | Bits.show(head))
|
||||
|
||||
let {prefix, rest} = Bits.break(length*8, rest)
|
||||
|
||||
String.reverse(Bits.hex.encode(byte_prefix)) | String.reverse(Bits.hex.encode(head))
|
||||
| String.reverse(Bits.hex.encode(prefix))
|
||||
|
||||
{String.reverse(Bits.hex.encode(byte_prefix)) | String.reverse(Bits.hex.encode(head))
|
||||
| String.reverse(Bits.hex.encode(prefix)), rest}
|
||||
Ether.RLP.Constants.bits_248 :
|
||||
let content_length = (Bits.to_nat(byte_prefix) - 192) * 8
|
||||
let {xs, rest} = Ether.RLP.proof.decode.list(rest)
|
||||
{String.reverse(Bits.hex.encode(byte_prefix)) | xs, rest}
|
||||
Ether.RLP.Constants.bits_255 :
|
||||
let content_length = (Bits.to_nat(byte_prefix) - 247) * 8
|
||||
let {head, rest} = Bits.break(content_length, rest)
|
||||
let length = Ether.RLP.proof.encode.read.binary(head)
|
||||
let {xs, rest} = Ether.RLP.proof.decode.list(rest)
|
||||
{String.reverse(Bits.hex.encode(byte_prefix)) | xs, rest}
|
||||
|
||||
// {Ether.RLP.Tree.tip(Bits.hex.decode(String.reverse(prefix))), rest}
|
||||
|
||||
} default ""
|
||||
} default {"", Bits.e}
|
@ -1,14 +1,18 @@
|
||||
Ether.tests : _
|
||||
//let v = Ether.RLP.Tree.list(
|
||||
// [
|
||||
// Ether.RLP.Tree.tip(Bits.read(String.reverse("1000111011111010110"))),
|
||||
// Ether.RLP.Tree.tip(Bits.read(String.reverse("1000111011111010110")))
|
||||
// ])
|
||||
log(Nat.show(Bits.to_nat(Ether.RLP.proof.pad_bytes2(Bits.read("1010100000000000")))))
|
||||
|
||||
Ether.RLP.proof.pad_bytes2(Bits.read("000000001"))
|
||||
|
||||
let bits = Nat.to_bits(10002202234)
|
||||
|
||||
let v = Ether.RLP.Tree.list(
|
||||
[
|
||||
Ether.RLP.Tree.tip(bits),
|
||||
Ether.RLP.Tree.tip(bits)
|
||||
])
|
||||
// let v = Ether.RLP.Tree.tip(Bits.read("1000000100000000000000000110110000000000000000000010000000000000000011011000111111111111111111111111111111111011111000000000000100011111111111111111111111111111111101111100000000000000000000000000000001000000000000000001101100100011111111111111111111111111111111101111100000000000010001111111111111111111111111111111110111110000000000000000000000000000000100000000000000000110110000000000000000000010000000000000000011011000000000000000000010110110"))
|
||||
let test1 = Ether.RLP.proof.encode.bytes(v)
|
||||
let test2 = Ether.RLP.encode.bytes(v)
|
||||
log(Pair.fst!!(Ether.RLP.proof.encode.read(test1)))
|
||||
log(Ether.RLP.encode.read(test2))
|
||||
let test2 = List.foldr!!(Bits.e, Bits.concat.go, test2)
|
||||
{test1, test2}
|
||||
//let buffer = Buffer8.from_hex("d69429d7d1dd5b6f9c864d9db560d72a247c178ae86b0a")
|
||||
//let hash = Crypto.Keccak.hash.bytes(buffer)
|
||||
//Buffer8.to_hex(hash)
|
155
base/Nat/AddExp.kind
Normal file
155
base/Nat/AddExp.kind
Normal file
@ -0,0 +1,155 @@
|
||||
type Nat.AddExp {
|
||||
const(value: Nat)
|
||||
var(idx: Nat)
|
||||
add(left: Nat.AddExp, right: Nat.AddExp)
|
||||
}
|
||||
|
||||
Nat.AddExp.from_nat: Nat -> Nat.AddExp
|
||||
Nat.AddExp.const
|
||||
|
||||
Nat.AddExp.dimension(
|
||||
exp: Nat.AddExp
|
||||
): Nat
|
||||
case exp {
|
||||
const:
|
||||
0
|
||||
add:
|
||||
let left_dim = Nat.AddExp.dimension(exp.left)
|
||||
let right_dim = Nat.AddExp.dimension(exp.right)
|
||||
Nat.max(left_dim, right_dim)
|
||||
var:
|
||||
Nat.succ(exp.idx)
|
||||
}
|
||||
|
||||
Nat.AddExp.constant(exp: Nat.AddExp): Type
|
||||
case exp {
|
||||
const:
|
||||
Unit
|
||||
var:
|
||||
Empty
|
||||
add:
|
||||
And<Nat.AddExp.constant(exp.left), Nat.AddExp.constant(exp.right)>
|
||||
}
|
||||
|
||||
Nat.AddExp.dimension.zero(
|
||||
exp: Nat.AddExp
|
||||
Hyp: Equal<Nat>(Nat.AddExp.dimension(exp), 0)
|
||||
): Nat.AddExp.constant(exp)
|
||||
(case exp {
|
||||
const:
|
||||
(Hyp)
|
||||
unit
|
||||
var:
|
||||
(Hyp)
|
||||
let contra = Nat.succ_neq_zero!(Hyp)
|
||||
Empty.absurd!(contra)
|
||||
add:
|
||||
(Hyp)
|
||||
let {left_small, right_small} = Nat.max.big(Nat.AddExp.dimension(exp.left), Nat.AddExp.dimension(exp.right))
|
||||
def max = Nat.max(Nat.AddExp.dimension(exp.left), Nat.AddExp.dimension(exp.right))
|
||||
let left_zero = Nat.Order.chain.aux!(Equal.rewrite<Nat>(
|
||||
max, 0, Hyp,
|
||||
(x) Equal<Bool>(Nat.lte(Nat.AddExp.dimension(exp.left), x), true),
|
||||
left_small
|
||||
))
|
||||
let right_zero = Nat.Order.chain.aux!(Equal.rewrite<Nat>(
|
||||
max, 0, Hyp
|
||||
(x) Equal<Bool>(Nat.lte(Nat.AddExp.dimension(exp.right), x), true),
|
||||
right_small
|
||||
))
|
||||
let left = Nat.AddExp.dimension.zero(exp.left, left_zero)
|
||||
let right = Nat.AddExp.dimension.zero(exp.right, right_zero)
|
||||
Pair.new!!(left, right)
|
||||
}: (Hyp: Equal<Nat>(Nat.AddExp.dimension(exp), 0)) -> Nat.AddExp.constant(exp))(
|
||||
Hyp
|
||||
)
|
||||
|
||||
Nat.AddExp.compute(
|
||||
exp: Nat.AddExp
|
||||
Hyp: Nat.AddExp.constant(exp)
|
||||
): Nat
|
||||
case exp with Hyp {
|
||||
const:
|
||||
exp.value
|
||||
var:
|
||||
Empty.absurd!(Hyp)
|
||||
add:
|
||||
open Hyp
|
||||
Nat.add(Nat.AddExp.compute(exp.left, Hyp.fst), Nat.AddExp.compute(exp.right, Hyp.snd))
|
||||
}!
|
||||
|
||||
Nat.AddExp.substitution(
|
||||
exp: Nat.AddExp
|
||||
): Variadic(Nat.AddExp.dimension(exp), Nat, Nat)
|
||||
def dim = Nat.AddExp.dimension(exp)
|
||||
def Hyp = Nat.Order.refl(dim)
|
||||
Nat.AddExp.substitution.aux0(dim, exp, Hyp)
|
||||
|
||||
Nat.AddExp.substitution.aux0(
|
||||
n: Nat
|
||||
exp: Nat.AddExp
|
||||
Hyp: Equal<Bool>(Nat.lte(Nat.AddExp.dimension(exp), n), true)
|
||||
): Variadic(n, Nat, Nat)
|
||||
case n with Hyp {
|
||||
zero:
|
||||
def Hyp = Nat.Order.chain.aux!(Hyp)
|
||||
def Hyp = Nat.AddExp.dimension.zero!(Hyp)
|
||||
Nat.AddExp.compute(exp, Hyp)
|
||||
succ:
|
||||
(value)
|
||||
def new_exp = Nat.AddExp.substitution.aux1(exp, value, n.pred)
|
||||
let Hyp = Nat.AddExp.substitution.aux2(exp, value, n.pred, Hyp)
|
||||
Nat.AddExp.substitution.aux0(n.pred, new_exp, Hyp)
|
||||
}!
|
||||
|
||||
Nat.AddExp.substitution.aux1(
|
||||
exp: Nat.AddExp
|
||||
value: Nat
|
||||
idx: Nat
|
||||
): Nat.AddExp
|
||||
case exp {
|
||||
const:
|
||||
exp
|
||||
var:
|
||||
case Nat.lte(idx, exp.idx) {
|
||||
true:
|
||||
Nat.AddExp.const(value)
|
||||
false:
|
||||
exp
|
||||
}
|
||||
add:
|
||||
Nat.AddExp.add(
|
||||
Nat.AddExp.substitution.aux1(exp.left, value, idx)
|
||||
Nat.AddExp.substitution.aux1(exp.right, value, idx)
|
||||
)
|
||||
}
|
||||
|
||||
Nat.AddExp.substitution.aux2(
|
||||
exp: Nat.AddExp
|
||||
value: Nat
|
||||
idx: Nat
|
||||
Hyp: Equal<Bool>(Nat.lte(Nat.AddExp.dimension(exp), Nat.succ(idx)), true)
|
||||
): let new_exp = Nat.AddExp.substitution.aux1(exp, value, idx)
|
||||
Equal<Bool>(Nat.lte(Nat.AddExp.dimension(new_exp), idx), true)
|
||||
case exp with Hyp {
|
||||
const:
|
||||
Equal.refl<Bool>(true)
|
||||
var:
|
||||
def cmp = Nat.lte(idx, exp.idx)
|
||||
let cmp_eq = refl :: cmp == cmp
|
||||
case cmp with cmp_eq: ^cmp == cmp {
|
||||
true:
|
||||
Equal.refl<Bool>(true)
|
||||
false:
|
||||
Nat.lte.comm.false(idx, exp.idx, cmp_eq)
|
||||
}! :: Equal<Bool>(Nat.lte(Nat.AddExp.dimension(cmp(() Nat.AddExp, Nat.AddExp.const(value), Nat.AddExp.var(exp.idx))), idx), true)
|
||||
add:
|
||||
let {left_bound, right_bound} = Nat.max.split.left(
|
||||
Nat.AddExp.dimension(exp.left),
|
||||
Nat.AddExp.dimension(exp.right),
|
||||
Nat.succ(idx), Hyp
|
||||
)
|
||||
let ind_left = Nat.AddExp.substitution.aux2(exp.left, value, idx, left_bound)
|
||||
let ind_right = Nat.AddExp.substitution.aux2(exp.right, value, idx, right_bound)
|
||||
Nat.max.combine.left!!!(ind_left, ind_right)
|
||||
}!
|
48
base/Nat/AlgExp.kind
Normal file
48
base/Nat/AlgExp.kind
Normal file
@ -0,0 +1,48 @@
|
||||
Variadic.Equal<A: Type, B: Type>(
|
||||
n: Nat
|
||||
l: Variadic(n)<A, B>
|
||||
r: Variadic(n)<A, B>
|
||||
): Variadic(n)<A, Type>
|
||||
case n with l r {
|
||||
zero:
|
||||
Equal<B>(l, r)
|
||||
succ:
|
||||
(x) Variadic.Equal<A, B>(n.pred, l(x), r(x))
|
||||
}!
|
||||
|
||||
Nat.AlgExp.from_nat(n: Nat): Nat.AlgExp
|
||||
Nat.AlgExp.const(n)
|
||||
|
||||
Nat.AlgExp.dimension(exp: Nat.AlgExp): Nat
|
||||
?dimension
|
||||
|
||||
Nat.AlgExp.substitution(exp: Nat.AlgExp): Variadic(Nat.AlgExp.dimension(exp), Nat, Nat)
|
||||
?substitution
|
||||
|
||||
Nat.AlgExp.eql(exp0: Nat.AlgExp, exp1: Nat.AlgExp): Bool
|
||||
?equal
|
||||
|
||||
type Nat.AlgExp {
|
||||
const(value: Nat)
|
||||
var(idx: Nat)
|
||||
add(left: Nat.AlgExp, right: Nat.AlgExp)
|
||||
mul(left: Nat.AlgExp, right: Nat.AlgExp)
|
||||
}
|
||||
|
||||
Nat.AlgExp.decide(
|
||||
exp0: Nat.AlgExp
|
||||
exp1: Nat.AlgExp
|
||||
): let eql = Nat.AlgExp.eql(exp0, exp1)
|
||||
if eql then
|
||||
Variadic.Equal(n, Nat.AlgExp.substitution(exp0), Nat.AlgExp.substitution(exp1))
|
||||
else
|
||||
Variadic.NotEqual(n, Nat.AlgExp.substitution(exp0), Nat.AlgExp.substitution(exp1))
|
||||
?equivalence
|
||||
|
||||
Test(a: Nat, b: Nat): Equal<Nat>((a + b) * (a + b), (a * a) + (2 * a * b) + (b * b))
|
||||
let x = Nat.AlgExp.var(0)
|
||||
let y = Nat.AlgExp.var(1)
|
||||
let exp0 = (x + y) * (x + y)
|
||||
let exp1 = (x * x) + (2 * x * y) + (y * y)
|
||||
Nat.AlgExp.decide(exp0, exp1, a, b)
|
||||
|
@ -93,141 +93,191 @@ Nat.Order.anti_symm(
|
||||
Hyp0
|
||||
Hyp1
|
||||
)
|
||||
// case a b with Hyp0 Hyp1 {
|
||||
// zero zero:
|
||||
// refl
|
||||
// zero succ:
|
||||
// contra = Bool.true_neq_false(mirror(Hyp1))
|
||||
// Empty.absurd!(contra)
|
||||
// succ zero:
|
||||
// contra = Bool.true_neq_false(mirror(Hyp0))
|
||||
// Empty.absurd!(contra)
|
||||
// succ succ:
|
||||
// ind = Nat.Order.anti_symm(
|
||||
// a.pred,
|
||||
// b.pred,
|
||||
// Hyp0,
|
||||
// Hyp1
|
||||
// )
|
||||
// let qed = apply(Nat.succ, ind)
|
||||
// qed
|
||||
|
||||
Nat.Order.chain.aux(
|
||||
a: Nat
|
||||
Hyp: Equal<Bool>(Nat.lte(a, 0), true)
|
||||
): Equal<Nat>(a, 0)
|
||||
(case a {
|
||||
zero:
|
||||
(Hyp)
|
||||
Equal.refl<Nat>(0)
|
||||
succ:
|
||||
(Hyp)
|
||||
let contra = Bool.false_neq_true(Hyp)
|
||||
Empty.absurd<Equal<Nat>(Nat.succ(a.pred), 0)>(contra)
|
||||
}: (Hyp: Equal<Bool>(Nat.lte(a, 0), true)) -> Equal<Nat>(a, 0))(
|
||||
Hyp
|
||||
)
|
||||
|
||||
Nat.Order.chain(
|
||||
a: Nat
|
||||
b: Nat
|
||||
c: Nat
|
||||
Hyp0: Equal<Bool>(Nat.lte(a, b), true)
|
||||
Hyp1: Equal<Bool>(Nat.lte(b, c), true)
|
||||
): Equal<Bool>(Nat.lte(a, c), true)
|
||||
(case b {
|
||||
zero:
|
||||
(Hyp0, Hyp1)
|
||||
let a_zero = Equal.mirror<Nat>(a, 0, Nat.Order.chain.aux(a, Hyp0))
|
||||
let qed = Equal.rewrite<Nat>(0, a, a_zero, (x) Equal<Bool>(Nat.lte(x, c), true), Hyp1)
|
||||
qed
|
||||
succ:
|
||||
(Hyp0, Hyp1)
|
||||
(case a {
|
||||
zero:
|
||||
(Hyp0, Hyp1)
|
||||
Equal.refl<Bool>(true)
|
||||
succ:
|
||||
(Hyp0, Hyp1)
|
||||
(case c {
|
||||
zero:
|
||||
(Hyp0, Hyp1)
|
||||
let b_zero = Nat.Order.chain.aux(Nat.succ(b.pred), Hyp1)
|
||||
let contra = Nat.succ_neq_zero(b.pred, b_zero)
|
||||
Empty.absurd(Equal<Bool>(Nat.lte(Nat.succ(a.pred), 0), true), contra)
|
||||
succ:
|
||||
(Hyp0, Hyp1)
|
||||
let ind = Nat.Order.chain(a.pred, b.pred, c.pred, Hyp0, Hyp1)
|
||||
ind
|
||||
}:
|
||||
(Hyp0: Equal<Bool>(Nat.lte(Nat.succ(a.pred), Nat.succ(b.pred)), true)) ->
|
||||
(Hyp1: Equal<Bool>(Nat.lte(Nat.succ(b.pred), c), true)) ->
|
||||
Equal<Bool>(Nat.lte(Nat.succ(a.pred), c), true))(
|
||||
Hyp0
|
||||
Hyp1
|
||||
)
|
||||
}:
|
||||
(Hyp0: Equal<Bool>(Nat.lte(a, Nat.succ(b.pred)), true)) ->
|
||||
(Hyp1: Equal<Bool>(Nat.lte(Nat.succ(b.pred), c), true)) ->
|
||||
Equal<Bool>(Nat.lte(a, c), true))(
|
||||
Hyp0
|
||||
Hyp1
|
||||
)
|
||||
}: (Hyp0: Equal<Bool>(Nat.lte(a, b), true), Hyp1: Equal<Bool>(Nat.lte(b, c), true)) -> Equal<Bool>(Nat.lte(a, c), true))(
|
||||
Hyp0
|
||||
Hyp1
|
||||
)
|
||||
|
||||
Nat.Order.add.left(
|
||||
a: Nat
|
||||
b: Nat
|
||||
c: Nat
|
||||
Hyp: Equal<Bool>(Nat.lte(a, b), true)
|
||||
): Equal<Bool>(Nat.lte(Nat.add(c, a), Nat.add(c, b)), true)
|
||||
(case c {
|
||||
zero:
|
||||
(Hyp)
|
||||
Hyp
|
||||
succ:
|
||||
(Hyp)
|
||||
Nat.Order.add.left(a, b, c.pred, Hyp)
|
||||
}:
|
||||
(Hyp: Equal<Bool>(Nat.lte(a, b), true)) ->
|
||||
Equal<Bool>(Nat.lte(Nat.add(c, a), Nat.add(c, b)), true))(
|
||||
Hyp
|
||||
)
|
||||
|
||||
Nat.Order.add.right(
|
||||
a: Nat
|
||||
b: Nat
|
||||
c: Nat
|
||||
Hyp: Equal<Bool>(Nat.lte(a, b), true)
|
||||
): Equal<Bool>(Nat.lte(Nat.add(a, c), Nat.add(b, c)), true)
|
||||
let lem = Nat.Order.add.left(a, b, c, Hyp)
|
||||
let lem = Equal.rewrite<Nat>(
|
||||
Nat.add(c, a), Nat.add(a, c), Nat.add.comm(c, a),
|
||||
(x) Equal<Bool>(Nat.lte(x, Nat.add(c, b)), true), lem
|
||||
)
|
||||
let qed = Equal.rewrite<Nat>(
|
||||
Nat.add(c, b), Nat.add(b, c), Nat.add.comm(c, b),
|
||||
(x) Equal<Bool>(Nat.lte(Nat.add(a, c), x), true), lem
|
||||
)
|
||||
qed
|
||||
|
||||
Nat.Order.add.combine(
|
||||
a: Nat
|
||||
b: Nat
|
||||
c: Nat
|
||||
d: Nat
|
||||
Hyp0: Equal<Bool>(Nat.lte(a, b), true)
|
||||
Hyp1: Equal<Bool>(Nat.lte(c, d), true)
|
||||
): Equal<Bool>(Nat.lte(Nat.add(a, c), Nat.add(b, d)), true)
|
||||
let left_lem = Nat.Order.add.right(a, b, c, Hyp0)
|
||||
let right_lem = Nat.Order.add.left(c, d, b, Hyp1)
|
||||
let qed = Nat.Order.chain(Nat.add(a, c), Nat.add(b, c), Nat.add(b,d), left_lem, right_lem)
|
||||
qed
|
||||
|
||||
Nat.Order.mul.left(
|
||||
a: Nat
|
||||
b: Nat
|
||||
c: Nat
|
||||
Hyp: Equal<Bool>(Nat.lte(a, b), Bool.true)
|
||||
): Equal<Bool>(Nat.lte(Nat.mul(c, a), Nat.mul(c, b)), Bool.true)
|
||||
// TODO
|
||||
case c {
|
||||
zero:
|
||||
Equal.refl<Bool>(true)
|
||||
succ:
|
||||
let ind = Nat.Order.mul.left(a, b, c.pred, Hyp)
|
||||
let qed = Nat.Order.add.combine(a, b, Nat.mul(c.pred,a),Nat.mul(c.pred,b), Hyp, ind)
|
||||
qed
|
||||
}: Equal<Bool>(Nat.lte(Nat.mul(c, a), Nat.mul(c, b)), true)
|
||||
|
||||
|
||||
Nat.Order.mul.right(
|
||||
a: Nat
|
||||
b: Nat
|
||||
c: Nat
|
||||
Hyp: Equal<Bool>(Nat.lte(a, b), true)
|
||||
): Equal<Bool>(Nat.lte(Nat.mul(a, c), Nat.mul(b, c)), true)
|
||||
let lem = Nat.Order.mul.left(a, b, c, Hyp)
|
||||
let lem = Equal.rewrite<Nat>(
|
||||
Nat.mul(c,a), Nat.mul(a, c), Nat.mul.comm(c, a)
|
||||
(x) Equal<Bool>(Nat.lte(x, Nat.mul(c, b)), Bool.true), lem
|
||||
)
|
||||
let qed = Equal.rewrite<Nat>(
|
||||
Nat.mul(c, b), Nat.mul(b, c), Nat.mul.comm(c, b)
|
||||
(x) Equal<Bool>(Nat.lte(Nat.mul(a, c), x), Bool.true), lem
|
||||
)
|
||||
qed
|
||||
|
||||
//Nat.Order.max.big(
|
||||
// a: Nat
|
||||
// b: Nat
|
||||
//): And<Equal<Bool>(Nat.lte(a, Nat.max(a, b)), true), Equal<Bool>(Nat.lte(b, Nat.max(a, b)), true)>
|
||||
// case a {
|
||||
// zero:
|
||||
// Pair.new!!(Equal.refl<Bool>(true), Nat.Order.refl(b))
|
||||
// succ:
|
||||
// let ind = Nat.Order.max(a.pred, b)
|
||||
// ?succ
|
||||
// }!
|
||||
|
||||
//Nat.Order.chain.aux(
|
||||
// a: Nat
|
||||
// Hyp: Nat.lte(a, 0) == true
|
||||
//): a == 0
|
||||
// case a with Hyp {
|
||||
// zero:
|
||||
// refl
|
||||
// succ:
|
||||
// contra = Bool.true_neq_false(mirror(Hyp))
|
||||
// Empty.absurd!(contra)
|
||||
// }!
|
||||
//
|
||||
//Nat.Order.chain(
|
||||
// a: Nat
|
||||
// b: Nat
|
||||
// c: Nat
|
||||
// Hyp0: Nat.lte(a, b) == true
|
||||
// Hyp1: Nat.lte(b, c) == true
|
||||
//): Nat.lte(a, c) == true
|
||||
// case b with Hyp0 Hyp1 {
|
||||
// zero:
|
||||
// a_zero = mirror(Nat.Order.chain.aux(a, Hyp0))
|
||||
// qed = Hyp1 :: rewrite X in Nat.lte(X, _) == _ with a_zero
|
||||
// qed
|
||||
// succ:
|
||||
// case a with Hyp0 Hyp1 {
|
||||
// zero:
|
||||
// refl
|
||||
// succ:
|
||||
// case c with Hyp0 Hyp1 {
|
||||
// zero:
|
||||
// b_zero = Nat.Order.chain.aux(Nat.succ(b.pred), Hyp1)
|
||||
// contra = Nat.succ_neq_zero!(b_zero)
|
||||
// Empty.absurd!(contra)
|
||||
// succ:
|
||||
// ind = Nat.Order.chain(a.pred, b.pred, c.pred, Hyp0, Hyp1)
|
||||
// ind
|
||||
// }!
|
||||
// }!
|
||||
// }!
|
||||
//
|
||||
//Nat.Order.add.left(
|
||||
// a: Nat
|
||||
// b: Nat
|
||||
// c: Nat
|
||||
// Hyp: Nat.lte(a, b) == true
|
||||
//): Nat.lte(c + a, c + b) == true
|
||||
// case c {
|
||||
// zero:
|
||||
// Hyp
|
||||
// succ:
|
||||
// Nat.Order.add.left(a, b, c.pred, Hyp)
|
||||
// }!
|
||||
//
|
||||
//Nat.Order.add.right(
|
||||
// a: Nat
|
||||
// b: Nat
|
||||
// c: Nat
|
||||
// Hyp: Nat.lte(a, b) == true
|
||||
//): Nat.lte(a + c, b + c) == true
|
||||
// (Nat.Order.add.left!!(c, Hyp)
|
||||
// :: rewrite X in Nat.lte(X, _) == _ with Nat.add.comm!!)
|
||||
// :: rewrite X in Nat.lte(_, X) == _ with Nat.add.comm!!
|
||||
//
|
||||
//Nat.Order.add.combine(
|
||||
// a: Nat
|
||||
// b: Nat
|
||||
// c: Nat
|
||||
// d: Nat
|
||||
// Hyp0: Nat.lte(a, b) == true
|
||||
// Hyp1: Nat.lte(c, d) == true
|
||||
//): Nat.lte(a + c, b + d) == true
|
||||
// left_lem = Nat.Order.add.right!!(c, Hyp0)
|
||||
// right_lem = Nat.Order.add.left!!(b, Hyp1)
|
||||
// qed = Nat.Order.chain!!!(left_lem, right_lem)
|
||||
// qed
|
||||
//
|
||||
//Nat.Order.mul.right(
|
||||
// a: Nat
|
||||
// b: Nat
|
||||
// c: Nat
|
||||
// Hyp: Nat.lte(a, b) == true
|
||||
//): Nat.lte(Nat.mul(a, c), Nat.mul(b, c)) == true
|
||||
// c(
|
||||
// (c) Equal<Bool>(Nat.lte(Nat.mul(a, c), Nat.mul(b, c)), true),
|
||||
// refl,
|
||||
// (c.pred)
|
||||
// let ind = Nat.Order.mul.right(a, b, c.pred, Hyp)
|
||||
// let qed = Nat.Order.add.combine(a, b, Nat.mul(a,c.pred), Nat.mul(b,c.pred), Hyp, ind)
|
||||
// qed
|
||||
// )
|
||||
//
|
||||
//Nat.Order.mul.left(
|
||||
// a: Nat
|
||||
// b: Nat
|
||||
// c: Nat
|
||||
// Hyp: Equal<Bool>(Nat.lte(a, b), Bool.true)
|
||||
//): Equal<Bool>(Nat.lte(Nat.mul(c, a), Nat.mul(c, b)), Bool.true)
|
||||
// lem = Nat.Order.mul.right(a, b, c, Hyp)
|
||||
// lem = lem :: rewrite X in Nat.lte(X, Nat.mul(b, c)) == true with Nat.mul.comm(a, c)
|
||||
// qed = lem :: rewrite X in Nat.lte(Nat.mul(c, a), X) == true with Nat.mul.comm(b, c)
|
||||
// qed
|
||||
//
|
||||
//Nat.Order.mul.combine(
|
||||
// a: Nat,
|
||||
// b: Nat,
|
||||
// c: Nat,
|
||||
// d: Nat,
|
||||
// Hyp0: Equal<Bool>(Nat.lte(a, b), Bool.true),
|
||||
// Hyp1: Equal<Bool>(Nat.lte(c, d), Bool.true)
|
||||
//): Equal<Bool>(Nat.lte(Nat.mul(a, c), Nat.mul(b, d)), Bool.true)
|
||||
// let left_lem = Nat.Order.mul.right(a, b, c, Hyp0);
|
||||
// let right_lem = Nat.Order.mul.left(c, d, b, Hyp1);
|
||||
// let qed = Nat.Order.chain(Nat.mul(a, c), Nat.mul(b, c), Nat.mul(b, d), left_lem, right_lem);
|
||||
// qed
|
||||
Nat.Order.trichotomy(
|
||||
a: Nat
|
||||
b: Nat
|
||||
): Either3<
|
||||
Equal<Bool>(Nat.lte(a, b), false)
|
||||
Equal<Nat>(a, b)
|
||||
Equal<Bool>(Nat.lte(b, a), false)
|
||||
>
|
||||
def cmp_ab = Nat.lte(a, b)
|
||||
def cmp_ba = Nat.lte(b, a)
|
||||
let lemma_ab = Equal.refl<Bool>(cmp_ab)
|
||||
let lemma_ba = Equal.refl<Bool>(cmp_ba)
|
||||
case cmp_ab with lemma_ab: cmp_ab^ == cmp_ab {
|
||||
false:
|
||||
Either3.fst!!!(Equal.refl<Bool>(false))
|
||||
true:
|
||||
case cmp_ba with lemma_ba: cmp_ba^ == cmp_ba {
|
||||
false:
|
||||
Either3.trd!!!(Equal.refl<Bool>(false))
|
||||
true:
|
||||
Either3.snd!!!(Nat.Order.anti_symm!!(lemma_ab, lemma_ba))
|
||||
}!
|
||||
}!
|
||||
|
||||
//Nat.Order.bernoulli(
|
||||
// a: Nat,
|
||||
|
@ -4,9 +4,9 @@ Nat.Order.mul.combine(
|
||||
c: Nat,
|
||||
d: Nat,
|
||||
Hyp0: Equal<Bool>(Nat.lte(a, b), Bool.true),
|
||||
Hyp1: Equal<Bool>(Nat.lte(c, d), Bool.true),
|
||||
Hyp1: Equal<Bool>(Nat.lte(c, d), Bool.true)
|
||||
): Equal<Bool>(Nat.lte(Nat.mul(a, c), Nat.mul(b, d)), Bool.true)
|
||||
let left_lem = Nat.Order.mul.right(a, b, c, Hyp0);
|
||||
let right_lem = Nat.Order.mul.left(c, d, b, Hyp1);
|
||||
let qed = Nat.Order.chain(Nat.mul(a, c), Nat.mul(b, c), Nat.mul(b, d), left_lem, right_lem);
|
||||
let left_lem = Nat.Order.mul.right(a, b, c, Hyp0)
|
||||
let right_lem = Nat.Order.mul.left(c, d, b, Hyp1)
|
||||
let qed = Nat.Order.chain(Nat.mul(a, c), Nat.mul(b, c), Nat.mul(b, d), left_lem, right_lem)
|
||||
qed
|
||||
|
@ -1,8 +1,13 @@
|
||||
Nat.add.assoc(a: Nat, b: Nat, c: Nat)
|
||||
: ((a + b) + c) == a + (b + c)
|
||||
case a{
|
||||
zero: refl
|
||||
Nat.add.assoc(
|
||||
a: Nat, b: Nat, c: Nat
|
||||
): Equal<Nat>(Nat.add(Nat.add(a, b), c), Nat.add(a, Nat.add(b, c)))
|
||||
case a {
|
||||
zero:
|
||||
Equal.refl<Nat>(Nat.add(b, c))
|
||||
succ:
|
||||
let h=Nat.add.assoc(a.pred, b, c)
|
||||
Equal.apply!!<Nat.add(Nat.add(a.pred,b),c), Nat.add(a.pred,Nat.add(b,c)),Nat.succ>(h)
|
||||
let h = Nat.add.assoc(a.pred, b, c)
|
||||
Equal.apply<Nat, Nat>(
|
||||
Nat.add(Nat.add(a.pred,b),c), Nat.add(a.pred,Nat.add(b,c)),
|
||||
Nat.succ, h
|
||||
)
|
||||
}!
|
||||
|
@ -1,9 +1,22 @@
|
||||
Nat.add.cancel_left(a: Nat, b: Nat, c: Nat, e0: (a + b) == a + c): b == c
|
||||
case a with e0 {
|
||||
zero: e0
|
||||
Nat.add.cancel_left(a: Nat, b: Nat, c: Nat, e0: Equal<Nat>(Nat.add(a, b), Nat.add(a, c))): Equal<Nat>(b, c)
|
||||
(case a {
|
||||
zero:
|
||||
(e0)
|
||||
e0
|
||||
succ:
|
||||
let e2 = e0 :: rewrite x in x == _ with Nat.add.succ_left(a.pred, b)
|
||||
let e3 = e2 :: rewrite x in _ == x with Nat.add.succ_left(a.pred, c)
|
||||
let e4 = Nat.succ_inj!!(e3)
|
||||
Nat.add.cancel_left!!!(e4)
|
||||
}!
|
||||
(e0)
|
||||
let e2 = Equal.rewrite<Nat>(
|
||||
Nat.add(Nat.succ(a.pred),b), Nat.succ(Nat.add(a.pred,b)),
|
||||
Nat.add.succ_left(a.pred, b),
|
||||
(x) Equal<Nat>(x, Nat.add(Nat.succ(a.pred),c)), e0
|
||||
)
|
||||
let e3 = Equal.rewrite<Nat>(
|
||||
Nat.add(Nat.succ(a.pred),c), Nat.succ(Nat.add(a.pred,c))
|
||||
Nat.add.succ_left(a.pred, c)
|
||||
(x) Equal<Nat>(Nat.succ(Nat.add(a.pred,b)), x), e2
|
||||
)
|
||||
let e4 = Nat.succ_inj(Nat.add(a.pred,b), Nat.add(a.pred,c), e3)
|
||||
Nat.add.cancel_left(a.pred, b, c, e4)
|
||||
}: (e0: Equal<Nat>(Nat.add(a, b), Nat.add(a, c))) -> Equal<Nat>(b, c))(
|
||||
e0
|
||||
)
|
||||
|
@ -1,6 +1,16 @@
|
||||
// if a + b == c + b, then a == c.
|
||||
Nat.add.cancel_right(a: Nat, b: Nat, c: Nat, h: (a + b) == c + b)
|
||||
: a == c
|
||||
let h1 = h :: rewrite x in x == Nat.add(c,b) with Nat.add.comm(a, b)
|
||||
let h2 = h1:: rewrite x in Nat.add(b,a) == x with Nat.add.comm(c, b)
|
||||
Nat.add.cancel_left(_ _ _ h2)
|
||||
Nat.add.cancel_right(
|
||||
a: Nat, b: Nat, c: Nat, h: Equal<Nat>(Nat.add(a, b), Nat.add(c, b))
|
||||
): Equal<Nat>(a, c)
|
||||
let lemma = Equal.rewrite<Nat>(
|
||||
Nat.add(a,b), Nat.add(b,a), Nat.add.comm(a, b),
|
||||
(x) Equal<Nat>(x, Nat.add(c, b))
|
||||
h
|
||||
)
|
||||
let lemma = Equal.rewrite<Nat>(
|
||||
Nat.add(c,b), Nat.add(b,c), Nat.add.comm(c, b),
|
||||
(x) Equal<Nat>(Nat.add(b, a), x)
|
||||
lemma
|
||||
)
|
||||
let qed = Nat.add.cancel_left(b, a, c, lemma)
|
||||
qed
|
||||
|
@ -1,13 +1,26 @@
|
||||
Nat.add.comm(a: Nat, b:Nat): (a + b) == (b + a)
|
||||
case a{
|
||||
zero: mirror(Nat.add.zero_right(b))
|
||||
Nat.add.comm(
|
||||
a: Nat, b:Nat
|
||||
): Equal<Nat>(Nat.add(a, b), Nat.add(b, a))
|
||||
case a {
|
||||
zero:
|
||||
Equal.mirror<Nat>(
|
||||
Nat.add(b,0), b
|
||||
Nat.add.zero_right(b)
|
||||
)
|
||||
succ:
|
||||
let p0 = Nat.add.succ_right(b, a.pred)
|
||||
let p1 = mirror(p0)
|
||||
let h2 = Nat.add.comm(b, a.pred)
|
||||
let p3 = p1 :: rewrite x in Nat.succ(x) == Nat.add(b,Nat.succ(a.pred)) with h2
|
||||
// here p3 should close the goal.
|
||||
let p4 = mirror(Nat.add.succ_left(a.pred,b))
|
||||
let p5 = p3 :: rewrite x in x == _ with p4
|
||||
p5
|
||||
}!
|
||||
let ind = Nat.add.comm(a.pred, b)
|
||||
let lemma = Equal.apply<Nat, Nat>(
|
||||
Nat.add(a.pred,b), Nat.add(b,a.pred)
|
||||
Nat.succ, ind
|
||||
)
|
||||
let succ_right = Equal.mirror<Nat>(
|
||||
Nat.add(b,Nat.succ(a.pred)), Nat.succ(Nat.add(b,a.pred))
|
||||
Nat.add.succ_right(b, a.pred)
|
||||
)
|
||||
let qed = Equal.rewrite<Nat>(
|
||||
Nat.succ(Nat.add(b,a.pred)), Nat.add(b,Nat.succ(a.pred)), succ_right
|
||||
(x) Equal<Nat>(Nat.add(Nat.succ(a.pred), b), x)
|
||||
lemma
|
||||
)
|
||||
qed
|
||||
}: Equal<Nat>(Nat.add(a, b), Nat.add(b, a))
|
||||
|
@ -1,5 +1,6 @@
|
||||
Nat.add.succ_both(a: Nat, b: Nat)
|
||||
: (Nat.succ(a) + Nat.succ(b)) == Nat.succ(Nat.succ(a + b))
|
||||
Nat.add.succ_both(
|
||||
a: Nat, b: Nat
|
||||
): (Nat.succ(a) + Nat.succ(b)) == Nat.succ(Nat.succ(a + b))
|
||||
case a {
|
||||
zero: refl
|
||||
succ: apply(Nat.succ, Nat.add.succ_both(a.pred, b))
|
||||
|
@ -1,2 +1,2 @@
|
||||
Nat.div_mod(n: Nat, m: Nat): Pair<Nat, Nat>
|
||||
Nat.div_mod.go(n, m, Nat.zero)
|
||||
Nat.div_mod.go(m, 0, n)
|
||||
|
@ -1,5 +1,7 @@
|
||||
Nat.div_mod.go(n: Nat, m: Nat, d: Nat): Pair<Nat, Nat>
|
||||
case Nat.sub_rem(n, m) as p {
|
||||
left: Nat.div_mod.go(p.value, m, Nat.succ(d)),
|
||||
right: Pair.new!!(d, n),
|
||||
}
|
||||
Nat.div_mod.go(n: Nat, d: Nat, r: Nat): Pair<Nat, Nat>
|
||||
case Nat.lte(n, r) {
|
||||
false:
|
||||
Pair.new!!(d, r)
|
||||
true:
|
||||
Nat.div_mod.go(n, Nat.succ(d), Nat.sub(r, n))
|
||||
}
|
||||
|
65
base/Nat/div_mod/recover.kind
Normal file
65
base/Nat/div_mod/recover.kind
Normal file
@ -0,0 +1,65 @@
|
||||
// (n % m) + (n / m) * m = n
|
||||
Nat.div_mod.recover(
|
||||
n: Nat, m: Nat
|
||||
Hyp: Equal<Bool>(Nat.lte(1, m), true)
|
||||
): Equal<Nat>(
|
||||
Nat.add(Nat.mod(n, m), Nat.mul(Nat.div(n, m), m))
|
||||
n
|
||||
)
|
||||
let lemma = Nat.div_mod.recover.go(n, m, 0, n, Hyp, refl)
|
||||
let comm = Nat.add.comm(Nat.mul(Nat.div(n, m), m), Nat.mod(n, m))
|
||||
let qed = lemma :: rewrite X in Equal<Nat>(X, n) with comm
|
||||
qed
|
||||
|
||||
//Nat.div_mod.go(2, 0, 7) Nat.div_mod.recover.go(7, 2, 0, 7, 0*2 + 7 == 7)
|
||||
//Nat.div_mod.go(2, 1, 5) Nat.div_mod.recover.go(7, 2, 1, 5, 1*2 + 5 == 7)
|
||||
//Nat.div_mod.go(2, 2, 3) Nat.div_mod.recover.go(7, 2, 2, 3, 2*2 + 3 == 7)
|
||||
//Nat.div_mod.go(2, 3, 1) Nat.div_mod.recover.go(7, 2, 3, 1, 3*2 + 1 == 7)
|
||||
//{3, 1}
|
||||
|
||||
Nat.div_mod.recover.go(
|
||||
m: Nat
|
||||
n: Nat
|
||||
d: Nat
|
||||
r: Nat
|
||||
Hyp0: Equal<Bool>(Nat.lte(1, n), true)
|
||||
Hyp1: Equal<Nat>(Nat.add(Nat.mul(d, n), r), m)
|
||||
): def p = Nat.div_mod.go(n, d, r)
|
||||
def d = Pair.fst<Nat, Nat>(p)
|
||||
def r = Pair.snd<Nat, Nat>(p)
|
||||
Equal<Nat>(
|
||||
Nat.add(Nat.mul(d, n), r)
|
||||
m
|
||||
)
|
||||
def cmp = Nat.lte(n, r)
|
||||
def cmp_eq = refl :: cmp == cmp
|
||||
case cmp with cmp_eq : cmp^ == cmp {
|
||||
true:
|
||||
let comm = Nat.add.comm(Nat.mul(d,n), r)
|
||||
let lemma = Hyp1 :: rewrite X in Equal<Nat>(X, m) with comm
|
||||
let sub = mirror(Nat.sub.add!!(cmp_eq))
|
||||
let lemma = lemma :: rewrite X in Equal<Nat>(Nat.add(X,Nat.mul(d,n)), m) with sub
|
||||
let assoc = mirror(Nat.add.assoc(Nat.sub(r,n), n, Nat.mul(d,n)))
|
||||
let lemma = chain(assoc, lemma)
|
||||
let comm = Nat.add.comm(Nat.add(n,Nat.mul(d,n)), Nat.sub(r,n))
|
||||
let lemma = chain(comm, lemma)
|
||||
let ind = Nat.div_mod.recover.go(m, n, Nat.succ(d), Nat.sub(r,n), Hyp0, lemma)
|
||||
ind
|
||||
false:
|
||||
Hyp1
|
||||
}! :: Equal<Nat>(
|
||||
def p =
|
||||
cmp(
|
||||
() Pair(Nat,Nat)
|
||||
Nat.div_mod.go(n,Nat.succ(d),Nat.sub(r,n))
|
||||
Pair.new(Nat,Nat,d,r)
|
||||
)
|
||||
Nat.add(
|
||||
Nat.mul(
|
||||
Pair.fst<Nat,Nat>(p)
|
||||
n
|
||||
)
|
||||
Pair.snd<Nat, Nat>(p)
|
||||
)
|
||||
m
|
||||
)
|
@ -1,8 +1,10 @@
|
||||
Nat.lte(n: Nat, m: Nat): Bool
|
||||
case n {
|
||||
zero: Bool.true,
|
||||
succ: case m {
|
||||
zero: Bool.false,
|
||||
succ: Nat.lte(n.pred, m.pred),
|
||||
}
|
||||
}
|
||||
zero:
|
||||
true,
|
||||
succ:
|
||||
case m {
|
||||
zero: false,
|
||||
succ: Nat.lte(n.pred, m.pred),
|
||||
}
|
||||
}
|
||||
|
44
base/Nat/lte/comm.kind
Normal file
44
base/Nat/lte/comm.kind
Normal file
@ -0,0 +1,44 @@
|
||||
Nat.lte.comm.false(
|
||||
a: Nat
|
||||
b: Nat
|
||||
Hyp: Equal<Bool>(Nat.lte(a, b), false)
|
||||
): Equal<Bool>(Nat.lte(Nat.succ(b), a), true)
|
||||
(case a {
|
||||
zero:
|
||||
(Hyp)
|
||||
let contra = Bool.true_neq_false(Hyp)
|
||||
Empty.absurd<Equal<Bool>(Nat.lte(Nat.succ(b), 0), true)>(contra)
|
||||
succ:
|
||||
(Hyp)
|
||||
(case b {
|
||||
zero:
|
||||
(Hyp)
|
||||
Equal.refl<Bool>(true)
|
||||
succ:
|
||||
(Hyp)
|
||||
let qed = Nat.lte.comm.false(a.pred, b.pred, Hyp)
|
||||
qed
|
||||
}: (Hyp: Equal<Bool>(Nat.lte(Nat.succ(a.pred), b), false)) -> Equal<Bool>(Nat.lte(Nat.succ(b), Nat.succ(a.pred)), true))(
|
||||
Hyp
|
||||
)
|
||||
}: (Hyp: Equal<Bool>(Nat.lte(a, b), false)) -> Equal<Bool>(Nat.lte(Nat.succ(b), a), true))(
|
||||
Hyp
|
||||
)
|
||||
|
||||
Nat.lte.comm.true(
|
||||
a: Nat
|
||||
b: Nat
|
||||
Hyp: Equal<Bool>(Nat.lte(Nat.succ(a), b), true)
|
||||
): Equal<Bool>(Nat.lte(b, a), false)
|
||||
case b with Hyp {
|
||||
zero:
|
||||
let contra = Bool.false_neq_true(Hyp)
|
||||
Empty.absurd!(contra)
|
||||
succ:
|
||||
case a with Hyp {
|
||||
zero:
|
||||
Equal.refl<Bool>(false)
|
||||
succ:
|
||||
Nat.lte.comm.true(a.pred, b.pred, Hyp)
|
||||
}!
|
||||
}!
|
17
base/Nat/lte/succ_left.kind
Normal file
17
base/Nat/lte/succ_left.kind
Normal file
@ -0,0 +1,17 @@
|
||||
Nat.lte.succ_left(
|
||||
a: Nat
|
||||
b: Nat
|
||||
Hyp: Equal<Bool>(Nat.lte(Nat.succ(a), b), true)
|
||||
): Equal<Bool>(Nat.lte(a, b), true)
|
||||
case b with Hyp {
|
||||
zero:
|
||||
let contra = Bool.false_neq_true(Hyp)
|
||||
Empty.absurd!(contra)
|
||||
succ:
|
||||
case a with Hyp {
|
||||
zero:
|
||||
refl
|
||||
succ:
|
||||
Nat.lte.succ_left(a.pred, b.pred, Hyp)
|
||||
}!
|
||||
}!
|
@ -1,5 +1,7 @@
|
||||
Nat.max(a:Nat, b:Nat): Nat
|
||||
case Nat.gtn(a, b) {
|
||||
true:a
|
||||
false:b
|
||||
}
|
||||
Nat.max(a: Nat, b: Nat): Nat
|
||||
case Nat.lte(a, b) {
|
||||
true:
|
||||
b
|
||||
false:
|
||||
a
|
||||
}
|
||||
|
26
base/Nat/max/big.kind
Normal file
26
base/Nat/max/big.kind
Normal file
@ -0,0 +1,26 @@
|
||||
Nat.max.big(
|
||||
a: Nat
|
||||
b: Nat
|
||||
): And<Equal<Bool>(Nat.lte(a, Nat.max(a, b)), true), Equal<Bool>(Nat.lte(b, Nat.max(a,b)), true)>
|
||||
def cmp_ab = Nat.lte(a, b)
|
||||
let lemma_ab = Equal.refl!(cmp_ab)
|
||||
(case cmp_ab {
|
||||
true:
|
||||
(lemma_ab)
|
||||
Pair.new!!(lemma_ab, Nat.Order.refl(b))
|
||||
false:
|
||||
(lemma_ab)
|
||||
let lemma_ba = Nat.lte.comm.false!!(lemma_ab)
|
||||
let lemma_ba = Nat.lte.succ_left!!(lemma_ba)
|
||||
Pair.new!!(Nat.Order.refl(a), lemma_ba)
|
||||
}: (lemma_ab: Equal<Bool>(Nat.lte(a, b), cmp_ab)) -> And<
|
||||
Equal<Bool>(Nat.lte(a, case cmp_ab { true: b, false: a }), true),
|
||||
Equal<Bool>(Nat.lte(b, case cmp_ab { true: b, false: a }), true)>)(
|
||||
lemma_ab
|
||||
)
|
||||
|
||||
Nat.max.big.left(a: Nat, b: Nat): Equal<Bool>(Nat.lte(a, Nat.max(a, b)), true)
|
||||
Pair.fst!!(Nat.max.big(a, b))
|
||||
|
||||
Nat.max.big.right(a: Nat, b: Nat): Equal<Bool>(Nat.lte(b, Nat.max(a,b)), true)
|
||||
Pair.snd!!(Nat.max.big(a, b))
|
22
base/Nat/max/combine.kind
Normal file
22
base/Nat/max/combine.kind
Normal file
@ -0,0 +1,22 @@
|
||||
Nat.max.combine.right(
|
||||
a: Nat
|
||||
b: Nat
|
||||
c: Nat
|
||||
Hyp: Equal<Bool>(Nat.lte(a, b), true)
|
||||
): Equal<Bool>(Nat.lte(a, Nat.max(b, c)), true)
|
||||
Nat.Order.chain!!!(Hyp, Nat.max.big.left(b, c))
|
||||
|
||||
Nat.max.combine.left(
|
||||
a: Nat
|
||||
b: Nat
|
||||
c: Nat
|
||||
Hyp0: Equal<Bool>(Nat.lte(a, b), true)
|
||||
Hyp1: Equal<Bool>(Nat.lte(c, b), true)
|
||||
): Equal<Bool>(Nat.lte(Nat.max(a, c), b), true)
|
||||
def cmp_ac = Nat.lte(a, c)
|
||||
case cmp_ac {
|
||||
true:
|
||||
Hyp1
|
||||
false:
|
||||
Hyp0
|
||||
}! :: Equal<Bool>(Nat.lte(cmp_ac(() Nat, c, a), b), true)
|
45
base/Nat/max/comm.kind
Normal file
45
base/Nat/max/comm.kind
Normal file
@ -0,0 +1,45 @@
|
||||
Nat.max.comm(
|
||||
a: Nat
|
||||
b: Nat
|
||||
): Equal<Nat>(Nat.max(a, b), Nat.max(b, a))
|
||||
let lemma = Nat.Order.trichotomy(a, b)
|
||||
case lemma {
|
||||
fst:
|
||||
let lemma_ba = Nat.lte.comm.false!!(lemma.value)
|
||||
let lemma_ba = Nat.lte.succ_left!!(lemma_ba)
|
||||
let qed = Equal.refl<Nat>(a)
|
||||
let qed = Equal.rewrite<Bool>(
|
||||
false, Nat.lte(a, b), mirror(lemma.value),
|
||||
(x) Equal<Nat>(x(() Nat, b, a), true(() Nat, a, b))
|
||||
qed
|
||||
)
|
||||
let qed = Equal.rewrite<Bool>(
|
||||
true, Nat.lte(b, a), mirror(lemma_ba),
|
||||
(x) Equal<Nat>(Nat.lte(a, b, () Nat, b, a), x(() Nat, a, b))
|
||||
qed
|
||||
)
|
||||
qed
|
||||
snd:
|
||||
let qed = Equal.refl<Nat>(Nat.max(a, a))
|
||||
let qed = Equal.rewrite<Nat>(
|
||||
a, b, lemma.value
|
||||
(x) Equal<Nat>(Nat.max(a, x), Nat.max(x, a))
|
||||
qed
|
||||
)
|
||||
qed
|
||||
trd:
|
||||
let lemma_ab = Nat.lte.comm.false!!(lemma.value)
|
||||
let lemma_ab = Nat.lte.succ_left!!(lemma_ab)
|
||||
let qed = Equal.refl<Nat>(b)
|
||||
let qed = Equal.rewrite<Bool>(
|
||||
false, Nat.lte(b, a), mirror(lemma.value),
|
||||
(x) Equal<Nat>(true(() Nat, b, a), x(() Nat, a, b))
|
||||
qed
|
||||
)
|
||||
let qed = Equal.rewrite<Bool>(
|
||||
true, Nat.lte(a, b), mirror(lemma_ab),
|
||||
(x) Equal<Nat>(x(() Nat, b, a), Nat.lte(b, a, () Nat, a, b))
|
||||
qed
|
||||
)
|
||||
qed
|
||||
}
|
8
base/Nat/max/split.kind
Normal file
8
base/Nat/max/split.kind
Normal file
@ -0,0 +1,8 @@
|
||||
Nat.max.split.left(
|
||||
a: Nat
|
||||
b: Nat
|
||||
c: Nat
|
||||
Hyp: Equal<Bool>(Nat.lte(Nat.max(a, b), c), true)
|
||||
): And<Equal<Bool>(Nat.lte(a, c), true), Equal<Bool>(Nat.lte(b, c), true)>
|
||||
let {left_lemma, right_lemma} = Nat.max.big(a, b)
|
||||
{Nat.Order.chain!!!(left_lemma, Hyp), Nat.Order.chain!!!(right_lemma, Hyp)}
|
@ -1,3 +1,3 @@
|
||||
// Finds the remainder of division of n by m
|
||||
Nat.mod(n: Nat, m: Nat): Nat
|
||||
Nat.mod.go(n, m, 0)
|
||||
Pair.snd!!(Nat.div_mod(n, m))
|
||||
|
35
base/Nat/mod/small.kind
Normal file
35
base/Nat/mod/small.kind
Normal file
@ -0,0 +1,35 @@
|
||||
//Nat.mod.small(
|
||||
// n: Nat
|
||||
// m: Nat
|
||||
// Hyp: Equal<Bool>(Nat.lte(1, m), true)
|
||||
//): Equal<Bool>(Nat.lte(m, Nat.mod(n, m)), false)
|
||||
// ?mod.small.body
|
||||
|
||||
Nat.mod.small.aux(
|
||||
n: Nat
|
||||
d: Nat
|
||||
r: Nat
|
||||
Hyp: Equal<Bool>(Nat.lte(1, n), true)
|
||||
): Equal<Bool>(Nat.lte(n, Pair.snd<Nat, Nat>(Nat.div_mod.go(n, d, r))), false)
|
||||
def cmp = Nat.lte(n, r)
|
||||
let cmp_eq = refl :: cmp == cmp
|
||||
case cmp with cmp_eq : cmp^ == cmp {
|
||||
true:
|
||||
Nat.mod.small.aux(n, Nat.succ(d), Nat.sub(r, n), Hyp)
|
||||
false:
|
||||
cmp_eq
|
||||
}! ::
|
||||
Equal<Bool>(
|
||||
Nat.lte(
|
||||
n
|
||||
Pair.snd(
|
||||
Nat, Nat
|
||||
cmp(
|
||||
() Pair(Nat,Nat)
|
||||
Nat.div_mod.go(n,Nat.succ(d),Nat.sub(r,n))
|
||||
Pair.new(Nat,Nat,d,r)
|
||||
)
|
||||
)
|
||||
)
|
||||
Bool.false
|
||||
)
|
@ -1,5 +1,7 @@
|
||||
Nat.mul(n: Nat, m: Nat): Nat
|
||||
case m {
|
||||
zero: Nat.zero,
|
||||
succ: Nat.add(n, Nat.mul(n, m.pred)),
|
||||
}
|
||||
case n {
|
||||
zero:
|
||||
0
|
||||
succ:
|
||||
Nat.add(m, Nat.mul(n.pred, m))
|
||||
}
|
||||
|
@ -1,8 +1,32 @@
|
||||
Nat.mul.assoc(a: Nat, b: Nat, c: Nat): (a * b * c) == (a * b) * c
|
||||
case c{
|
||||
zero: refl
|
||||
succ:
|
||||
let begin = Equal.refl<_, (a * b) + (a * (b * c.pred))>
|
||||
let second = begin :: rewrite x in x == (a * b) + (a * (b * c.pred)) with mirror(Nat.mul.distrib_left(a, b, b * c.pred))
|
||||
second :: rewrite x in _ == (a * b) + x with Nat.mul.assoc(a,b,c.pred)
|
||||
}!
|
||||
Nat.mul.assoc(
|
||||
a: Nat, b: Nat, c: Nat
|
||||
): Equal<Nat>(Nat.mul(a, Nat.mul(b, c)), Nat.mul(Nat.mul(a, b), c))
|
||||
case a {
|
||||
zero:
|
||||
Equal.refl<Nat>(0)
|
||||
succ:
|
||||
let ind = Nat.mul.assoc(a.pred, b, c)
|
||||
let lemma = Equal.apply<Nat, Nat>(
|
||||
Nat.mul(a.pred,Nat.mul(b,c)), Nat.mul(Nat.mul(a.pred,b),c), Nat.add(Nat.mul(b, c))
|
||||
ind
|
||||
)
|
||||
let distrib = Equal.mirror<Nat>(
|
||||
Nat.mul(Nat.add(b,Nat.mul(a.pred,b)),c), Nat.add(Nat.mul(b,c),Nat.mul(Nat.mul(a.pred,b),c))
|
||||
Nat.mul.distrib_right(b, Nat.mul(a.pred, b), c)
|
||||
)
|
||||
let qed = Equal.rewrite<Nat>(
|
||||
Nat.add(Nat.mul(b,c),Nat.mul(Nat.mul(a.pred,b),c))
|
||||
Nat.mul(Nat.add(b,Nat.mul(a.pred,b)),c)
|
||||
distrib,
|
||||
(x) Equal<Nat>(Nat.add(Nat.mul(b,c),Nat.mul(a.pred,Nat.mul(b,c))), x)
|
||||
lemma
|
||||
)
|
||||
qed
|
||||
}: Equal<Nat>(Nat.mul(a, Nat.mul(b, c)), Nat.mul(Nat.mul(a, b), c))
|
||||
|
||||
// induction on a
|
||||
// - ind: a.pred * b * c == (a.pred * b) * c ok
|
||||
// (b * c) + (a.pred * b * c) == (b * c) + ((a.pred * b) * c) ok
|
||||
// (b * c) + (a.pred * b * c) == (b + a.pred * b) * c
|
||||
// succ(a.pred) * b * c == (succ(a.pred) * b) * c
|
||||
// - goal: succ(a.pred) * b * c == (succ(a.pred) * b) * c
|
||||
|
@ -1,5 +1,24 @@
|
||||
Nat.mul.comm(a: Nat, b: Nat): (a * b) == b * a
|
||||
case b {
|
||||
zero: mirror(Nat.mul.zero_left(a))
|
||||
succ: mirror(Nat.mul.comm(Nat.succ(b.pred), a))
|
||||
}!
|
||||
Nat.mul.comm(a: Nat, b: Nat): Equal<Nat>(Nat.mul(a, b), Nat.mul(b, a))
|
||||
case a {
|
||||
zero:
|
||||
Equal.mirror<Nat>(Nat.mul(b, 0), 0, Nat.mul.zero_right(b))
|
||||
succ:
|
||||
let ind = Nat.mul.comm(a.pred, b)
|
||||
let lemma = Equal.apply<Nat, Nat>(
|
||||
Nat.mul(a.pred,b), Nat.mul(b,a.pred)
|
||||
Nat.add(b), ind
|
||||
)
|
||||
let succ_right = mirror(Nat.mul.succ_right(b, a.pred))
|
||||
let qed = Equal.rewrite<Nat>(
|
||||
Nat.add(b,Nat.mul(b,a.pred)), Nat.mul(b,Nat.succ(a.pred))
|
||||
succ_right,
|
||||
(x) Equal<Nat>(Nat.add(b,Nat.mul(a.pred,b)), x)
|
||||
lemma
|
||||
)
|
||||
qed
|
||||
}: Equal<Nat>(Nat.mul(a, b), Nat.mul(b, a))
|
||||
|
||||
// ind: a.pred * b == b * a.pred
|
||||
// b + a.pred * b == b + b * a.pred
|
||||
// b + a.pred * b == b * succ(a.pred)
|
||||
// goal: succ(a.pred) * b == b * succ(a.pred)
|
||||
|
@ -1,11 +1,21 @@
|
||||
Nat.mul.distrib_left(a: Nat, b: Nat, c: Nat):
|
||||
(a * (b + c)) == ((a * b) + (a * c))
|
||||
case b{
|
||||
zero: refl
|
||||
succ:
|
||||
let final = Equal.refl<_, (a + (a * b.pred)) + (a * c)>
|
||||
let final2 = final :: rewrite x in x == (a + (a * b.pred)) + (a * c) with Nat.add.assoc(a, a * b.pred, a * c)
|
||||
let f = final2 :: rewrite x in (a + x) == (a + (a * b.pred)) + (a*c) with mirror(Nat.mul.distrib_left(a, b.pred, c))
|
||||
f
|
||||
}!
|
||||
|
||||
Nat.mul.distrib_left(
|
||||
a: Nat, b: Nat, c: Nat
|
||||
): Equal<Nat>(Nat.mul(a, Nat.add(b, c)), Nat.add(Nat.mul(a, b), Nat.mul(a, c)))
|
||||
let lemma = Nat.mul.distrib_right(b, c, a)
|
||||
let lemma = Equal.rewrite<Nat>(
|
||||
Nat.mul(Nat.add(b, c), a), Nat.mul(a, Nat.add(b, c))
|
||||
Nat.mul.comm(Nat.add(b, c), a)
|
||||
(x) Equal<Nat>(x, Nat.add(Nat.mul(b,a),Nat.mul(c,a)))
|
||||
lemma
|
||||
)
|
||||
let lemma = Equal.rewrite<Nat>(
|
||||
Nat.mul(b, a), Nat.mul(a, b), Nat.mul.comm(b, a)
|
||||
(x) Equal<Nat>(Nat.mul(a,Nat.add(b,c)), Nat.add(x, Nat.mul(c,a)))
|
||||
lemma
|
||||
)
|
||||
let qed = Equal.rewrite<Nat>(
|
||||
Nat.mul(c, a), Nat.mul(a, c), Nat.mul.comm(c, a)
|
||||
(x) Equal<Nat>(Nat.mul(a, Nat.add(b,c)), Nat.add(Nat.mul(a, b), x))
|
||||
lemma
|
||||
)
|
||||
qed
|
||||
|
27
base/Nat/mul/distrib_right.kind
Normal file
27
base/Nat/mul/distrib_right.kind
Normal file
@ -0,0 +1,27 @@
|
||||
Nat.mul.distrib_right(
|
||||
a: Nat, b: Nat, c: Nat
|
||||
): Equal<Nat>(Nat.mul(Nat.add(a, b), c), Nat.add(Nat.mul(a, c), Nat.mul(b, c)))
|
||||
case a {
|
||||
zero:
|
||||
Equal.refl<Nat>(Nat.mul(b, c))
|
||||
succ:
|
||||
// ind: (a.pred + b) * c == (a.pred * c) + (b * c)
|
||||
// lemma: c + (a.pred + b) * c == c + (a.pred * c) + (b * c)
|
||||
// qed: c + (a.pred + b) * c == (c + (a.pred * c)) + (b * c)
|
||||
let ind = Nat.mul.distrib_right(
|
||||
a.pred, b, c
|
||||
)
|
||||
let lemma = Equal.apply<Nat, Nat>(
|
||||
Nat.mul(Nat.add(a.pred,b),c), Nat.add(Nat.mul(a.pred,c),Nat.mul(b,c)), Nat.add(c), ind
|
||||
)
|
||||
let assoc = Equal.mirror<Nat>(
|
||||
Nat.add(Nat.add(c,Nat.mul(a.pred,c)),Nat.mul(b,c)), Nat.add(c,Nat.add(Nat.mul(a.pred,c),Nat.mul(b,c)))
|
||||
Nat.add.assoc(c, Nat.mul(a.pred, c), Nat.mul(b, c))
|
||||
)
|
||||
let qed = Equal.rewrite<Nat>(
|
||||
Nat.add(c,Nat.add(Nat.mul(a.pred,c),Nat.mul(b,c))), Nat.add(Nat.add(c,Nat.mul(a.pred,c)),Nat.mul(b,c)), assoc,
|
||||
(x) Equal<Nat>(Nat.add(c, Nat.mul(Nat.add(a.pred, b), c)), x)
|
||||
lemma
|
||||
)
|
||||
qed
|
||||
}: Equal<Nat>(Nat.mul(Nat.add(a, b), c), Nat.add(Nat.mul(a, c), Nat.mul(b, c)))
|
@ -1,7 +1,2 @@
|
||||
Nat.mul.one_left(a: Nat): (1 * a) == a
|
||||
case a{
|
||||
zero: refl
|
||||
succ:
|
||||
let h = Nat.mul.one_left(a.pred)
|
||||
Equal.apply!!<Nat.mul(1,a.pred),a.pred,Nat.succ>(h)
|
||||
}!
|
||||
Nat.mul.one_left(a: Nat): Equal<Nat>(Nat.mul(1, a), a)
|
||||
Nat.add.zero_right(a)
|
||||
|
@ -1,2 +1,11 @@
|
||||
Nat.mul.one_right(a: Nat): (a * 1) == a
|
||||
Nat.add.zero_right(a)
|
||||
Nat.mul.one_right(a: Nat): Equal<Nat>(Nat.mul(a, 1), a)
|
||||
case a {
|
||||
zero:
|
||||
Equal.refl<Nat>(0)
|
||||
succ:
|
||||
let ind = Nat.mul.one_right(a.pred)
|
||||
let qed = Equal.apply<Nat, Nat>(
|
||||
Nat.mul(a.pred, 1), a.pred, Nat.succ, ind
|
||||
)
|
||||
qed
|
||||
}: Equal<Nat>(Nat.mul(a, 1), a)
|
||||
|
@ -1,7 +1,2 @@
|
||||
// FIXME: this proof isn't working as written anymore
|
||||
Nat.mul.succ_left(a: Nat, b: Nat): (Nat.succ(a) * b) == b + (a * b)
|
||||
Nat.mul.succ_left(a, b)
|
||||
//let h = Nat.mul.succ_right(b,a)
|
||||
//let left = h :: rewrite x in x == _ with Nat.mul.comm(_ _)
|
||||
//let final = left :: rewrite x in _ == Nat.add(b,x) with Nat.mul.comm(_ _)
|
||||
//final
|
||||
Nat.mul.succ_left(a: Nat, b: Nat): Equal<Nat>(Nat.mul(Nat.succ(a), b), Nat.add(b, Nat.mul(a, b)))
|
||||
Equal.refl<Nat>(Nat.mul(Nat.succ(a), b))
|
||||
|
@ -1,3 +1,42 @@
|
||||
Nat.mul.succ_right(a: Nat, b: Nat)
|
||||
: (a * Nat.succ(b)) == a + (a * b)
|
||||
refl
|
||||
Nat.mul.succ_right(
|
||||
a: Nat, b: Nat
|
||||
): Equal<Nat>(Nat.mul(a, Nat.succ(b)), Nat.add(a, Nat.mul(a, b)))
|
||||
case a {
|
||||
zero:
|
||||
Equal.refl<Nat>(0)
|
||||
succ:
|
||||
let ind = Nat.mul.succ_right(a.pred, b)
|
||||
let lemma = Equal.apply<Nat, Nat>(
|
||||
Nat.mul(a.pred,Nat.succ(b)), Nat.add(a.pred, Nat.mul(a.pred, b)),
|
||||
(x) Nat.add(b, x), ind
|
||||
)
|
||||
let assoc_to =
|
||||
Equal.mirror<Nat>(
|
||||
Nat.add(Nat.add(b, a.pred), Nat.mul(a.pred, b)), Nat.add(b, Nat.add(a.pred, Nat.mul(a.pred, b))),
|
||||
Nat.add.assoc(b, a.pred, Nat.mul(a.pred, b))
|
||||
)
|
||||
let lemma = Equal.rewrite<Nat>(
|
||||
Nat.add(b, Nat.add(a.pred, Nat.mul(a.pred,b))), Nat.add(Nat.add(b, a.pred),Nat.mul(a.pred,b)),
|
||||
assoc_to,
|
||||
(x) Equal<Nat>(Nat.add(b, Nat.mul(a.pred, Nat.succ(b))), x),
|
||||
lemma
|
||||
)
|
||||
let lemma = Equal.rewrite<Nat>(
|
||||
Nat.add(b, a.pred), Nat.add(a.pred, b),
|
||||
Nat.add.comm(b, a.pred),
|
||||
(x) Equal<Nat>(Nat.add(b, Nat.mul(a.pred, Nat.succ(b))), Nat.add(x,Nat.mul(a.pred,b))),
|
||||
lemma
|
||||
)
|
||||
let assoc_back = Nat.add.assoc(a.pred, b, Nat.mul(a.pred, b))
|
||||
let lemma = Equal.rewrite<Nat>(
|
||||
Nat.add(Nat.add(a.pred, b),Nat.mul(a.pred,b)), Nat.add(a.pred, Nat.add(b, Nat.mul(a.pred,b))),
|
||||
assoc_back,
|
||||
(x) Equal<Nat>(Nat.add(b, Nat.mul(a.pred, Nat.succ(b))), x),
|
||||
lemma
|
||||
)
|
||||
let qed = Equal.apply<Nat, Nat>(
|
||||
Nat.add(b,Nat.mul(a.pred,Nat.succ(b))), Nat.add(a.pred,Nat.add(b,Nat.mul(a.pred,b))),
|
||||
Nat.succ, lemma
|
||||
)
|
||||
qed
|
||||
}: Equal<Nat>(Nat.mul(a, Nat.succ(b)), Nat.add(a, Nat.mul(a, b)))
|
||||
|
@ -1,7 +1,8 @@
|
||||
Nat.mul.zero_left(a: Nat): (0 * a) == 0
|
||||
case a{
|
||||
zero: refl
|
||||
Nat.mul.zero_left(a: Nat): Equal<Nat>(Nat.mul(0, a), 0)
|
||||
case a {
|
||||
zero:
|
||||
Equal.refl<Nat>(0)
|
||||
succ:
|
||||
let h = Nat.mul.zero_left(a.pred)
|
||||
apply((x) (0+x), h)
|
||||
}!
|
||||
h
|
||||
}: Equal<Nat>(Nat.mul(0, a), 0)
|
||||
|
@ -1,2 +1,7 @@
|
||||
Nat.mul.zero_right(a: Nat): (a * 0) == 0
|
||||
refl
|
||||
Nat.mul.zero_right(a: Nat): Equal<Nat>(Nat.mul(a, 0), 0)
|
||||
case a {
|
||||
zero:
|
||||
Equal.refl<Nat>(0)
|
||||
succ:
|
||||
Nat.mul.zero_right(a.pred)
|
||||
}: Equal<Nat>(Nat.mul(a, 0), 0)
|
||||
|
24
base/Nat/sub/add.kind
Normal file
24
base/Nat/sub/add.kind
Normal file
@ -0,0 +1,24 @@
|
||||
Nat.sub.add(
|
||||
n: Nat
|
||||
m: Nat
|
||||
Hyp: Equal<Bool>(Nat.lte(n, m), true)
|
||||
): Equal<Nat>(Nat.add(Nat.sub(m, n), n), m)
|
||||
case m with Hyp {
|
||||
zero:
|
||||
let zero_n = mirror(Nat.Order.chain.aux!(Hyp))
|
||||
let lemma = refl :: Nat.add(Nat.sub(0, 0), 0) == 0
|
||||
let qed = lemma :: rewrite X in Equal<Nat>(Nat.add(Nat.sub(0, X), X), 0) with zero_n
|
||||
qed
|
||||
succ:
|
||||
case n with Hyp {
|
||||
zero:
|
||||
let qed = Nat.add.zero_right(Nat.succ(m.pred))
|
||||
qed
|
||||
succ:
|
||||
let lemma = Nat.sub.add(n.pred, m.pred, Hyp)
|
||||
let lemma = apply(Nat.succ, lemma)
|
||||
let lemma_left = Nat.add.succ_right(Nat.sub(m.pred,n.pred),n.pred)
|
||||
let qed = chain(lemma_left, lemma)
|
||||
qed
|
||||
}!
|
||||
}!
|
@ -1,2 +1,2 @@
|
||||
Nat.succ_neq_zero(a: Nat): Not(Equal<Nat, Nat.succ(a), 0>)
|
||||
(e) Bool.false_neq_true(apply(Nat.is_zero, e))
|
||||
(e) Bool.false_neq_true(Equal.apply<Nat, Bool>(Nat.succ(a), 0, Nat.is_zero, e))
|
||||
|
@ -66,19 +66,98 @@ String.hex.encode.utf8(str: String): String
|
||||
String.concat(hex, String.to_hex(str.tail))
|
||||
}
|
||||
|
||||
// TODO: create String.hex.decode.utf8
|
||||
String.hex.decode.utf8(hex: String): String
|
||||
//U16.from_hex.utf8(hex)
|
||||
let rmv_start = String.drop(4, hex) // remove "0x" + first byte
|
||||
Bytes.to_string.aux(rmv_start)
|
||||
|
||||
String.hex.decode.utf8.aux(hex: String): U16
|
||||
log("b: "| hex)
|
||||
let c = Bytes.take(2, hex)
|
||||
String.to_u16(c)
|
||||
// 28 Sep 21
|
||||
// Author: Maisa Milena
|
||||
// FIXME:
|
||||
// - parse characters using 3 and 4 bytes
|
||||
// - deal with parse error
|
||||
// Hint: check the test cases in Bytes/test/parse_string.kind
|
||||
// and add more tests
|
||||
|
||||
// IMPORTANT: do not use these functions yet. Still WIP
|
||||
|
||||
String.hex.test: _
|
||||
log("decode")
|
||||
// String.hex.decode.utf8("0x3233343536373839")
|
||||
String.hex.decode.utf8("0xa2")
|
||||
// Decode a UTF8 data into a String
|
||||
|
||||
String.hex.decode.utf8(b: String): String
|
||||
String.hex.decode.utf8.aux(b, "")
|
||||
|
||||
String.hex.decode.utf8.take_pair(b: String): Pair(String, Maybe(String))
|
||||
let fst = String.take(2, b)
|
||||
let snd = String.drop(2, String.take(4, b))
|
||||
if String.is_empty(snd)
|
||||
then {fst, Maybe.none!}
|
||||
else {fst, Maybe.some!(snd)}
|
||||
|
||||
String.hex.decode.utf8.aux(b: String, s: String): String
|
||||
// Auxiliary
|
||||
let concat_s = (a: String) s | a
|
||||
let b_tail = String.drop(2, b)
|
||||
|
||||
let {fst, snd} = String.hex.decode.utf8.take_pair(b)
|
||||
case snd {
|
||||
none: s
|
||||
some:
|
||||
let snd = snd.value
|
||||
let snd = Nat.hex.decode(String.reverse(snd))
|
||||
let fst = Nat.hex.decode(String.reverse(fst))
|
||||
|
||||
let fst = Nat.to_u16(fst)
|
||||
let snd = Nat.to_u16(snd)
|
||||
|
||||
let control_num = 999#16
|
||||
let s_temp =
|
||||
if U16.gtn(snd, 127) then
|
||||
case String.hex.decode.utf8.gtn_one_byte(fst, snd) as res {
|
||||
none: control_num // got parsing error or help parsing symbols. Confusing, I know
|
||||
some: res.value
|
||||
}
|
||||
else
|
||||
snd
|
||||
|
||||
if U16.ltn(s_temp, 0xffff) then
|
||||
// log("c ltn 0xffff: " | U16.show(s_temp))
|
||||
let parsed =
|
||||
if U16.eql(s_temp, control_num)
|
||||
then "" // Couldn't parse byte, but may be not and error (like for some symbols)
|
||||
else Char.to_string(s_temp)
|
||||
// log(" parsed value: " | parsed)
|
||||
String.hex.decode.utf8.aux(b_tail, concat_s(parsed)) // String.fromCharCode(c)
|
||||
else if U16.lte(s_temp, 0x10ffff) then// c <= 0x10ffff
|
||||
let aux = U16.sub(s_temp, 0x10000)
|
||||
let a = Char.to_string(U16.or(U16.shr(s_temp, 10), 0xd800)) // String.fromCharCode(c >> 10 | 0xd800)
|
||||
let b = Char.to_string(U16.or(U16.and(s_temp, 0x3FF), 0xdc00)) // String.fromCharCode(c & 0x3FF | 0xdc00)
|
||||
let parsed = a | b
|
||||
// log("c ltn 0x10ffff: " | parsed)
|
||||
String.hex.decode.utf8.aux(b_tail, concat_s(parsed))
|
||||
else ""
|
||||
}
|
||||
|
||||
// Auxiliar to parse chunks bigger than 1 byte
|
||||
String.hex.decode.utf8.gtn_one_byte(c: U16, fst: U16): Maybe(U16)
|
||||
let two_bytes = Bool.and(U16.gtn(c, 191), U16.ltn(c, 224)) // (c > 191 && c < 224)
|
||||
let three_bytes = Bool.and(U16.gtn(c, 223), U16.ltn(c, 240)) // (c > 223 && c < 240)
|
||||
let four_bytes = Bool.and(U16.gtn(c, 239), U16.ltn(c, 248)) // (c > 239 && c < 248)
|
||||
if two_bytes then
|
||||
let l = U16.shl(U16.and(c, 31), 6) // (c & 31) << 6
|
||||
let r = U16.and(fst, 63) // bytes[i++] & 63
|
||||
let res = U16.or(l, r)
|
||||
Maybe.some!(res) // l | r
|
||||
else if three_bytes then
|
||||
let l = U16.shl(U16.and(c, 15), 12) // (c & 15) << 12
|
||||
let m = U16.shl(U16.and(fst, 63), 6) // (bytes[i++] & 63) << 6
|
||||
let r = U16.and(fst, 63) // bytes[i++] & 63
|
||||
let res = U16.or(l, U16.or(m, r))
|
||||
Maybe.some!(res) // l | m | r;
|
||||
else if four_bytes then
|
||||
let l = U16.shl(U16.and(c, 7), 18) // (c & 7) << 18
|
||||
let m0 = U16.shl(U16.and(fst, 63), 12) // (bytes[i++] & 63) << 12
|
||||
let m1 = U16.shl(U16.and(fst, 63), 6) // (bytes[i++] & 63) << 6
|
||||
let r = U16.and(fst, 63) // bytes[i++] & 63
|
||||
let res = U16.or(U16.or(l, m0), U16.or(m1, r))
|
||||
Maybe.some!(res) // l | m0 | m1 | r
|
||||
else Maybe.none! // UTF-8 decode: unknown multibyte or auxiliary to parse symbols
|
||||
|
||||
// Reference:
|
||||
// - https://gist.github.com/pascaldekloe/62546103a1576803dade9269ccf76330
|
||||
// -
|
3
base/String/hexstring/arrayify.kind
Normal file
3
base/String/hexstring/arrayify.kind
Normal file
@ -0,0 +1,3 @@
|
||||
String.hexstring.arrayify(value: String): Buffer8
|
||||
let {_,buf} = Buffer8.from_hex(String.to_hex(value))
|
||||
buf
|
@ -1,5 +1,5 @@
|
||||
// Return 2 characters from "bytes", if available
|
||||
Bytes.at(bytes: String): Maybe(String)
|
||||
String.hexstring.at(bytes: String): Maybe(String)
|
||||
case bytes {
|
||||
nil: Maybe.none!
|
||||
cons:
|
7
base/String/hexstring/from_nat.kind
Normal file
7
base/String/hexstring/from_nat.kind
Normal file
@ -0,0 +1,7 @@
|
||||
String.hexstring.from_nat(num: Nat): String
|
||||
let hex = Nat.to_string_base(16, num)
|
||||
if Nat.eql(String.length(hex) % 2, 0) then
|
||||
"0x" | hex
|
||||
else
|
||||
"0x0" | hex
|
||||
|
@ -10,9 +10,3 @@ Test: _
|
||||
let a = Foo.new(Bar.new({"list": [[1,2,3],[4,5,6],[7,8,9]]}))
|
||||
let a = a@bar@map{"list"}[0][0] <= Nat.mul(10)
|
||||
a@bar@map{"list"}[0][0]
|
||||
|
||||
|
||||
//let y = x[0][2] <- 42
|
||||
//let y = List.mut(List(Nat),0,(x) List.mut(Nat,2,(x) 42,x),x)
|
||||
//let y = Maybe.bind(_,_,List.get(_,0,x),(x) Maybe.some(_,x))
|
||||
//List.show!(List.show!(Nat.show), y)
|
||||
|
87
base/Tiger/SL.kind
Normal file
87
base/Tiger/SL.kind
Normal file
@ -0,0 +1,87 @@
|
||||
// straight-line programs Type and (very inefficient) interpreter
|
||||
// statement
|
||||
type Tiger.SL.Stm {
|
||||
CompoundStm(fst: Tiger.SL.Stm, snd: Tiger.SL.Stm)
|
||||
AssignStm(id: String, exp: Tiger.SL.Exp)
|
||||
PrintStm(exp_list: List<Tiger.SL.Exp>)
|
||||
}
|
||||
|
||||
// expression
|
||||
type Tiger.SL.Exp {
|
||||
IdExp(id: String)
|
||||
NumExp(num: Int) // #TODO include other numbers?
|
||||
OpExp(op: Tiger.SL.Binop, fst: Tiger.SL.Exp, snd: Tiger.SL.Exp)
|
||||
EseqExp(stm: Tiger.SL.Stm, exp: Tiger.SL.Exp)
|
||||
}
|
||||
|
||||
type Tiger.SL.ExpList {
|
||||
PairExpList(head: Tiger.SL.Exp, tail: Tiger.SL.ExpList)
|
||||
LastExpList(head: Tiger.SL.Exp)
|
||||
}
|
||||
|
||||
type Tiger.SL.Binop {
|
||||
plus
|
||||
minus
|
||||
times
|
||||
div
|
||||
}
|
||||
|
||||
maxargs(stm: Tiger.SL.Stm): Nat
|
||||
case stm {
|
||||
CompoundStm: Nat.max(maxargs(stm.fst), maxargs(stm.snd))
|
||||
AssignStm: 0
|
||||
PrintStm: List.length!(stm.exp_list)
|
||||
}
|
||||
|
||||
Tiger.SL.interpStm(stm: Tiger.SL.Stm, table: List<Pair<String, Int>>): List<Pair<String, Int>>
|
||||
case stm {
|
||||
CompoundStm:
|
||||
let new_table = Tiger.SL.interpStm(stm.fst, table)
|
||||
Tiger.SL.interpStm(stm.snd, new_table)
|
||||
AssignStm:
|
||||
let {i, new_table} = Tiger.SL.interpExp(stm.exp, table)
|
||||
{stm.id, i} & new_table
|
||||
PrintStm:
|
||||
for exp in stm.exp_list with table:
|
||||
let {i, table} = Tiger.SL.interpExp(exp, table)
|
||||
log(Int.show(i))
|
||||
table
|
||||
table
|
||||
}
|
||||
|
||||
Tiger.SL.lookup(id: String, table: List<Pair<String, Int>>): Int
|
||||
case table {
|
||||
nil:
|
||||
0 :: Int
|
||||
cons:
|
||||
let {table_id, val} = table.head
|
||||
if id =? table_id then
|
||||
val
|
||||
else
|
||||
Tiger.SL.lookup(id, table.tail)
|
||||
}
|
||||
|
||||
Tiger.SL.interpExp(exp: Tiger.SL.Exp, table: List<Pair<String, Int>>): Pair<Int, List<Pair<String, Int>>>
|
||||
case exp {
|
||||
IdExp:
|
||||
{Tiger.SL.lookup(exp.id, table), table}
|
||||
NumExp:
|
||||
{exp.num, table}
|
||||
OpExp:
|
||||
let {fst_val, table} = Tiger.SL.interpExp(exp.fst, table)
|
||||
let {snd_val, table} = Tiger.SL.interpExp(exp.snd, table)
|
||||
case exp.op {
|
||||
plus:
|
||||
{fst_val + snd_val, table}
|
||||
minus:
|
||||
{fst_val - snd_val, table}
|
||||
times:
|
||||
{fst_val * snd_val, table}
|
||||
div:
|
||||
{fst_val / snd_val, table}
|
||||
}
|
||||
EseqExp:
|
||||
let table = Tiger.SL.interpStm(exp.stm, table)
|
||||
Tiger.SL.interpExp(exp.exp, table)
|
||||
}
|
||||
|
10
base/User/caotic/debug/Bool.kind
Normal file
10
base/User/caotic/debug/Bool.kind
Normal file
@ -0,0 +1,10 @@
|
||||
type Bool {
|
||||
true
|
||||
false
|
||||
}
|
||||
|
||||
Bool.true_neq_false: Bool.true != Bool.false
|
||||
(e) Equal.rewrite!!!(e, (x) case x { true: Unit, false: Empty }, Unit.new)
|
||||
|
||||
Bool.false_neq_true: Bool.false != Bool.true
|
||||
(e) Equal.rewrite!!!(e, (x) case x { true: Empty, false: Unit }, Unit.new)
|
5
base/User/caotic/debug/Empty.kind
Normal file
5
base/User/caotic/debug/Empty.kind
Normal file
@ -0,0 +1,5 @@
|
||||
type Empty {
|
||||
}
|
||||
|
||||
Empty.absurd<A: Type>(contra: Empty): A
|
||||
case contra {}
|
49
base/User/caotic/debug/Equal.kind
Normal file
49
base/User/caotic/debug/Equal.kind
Normal file
@ -0,0 +1,49 @@
|
||||
//Equal : @(A:*) @(a:A) @(b:A) * =
|
||||
// #A #a #b
|
||||
// %Equal.Self(
|
||||
// P:@(b:A) @(:(((Equal A) a) b)) *)
|
||||
// @(refl:((P a) ((Equal.refl A) a)))
|
||||
// ((P b) Equal.Self);
|
||||
//
|
||||
//Equal.refl : %(A:*) %(a:A) (((Equal A) a) a) =
|
||||
// #A #a #P #refl
|
||||
// refl;
|
||||
|
||||
Equal(A: Type, a: A, b: A): Type
|
||||
Equal.Self<
|
||||
P: (b: A) -> (Equal(A, a, b)) -> Type
|
||||
> ->
|
||||
(refl:
|
||||
P(a, Equal.refl(A, a))) ->
|
||||
P(b, Equal.Self)
|
||||
|
||||
Equal.refl(A: Type, a: A): Equal(A, a, a)
|
||||
(P, r) r
|
||||
//
|
||||
//type Equal <A: Type> <a: A> ~ (b: A) {
|
||||
// refl ~ (b = a)
|
||||
//}
|
||||
|
||||
Equal.rewrite<A: Type, a: A, b: A>(e: Equal<A,a,b>)<P: A -> Type>(x: P(a)): P(b)
|
||||
case e {
|
||||
refl: x
|
||||
}: P(e.b)
|
||||
|
||||
Equal.mirror<A: Type, a: A, b: A>(e: Equal<A, a, b>): Equal<A, b, a>
|
||||
case e {
|
||||
refl: Equal.refl<A, a>
|
||||
} : Equal<A, e.b, a>
|
||||
|
||||
Equal.apply<
|
||||
A: Type,
|
||||
B: Type,
|
||||
a: A,
|
||||
b: A,
|
||||
f: A -> B
|
||||
>(e: Equal<A,a,b>): Equal<B, f(a), f(b)>
|
||||
case e {
|
||||
refl: Equal.refl<B, f(a)>
|
||||
}: Equal<B, f(a), f(e.b)>
|
||||
|
||||
Empty.absurd<P: Type>(x: Empty): P
|
||||
case x {}
|
248
base/User/caotic/debug/Nat.kind
Normal file
248
base/User/caotic/debug/Nat.kind
Normal file
@ -0,0 +1,248 @@
|
||||
type Nat {
|
||||
zero,
|
||||
succ(pred: Nat),
|
||||
}
|
||||
|
||||
Nat.add(n: Nat, m: Nat): Nat
|
||||
case n {
|
||||
zero:
|
||||
m
|
||||
succ:
|
||||
Nat.succ(Nat.add(n.pred, m))
|
||||
}
|
||||
|
||||
//Nat.succ_neq_zero(a: Nat): (Equal<Nat, Nat.succ(a), 0> -> Empty)
|
||||
// (e) Bool.false_neq_true(Equal.apply!!!!(Nat.is_zero, e))
|
||||
//
|
||||
//Nat.mul.zero_left(a: Nat): Equal!(Nat.mul(0, a), 0)
|
||||
// case a {
|
||||
// zero:
|
||||
// Equal.refl!!
|
||||
// succ:
|
||||
// let h = Nat.mul.zero_left(a.pred)
|
||||
// Equal.apply!!!!((x) Nat.add(0, x), h)
|
||||
// }!
|
||||
//
|
||||
//Nat.mul.comm(a: Nat, b: Nat): Equal!(Nat.mul(a, b), Nat.mul(b, a))
|
||||
// case b {
|
||||
// zero:
|
||||
// Equal.mirror!!!(Nat.mul.zero_left(a))
|
||||
// succ:
|
||||
// Equal.mirror!!!(Nat.mul.comm(Nat.succ(b.pred), a))
|
||||
// }!
|
||||
|
||||
Nat.mul(n: Nat, m: Nat): Nat
|
||||
case m {
|
||||
zero:
|
||||
Nat.zero,
|
||||
succ:
|
||||
Nat.add(n, Nat.mul(n, m.pred)),
|
||||
}
|
||||
|
||||
Nat.lte(n: Nat, m: Nat): Bool
|
||||
case n {
|
||||
zero:
|
||||
Bool.true,
|
||||
succ:
|
||||
case m {
|
||||
zero:
|
||||
Bool.false,
|
||||
succ:
|
||||
Nat.lte(n.pred, m.pred),
|
||||
}
|
||||
}
|
||||
|
||||
//Nat.is_zero(n: Nat): Bool
|
||||
// case n {
|
||||
// zero:
|
||||
// Bool.true,
|
||||
// succ:
|
||||
// Bool.false,
|
||||
// }
|
||||
//
|
||||
//Nat.add.zero_right(a: Nat): Equal!(Nat.add(a, 0), a)
|
||||
// case a {
|
||||
// zero:
|
||||
// refl
|
||||
// succ:
|
||||
// let p0 = Nat.add.zero_right(a.pred)
|
||||
// let p1 = Equal.apply!!!!(Nat.succ, p0)
|
||||
// p1
|
||||
// }!
|
||||
//
|
||||
//Nat.add.succ_right(a: Nat, b: Nat): Equal!(Nat.add(a, Nat.succ(b)), Nat.succ(Nat.add(a, b)))
|
||||
// case a {
|
||||
// zero: refl
|
||||
// succ:
|
||||
// let h = Nat.add.succ_right(a.pred, b)
|
||||
// let h1 = Equal.apply!!!!(Nat.succ, h)
|
||||
// h1
|
||||
// }!
|
||||
//
|
||||
//Nat.add.succ_left(a: Nat, b: Nat): Equal!(Nat.add(Nat.succ(a), b), Nat.succ(Nat.add(a, b)))
|
||||
// refl
|
||||
//
|
||||
//Nat.add.comm(a: Nat, b: Nat): Equal!(Nat.add(a, b), Nat.add(b, a))
|
||||
// case a {
|
||||
// zero:
|
||||
// Equal.mirror!!!(Nat.add.zero_right(b))
|
||||
// succ:
|
||||
// let p0 = Nat.add.succ_right(b, a.pred)
|
||||
// let p1 = Equal.mirror!!!(p0)
|
||||
// let h2 = Nat.add.comm(b, a.pred)
|
||||
// let p3 = Equal.rewrite!!!(h2, (x) Equal!(Nat.succ(x), Nat.add(b,Nat.succ(a.pred))), p1)
|
||||
// // here p3 should close the goal.
|
||||
// let p4 = Equal.mirror!!!(Nat.add.succ_left(a.pred,b))
|
||||
// let p5 = Equal.rewrite!!!(p4, (x) Equal!(x, _), p3)
|
||||
// p5
|
||||
// }!
|
||||
//
|
||||
//Nat.Order.refl(a: Nat): Equal!(Nat.lte(a, a), Bool.true)
|
||||
// case a {
|
||||
// zero:
|
||||
// refl
|
||||
// succ:
|
||||
// let ind = Nat.Order.refl(a.pred)
|
||||
// ind
|
||||
// }!
|
||||
//
|
||||
//Nat.add(n: Nat, m: Nat): Nat
|
||||
// case n {
|
||||
// zero: m
|
||||
// succ: Nat.succ(Nat.add(n.pred, m))
|
||||
// }
|
||||
|
||||
Nat.Order.mul.right(
|
||||
a: Nat
|
||||
b: Nat
|
||||
c: Nat
|
||||
Hyp: Equal(Bool, Nat.lte(a, b), Bool.true)
|
||||
): Equal(Bool, Nat.lte(Nat.mul(a, c), Nat.mul(b, c)), Bool.true)
|
||||
?b
|
||||
Nat.Order.mul.left(
|
||||
a: Nat
|
||||
b: Nat
|
||||
c: Nat
|
||||
Hyp: Equal<Bool>(Nat.lte(a, b), Bool.true)
|
||||
): Equal<Bool>(Nat.lte(Nat.mul(c, a), Nat.mul(c, b)), Bool.true)
|
||||
_
|
||||
// let lem = Nat.Order.mul.right(a, b, c, Hyp)
|
||||
// let lem = Equal.rewrite(
|
||||
// Nat, Nat.mul(a, c),
|
||||
// Nat.mul(c, a), Nat.mul.comm(a, c),
|
||||
// (X) Equal<Bool>(Nat.lte(X, Nat.mul(b, c)), Bool.true), lem)
|
||||
// let qed = Equal.rewrite(
|
||||
// Nat, Nat.mul(b, c),
|
||||
// Nat.mul(c, b), Nat.mul.comm(b, c),
|
||||
// (X) Equal<Bool>(Nat.lte(Nat.mul(c, a), X), Bool.true), lem)
|
||||
// qed
|
||||
|
||||
//Nat.Order.chain.aux(
|
||||
// a: Nat
|
||||
// Hyp: Equal!(Nat.lte(a, 0), Bool.true)
|
||||
//): Equal!(a, 0)
|
||||
// (case a {
|
||||
// zero:
|
||||
// (Hyp)
|
||||
// refl
|
||||
// succ:
|
||||
// (Hyp)
|
||||
// let contra = Bool.true_neq_false(Equal.mirror!!!(Hyp))
|
||||
// Empty.absurd<Equal<Nat>(Nat.succ(a.pred), 0)>(contra)
|
||||
// }: (Hyp: Equal!(Nat.lte(a, 0), Bool.true)) -> Equal!(a, 0))(Hyp)
|
||||
|
||||
Nat.Order.chain(
|
||||
a: Nat
|
||||
b: Nat
|
||||
c: Nat
|
||||
Hyp0: Equal(Bool, Nat.lte(a, b), Bool.true)
|
||||
Hyp1: Equal(Bool, Nat.lte(b, c), Bool.true)
|
||||
): Equal(Bool, Nat.lte(a, c), Bool.true)
|
||||
(case b {
|
||||
zero:
|
||||
(Hyp0, Hyp1)
|
||||
let a_zero = Equal.mirror<Nat>(a, 0, Nat.Order.chain.aux(a, Hyp0))
|
||||
let qed = Equal.rewrite<Nat>(0, a, a_zero, (X) Equal<Bool>(Nat.lte(X, c), Bool.true), Hyp1)
|
||||
qed
|
||||
succ:
|
||||
(Hyp0, Hyp1)
|
||||
(case a {
|
||||
zero:
|
||||
(Hyp0, Hyp1)
|
||||
refl
|
||||
succ:
|
||||
(Hyp0, Hyp1)
|
||||
(case c {
|
||||
zero:
|
||||
(Hyp0, Hyp1)
|
||||
let b_zero = Nat.Order.chain.aux(Nat.succ(b.pred), Hyp1)
|
||||
let contra = Nat.succ_neq_zero!(b_zero)
|
||||
Empty.absurd!(contra)
|
||||
succ:
|
||||
(Hyp0, Hyp1)
|
||||
let ind = Nat.Order.chain(a.pred, b.pred, c.pred, Hyp0, Hyp1)
|
||||
ind
|
||||
}: (Hyp0: Equal!(Nat.lte(Nat.succ(a.pred), Nat.succ(b.pred)), Bool.true), Hyp1: Equal!(Nat.lte(Nat.succ(b.pred), c), Bool.true)) -> Equal!(Nat.lte(Nat.succ(a.pred), c), Bool.true))(Hyp0, Hyp1)
|
||||
}: (Hyp0: Equal!(Nat.lte(a, Nat.succ(b.pred)), Bool.true), Hyp1: Equal!(Nat.lte(Nat.succ(b.pred), c), Bool.true)) -> Equal!(Nat.lte(a, c), Bool.true))(Hyp0, Hyp1)
|
||||
}: (Hyp0: Equal!(Nat.lte(a, b), Bool.true), Hyp1: Equal!(Nat.lte(b, c), Bool.true)) -> Equal!(Nat.lte(a, c), Bool.true))(Hyp0, Hyp1)
|
||||
|
||||
Nat.Order.add.left(
|
||||
a: Nat
|
||||
b: Nat
|
||||
c: Nat
|
||||
Hyp: Equal(Bool, Nat.lte(a, b), Bool.true)
|
||||
): Equal(Bool, Nat.lte(Nat.add(c, a), Nat.add(c, b)), Bool.true)
|
||||
case c {
|
||||
zero:
|
||||
Hyp
|
||||
succ:
|
||||
Nat.Order.add.left(a, b, c.pred, Hyp)
|
||||
}!
|
||||
|
||||
Nat.Order.add.right(
|
||||
a: Nat
|
||||
b: Nat
|
||||
c: Nat
|
||||
Hyp: Equal!(Nat.lte(a, b), Bool.true)
|
||||
): Equal!(Nat.lte(Nat.add(a, c), Nat.add(b, c)), Bool.true)
|
||||
Equal.rewrite!!!(Nat.add.comm!!, (X) Equal!(Nat.lte(_, X), _),
|
||||
Equal.rewrite!!!(Nat.add.comm!!, (X) Equal!(Nat.lte(X, _), _),
|
||||
Nat.Order.add.left!!(c, Hyp)))
|
||||
|
||||
Nat.Order.add.combine(
|
||||
a: Nat
|
||||
b: Nat
|
||||
c: Nat
|
||||
d: Nat
|
||||
Hyp0: Equal(Bool, Nat.lte(a, b), Bool.true)
|
||||
Hyp1: Equal(Bool, Nat.lte(c, d), Bool.true)
|
||||
): Equal(Bool, Nat.lte(Nat.add(a, c), Nat.add(b, d)), Bool.true)
|
||||
let left_lem = Nat.Order.add.right(a, b, c, Hyp0)
|
||||
let right_lem = Nat.Order.add.left(c, d, b, Hyp1)
|
||||
let qed = Nat.Order.chain(a, b, c, left_lem, right_lem)
|
||||
qed
|
||||
|
||||
//Nat.Order.mul.combine(
|
||||
// a: Nat,
|
||||
// b: Nat,
|
||||
// c: Nat,
|
||||
// d: Nat,
|
||||
// Hyp0: Equal<Bool>(Nat.lte(a, b), Bool.true),
|
||||
// Hyp1: Equal<Bool>(Nat.lte(c, d), Bool.true)
|
||||
//): Equal<Bool>(Nat.lte(Nat.mul(a, c), Nat.mul(b, d)), Bool.true)
|
||||
// let left_lem = Nat.Order.mul.right(a, b, c, Hyp0); // DOESN'T
|
||||
// let right_lem = Nat.Order.mul.left(c, d, a, Hyp1);
|
||||
// let qed = Nat.Order.chain(Nat.mul(a, c), Nat.mul(b, c), Nat.mul(b, d), left_lem, right_lem);
|
||||
// qed
|
||||
|
||||
Nat.Order.mul.combine(
|
||||
a: Nat,
|
||||
c: Nat,
|
||||
d: Nat,
|
||||
Hyp0: Equal(Bool,Nat.lte(a, a), Bool.true),
|
||||
Special: Equal(Bool, Nat.lte(c, d), Bool.true)
|
||||
): Equal(Bool, Nat.lte(Nat.mul(a, c), Nat.mul(a, d)), Bool.true)
|
||||
//let left_lem = Nat.Order.refl(Nat.mul(a, c)); // WORKS
|
||||
let left_lem = Nat.Order.mul.right(a, a, c, Hyp0); // DOESN'T
|
||||
let right_lem = Nat.Order.mul.left(c, d, a, Special);
|
||||
?a
|
3
base/User/caotic/debug/Unit.kind
Normal file
3
base/User/caotic/debug/Unit.kind
Normal file
@ -0,0 +1,3 @@
|
||||
type Unit {
|
||||
new
|
||||
}
|
@ -1,92 +0,0 @@
|
||||
// i'm studying compilers using "modern compiler implementation in ML" by Andrew Appel
|
||||
// translating to Kind as I go. i'm not too worried about following the book too closely.
|
||||
// for example i'll likely use kind's `Parser` to parse programs instead of Lex and Yacc.
|
||||
// but i'm using ML's naming conventions. it looks ugly but makes lookups easier.
|
||||
|
||||
// position on source code, to produce error messages
|
||||
User.rigille.Tiger.pos: Type
|
||||
Pair<Nat, Nat>
|
||||
|
||||
User.rigille.Tiger.symbol: Type
|
||||
String
|
||||
|
||||
type User.rigille.Tiger.var {
|
||||
SimpleVar(name: User.rigille.Tiger.symbol, pos: User.rigille.Tiger.pos)
|
||||
FieldVar(var: User.rigille.Tiger.var, name: User.rigille.Tiger.symbol, pos: User.rigille.Tiger.pos)
|
||||
SubscriptVar(var: User.rigille.Tiger.var, exp: User.rigille.Tiger.exp, pos: User.rigille.Tiger.pos)
|
||||
}
|
||||
|
||||
type User.rigille.Tiger.record_fields {
|
||||
new(
|
||||
name: User.rigille.Tiger.symbol
|
||||
args: List<User.rigille.Tiger.exp>
|
||||
pos: User.rigille.Tiger.pos
|
||||
)
|
||||
}
|
||||
type User.rigille.Tiger.exp {
|
||||
NilExp
|
||||
VarExp(var: User.rigille.Tiger.var)
|
||||
IntExp(val: Int)
|
||||
StringExp(val: String, pos: User.rigille.Tiger.pos)
|
||||
CallExp(
|
||||
func: User.rigille.Tiger.symbol
|
||||
args: List<User.rigille.Tiger.exp>
|
||||
pos: User.rigille.Tiger.pos
|
||||
)
|
||||
OpExp(
|
||||
left: User.rigille.Tiger.exp
|
||||
oper: User.rigille.Tiger.oper
|
||||
right: User.rigille.Tiger.exp
|
||||
pos: User.rigille.Tiger.pos
|
||||
)
|
||||
RecordExp(
|
||||
fields: List<User.rigille.Tiger.record_fields>
|
||||
typ: User.rigille.Tiger.symbol
|
||||
pos: User.rigille.Tiger.pos
|
||||
)
|
||||
SeqExp(
|
||||
val: List<User.rigille.Tiger.exp>
|
||||
)
|
||||
AssignExp(
|
||||
var: User.rigille.Tiger.var
|
||||
exp: User.rigille.Tiger.exp
|
||||
pos: User.rigille.Tiger.pos
|
||||
)
|
||||
IfExp(
|
||||
test: User.rigille.Tiger.exp
|
||||
then: User.rigille.Tiger.exp
|
||||
else: Maybe<User.rigille.Tiger.exp>
|
||||
)
|
||||
WhileExp(
|
||||
test: User.rigille.Tiger.exp
|
||||
body: User.rigille.Tiger.exp
|
||||
pos: User.rigille.Tiger.pos
|
||||
)
|
||||
ForExp(
|
||||
var: User.rigille.Tiger.symbol
|
||||
escape: Bool
|
||||
lo: User.rigille.Tiger.exp
|
||||
hi: User.rigille.Tiger.exp
|
||||
body: User.rigille.Tiger.exp
|
||||
pos: User.rigille.Tiger.pos
|
||||
)
|
||||
BreakExp(
|
||||
pos: User.rigille.Tiger.pos
|
||||
)
|
||||
LetExp(
|
||||
decs: List<User.rigille.Tiger.dec>
|
||||
body: User.rigille.Tiger.exp
|
||||
pos: User.rigille.Tiger.pos
|
||||
)
|
||||
ArrayExp(
|
||||
typ: User.rigille.Tiger.symbol
|
||||
size: User.rigille.Tiger.exp
|
||||
pos: User.rigille.Tiger.pos
|
||||
)
|
||||
}
|
||||
|
||||
type User.rigille.Tiger.oper {
|
||||
}
|
||||
|
||||
type User.rigille.Tiger.dec {
|
||||
}
|
@ -1,87 +0,0 @@
|
||||
// straight-line programs Type and (very inefficient) interpreter
|
||||
// statement
|
||||
type User.rigille.Tiger.SL.Stm {
|
||||
CompoundStm(fst: User.rigille.Tiger.SL.Stm, snd: User.rigille.Tiger.SL.Stm)
|
||||
AssignStm(id: String, exp: User.rigille.Tiger.SL.Exp)
|
||||
PrintStm(exp_list: List<User.rigille.Tiger.SL.Exp>)
|
||||
}
|
||||
|
||||
// expression
|
||||
type User.rigille.Tiger.SL.Exp {
|
||||
IdExp(id: String)
|
||||
NumExp(num: Int) // #TODO include other numbers?
|
||||
OpExp(op: User.rigille.Tiger.SL.Binop, fst: User.rigille.Tiger.SL.Exp, snd: User.rigille.Tiger.SL.Exp)
|
||||
EseqExp(stm: User.rigille.Tiger.SL.Stm, exp: User.rigille.Tiger.SL.Exp)
|
||||
}
|
||||
|
||||
type User.rigille.Tiger.SL.ExpList {
|
||||
PairExpList(head: User.rigille.Tiger.SL.Exp, tail: User.rigille.Tiger.SL.ExpList)
|
||||
LastExpList(head: User.rigille.Tiger.SL.Exp)
|
||||
}
|
||||
|
||||
type User.rigille.Tiger.SL.Binop {
|
||||
plus
|
||||
minus
|
||||
times
|
||||
div
|
||||
}
|
||||
|
||||
maxargs(stm: User.rigille.Tiger.SL.Stm): Nat
|
||||
case stm {
|
||||
CompoundStm: Nat.max(maxargs(stm.fst), maxargs(stm.snd))
|
||||
AssignStm: 0
|
||||
PrintStm: List.length!(stm.exp_list)
|
||||
}
|
||||
|
||||
User.rigille.Tiger.SL.interpStm(stm: User.rigille.Tiger.SL.Stm, table: List<Pair<String, Int>>): List<Pair<String, Int>>
|
||||
case stm {
|
||||
CompoundStm:
|
||||
let new_table = User.rigille.Tiger.SL.interpStm(stm.fst, table)
|
||||
User.rigille.Tiger.SL.interpStm(stm.snd, new_table)
|
||||
AssignStm:
|
||||
let {i, new_table} = User.rigille.Tiger.SL.interpExp(stm.exp, table)
|
||||
{stm.id, i} & new_table
|
||||
PrintStm:
|
||||
for exp in stm.exp_list with table:
|
||||
let {i, table} = User.rigille.Tiger.SL.interpExp(exp, table)
|
||||
log(Int.show(i))
|
||||
table
|
||||
table
|
||||
}
|
||||
|
||||
User.rigille.Tiger.SL.lookup(id: String, table: List<Pair<String, Int>>): Int
|
||||
case table {
|
||||
nil:
|
||||
0 :: Int
|
||||
cons:
|
||||
let {table_id, val} = table.head
|
||||
if id =? table_id then
|
||||
val
|
||||
else
|
||||
User.rigille.Tiger.SL.lookup(id, table.tail)
|
||||
}
|
||||
|
||||
User.rigille.Tiger.SL.interpExp(exp: User.rigille.Tiger.SL.Exp, table: List<Pair<String, Int>>): Pair<Int, List<Pair<String, Int>>>
|
||||
case exp {
|
||||
IdExp:
|
||||
{User.rigille.Tiger.SL.lookup(exp.id, table), table}
|
||||
NumExp:
|
||||
{exp.num, table}
|
||||
OpExp:
|
||||
let {fst_val, table} = User.rigille.Tiger.SL.interpExp(exp.fst, table)
|
||||
let {snd_val, table} = User.rigille.Tiger.SL.interpExp(exp.snd, table)
|
||||
case exp.op {
|
||||
plus:
|
||||
{fst_val + snd_val, table}
|
||||
minus:
|
||||
{fst_val - snd_val, table}
|
||||
times:
|
||||
{fst_val * snd_val, table}
|
||||
div:
|
||||
{fst_val / snd_val, table}
|
||||
}
|
||||
EseqExp:
|
||||
let table = User.rigille.Tiger.SL.interpStm(exp.stm, table)
|
||||
User.rigille.Tiger.SL.interpExp(exp.exp, table)
|
||||
}
|
||||
|
Loading…
Reference in New Issue
Block a user