mirror of
https://github.com/HigherOrderCO/Kind1.git
synced 2024-10-26 12:27:36 +03:00
commit yesterday's unfinished work
This commit is contained in:
parent
8dfd06447a
commit
266302def9
9
base/Nat/div_mod/spec.kind
Normal file
9
base/Nat/div_mod/spec.kind
Normal file
@ -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<Nat, Nat>, Pair.new(Nat, Nat, q, r), Nat.div_mod(n, d))
|
||||
?test
|
3
base/Nat/ltn/mul.kind
Normal file
3
base/Nat/ltn/mul.kind
Normal file
@ -0,0 +1,3 @@
|
||||
// TODO
|
||||
Nat.ltn.mul(
|
||||
)
|
@ -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 {
|
||||
|
9
base/Nat/mod/mul_both.kind
Normal file
9
base/Nat/mod/mul_both.kind
Normal file
@ -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
|
@ -68,46 +68,15 @@ Word.to_nat.from_nat<size: 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 {
|
||||
|
@ -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)))
|
||||
|
Loading…
Reference in New Issue
Block a user