From 266302def95c97828f107a00d8d12333ed14fcdf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=ADgille=20S=2E=20B=2E=20Menezes?= Date: Tue, 30 Nov 2021 10:55:45 -0300 Subject: [PATCH] commit yesterday's unfinished work --- base/Nat/div_mod/spec.kind | 9 +++++++ base/Nat/ltn/mul.kind | 3 +++ base/Nat/mod/le_mod.kind | 2 +- base/Nat/mod/mul_both.kind | 9 +++++++ base/Word/to_nat/from_nat.kind | 45 ++++++---------------------------- base/Word/to_nat/inc.kind | 32 +++++++++++++++++++++--- 6 files changed, 57 insertions(+), 43 deletions(-) create mode 100644 base/Nat/div_mod/spec.kind create mode 100644 base/Nat/ltn/mul.kind create mode 100644 base/Nat/mod/mul_both.kind diff --git a/base/Nat/div_mod/spec.kind b/base/Nat/div_mod/spec.kind new file mode 100644 index 00000000..932a6d20 --- /dev/null +++ b/base/Nat/div_mod/spec.kind @@ -0,0 +1,9 @@ +Nat.div_mod.spec( + n: Nat + q: Nat + d: Nat + r: Nat + H0: Equal(Nat, n, Nat.add(r, Nat.mul(q, d))) + H1: Equal(Bool, Nat.lte(Nat.succ(r), d), true) +): Equal(Pair, Pair.new(Nat, Nat, q, r), Nat.div_mod(n, d)) + ?test diff --git a/base/Nat/ltn/mul.kind b/base/Nat/ltn/mul.kind new file mode 100644 index 00000000..a4a292d3 --- /dev/null +++ b/base/Nat/ltn/mul.kind @@ -0,0 +1,3 @@ +// TODO +Nat.ltn.mul( +) diff --git a/base/Nat/mod/le_mod.kind b/base/Nat/mod/le_mod.kind index baf91c2b..eb1bce90 100644 --- a/base/Nat/mod/le_mod.kind +++ b/base/Nat/mod/le_mod.kind @@ -1,6 +1,6 @@ Nat.mod.le_mod( x: Nat, y: Nat, H: Nat.lte(Nat.succ(x), y) == true -): Nat.mod(x, y) == x +): Equal(Nat, Nat.mod(x, y), x) let simpl = refl :: Pair.snd(Nat,Nat,Nat.lte(y,x,() Pair(Nat,Nat),Nat.div_mod.go(y,1,Nat.sub(x,y)),Pair.new(Nat,Nat,0,x))) == Nat.mod(x, y) let H2 = Nat.Order.trichotomy(y, x) case simpl { diff --git a/base/Nat/mod/mul_both.kind b/base/Nat/mod/mul_both.kind new file mode 100644 index 00000000..8ca5fb30 --- /dev/null +++ b/base/Nat/mod/mul_both.kind @@ -0,0 +1,9 @@ +Nat.mod.mul_both( + a: Nat + b: Nat + c: Nat + H0: Equal(Bool, Nat.lte(1, a), true) + H1: Equal(Bool, Nat.lte(1, c), true) +): Equal(Nat, Nat.mul(a, Nat.mod(b, c)), Nat.mod(Nat.mul(a, b), Nat.mul(a, c))) + let bound_lemma = Nat.lte.comm.false(c, Nat.mod(b, c), Nat.mod.small(b, c, H1)) + ?mul_both diff --git a/base/Word/to_nat/from_nat.kind b/base/Word/to_nat/from_nat.kind index 38fa7db2..7e73d829 100644 --- a/base/Word/to_nat/from_nat.kind +++ b/base/Word/to_nat/from_nat.kind @@ -68,46 +68,15 @@ Word.to_nat.from_nat( chain(lemma_left, lemma_right) succ: let lemma = refl :: Word.inc(Nat.succ(size.pred),Nat.to_word(Nat.succ(size.pred),n.pred)) == Nat.to_word(Nat.succ(size.pred),Nat.succ(n.pred)) - case lemma { - refl: - let ind = mirror(Word.to_nat.from_nat(Nat.succ(size.pred), n.pred)) - (case Nat.to_word(Nat.succ(size.pred),n.pred) { - e: - (ind) - case (refl :: 1 == Nat.pow(2, 0)) { - refl: - mirror(Nat.mod.one(Nat.succ(n.pred))) - }: 0 == Nat.mod(Nat.succ(n.pred), self.b) - o: - (ind) - case ind { - refl: - let right_small = ?todo :: Nat.lte(Nat.succ(Nat.succ(n.pred)), Nat.pow(2,Nat.succ(self.size))) == true - let right_ok = mirror(Nat.mod.le_mod(Nat.succ(n.pred),Nat.pow(2,Nat.succ(self.size)), right_small)) - let left_small = Nat.lte.succ_left(Nat.succ(n.pred), Nat.pow(2,Nat.succ(self.size)), right_small) - let left_ok = mirror(Nat.mod.le_mod(n.pred,Nat.pow(2,Nat.succ(self.size)), left_small)) - case right_ok { - refl: - case left_ok { - refl: - ?refl - }: Nat.succ(left_ok.b) == Nat.succ(n.pred) - }: Nat.succ(Nat.mod(n.pred,Nat.pow(2,Nat.succ(size.pred)))) == right_ok.b - }: Nat.succ(ind.b) == Nat.mod(Nat.succ(n.pred),Nat.pow(2,Nat.succ(self.size))) - //?oooo-38-18 - i: - (ind) - ?iiii - }: (ind: Nat.mod(n.pred,Nat.pow(2,Nat.succ(size.pred))) == Word.to_nat(self.size,self)) -> Word.to_nat(self.size, Word.inc(self.size, self)) == Nat.mod(Nat.succ(n.pred),Nat.pow(2,self.size)))(ind) - // Nat.succ(Nat.mul(2,Word.to_nat(self.size,self.pred))) == Nat.mod(Nat.succ(n.pred),Nat.pow(2,Nat.succ(self.size))) - // Nat.mod(n.pred,Nat.pow(2,self.size)) == Word.to_nat(self.size,Nat.to_word(self.size,n.pred)) - // Word.to_nat(Nat.succ(size.pred), Word.inc(size.pred, Nat.to_word(Nat.succ(size.pred),n.pred))) == Nat.mod(Nat.succ(n.pred),Nat.pow(2,self.size)) - }: Word.to_nat(Nat.succ(size.pred), lemma.b) == Nat.mod(Nat.succ(n.pred),Nat.pow(2,Nat.succ(size.pred))) + ?succ }! }! -// to_nat(to_word(succ(size.pred), succ(n.pred))) == succ(n.pred) % 2^succ(size.pred) -// to_nat(inc(to_word(succ(size.pred), n.pred))) == succ(n.pred) % 2^succ(size.pred) -// - to_nat(2*self) == succ(self.size) % 2^succ(self.size) +// to_nat(_, to_word(_, succ(n.pred))) == mod(succ(n.pred), 2^succ(size.pred)) +// to_nat(_, inc(to_word(_, n.pred))) == mod(succ(n.pred), 2^succ(size.pred)) +// * to_nat(_, inc(to_word(_, n.pred))) == mod(succ(n.pred), 2^succ(size.pred)) +// ind: +// to_nat(_, to_word(_, n.pred)) == mod(n.pred, 2^succ(size.pred)) + Word.to_nat.zero(size: Nat): 0 == Word.to_nat(size, Word.zero(size)) case size { diff --git a/base/Word/to_nat/inc.kind b/base/Word/to_nat/inc.kind index b92d7230..b8ebcf77 100644 --- a/base/Word/to_nat/inc.kind +++ b/base/Word/to_nat/inc.kind @@ -1,12 +1,36 @@ Word.to_nat.inc< size: Nat >(w: Word(size) -): Word.to_nat(size, Word.inc(size, w)) == Nat.mod(Nat.succ(Word.to_nat(size, w)), Nat.pow(2, size)) +): Nat.mod(Nat.succ(Word.to_nat(size, w)), Nat.pow(2, size)) == Word.to_nat(size, Word.inc(size, w)) case w { e: refl o: - ?o-38-18-77 + let calc = refl :: Equal(Nat, Nat.mul(2,Word.to_nat(w.size,w.pred)), Word.to_nat(Nat.succ(w.size),Word.o(w.size,w.pred))) + case calc { + refl: + let pre_bound = Word.to_nat.bound(w.size,w.pred) + let bound = case Nat.mul.distrib_left(2, 1, Word.to_nat(w.size,w.pred)) { + refl: + Nat.Order.mul.left(Nat.succ(Word.to_nat(w.size,w.pred)), Nat.pow(2,w.size), 2, pre_bound) + }: Equal(Bool, Nat.lte(self.b, Nat.mul(2, Nat.pow(2, w.size))), true) + let qed = Nat.mod.le_mod(Nat.succ(Nat.mul(2,Word.to_nat(w.size,w.pred))),Nat.pow(2,Nat.succ(w.size)), bound) + qed + }: Equal(Nat, Nat.mod(Nat.succ(calc.b),Nat.pow(2,Nat.succ(w.size))), Nat.succ(Nat.mul(2,Word.to_nat(w.size,w.pred)))) i: - ?i - }: Equal(Nat, Word.to_nat(w.size,Word.inc(w.size,w)), Nat.mod(Nat.succ(Word.to_nat(w.size,w)),Nat.pow(2,w.size))) + let calc = refl :: Equal(Nat, Nat.succ(Nat.mul(2,Word.to_nat(w.size,w.pred))), Word.to_nat(Nat.succ(w.size),Word.i(w.size,w.pred))) + case calc { + refl: + let ind = Word.to_nat.inc(w.size, w.pred) + case ind { + refl: +// mul(c,mod(n,m)) == mod(mul(c, n), mul(c, m)) + +// mul(2,mod(succ(n),pow(2,size))) == mul(2,mod(succ(n),pow(2,size))) +// mod(mul(2,mod(succ(n),pow(2,size))),pow(2,succ(size))) == mul(2,mod(succ(n),pow(2,size))) +// mod(mul(2,mod(succ(n),pow(2,size))),pow(2,succ(size))) == mul(2,mod(succ(n),pow(2,size))) +// mod(succ(succ(mul(2,n))),pow(2,succ(size))) == mul(2, mod(succ(n),pow(2,size))) + ?refl + }: Nat.mod(Nat.succ(Nat.succ(Nat.mul(2,Word.to_nat(w.size,w.pred)))),Nat.pow(2,Nat.succ(w.size))) == Nat.mul(2,ind.b) + }: Equal(Nat, Nat.mod(Nat.succ(calc.b),Nat.pow(2,Nat.succ(w.size))), Nat.mul(2,Word.to_nat(w.size,Word.inc(w.size,w.pred)))) + }: Equal(Nat, Nat.mod(Nat.succ(Word.to_nat(w.size,w)),Nat.pow(2,w.size)), Word.to_nat(w.size,Word.inc(w.size,w)))