HigherOrderCO/Kind1
1
1
Fork 0
mirror of https://github.com/HigherOrderCO/Kind1.git synced 2024-10-26 12:27:36 +03:00
Code Issues Packages Projects Releases Wiki Activity

bound result of Word.to_nat

Browse Source
This commit is contained in:
Rígille S. B. Menezes 2021-11-29 13:25:36 -03:00
parent 92b812d14c
commit 8dfd06447a
3 changed files with 42 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
base/Word/inc.kind
View File

@ -1,6 +1,9 @@
Word.inc<size: Nat>(word: Word(size)): Word(size)
case word {
e: Word.e,
o: Word.i<word.size>(word.pred),
i: Word.o<word.size>(Word.inc<word.size>(word.pred))
} : Word(word.size)
e:
Word.e,
o:
Word.i<word.size>(word.pred),
i:
Word.o<word.size>(Word.inc<word.size>(word.pred))
}: Word(word.size)

23
base/Word/to_nat/bound.kind Normal file
View File

@ -0,0 +1,23 @@
Word.to_nat.bound<
size: Nat
>(w: Word(size)
): Equal(Bool, Nat.lte(Nat.succ(Word.to_nat(size, w)), Nat.pow(2, size)), true)
case w {
e:
refl
o:
let ind = Word.to_nat.bound(w.size, w.pred)
let lemma = 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, ind)
}: Equal(Bool, Nat.lte(self.b, Nat.mul(2, Nat.pow(2, w.size))), true)
let qed = Nat.lte.succ_left(Nat.succ(Nat.mul(2, Word.to_nat(w.size,w.pred))), Nat.mul(2, Nat.pow(2,w.size)), lemma)
qed
i:
let ind = Word.to_nat.bound(w.size, w.pred)
let qed = 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, ind)
}: Equal(Bool, Nat.lte(self.b, Nat.mul(2, Nat.pow(2, w.size))), true)
qed
}: Equal(Bool, Nat.lte(Nat.succ(Word.to_nat(w.size, w)), Nat.pow(2, w.size)), true)

12
base/Word/to_nat/inc.kind Normal file
View File

@ -0,0 +1,12 @@
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))
case w {
e:
refl
o:
?o-38-18-77
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)))