From 5c968ac99f90647623d21190084d613f01e88c8f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=ADgille=20S=2E=20B=2E=20Menezes?= Date: Fri, 6 Aug 2021 21:38:21 -0300 Subject: [PATCH 01/17] move compiler study to base so names are smaller --- base/Tiger.kind | 92 +++++++++++++++++++++++++++++++++ base/Tiger/SL.kind | 87 +++++++++++++++++++++++++++++++ base/User/rigille/Tiger.kind | 92 --------------------------------- base/User/rigille/Tiger/SL.kind | 87 ------------------------------- 4 files changed, 179 insertions(+), 179 deletions(-) create mode 100644 base/Tiger.kind create mode 100644 base/Tiger/SL.kind delete mode 100644 base/User/rigille/Tiger.kind delete mode 100644 base/User/rigille/Tiger/SL.kind diff --git a/base/Tiger.kind b/base/Tiger.kind new file mode 100644 index 00000000..9bd990ee --- /dev/null +++ b/base/Tiger.kind @@ -0,0 +1,92 @@ +// 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 +Tiger.pos: Type + Pair + +Tiger.symbol: Type + String + +type Tiger.var { + SimpleVar(name: Tiger.symbol, pos: Tiger.pos) + FieldVar(var: Tiger.var, name: Tiger.symbol, pos: Tiger.pos) + SubscriptVar(var: Tiger.var, exp: Tiger.exp, pos: Tiger.pos) +} + +type Tiger.record_fields { + new( + name: Tiger.symbol + args: List + pos: Tiger.pos + ) +} +type Tiger.exp { + NilExp + VarExp(var: Tiger.var) + IntExp(val: Int) + StringExp(val: String, pos: Tiger.pos) + CallExp( + func: Tiger.symbol + args: List + pos: Tiger.pos + ) + OpExp( + left: Tiger.exp + oper: Tiger.oper + right: Tiger.exp + pos: Tiger.pos + ) + RecordExp( + fields: List + typ: Tiger.symbol + pos: Tiger.pos + ) + SeqExp( + val: List + ) + AssignExp( + var: Tiger.var + exp: Tiger.exp + pos: Tiger.pos + ) + IfExp( + test: Tiger.exp + then: Tiger.exp + else: Maybe + ) + WhileExp( + test: Tiger.exp + body: Tiger.exp + pos: Tiger.pos + ) + ForExp( + var: Tiger.symbol + escape: Bool + lo: Tiger.exp + hi: Tiger.exp + body: Tiger.exp + pos: Tiger.pos + ) + BreakExp( + pos: Tiger.pos + ) + LetExp( + decs: List + body: Tiger.exp + pos: Tiger.pos + ) + ArrayExp( + typ: Tiger.symbol + size: Tiger.exp + pos: Tiger.pos + ) +} + +type Tiger.oper { +} + +type Tiger.dec { +} diff --git a/base/Tiger/SL.kind b/base/Tiger/SL.kind new file mode 100644 index 00000000..9396fd02 --- /dev/null +++ b/base/Tiger/SL.kind @@ -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) +} + +// 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>): List> + 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>): 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>> + 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) + } + diff --git a/base/User/rigille/Tiger.kind b/base/User/rigille/Tiger.kind deleted file mode 100644 index f15cf050..00000000 --- a/base/User/rigille/Tiger.kind +++ /dev/null @@ -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 - -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 - 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 - 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 - typ: User.rigille.Tiger.symbol - pos: User.rigille.Tiger.pos - ) - SeqExp( - val: List - ) - 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 - ) - 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 - 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 { -} diff --git a/base/User/rigille/Tiger/SL.kind b/base/User/rigille/Tiger/SL.kind deleted file mode 100644 index 374c9107..00000000 --- a/base/User/rigille/Tiger/SL.kind +++ /dev/null @@ -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) -} - -// 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>): List> - 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>): 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>> - 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) - } - From a76da4475144b1cf1149b5ce42568e0d11b91fb3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=ADgille=20S=2E=20B=2E=20Menezes?= Date: Fri, 6 Aug 2021 22:00:17 -0300 Subject: [PATCH 02/17] finish definition of Tiger abstract syntax --- base/Tiger.kind | 57 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 57 insertions(+) diff --git a/base/Tiger.kind b/base/Tiger.kind index 9bd990ee..7bcc0a07 100644 --- a/base/Tiger.kind +++ b/base/Tiger.kind @@ -23,6 +23,7 @@ type Tiger.record_fields { pos: Tiger.pos ) } + type Tiger.exp { NilExp VarExp(var: Tiger.var) @@ -86,7 +87,63 @@ type Tiger.exp { } type Tiger.oper { + PlusOp + MinusOp + TimesOp + DivideOp + EqOp + NeqOp + LtOp + LeOp + GtOp + GeOp } type Tiger.dec { + FunctionDec( + val: List + ) + VarDec( + name: Tiger.symbol + escape: Bool + typ: Maybe> + ) + TypeDec( + val: List + ) +} + +type Tiger.typedec { + new( + name: Tiger.symbol + ty: Tiger.ty + pos: Tiger.pos + ) +} + +type Tiger.ty { + new( + NameTy: Pair + RecordTy: List + ArrayTy: Pair + ) +} + +type Tiger.field { + new( + name: Tiger.symbol + escape: Bool + typ: Tiger.symbol + pos: Tiger.pos + ) +} + +type Tiger.fundec { + new( + name: Tiger.symbol + params: List + result: Maybe> + body: Tiger.exp + pos: Tiger.pos + ) } From 744a40557fea9684699bba421b24e341abc77fce Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=ADgille=20S=2E=20B=2E=20Menezes?= Date: Fri, 8 Oct 2021 22:56:02 -0300 Subject: [PATCH 03/17] fix Nat.mul proofs --- base/Nat/Order.kind | 287 ++++++++++++++++++-------------- base/Nat/add/assoc.kind | 7 +- base/Nat/mul.kind | 10 +- base/Nat/mul/assoc.kind | 40 ++++- base/Nat/mul/comm.kind | 29 +++- base/Nat/mul/distrib_left.kind | 32 ++-- base/Nat/mul/distrib_right.kind | 27 +++ base/Nat/mul/one_left.kind | 9 +- base/Nat/mul/one_right.kind | 13 +- base/Nat/mul/succ_left.kind | 9 +- base/Nat/mul/succ_right.kind | 45 ++++- base/Nat/mul/zero_left.kind | 11 +- base/Nat/mul/zero_right.kind | 9 +- base/Nat/succ_neq_zero.kind | 2 +- 14 files changed, 346 insertions(+), 184 deletions(-) create mode 100644 base/Nat/mul/distrib_right.kind diff --git a/base/Nat/Order.kind b/base/Nat/Order.kind index 8de9a3cd..33f99a8c 100644 --- a/base/Nat/Order.kind +++ b/base/Nat/Order.kind @@ -93,141 +93,176 @@ 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: 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 +Nat.Order.chain.aux( + a: Nat + Hyp: Equal(Nat.lte(a, 0), true) +): Equal(a, 0) + (case a { + zero: + (Hyp) + Equal.refl(0) + succ: + (Hyp) + let contra = Bool.false_neq_true(Hyp) + Empty.absurd(Nat.succ(a.pred), 0)>(contra) + }: (Hyp: Equal(Nat.lte(a, 0), true)) -> Equal(a, 0))( + Hyp + ) + +Nat.Order.chain( + a: Nat + b: Nat + c: Nat + Hyp0: Equal(Nat.lte(a, b), true) + Hyp1: Equal(Nat.lte(b, c), true) +): Equal(Nat.lte(a, c), true) + (case b { + zero: + (Hyp0, Hyp1) + let a_zero = Equal.mirror(a, 0, Nat.Order.chain.aux(a, Hyp0)) + let qed = Equal.rewrite(0, a, a_zero, (x) Equal(Nat.lte(x, c), true), Hyp1) + qed + succ: + (Hyp0, Hyp1) + (case a { + zero: + (Hyp0, Hyp1) + Equal.refl(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(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(Nat.lte(Nat.succ(a.pred), Nat.succ(b.pred)), true)) -> + (Hyp1: Equal(Nat.lte(Nat.succ(b.pred), c), true)) -> + Equal(Nat.lte(Nat.succ(a.pred), c), true))( + Hyp0 + Hyp1 + ) + }: + (Hyp0: Equal(Nat.lte(a, Nat.succ(b.pred)), true)) -> + (Hyp1: Equal(Nat.lte(Nat.succ(b.pred), c), true)) -> + Equal(Nat.lte(a, c), true))( + Hyp0 + Hyp1 + ) + }: (Hyp0: Equal(Nat.lte(a, b), true), Hyp1: Equal(Nat.lte(b, c), true)) -> Equal(Nat.lte(a, c), true))( + Hyp0 + Hyp1 + ) + +Nat.Order.add.left( + a: Nat + b: Nat + c: Nat + Hyp: Equal(Nat.lte(a, b), true) +): Equal(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(Nat.lte(a, b), true)) -> + Equal(Nat.lte(Nat.add(c, a), Nat.add(c, b)), true))( + Hyp + ) + +Nat.Order.add.right( + a: Nat + b: Nat + c: Nat + Hyp: Equal(Nat.lte(a, b), true) +): Equal(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.add(c, a), Nat.add(a, c), Nat.add.comm(c, a), + (x) Equal(Nat.lte(x, Nat.add(c, b)), true), lem + ) + let qed = Equal.rewrite( + Nat.add(c, b), Nat.add(b, c), Nat.add.comm(c, b), + (x) Equal(Nat.lte(Nat.add(a, c), x), true), lem + ) + qed + +Nat.Order.add.combine( + a: Nat + b: Nat + c: Nat + d: Nat + Hyp0: Equal(Nat.lte(a, b), true) + Hyp1: Equal(Nat.lte(c, d), true) +): Equal(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 // 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(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(Nat.lte(a, b), Bool.true) -//): Equal(Nat.lte(Nat.mul(c, a), Nat.mul(c, b)), Bool.true) + +Nat.Order.mul.right( + a: Nat + b: Nat + c: Nat + Hyp: Equal(Nat.lte(a, b), true) +): Equal(Nat.lte(Nat.mul(a, c), Nat.mul(b, c)), true) + // TODO + case c { + zero: + Equal.refl(true) + succ: + 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 + }: Equal(Nat.lte(Nat.mul(a, c), Nat.mul(b, c)), true) + +Nat.Order.mul.left( + a: Nat + b: Nat + c: Nat + Hyp: Equal(Nat.lte(a, b), Bool.true) +): Equal(Nat.lte(Nat.mul(c, a), Nat.mul(c, b)), Bool.true) + // TODO + let lem = Nat.Order.mul.right(a, b, c, Hyp) + let lem = Equal.rewrite( + Nat.mul(a, c), Nat.mul(c, a), Nat.mul.comm(a, c), + (x) Equal(Nat.lte(x, Nat.mul(b, c)), Bool.true), lem + ) + let qed = Equal.rewrite( + Nat.mul(b, c), Nat.mul(c, b), Nat.mul.comm(b, c), + (x) Equal(Nat.lte(Nat.mul(c, a), x), Bool.true), lem + ) + qed // 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(Nat.lte(a, b), Bool.true), -// Hyp1: Equal(Nat.lte(c, d), Bool.true) -//): Equal(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.mul.combine( + a: Nat, + b: Nat, + c: Nat, + d: Nat, + Hyp0: Equal(Nat.lte(a, b), Bool.true), + Hyp1: Equal(Nat.lte(c, d), Bool.true) +): Equal(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.bernoulli( // a: Nat, diff --git a/base/Nat/add/assoc.kind b/base/Nat/add/assoc.kind index 916525d2..7faee5a3 100644 --- a/base/Nat/add/assoc.kind +++ b/base/Nat/add/assoc.kind @@ -1,6 +1,7 @@ -Nat.add.assoc(a: Nat, b: Nat, c: Nat) - : ((a + b) + c) == a + (b + c) - case a{ +Nat.add.assoc( + a: Nat, b: Nat, c: Nat +): Equal(Nat.add(Nat.add(a, b), c), Nat.add(a, Nat.add(b, c))) + case a { zero: refl succ: let h=Nat.add.assoc(a.pred, b, c) diff --git a/base/Nat/mul.kind b/base/Nat/mul.kind index d8c204a9..8cab99e6 100644 --- a/base/Nat/mul.kind +++ b/base/Nat/mul.kind @@ -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)), - } \ No newline at end of file + case n { + zero: + 0 + succ: + Nat.add(m, Nat.mul(n.pred, m)) + } diff --git a/base/Nat/mul/assoc.kind b/base/Nat/mul/assoc.kind index bbedf7c1..a24f42c7 100644 --- a/base/Nat/mul/assoc.kind +++ b/base/Nat/mul/assoc.kind @@ -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.mul(a, Nat.mul(b, c)), Nat.mul(Nat.mul(a, b), c)) + case a { + zero: + Equal.refl(0) + succ: + let ind = Nat.mul.assoc(a.pred, b, c) + let lemma = Equal.apply( + 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.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.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.add(Nat.mul(b,c),Nat.mul(a.pred,Nat.mul(b,c))), x) + lemma + ) + qed + }: Equal(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 diff --git a/base/Nat/mul/comm.kind b/base/Nat/mul/comm.kind index 8429bb6b..f6f3e87e 100644 --- a/base/Nat/mul/comm.kind +++ b/base/Nat/mul/comm.kind @@ -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.mul(a, b), Nat.mul(b, a)) + case a { + zero: + Equal.mirror(Nat.mul(b, 0), 0, Nat.mul.zero_right(b)) + succ: + let ind = Nat.mul.comm(a.pred, b) + let lemma = Equal.apply( + 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.add(b,Nat.mul(b,a.pred)), Nat.mul(b,Nat.succ(a.pred)) + succ_right, + (x) Equal(Nat.add(b,Nat.mul(a.pred,b)), x) + lemma + ) + qed + }: Equal(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) diff --git a/base/Nat/mul/distrib_left.kind b/base/Nat/mul/distrib_left.kind index df42f507..1136e489 100644 --- a/base/Nat/mul/distrib_left.kind +++ b/base/Nat/mul/distrib_left.kind @@ -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.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.mul(Nat.add(b, c), a), Nat.mul(a, Nat.add(b, c)) + Nat.mul.comm(Nat.add(b, c), a) + (x) Equal(x, Nat.add(Nat.mul(b,a),Nat.mul(c,a))) + lemma + ) + let lemma = Equal.rewrite( + Nat.mul(b, a), Nat.mul(a, b), Nat.mul.comm(b, a) + (x) Equal(Nat.mul(a,Nat.add(b,c)), Nat.add(x, Nat.mul(c,a))) + lemma + ) + let qed = Equal.rewrite( + Nat.mul(c, a), Nat.mul(a, c), Nat.mul.comm(c, a) + (x) Equal(Nat.mul(a, Nat.add(b,c)), Nat.add(Nat.mul(a, b), x)) + lemma + ) + qed diff --git a/base/Nat/mul/distrib_right.kind b/base/Nat/mul/distrib_right.kind new file mode 100644 index 00000000..abd13520 --- /dev/null +++ b/base/Nat/mul/distrib_right.kind @@ -0,0 +1,27 @@ +Nat.mul.distrib_right( + a: Nat, b: Nat, c: Nat +): Equal(Nat.mul(Nat.add(a, b), c), Nat.add(Nat.mul(a, c), Nat.mul(b, c))) + case a { + zero: + Equal.refl(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.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.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.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.add(c, Nat.mul(Nat.add(a.pred, b), c)), x) + lemma + ) + qed + }: Equal(Nat.mul(Nat.add(a, b), c), Nat.add(Nat.mul(a, c), Nat.mul(b, c))) diff --git a/base/Nat/mul/one_left.kind b/base/Nat/mul/one_left.kind index 322b2d3b..b16e3b7d 100644 --- a/base/Nat/mul/one_left.kind +++ b/base/Nat/mul/one_left.kind @@ -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!!(h) - }! +Nat.mul.one_left(a: Nat): Equal(Nat.mul(1, a), a) + Nat.add.zero_right(a) diff --git a/base/Nat/mul/one_right.kind b/base/Nat/mul/one_right.kind index 955006ec..6ba0f00b 100644 --- a/base/Nat/mul/one_right.kind +++ b/base/Nat/mul/one_right.kind @@ -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.mul(a, 1), a) + case a { + zero: + Equal.refl(0) + succ: + let ind = Nat.mul.one_right(a.pred) + let qed = Equal.apply( + Nat.mul(a.pred, 1), a.pred, Nat.succ, ind + ) + qed + }: Equal(Nat.mul(a, 1), a) diff --git a/base/Nat/mul/succ_left.kind b/base/Nat/mul/succ_left.kind index 91531c07..0f394833 100644 --- a/base/Nat/mul/succ_left.kind +++ b/base/Nat/mul/succ_left.kind @@ -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.mul(Nat.succ(a), b), Nat.add(b, Nat.mul(a, b))) + Equal.refl(Nat.mul(Nat.succ(a), b)) diff --git a/base/Nat/mul/succ_right.kind b/base/Nat/mul/succ_right.kind index 87333175..d73f55c7 100644 --- a/base/Nat/mul/succ_right.kind +++ b/base/Nat/mul/succ_right.kind @@ -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.mul(a, Nat.succ(b)), Nat.add(a, Nat.mul(a, b))) + case a { + zero: + Equal.refl(0) + succ: + let ind = Nat.mul.succ_right(a.pred, b) + let lemma = Equal.apply( + 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.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.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.add(b, Nat.mul(a.pred, Nat.succ(b))), x), + lemma + ) + let lemma = Equal.rewrite( + Nat.add(b, a.pred), Nat.add(a.pred, b), + Nat.add.comm(b, a.pred), + (x) Equal(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.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.add(b, Nat.mul(a.pred, Nat.succ(b))), x), + lemma + ) + let qed = Equal.apply( + 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.mul(a, Nat.succ(b)), Nat.add(a, Nat.mul(a, b))) diff --git a/base/Nat/mul/zero_left.kind b/base/Nat/mul/zero_left.kind index 87c93c40..85e276ad 100644 --- a/base/Nat/mul/zero_left.kind +++ b/base/Nat/mul/zero_left.kind @@ -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.mul(0, a), 0) + case a { + zero: + Equal.refl(0) succ: let h = Nat.mul.zero_left(a.pred) - apply((x) (0+x), h) - }! + h + }: Equal(Nat.mul(0, a), 0) diff --git a/base/Nat/mul/zero_right.kind b/base/Nat/mul/zero_right.kind index cf6113c6..9ef6d5e5 100644 --- a/base/Nat/mul/zero_right.kind +++ b/base/Nat/mul/zero_right.kind @@ -1,2 +1,7 @@ -Nat.mul.zero_right(a: Nat): (a * 0) == 0 - refl +Nat.mul.zero_right(a: Nat): Equal(Nat.mul(a, 0), 0) + case a { + zero: + Equal.refl(0) + succ: + Nat.mul.zero_right(a.pred) + }: Equal(Nat.mul(a, 0), 0) diff --git a/base/Nat/succ_neq_zero.kind b/base/Nat/succ_neq_zero.kind index fd028a1e..36dd602b 100644 --- a/base/Nat/succ_neq_zero.kind +++ b/base/Nat/succ_neq_zero.kind @@ -1,2 +1,2 @@ Nat.succ_neq_zero(a: Nat): Not(Equal) - (e) Bool.false_neq_true(apply(Nat.is_zero, e)) + (e) Bool.false_neq_true(Equal.apply(Nat.succ(a), 0, Nat.is_zero, e)) From 34eca25dd33aa0d2e47a8b24cbb200e058f61de3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=ADgille=20S=2E=20B=2E=20Menezes?= Date: Sat, 9 Oct 2021 17:34:09 -0300 Subject: [PATCH 04/17] remove some more holes from addition theorems --- base/Nat/add/assoc.kind | 10 +++++++--- base/Nat/add/cancel_left.kind | 29 +++++++++++++++++++++-------- base/Nat/add/cancel_right.kind | 9 +++++---- 3 files changed, 33 insertions(+), 15 deletions(-) diff --git a/base/Nat/add/assoc.kind b/base/Nat/add/assoc.kind index 7faee5a3..ec281365 100644 --- a/base/Nat/add/assoc.kind +++ b/base/Nat/add/assoc.kind @@ -2,8 +2,12 @@ Nat.add.assoc( a: Nat, b: Nat, c: Nat ): Equal(Nat.add(Nat.add(a, b), c), Nat.add(a, Nat.add(b, c))) case a { - zero: refl + zero: + Equal.refl(Nat.add(b, c)) succ: - let h=Nat.add.assoc(a.pred, b, c) - Equal.apply!!(h) + 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 + ) }! diff --git a/base/Nat/add/cancel_left.kind b/base/Nat/add/cancel_left.kind index 2f92de01..76d45eb9 100644 --- a/base/Nat/add/cancel_left.kind +++ b/base/Nat/add/cancel_left.kind @@ -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.add(a, b), Nat.add(a, c))): Equal(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.add(Nat.succ(a.pred),b), Nat.succ(Nat.add(a.pred,b)), + Nat.add.succ_left(a.pred, b), + (x) Equal(x, Nat.add(Nat.succ(a.pred),c)), e0 + ) + let e3 = Equal.rewrite( + Nat.add(Nat.succ(a.pred),c), Nat.succ(Nat.add(a.pred,c)) + Nat.add.succ_left(a.pred, c) + (x) Equal(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.add(a, b), Nat.add(a, c))) -> Equal(b, c))( + e0 + ) diff --git a/base/Nat/add/cancel_right.kind b/base/Nat/add/cancel_right.kind index a790467b..f7202488 100644 --- a/base/Nat/add/cancel_right.kind +++ b/base/Nat/add/cancel_right.kind @@ -1,6 +1,7 @@ // 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_right( + a: Nat, b: Nat, c: Nat, h: Equal(Nat.add(a, b), Nat.add(c, b)) +): Equal(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) From 1368f8c6a7d4e3e9c74559da8a5b7ed31cd41554 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=ADgille=20S=2E=20B=2E=20Menezes?= Date: Sun, 10 Oct 2021 15:37:09 -0300 Subject: [PATCH 05/17] remove more holes --- base/Nat/Order.kind | 50 ++++++++++++++-------------------- base/Nat/add/cancel_right.kind | 15 ++++++++-- base/Nat/add/comm.kind | 37 +++++++++++++++++-------- base/Nat/add/succ_both.kind | 5 ++-- 4 files changed, 61 insertions(+), 46 deletions(-) diff --git a/base/Nat/Order.kind b/base/Nat/Order.kind index 33f99a8c..69159c49 100644 --- a/base/Nat/Order.kind +++ b/base/Nat/Order.kind @@ -208,26 +208,6 @@ Nat.Order.add.combine( 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 -// 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: Equal(Nat.lte(a, b), true) -): Equal(Nat.lte(Nat.mul(a, c), Nat.mul(b, c)), true) - // TODO - case c { - zero: - Equal.refl(true) - succ: - 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 - }: Equal(Nat.lte(Nat.mul(a, c), Nat.mul(b, c)), true) Nat.Order.mul.left( a: Nat @@ -236,20 +216,32 @@ Nat.Order.mul.left( Hyp: Equal(Nat.lte(a, b), Bool.true) ): Equal(Nat.lte(Nat.mul(c, a), Nat.mul(c, b)), Bool.true) // TODO - let lem = Nat.Order.mul.right(a, b, c, Hyp) + case c { + zero: + Equal.refl(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(Nat.lte(Nat.mul(c, a), Nat.mul(c, b)), true) + + +Nat.Order.mul.right( + a: Nat + b: Nat + c: Nat + Hyp: Equal(Nat.lte(a, b), true) +): Equal(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.mul(a, c), Nat.mul(c, a), Nat.mul.comm(a, c), - (x) Equal(Nat.lte(x, Nat.mul(b, c)), Bool.true), lem + Nat.mul(c,a), Nat.mul(a, c), Nat.mul.comm(c, a) + (x) Equal(Nat.lte(x, Nat.mul(c, b)), Bool.true), lem ) let qed = Equal.rewrite( - Nat.mul(b, c), Nat.mul(c, b), Nat.mul.comm(b, c), - (x) Equal(Nat.lte(Nat.mul(c, a), x), Bool.true), lem + Nat.mul(c, b), Nat.mul(b, c), Nat.mul.comm(c, b) + (x) Equal(Nat.lte(Nat.mul(a, c), x), Bool.true), lem ) qed -// 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, diff --git a/base/Nat/add/cancel_right.kind b/base/Nat/add/cancel_right.kind index f7202488..c6ea768d 100644 --- a/base/Nat/add/cancel_right.kind +++ b/base/Nat/add/cancel_right.kind @@ -2,6 +2,15 @@ Nat.add.cancel_right( a: Nat, b: Nat, c: Nat, h: Equal(Nat.add(a, b), Nat.add(c, b)) ): Equal(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) + let lemma = Equal.rewrite( + Nat.add(a,b), Nat.add(b,a), Nat.add.comm(a, b), + (x) Equal(x, Nat.add(c, b)) + h + ) + let lemma = Equal.rewrite( + Nat.add(c,b), Nat.add(b,c), Nat.add.comm(c, b), + (x) Equal(Nat.add(b, a), x) + lemma + ) + let qed = Nat.add.cancel_left(b, a, c, lemma) + qed diff --git a/base/Nat/add/comm.kind b/base/Nat/add/comm.kind index 2d8e2ae8..8b924977 100644 --- a/base/Nat/add/comm.kind +++ b/base/Nat/add/comm.kind @@ -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.add(a, b), Nat.add(b, a)) + case a { + zero: + Equal.mirror( + 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.add(a.pred,b), Nat.add(b,a.pred) + Nat.succ, ind + ) + let succ_right = Equal.mirror( + 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.succ(Nat.add(b,a.pred)), Nat.add(b,Nat.succ(a.pred)), succ_right + (x) Equal(Nat.add(Nat.succ(a.pred), b), x) + lemma + ) + qed + }: Equal(Nat.add(a, b), Nat.add(b, a)) diff --git a/base/Nat/add/succ_both.kind b/base/Nat/add/succ_both.kind index 1123c654..33f2e4c6 100644 --- a/base/Nat/add/succ_both.kind +++ b/base/Nat/add/succ_both.kind @@ -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)) From b9a0defe1676a62492b735ca9f5869a79810a560 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=ADgille=20S=2E=20B=2E=20Menezes?= Date: Mon, 11 Oct 2021 13:05:14 -0300 Subject: [PATCH 06/17] create blueprint for decision procedure --- base/Nat/AlgExp.kind | 48 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 48 insertions(+) create mode 100644 base/Nat/AlgExp.kind diff --git a/base/Nat/AlgExp.kind b/base/Nat/AlgExp.kind new file mode 100644 index 00000000..839796b6 --- /dev/null +++ b/base/Nat/AlgExp.kind @@ -0,0 +1,48 @@ +Variadic.Equal( + n: Nat + l: Variadic(n) + r: Variadic(n) +): Variadic(n) + case n with l r { + zero: + Equal(l, r) + succ: + (x) Variadic.Equal(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((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) + From 4527b483e90061671fba6f163085778b4d1891c6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=ADgille=20S=2E=20B=2E=20Menezes?= Date: Mon, 11 Oct 2021 19:21:49 -0300 Subject: [PATCH 07/17] prove commutativity of Nat.max --- base/Either3.kind | 5 +++ base/Nat/Order.kind | 47 +++++++++++++++++------- base/Nat/Order/mul.kind | 8 ++--- base/Nat/lte.kind | 14 ++++---- base/Nat/lte/comm.kind | 44 +++++++++++++++++++++++ base/Nat/max.kind | 12 ++++--- base/Nat/max/comm.kind | 43 ++++++++++++++++++++++ base/Test.kind | 80 +++++++++++++++++++++++++++++++++++++++-- 8 files changed, 224 insertions(+), 29 deletions(-) create mode 100644 base/Either3.kind create mode 100644 base/Nat/lte/comm.kind create mode 100644 base/Nat/max/comm.kind diff --git a/base/Either3.kind b/base/Either3.kind new file mode 100644 index 00000000..dc45d82c --- /dev/null +++ b/base/Either3.kind @@ -0,0 +1,5 @@ +type Either3 { + fst(value: A) + snd(value: B) + trd(value: C) +} diff --git a/base/Nat/Order.kind b/base/Nat/Order.kind index 69159c49..e54d9362 100644 --- a/base/Nat/Order.kind +++ b/base/Nat/Order.kind @@ -243,18 +243,41 @@ Nat.Order.mul.right( ) qed -Nat.Order.mul.combine( - a: Nat, - b: Nat, - c: Nat, - d: Nat, - Hyp0: Equal(Nat.lte(a, b), Bool.true), - Hyp1: Equal(Nat.lte(c, d), Bool.true) -): Equal(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.max.big( +// a: Nat +// b: Nat +//): And(Nat.lte(a, Nat.max(a, b)), true), Equal(Nat.lte(b, Nat.max(a, b)), true)> +// case a { +// zero: +// Pair.new!!(Equal.refl(true), Nat.Order.refl(b)) +// succ: +// let ind = Nat.Order.max(a.pred, b) +// ?succ +// }! + +Nat.Order.trichotomy( + a: Nat + b: Nat +): Either3< + Equal(Nat.lte(a, b), false) + Equal(a, b) + Equal(Nat.lte(b, a), false) + > + def cmp_ab = Nat.lte(a, b) + def cmp_ba = Nat.lte(b, a) + let lemma_ab = Equal.refl(cmp_ab) + let lemma_ba = Equal.refl(cmp_ba) + case cmp_ab with lemma_ab: cmp_ab^ == cmp_ab { + false: + Either3.fst!!!(Equal.refl(false)) + true: + case cmp_ba with lemma_ba: cmp_ba^ == cmp_ba { + false: + Either3.trd!!!(Equal.refl(false)) + true: + Either3.snd!!!(Nat.Order.anti_symm!!(lemma_ab, lemma_ba)) + }! + }! //Nat.Order.bernoulli( // a: Nat, diff --git a/base/Nat/Order/mul.kind b/base/Nat/Order/mul.kind index e8fcfc2c..33d0355d 100644 --- a/base/Nat/Order/mul.kind +++ b/base/Nat/Order/mul.kind @@ -4,9 +4,9 @@ Nat.Order.mul.combine( c: Nat, d: Nat, Hyp0: Equal(Nat.lte(a, b), Bool.true), - Hyp1: Equal(Nat.lte(c, d), Bool.true), + Hyp1: Equal(Nat.lte(c, d), Bool.true) ): Equal(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 diff --git a/base/Nat/lte.kind b/base/Nat/lte.kind index 1a700b51..fc86dc92 100644 --- a/base/Nat/lte.kind +++ b/base/Nat/lte.kind @@ -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), - } - } \ No newline at end of file + zero: + true, + succ: + case m { + zero: false, + succ: Nat.lte(n.pred, m.pred), + } + } diff --git a/base/Nat/lte/comm.kind b/base/Nat/lte/comm.kind new file mode 100644 index 00000000..b023a88b --- /dev/null +++ b/base/Nat/lte/comm.kind @@ -0,0 +1,44 @@ +Nat.lte.comm.false( + a: Nat + b: Nat + Hyp: Equal(Nat.lte(a, b), false) +): Equal(Nat.lte(b, a), true) + (case a { + zero: + (Hyp) + let contra = Bool.true_neq_false(Hyp) + Empty.absurd(Nat.lte(b, 0), true)>(contra) + succ: + (Hyp) + (case b { + zero: + (Hyp) + Equal.refl(true) + succ: + (Hyp) + let qed = Nat.lte.comm.false(a.pred, b.pred, Hyp) + qed + }: (Hyp: Equal(Nat.lte(Nat.succ(a.pred), b), false)) -> Equal(Nat.lte(b, Nat.succ(a.pred)), true))( + Hyp + ) + }: (Hyp: Equal(Nat.lte(a, b), false)) -> Equal(Nat.lte(b, a), true))( + Hyp + ) + +Nat.lte.comm.true( + a: Nat + b: Nat + Hyp: Equal(Nat.lte(Nat.succ(a), b), true) +): Equal(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(false) + succ: + Nat.lte.comm.true(a.pred, b.pred, Hyp) + }! + }! diff --git a/base/Nat/max.kind b/base/Nat/max.kind index 238a6ccd..a3f62791 100644 --- a/base/Nat/max.kind +++ b/base/Nat/max.kind @@ -1,5 +1,7 @@ -Nat.max(a:Nat, b:Nat): Nat - case Nat.gtn(a, b) { - true:a - false:b - } \ No newline at end of file +Nat.max(a: Nat, b: Nat): Nat + case Nat.lte(a, b) { + true: + b + false: + a + } diff --git a/base/Nat/max/comm.kind b/base/Nat/max/comm.kind new file mode 100644 index 00000000..f797e18c --- /dev/null +++ b/base/Nat/max/comm.kind @@ -0,0 +1,43 @@ +Nat.max.comm( + a: Nat + b: Nat +): Equal(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 qed = Equal.refl(a) + let qed = Equal.rewrite( + false, Nat.lte(a, b), mirror(lemma.value), + (x) Equal(x(() Nat, b, a), true(() Nat, a, b)) + qed + ) + let qed = Equal.rewrite( + true, Nat.lte(b, a), mirror(lemma_ba), + (x) Equal(Nat.lte(a, b, () Nat, b, a), x(() Nat, a, b)) + qed + ) + qed + snd: + let qed = Equal.refl(Nat.max(a, a)) + let qed = Equal.rewrite( + a, b, lemma.value + (x) Equal(Nat.max(a, x), Nat.max(x, a)) + qed + ) + qed + trd: + let lemma_ab = Nat.lte.comm.false!!(lemma.value) + let qed = Equal.refl(b) + let qed = Equal.rewrite( + false, Nat.lte(b, a), mirror(lemma.value), + (x) Equal(true(() Nat, b, a), x(() Nat, a, b)) + qed + ) + let qed = Equal.rewrite( + true, Nat.lte(a, b), mirror(lemma_ab), + (x) Equal(x(() Nat, b, a), Nat.lte(b, a, () Nat, a, b)) + qed + ) + qed + } diff --git a/base/Test.kind b/base/Test.kind index e8882249..8d298268 100644 --- a/base/Test.kind +++ b/base/Test.kind @@ -1,3 +1,79 @@ +type Nat.AddExp { + const(value: Nat) + var(idx: Nat) + add(left: Nat.AddExp, right: Nat.AddExp) +} + +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.dimension.zero( + exp: Nat.AddExp + Hyp: Equal(Nat.AddExp.dimension(exp), 0) +): Nat.AddExp.constant(exp) + (case exp { + const: + (Hyp) + unit + var: + (Hyp) + ?var + add: + (Hyp) + def left_dim = Nat.AddExp.dimension(exp.left) + let left_lemma = + (case left_dim { + zero: + (left_dim, Hyp) + ?zero + succ: + (left_dim, Hyp) + ?succ + }: (left_dim: Nat + Hyp: Equal(Nat.max(left_dim, Nat.AddExp.dimension(exp.right)), 0)) -> + Equal(left_dim, 0))( + left_dim, + Hyp + ) +// let left = Nat.AddExp.dimension.zero(exp.left) +// let right = Nat.AddExp.dimension.zero(exp.right) + ?add + //Pair.new!!(left, right) + }: (Hyp: Equal(Nat.AddExp.dimension(exp), 0)) -> Nat.AddExp.constant(exp))( + Hyp + ) + +Nat.AddExp.substitution( + exp: Nat.AddExp +): Variadic(Nat.AddExp.dimension(exp), Nat, Nat) + ?substitution + +Nat.AddExp.substitution.aux( + n: Nat + exp: Nat.AddExp +): Variadic(n, Nat, Nat) + ?substitution + Test: _ - let b = Litereum.serialize.varlen.go(12) - Litereum.deserialize.varlen.go(b) \ No newline at end of file + "hi" From 528db93c6c92b7d9ed3abc918b0e0ac0e9f08653 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=ADgille=20S=2E=20B=2E=20Menezes?= Date: Mon, 11 Oct 2021 22:59:22 -0300 Subject: [PATCH 08/17] substitution looking good --- base/Nat/max/big.kind | 25 ++++++++++ base/Test.kind | 108 +++++++++++++++++++++++++++++++++--------- 2 files changed, 110 insertions(+), 23 deletions(-) create mode 100644 base/Nat/max/big.kind diff --git a/base/Nat/max/big.kind b/base/Nat/max/big.kind new file mode 100644 index 00000000..35eaab1a --- /dev/null +++ b/base/Nat/max/big.kind @@ -0,0 +1,25 @@ +Nat.max.big( + a: Nat + b: Nat +): And(Nat.lte(a, Nat.max(a, b)), true), Equal(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) + Pair.new!!(Nat.Order.refl(a), lemma_ba) + }: (lemma_ab: Equal(Nat.lte(a, b), cmp_ab)) -> And< + Equal(Nat.lte(a, case cmp_ab { true: b, false: a }), true), + Equal(Nat.lte(b, case cmp_ab { true: b, false: a }), true)>)( + lemma_ab + ) + +Nat.max.big.left(a: Nat, b: Nat): Equal(Nat.lte(a, Nat.max(a, b)), true) + Pair.fst!!(Nat.max.big(a, b)) + +Nat.max.big.right(a: Nat, b: Nat): Equal(Nat.lte(b, Nat.max(a,b)), true) + Pair.snd!!(Nat.max.big(a, b)) diff --git a/base/Test.kind b/base/Test.kind index 8d298268..49fc720e 100644 --- a/base/Test.kind +++ b/base/Test.kind @@ -38,42 +38,104 @@ Nat.AddExp.dimension.zero( unit var: (Hyp) - ?var + let contra = Nat.succ_neq_zero!(Hyp) + Empty.absurd!(contra) add: (Hyp) - def left_dim = Nat.AddExp.dimension(exp.left) - let left_lemma = - (case left_dim { - zero: - (left_dim, Hyp) - ?zero - succ: - (left_dim, Hyp) - ?succ - }: (left_dim: Nat - Hyp: Equal(Nat.max(left_dim, Nat.AddExp.dimension(exp.right)), 0)) -> - Equal(left_dim, 0))( - left_dim, - Hyp - ) -// let left = Nat.AddExp.dimension.zero(exp.left) -// let right = Nat.AddExp.dimension.zero(exp.right) - ?add - //Pair.new!!(left, right) + 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( + max, 0, Hyp, + (x) Equal(Nat.lte(Nat.AddExp.dimension(exp.left), x), true), + left_small + )) + let right_zero = Nat.Order.chain.aux!(Equal.rewrite( + max, 0, Hyp + (x) Equal(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.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) - ?substitution + def dim = Nat.AddExp.dimension(exp) + def Hyp = Nat.Order.refl(dim) + Nat.AddExp.substitution.aux0(dim, exp, Hyp) -Nat.AddExp.substitution.aux( +Nat.AddExp.substitution.aux0( n: Nat exp: Nat.AddExp + Hyp: Equal(Nat.lte(Nat.AddExp.dimension(exp), n), true) ): Variadic(n, Nat, Nat) - ?substitution + 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, Nat.succ(n.pred)) + let Hyp = Nat.AddExp.substitution.aux2(exp, value, Nat.succ(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(Nat.lte(Nat.AddExp.dimension(exp), idx), true) +): let new_exp = Nat.AddExp.substitution.aux1(exp, value, idx) + Equal(Nat.lte(Nat.AddExp.dimension(new_exp), Nat.pred(idx)), true) + case exp with Hyp { + const: + Equal.refl(true) + var: + ?var + add: + ?add + }! Test: _ "hi" From 1eee54b72e2a5e1e98486c9a1fae381c965aa278 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=ADgille=20S=2E=20B=2E=20Menezes?= Date: Wed, 13 Oct 2021 12:20:13 -0300 Subject: [PATCH 09/17] prove more theorems about natural numbers --- base/Nat/AddExp.kind | 155 +++++++++++++++++++++++++++++++++++ base/Nat/lte/comm.kind | 8 +- base/Nat/lte/succ_left.kind | 17 ++++ base/Nat/max/big.kind | 1 + base/Nat/max/combine.kind | 22 +++++ base/Nat/max/comm.kind | 2 + base/Nat/max/split.kind | 8 ++ base/Test.kind | 157 ++++-------------------------------- 8 files changed, 225 insertions(+), 145 deletions(-) create mode 100644 base/Nat/AddExp.kind create mode 100644 base/Nat/lte/succ_left.kind create mode 100644 base/Nat/max/combine.kind create mode 100644 base/Nat/max/split.kind diff --git a/base/Nat/AddExp.kind b/base/Nat/AddExp.kind new file mode 100644 index 00000000..091ae9db --- /dev/null +++ b/base/Nat/AddExp.kind @@ -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.dimension.zero( + exp: Nat.AddExp + Hyp: Equal(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( + max, 0, Hyp, + (x) Equal(Nat.lte(Nat.AddExp.dimension(exp.left), x), true), + left_small + )) + let right_zero = Nat.Order.chain.aux!(Equal.rewrite( + max, 0, Hyp + (x) Equal(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.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(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(Nat.lte(Nat.AddExp.dimension(exp), Nat.succ(idx)), true) +): let new_exp = Nat.AddExp.substitution.aux1(exp, value, idx) + Equal(Nat.lte(Nat.AddExp.dimension(new_exp), idx), true) + case exp with Hyp { + const: + Equal.refl(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(true) + false: + Nat.lte.comm.false(idx, exp.idx, cmp_eq) + }! :: Equal(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) + }! diff --git a/base/Nat/lte/comm.kind b/base/Nat/lte/comm.kind index b023a88b..c0d428c9 100644 --- a/base/Nat/lte/comm.kind +++ b/base/Nat/lte/comm.kind @@ -2,12 +2,12 @@ Nat.lte.comm.false( a: Nat b: Nat Hyp: Equal(Nat.lte(a, b), false) -): Equal(Nat.lte(b, a), true) +): Equal(Nat.lte(Nat.succ(b), a), true) (case a { zero: (Hyp) let contra = Bool.true_neq_false(Hyp) - Empty.absurd(Nat.lte(b, 0), true)>(contra) + Empty.absurd(Nat.lte(Nat.succ(b), 0), true)>(contra) succ: (Hyp) (case b { @@ -18,10 +18,10 @@ Nat.lte.comm.false( (Hyp) let qed = Nat.lte.comm.false(a.pred, b.pred, Hyp) qed - }: (Hyp: Equal(Nat.lte(Nat.succ(a.pred), b), false)) -> Equal(Nat.lte(b, Nat.succ(a.pred)), true))( + }: (Hyp: Equal(Nat.lte(Nat.succ(a.pred), b), false)) -> Equal(Nat.lte(Nat.succ(b), Nat.succ(a.pred)), true))( Hyp ) - }: (Hyp: Equal(Nat.lte(a, b), false)) -> Equal(Nat.lte(b, a), true))( + }: (Hyp: Equal(Nat.lte(a, b), false)) -> Equal(Nat.lte(Nat.succ(b), a), true))( Hyp ) diff --git a/base/Nat/lte/succ_left.kind b/base/Nat/lte/succ_left.kind new file mode 100644 index 00000000..58e28317 --- /dev/null +++ b/base/Nat/lte/succ_left.kind @@ -0,0 +1,17 @@ +Nat.lte.succ_left( + a: Nat + b: Nat + Hyp: Equal(Nat.lte(Nat.succ(a), b), true) +): Equal(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) + }! + }! diff --git a/base/Nat/max/big.kind b/base/Nat/max/big.kind index 35eaab1a..d97aae23 100644 --- a/base/Nat/max/big.kind +++ b/base/Nat/max/big.kind @@ -11,6 +11,7 @@ Nat.max.big( 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(Nat.lte(a, b), cmp_ab)) -> And< Equal(Nat.lte(a, case cmp_ab { true: b, false: a }), true), diff --git a/base/Nat/max/combine.kind b/base/Nat/max/combine.kind new file mode 100644 index 00000000..23b5cf91 --- /dev/null +++ b/base/Nat/max/combine.kind @@ -0,0 +1,22 @@ +Nat.max.combine.right( + a: Nat + b: Nat + c: Nat + Hyp: Equal(Nat.lte(a, b), true) +): Equal(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(Nat.lte(a, b), true) + Hyp1: Equal(Nat.lte(c, b), true) +): Equal(Nat.lte(Nat.max(a, c), b), true) + def cmp_ac = Nat.lte(a, c) + case cmp_ac { + true: + Hyp1 + false: + Hyp0 + }! :: Equal(Nat.lte(cmp_ac(() Nat, c, a), b), true) diff --git a/base/Nat/max/comm.kind b/base/Nat/max/comm.kind index f797e18c..bc4cff16 100644 --- a/base/Nat/max/comm.kind +++ b/base/Nat/max/comm.kind @@ -6,6 +6,7 @@ Nat.max.comm( 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(a) let qed = Equal.rewrite( false, Nat.lte(a, b), mirror(lemma.value), @@ -28,6 +29,7 @@ Nat.max.comm( qed trd: let lemma_ab = Nat.lte.comm.false!!(lemma.value) + let lemma_ab = Nat.lte.succ_left!!(lemma_ab) let qed = Equal.refl(b) let qed = Equal.rewrite( false, Nat.lte(b, a), mirror(lemma.value), diff --git a/base/Nat/max/split.kind b/base/Nat/max/split.kind new file mode 100644 index 00000000..9935fb19 --- /dev/null +++ b/base/Nat/max/split.kind @@ -0,0 +1,8 @@ +Nat.max.split.left( + a: Nat + b: Nat + c: Nat + Hyp: Equal(Nat.lte(Nat.max(a, b), c), true) +): And(Nat.lte(a, c), true), Equal(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)} diff --git a/base/Test.kind b/base/Test.kind index 49fc720e..15735099 100644 --- a/base/Test.kind +++ b/base/Test.kind @@ -1,141 +1,16 @@ -type Nat.AddExp { - const(value: Nat) - var(idx: Nat) - add(left: Nat.AddExp, right: Nat.AddExp) -} - -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.dimension.zero( - exp: Nat.AddExp - Hyp: Equal(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( - max, 0, Hyp, - (x) Equal(Nat.lte(Nat.AddExp.dimension(exp.left), x), true), - left_small - )) - let right_zero = Nat.Order.chain.aux!(Equal.rewrite( - max, 0, Hyp - (x) Equal(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.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(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, Nat.succ(n.pred)) - let Hyp = Nat.AddExp.substitution.aux2(exp, value, Nat.succ(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(Nat.lte(Nat.AddExp.dimension(exp), idx), true) -): let new_exp = Nat.AddExp.substitution.aux1(exp, value, idx) - Equal(Nat.lte(Nat.AddExp.dimension(new_exp), Nat.pred(idx)), true) - case exp with Hyp { - const: - Equal.refl(true) - var: - ?var - add: - ?add - }! - -Test: _ - "hi" +Test( + f: A -> B, + Hyp: ( + C: Type + g: B -> C + h: B -> C + a: A + HHyp: g(f(a)) == h(f(a)) + b: B + ) -> g(b) == h(b) + target: B +): [a: A] f(a) == target + let g = ((b) true) :: B -> Bool + let h = ((b) Decidable([a: A] f(a) == b)) :: B -> Bool + let hmm = Hyp(Type, g, h) + ?test From d4a38801def77c0cd876b66601d2b774b5d3109a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=ADgille=20S=2E=20B=2E=20Menezes?= Date: Wed, 13 Oct 2021 12:23:43 -0300 Subject: [PATCH 10/17] remove tiger --- base/Tiger.kind | 149 ------------------------------------------------ 1 file changed, 149 deletions(-) delete mode 100644 base/Tiger.kind diff --git a/base/Tiger.kind b/base/Tiger.kind deleted file mode 100644 index 7bcc0a07..00000000 --- a/base/Tiger.kind +++ /dev/null @@ -1,149 +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 -Tiger.pos: Type - Pair - -Tiger.symbol: Type - String - -type Tiger.var { - SimpleVar(name: Tiger.symbol, pos: Tiger.pos) - FieldVar(var: Tiger.var, name: Tiger.symbol, pos: Tiger.pos) - SubscriptVar(var: Tiger.var, exp: Tiger.exp, pos: Tiger.pos) -} - -type Tiger.record_fields { - new( - name: Tiger.symbol - args: List - pos: Tiger.pos - ) -} - -type Tiger.exp { - NilExp - VarExp(var: Tiger.var) - IntExp(val: Int) - StringExp(val: String, pos: Tiger.pos) - CallExp( - func: Tiger.symbol - args: List - pos: Tiger.pos - ) - OpExp( - left: Tiger.exp - oper: Tiger.oper - right: Tiger.exp - pos: Tiger.pos - ) - RecordExp( - fields: List - typ: Tiger.symbol - pos: Tiger.pos - ) - SeqExp( - val: List - ) - AssignExp( - var: Tiger.var - exp: Tiger.exp - pos: Tiger.pos - ) - IfExp( - test: Tiger.exp - then: Tiger.exp - else: Maybe - ) - WhileExp( - test: Tiger.exp - body: Tiger.exp - pos: Tiger.pos - ) - ForExp( - var: Tiger.symbol - escape: Bool - lo: Tiger.exp - hi: Tiger.exp - body: Tiger.exp - pos: Tiger.pos - ) - BreakExp( - pos: Tiger.pos - ) - LetExp( - decs: List - body: Tiger.exp - pos: Tiger.pos - ) - ArrayExp( - typ: Tiger.symbol - size: Tiger.exp - pos: Tiger.pos - ) -} - -type Tiger.oper { - PlusOp - MinusOp - TimesOp - DivideOp - EqOp - NeqOp - LtOp - LeOp - GtOp - GeOp -} - -type Tiger.dec { - FunctionDec( - val: List - ) - VarDec( - name: Tiger.symbol - escape: Bool - typ: Maybe> - ) - TypeDec( - val: List - ) -} - -type Tiger.typedec { - new( - name: Tiger.symbol - ty: Tiger.ty - pos: Tiger.pos - ) -} - -type Tiger.ty { - new( - NameTy: Pair - RecordTy: List - ArrayTy: Pair - ) -} - -type Tiger.field { - new( - name: Tiger.symbol - escape: Bool - typ: Tiger.symbol - pos: Tiger.pos - ) -} - -type Tiger.fundec { - new( - name: Tiger.symbol - params: List - result: Maybe> - body: Tiger.exp - pos: Tiger.pos - ) -} From 69b0c5ff134be7ee7a1293c163c1f4dab2613db0 Mon Sep 17 00:00:00 2001 From: rheidner Date: Wed, 13 Oct 2021 14:13:26 -0300 Subject: [PATCH 11/17] create tail version of bits.hex.encode --- base/Bits/hex_tail.kind | 65 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 65 insertions(+) create mode 100644 base/Bits/hex_tail.kind diff --git a/base/Bits/hex_tail.kind b/base/Bits/hex_tail.kind new file mode 100644 index 00000000..0164f5c5 --- /dev/null +++ b/base/Bits/hex_tail.kind @@ -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) + } + } + } + } \ No newline at end of file From 4f40c9a8ce5c21aedc582751cbcf41353b7f2094 Mon Sep 17 00:00:00 2001 From: caotic123 Date: Wed, 13 Oct 2021 17:57:40 -0300 Subject: [PATCH 12/17] Move files and update on Bytes --- base/Bytes.kind | 4 - base/Bytes/arrayify.kind | 4 - base/Bytes/drop.kind | 2 - base/Bytes/from_nat.kind | 6 -- base/Bytes/from_string.kind | 2 - base/Bytes/length.kind | 2 - base/Bytes/pad.kind | 7 -- base/Bytes/pad_rigth.kind | 2 - base/Bytes/parse_string.kind | 93 -------------------- base/Bytes/reverse.kind | 7 -- base/Bytes/slice.kind | 2 - base/Bytes/take.kind | 3 - base/Bytes/test/all.kind | 18 ---- base/Bytes/test/from_nat.kind | 29 ------- base/Bytes/test/from_string.kind | 53 ------------ base/Bytes/test/length.kind | 44 ---------- base/Bytes/test/parse_string.kind | 64 -------------- base/Bytes/test/slice.kind | 43 ---------- base/Bytes/test/to_nat.kind | 29 ------- base/Bytes/to_nat.kind | 3 - base/BytesLike.kind | 2 - base/String/hex.kind | 105 ++++++++++++++++++++--- base/String/hexstring/arrayify.kind | 3 + base/{Bytes => String/hexstring}/at.kind | 2 +- base/String/hexstring/from_nat.kind | 7 ++ 25 files changed, 103 insertions(+), 433 deletions(-) delete mode 100644 base/Bytes.kind delete mode 100644 base/Bytes/arrayify.kind delete mode 100644 base/Bytes/drop.kind delete mode 100644 base/Bytes/from_nat.kind delete mode 100644 base/Bytes/from_string.kind delete mode 100644 base/Bytes/length.kind delete mode 100644 base/Bytes/pad.kind delete mode 100644 base/Bytes/pad_rigth.kind delete mode 100644 base/Bytes/parse_string.kind delete mode 100644 base/Bytes/reverse.kind delete mode 100644 base/Bytes/slice.kind delete mode 100644 base/Bytes/take.kind delete mode 100644 base/Bytes/test/all.kind delete mode 100644 base/Bytes/test/from_nat.kind delete mode 100644 base/Bytes/test/from_string.kind delete mode 100644 base/Bytes/test/length.kind delete mode 100644 base/Bytes/test/parse_string.kind delete mode 100644 base/Bytes/test/slice.kind delete mode 100644 base/Bytes/test/to_nat.kind delete mode 100644 base/Bytes/to_nat.kind delete mode 100644 base/BytesLike.kind create mode 100644 base/String/hexstring/arrayify.kind rename base/{Bytes => String/hexstring}/at.kind (83%) create mode 100644 base/String/hexstring/from_nat.kind diff --git a/base/Bytes.kind b/base/Bytes.kind deleted file mode 100644 index eade023f..00000000 --- a/base/Bytes.kind +++ /dev/null @@ -1,4 +0,0 @@ -// A Bytes -// valid byte range (i.e. between 0 and 255 inclusive) -Bytes: Type - String \ No newline at end of file diff --git a/base/Bytes/arrayify.kind b/base/Bytes/arrayify.kind deleted file mode 100644 index 2e7a4dfa..00000000 --- a/base/Bytes/arrayify.kind +++ /dev/null @@ -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 \ No newline at end of file diff --git a/base/Bytes/drop.kind b/base/Bytes/drop.kind deleted file mode 100644 index 02783458..00000000 --- a/base/Bytes/drop.kind +++ /dev/null @@ -1,2 +0,0 @@ -Bytes.drop(n: Nat, b: Bytes): Bytes - String.drop(n, b) \ No newline at end of file diff --git a/base/Bytes/from_nat.kind b/base/Bytes/from_nat.kind deleted file mode 100644 index d30907d7..00000000 --- a/base/Bytes/from_nat.kind +++ /dev/null @@ -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 - \ No newline at end of file diff --git a/base/Bytes/from_string.kind b/base/Bytes/from_string.kind deleted file mode 100644 index 1a537d7c..00000000 --- a/base/Bytes/from_string.kind +++ /dev/null @@ -1,2 +0,0 @@ -Bytes.from_string(s: String): Bytes - "0x"|String.to_hex(s) diff --git a/base/Bytes/length.kind b/base/Bytes/length.kind deleted file mode 100644 index 7ebdaa4c..00000000 --- a/base/Bytes/length.kind +++ /dev/null @@ -1,2 +0,0 @@ -Bytes.length(b: Bytes): Nat - (String.length(b) - 2) / 2 \ No newline at end of file diff --git a/base/Bytes/pad.kind b/base/Bytes/pad.kind deleted file mode 100644 index d52fce4c..00000000 --- a/base/Bytes/pad.kind +++ /dev/null @@ -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) \ No newline at end of file diff --git a/base/Bytes/pad_rigth.kind b/base/Bytes/pad_rigth.kind deleted file mode 100644 index 41632fb7..00000000 --- a/base/Bytes/pad_rigth.kind +++ /dev/null @@ -1,2 +0,0 @@ -Bytes.pad_right(len: Nat, hex: String): String - String.pad_right(len, String.to_char("0"), hex) \ No newline at end of file diff --git a/base/Bytes/parse_string.kind b/base/Bytes/parse_string.kind deleted file mode 100644 index 67faf546..00000000 --- a/base/Bytes/parse_string.kind +++ /dev/null @@ -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 -// - \ No newline at end of file diff --git a/base/Bytes/reverse.kind b/base/Bytes/reverse.kind deleted file mode 100644 index e3bb708c..00000000 --- a/base/Bytes/reverse.kind +++ /dev/null @@ -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 \ No newline at end of file diff --git a/base/Bytes/slice.kind b/base/Bytes/slice.kind deleted file mode 100644 index 47fbf5d5..00000000 --- a/base/Bytes/slice.kind +++ /dev/null @@ -1,2 +0,0 @@ -Bytes.slice(i: Nat, j: Nat, bs: Bytes): Bytes - "0x" | String.slice((i*2)+2, ((j*2)+2), bs) diff --git a/base/Bytes/take.kind b/base/Bytes/take.kind deleted file mode 100644 index 3ff6a8ea..00000000 --- a/base/Bytes/take.kind +++ /dev/null @@ -1,3 +0,0 @@ -// Take the first 'n' characters from 'b' -Bytes.take(n: Nat, b: Bytes): Bytes - String.take(n, b) diff --git a/base/Bytes/test/all.kind b/base/Bytes/test/all.kind deleted file mode 100644 index 888f3322..00000000 --- a/base/Bytes/test/all.kind +++ /dev/null @@ -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 - - diff --git a/base/Bytes/test/from_nat.kind b/base/Bytes/test/from_nat.kind deleted file mode 100644 index 7ea08391..00000000 --- a/base/Bytes/test/from_nat.kind +++ /dev/null @@ -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 - ]) - - diff --git a/base/Bytes/test/from_string.kind b/base/Bytes/test/from_string.kind deleted file mode 100644 index b2b216cb..00000000 --- a/base/Bytes/test/from_string.kind +++ /dev/null @@ -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 - ]) - - diff --git a/base/Bytes/test/length.kind b/base/Bytes/test/length.kind deleted file mode 100644 index 34d3afdc..00000000 --- a/base/Bytes/test/length.kind +++ /dev/null @@ -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 - ]) - diff --git a/base/Bytes/test/parse_string.kind b/base/Bytes/test/parse_string.kind deleted file mode 100644 index b49d973e..00000000 --- a/base/Bytes/test/parse_string.kind +++ /dev/null @@ -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 - ]) diff --git a/base/Bytes/test/slice.kind b/base/Bytes/test/slice.kind deleted file mode 100644 index a3ac29f7..00000000 --- a/base/Bytes/test/slice.kind +++ /dev/null @@ -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 - ]) diff --git a/base/Bytes/test/to_nat.kind b/base/Bytes/test/to_nat.kind deleted file mode 100644 index 526cdbee..00000000 --- a/base/Bytes/test/to_nat.kind +++ /dev/null @@ -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 - ]) diff --git a/base/Bytes/to_nat.kind b/base/Bytes/to_nat.kind deleted file mode 100644 index a82f472e..00000000 --- a/base/Bytes/to_nat.kind +++ /dev/null @@ -1,3 +0,0 @@ -Bytes.to_nat(b: Bytes): Nat - Nat.hex.decode(String.reverse(b)) - \ No newline at end of file diff --git a/base/BytesLike.kind b/base/BytesLike.kind deleted file mode 100644 index d4a124e9..00000000 --- a/base/BytesLike.kind +++ /dev/null @@ -1,2 +0,0 @@ -BytesLike: Type - Either \ No newline at end of file diff --git a/base/String/hex.kind b/base/String/hex.kind index a605bf27..61699803 100644 --- a/base/String/hex.kind +++ b/base/String/hex.kind @@ -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 +// - \ No newline at end of file diff --git a/base/String/hexstring/arrayify.kind b/base/String/hexstring/arrayify.kind new file mode 100644 index 00000000..5297f260 --- /dev/null +++ b/base/String/hexstring/arrayify.kind @@ -0,0 +1,3 @@ +String.hexstring.arrayify(value: String): Buffer8 + let {_,buf} = Buffer8.from_hex(String.to_hex(value)) + buf \ No newline at end of file diff --git a/base/Bytes/at.kind b/base/String/hexstring/at.kind similarity index 83% rename from base/Bytes/at.kind rename to base/String/hexstring/at.kind index f6c1d626..62879e0f 100644 --- a/base/Bytes/at.kind +++ b/base/String/hexstring/at.kind @@ -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: diff --git a/base/String/hexstring/from_nat.kind b/base/String/hexstring/from_nat.kind new file mode 100644 index 00000000..048feb2a --- /dev/null +++ b/base/String/hexstring/from_nat.kind @@ -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 + \ No newline at end of file From f19e5c554612a5a435367eb06b8c0972c2827568 Mon Sep 17 00:00:00 2001 From: caotic123 Date: Thu, 14 Oct 2021 00:21:06 -0300 Subject: [PATCH 13/17] Fix proofs after rigile modifications --- base/Bits/concat.kind | 12 +- base/Bits/pad_right.kind | 2 + base/Ether/RLP/proof/encode.kind | 64 +++++--- base/Ether/tests.kind | 22 +-- base/User/caotic/debug/Bool.kind | 10 ++ base/User/caotic/debug/Empty.kind | 5 + base/User/caotic/debug/Equal.kind | 49 ++++++ base/User/caotic/debug/Nat.kind | 248 ++++++++++++++++++++++++++++++ base/User/caotic/debug/Unit.kind | 3 + 9 files changed, 382 insertions(+), 33 deletions(-) create mode 100644 base/Bits/pad_right.kind create mode 100644 base/User/caotic/debug/Bool.kind create mode 100644 base/User/caotic/debug/Empty.kind create mode 100644 base/User/caotic/debug/Equal.kind create mode 100644 base/User/caotic/debug/Nat.kind create mode 100644 base/User/caotic/debug/Unit.kind diff --git a/base/Bits/concat.kind b/base/Bits/concat.kind index cbcab1e8..17f6f6d0 100644 --- a/base/Bits/concat.kind +++ b/base/Bits/concat.kind @@ -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)) - } \ No newline at end of file + } + +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) diff --git a/base/Bits/pad_right.kind b/base/Bits/pad_right.kind new file mode 100644 index 00000000..640edd80 --- /dev/null +++ b/base/Bits/pad_right.kind @@ -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)) diff --git a/base/Ether/RLP/proof/encode.kind b/base/Ether/RLP/proof/encode.kind index 096ad35b..1d45e219 100644 --- a/base/Ether/RLP/proof/encode.kind +++ b/base/Ether/RLP/proof/encode.kind @@ -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 + 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 + 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 "" \ No newline at end of file + } default {"", Bits.e} \ No newline at end of file diff --git a/base/Ether/tests.kind b/base/Ether/tests.kind index 22b46b35..faab93a6 100644 --- a/base/Ether/tests.kind +++ b/base/Ether/tests.kind @@ -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) \ No newline at end of file diff --git a/base/User/caotic/debug/Bool.kind b/base/User/caotic/debug/Bool.kind new file mode 100644 index 00000000..a9130822 --- /dev/null +++ b/base/User/caotic/debug/Bool.kind @@ -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) diff --git a/base/User/caotic/debug/Empty.kind b/base/User/caotic/debug/Empty.kind new file mode 100644 index 00000000..373be36d --- /dev/null +++ b/base/User/caotic/debug/Empty.kind @@ -0,0 +1,5 @@ +type Empty { +} + +Empty.absurd(contra: Empty): A + case contra {} diff --git a/base/User/caotic/debug/Equal.kind b/base/User/caotic/debug/Equal.kind new file mode 100644 index 00000000..134f18e8 --- /dev/null +++ b/base/User/caotic/debug/Equal.kind @@ -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 ~ (b: A) { +// refl ~ (b = a) +//} + +Equal.rewrite(e: Equal) Type>(x: P(a)): P(b) + case e { + refl: x + }: P(e.b) + +Equal.mirror(e: Equal): Equal + case e { + refl: Equal.refl + } : Equal + +Equal.apply< + A: Type, + B: Type, + a: A, + b: A, + f: A -> B +>(e: Equal): Equal + case e { + refl: Equal.refl + }: Equal + +Empty.absurd(x: Empty): P + case x {} diff --git a/base/User/caotic/debug/Nat.kind b/base/User/caotic/debug/Nat.kind new file mode 100644 index 00000000..88e780ed --- /dev/null +++ b/base/User/caotic/debug/Nat.kind @@ -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 -> 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(Nat.lte(a, b), Bool.true) +): Equal(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(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(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(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(a, 0, Nat.Order.chain.aux(a, Hyp0)) + let qed = Equal.rewrite(0, a, a_zero, (X) Equal(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(Nat.lte(a, b), Bool.true), +// Hyp1: Equal(Nat.lte(c, d), Bool.true) +//): Equal(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 \ No newline at end of file diff --git a/base/User/caotic/debug/Unit.kind b/base/User/caotic/debug/Unit.kind new file mode 100644 index 00000000..546178a0 --- /dev/null +++ b/base/User/caotic/debug/Unit.kind @@ -0,0 +1,3 @@ +type Unit { + new +} From 50516d41de13c464bdcf662eea7d02dcc3f0b4d3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=ADgille=20S=2E=20B=2E=20Menezes?= Date: Fri, 15 Oct 2021 12:22:48 -0300 Subject: [PATCH 14/17] prove a - b + b = a when b <= a --- base/Nat/div_mod.kind | 2 +- base/Nat/div_mod/go.kind | 12 ++++++---- base/Nat/div_mod/recover.kind | 43 +++++++++++++++++++++++++++++++++++ base/Nat/sub/add.kind | 24 +++++++++++++++++++ 4 files changed, 75 insertions(+), 6 deletions(-) create mode 100644 base/Nat/div_mod/recover.kind create mode 100644 base/Nat/sub/add.kind diff --git a/base/Nat/div_mod.kind b/base/Nat/div_mod.kind index 1240cbbb..3f570b99 100644 --- a/base/Nat/div_mod.kind +++ b/base/Nat/div_mod.kind @@ -1,2 +1,2 @@ Nat.div_mod(n: Nat, m: Nat): Pair - Nat.div_mod.go(n, m, Nat.zero) + Nat.div_mod.go(m, n, 0) diff --git a/base/Nat/div_mod/go.kind b/base/Nat/div_mod/go.kind index 932e7e89..b3936d50 100644 --- a/base/Nat/div_mod/go.kind +++ b/base/Nat/div_mod/go.kind @@ -1,5 +1,7 @@ -Nat.div_mod.go(n: Nat, m: Nat, d: Nat): Pair - case Nat.sub_rem(n, m) as p { - left: Nat.div_mod.go(p.value, m, Nat.succ(d)), - right: Pair.new!!(d, n), - } \ No newline at end of file +Nat.div_mod.go(n: Nat, d: Nat, r: Nat): Pair + case Nat.lte(n, r) { + false: + Pair.new!!(d, r) + true: + Nat.div_mod.go(n, Nat.succ(d), Nat.sub(r, n)) + } diff --git a/base/Nat/div_mod/recover.kind b/base/Nat/div_mod/recover.kind new file mode 100644 index 00000000..a4eebf56 --- /dev/null +++ b/base/Nat/div_mod/recover.kind @@ -0,0 +1,43 @@ +//Nat.div_mod.recover( +// n: Nat, m: Nat +//): Equal( +// Nat.add(Nat.mod(n, m), Nat.mul(Nat.div(n, m), m)) +// m +//) +// ?recover + +//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 + Hyp: Equal(Nat.add(Nat.mul(d, n), r), m) +): def p = Nat.div_mod.go(n, d, r) + def d = Pair.fst(p) + def r = Pair.snd(p) + Equal( + Nat.add(Nat.mul(d, n), r) + m + ) + def cmp = Nat.lte(n, r) + def cmp_eq = refl :: cmp == cmp + (case cmp { + true: + (cmp_eq) + let ind = Nat.div_mod.recover.go(m, n,Nat.succ(d), Nat.sub(r,n), ?lemma) + ind + false: + (cmp_eq) + Hyp + }: (cmp_eq: Equal(Nat.lte(n, r), cmp)) -> Equal( + Nat.add(Nat.mul(Pair.fst(Nat,Nat,cmp(() Pair(Nat,Nat),Nat.div_mod.go(n,Nat.succ(d),Nat.sub(r,n)),Pair.new(Nat,Nat,d,r))),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)))) + m + ))( + cmp_eq + ) diff --git a/base/Nat/sub/add.kind b/base/Nat/sub/add.kind new file mode 100644 index 00000000..d6b96235 --- /dev/null +++ b/base/Nat/sub/add.kind @@ -0,0 +1,24 @@ +Nat.sub.add( + n: Nat + m: Nat + Hyp: Equal(Nat.lte(n, m), true) +): Equal(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.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 + }! + }! From 6953d0e360b4e32c8f9621023b30b155d5743c37 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=ADgille=20S=2E=20B=2E=20Menezes?= Date: Fri, 15 Oct 2021 13:45:19 -0300 Subject: [PATCH 15/17] proof how to recover a number after division --- base/Nat/div_mod.kind | 2 +- base/Nat/div_mod/recover.kind | 52 +++++++++++++++++++++++++---------- base/Nat/mod.kind | 2 +- 3 files changed, 40 insertions(+), 16 deletions(-) diff --git a/base/Nat/div_mod.kind b/base/Nat/div_mod.kind index 3f570b99..ee211b20 100644 --- a/base/Nat/div_mod.kind +++ b/base/Nat/div_mod.kind @@ -1,2 +1,2 @@ Nat.div_mod(n: Nat, m: Nat): Pair - Nat.div_mod.go(m, n, 0) + Nat.div_mod.go(m, 0, n) diff --git a/base/Nat/div_mod/recover.kind b/base/Nat/div_mod/recover.kind index a4eebf56..9fe44206 100644 --- a/base/Nat/div_mod/recover.kind +++ b/base/Nat/div_mod/recover.kind @@ -1,10 +1,13 @@ -//Nat.div_mod.recover( -// n: Nat, m: Nat -//): Equal( -// Nat.add(Nat.mod(n, m), Nat.mul(Nat.div(n, m), m)) -// m -//) -// ?recover +Nat.div_mod.recover( + n: Nat, m: Nat +): Equal( + 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, refl) + let comm = Nat.add.comm(Nat.mul(Nat.div(n, m), m), Nat.mod(n, m)) + let qed = lemma :: rewrite X in Equal(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) @@ -30,14 +33,35 @@ Nat.div_mod.recover.go( (case cmp { true: (cmp_eq) - let ind = Nat.div_mod.recover.go(m, n,Nat.succ(d), Nat.sub(r,n), ?lemma) + let comm = Nat.add.comm(Nat.mul(d,n), r) + let lemma = Hyp :: rewrite X in Equal(X, m) with comm + let sub = mirror(Nat.sub.add!!(cmp_eq)) + let lemma = lemma :: rewrite X in Equal(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), lemma) ind false: (cmp_eq) Hyp - }: (cmp_eq: Equal(Nat.lte(n, r), cmp)) -> Equal( - Nat.add(Nat.mul(Pair.fst(Nat,Nat,cmp(() Pair(Nat,Nat),Nat.div_mod.go(n,Nat.succ(d),Nat.sub(r,n)),Pair.new(Nat,Nat,d,r))),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)))) - m - ))( - cmp_eq - ) + }: (cmp_eq: Equal(Nat.lte(n, r), cmp)) -> + Equal( + 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(p) + n + ) + Pair.snd(p) + ) + m + ))( + cmp_eq + ) diff --git a/base/Nat/mod.kind b/base/Nat/mod.kind index ec52bce4..5ad6f435 100644 --- a/base/Nat/mod.kind +++ b/base/Nat/mod.kind @@ -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) \ No newline at end of file + Pair.snd!!(Nat.div_mod(n, m)) From 41a0703a140b40da71bace67c715160e1dac135e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=ADgille=20S=2E=20B=2E=20Menezes?= Date: Fri, 15 Oct 2021 14:06:10 -0300 Subject: [PATCH 16/17] guarantee proof terminates --- base/Nat/div_mod/recover.kind | 38 +++++++++++++++++------------------ base/Nat/mod/small.kind | 5 +++++ 2 files changed, 23 insertions(+), 20 deletions(-) create mode 100644 base/Nat/mod/small.kind diff --git a/base/Nat/div_mod/recover.kind b/base/Nat/div_mod/recover.kind index 9fe44206..d6fd3776 100644 --- a/base/Nat/div_mod/recover.kind +++ b/base/Nat/div_mod/recover.kind @@ -1,10 +1,12 @@ +// (n % m) + (n / m) * m = n Nat.div_mod.recover( n: Nat, m: Nat + Hyp: Equal(Nat.lte(1, m), true) ): Equal( 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, refl) + 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(X, n) with comm qed @@ -20,7 +22,8 @@ Nat.div_mod.recover.go( n: Nat d: Nat r: Nat - Hyp: Equal(Nat.add(Nat.mul(d, n), r), m) + Hyp0: Equal(Nat.lte(1, n), true) + Hyp1: Equal(Nat.add(Nat.mul(d, n), r), m) ): def p = Nat.div_mod.go(n, d, r) def d = Pair.fst(p) def r = Pair.snd(p) @@ -30,24 +33,21 @@ Nat.div_mod.recover.go( ) def cmp = Nat.lte(n, r) def cmp_eq = refl :: cmp == cmp - (case cmp { + case cmp with cmp_eq : cmp^ == cmp { true: - (cmp_eq) - let comm = Nat.add.comm(Nat.mul(d,n), r) - let lemma = Hyp :: rewrite X in Equal(X, m) with comm - let sub = mirror(Nat.sub.add!!(cmp_eq)) - let lemma = lemma :: rewrite X in Equal(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), lemma) - ind + let comm = Nat.add.comm(Nat.mul(d,n), r) + let lemma = Hyp1 :: rewrite X in Equal(X, m) with comm + let sub = mirror(Nat.sub.add!!(cmp_eq)) + let lemma = lemma :: rewrite X in Equal(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: - (cmp_eq) - Hyp - }: (cmp_eq: Equal(Nat.lte(n, r), cmp)) -> - Equal( + Hyp1 + }! :: Equal( def p = cmp( () Pair(Nat,Nat) @@ -62,6 +62,4 @@ Nat.div_mod.recover.go( Pair.snd(p) ) m - ))( - cmp_eq ) diff --git a/base/Nat/mod/small.kind b/base/Nat/mod/small.kind new file mode 100644 index 00000000..762761c5 --- /dev/null +++ b/base/Nat/mod/small.kind @@ -0,0 +1,5 @@ +Nat.mod.small( + n: Nat + m: Nat +): ?mod.small.type + ?mod.small.body From fe95f53a7d00879092d5bceb882d4614d104bdad Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=ADgille=20S=2E=20B=2E=20Menezes?= Date: Fri, 15 Oct 2021 14:32:13 -0300 Subject: [PATCH 17/17] proove Nat.mod is small --- base/Nat/mod/small.kind | 38 ++++++++++++++++++++++++++++++++++---- 1 file changed, 34 insertions(+), 4 deletions(-) diff --git a/base/Nat/mod/small.kind b/base/Nat/mod/small.kind index 762761c5..3c640248 100644 --- a/base/Nat/mod/small.kind +++ b/base/Nat/mod/small.kind @@ -1,5 +1,35 @@ -Nat.mod.small( +//Nat.mod.small( +// n: Nat +// m: Nat +// Hyp: Equal(Nat.lte(1, m), true) +//): Equal(Nat.lte(m, Nat.mod(n, m)), false) +// ?mod.small.body + +Nat.mod.small.aux( n: Nat - m: Nat -): ?mod.small.type - ?mod.small.body + d: Nat + r: Nat + Hyp: Equal(Nat.lte(1, n), true) +): Equal(Nat.lte(n, Pair.snd(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( + 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 + )