Kindelia/Kind2
1
1
Fork 0
mirror of https://github.com/Kindelia/Kind2.git synced 2024-11-05 07:05:32 +03:00
Code Issues Projects Releases Wiki Activity

start proof about conversion from Nat to word

Browse Source
This commit is contained in:
Rígille S. B. Menezes 2021-11-21 12:38:28 -03:00
parent 2dd72e2424
commit 1ff9f8210b
15 changed files with 190 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
base/Bool/xor.kind Normal file
View File

@ -0,0 +1,7 @@
Bool.xor(a: Bool, b: Bool): Bool
case a {
true:
Bool.not(b)
false:
b
}

2
base/Nat/lte/succ_right.kind
View File

@ -5,4 +5,4 @@ Nat.lte.succ_right(x : Nat, y : Nat, H : Nat.lte(x, y) == true) : Nat.lte(x, Nat
succ : Nat.lte.succ_right(x.pred, y.pred, H)
zero : Empty.absurd!(Bool.false_neq_true(H))
}!
}!
}!

6
base/Nat/mod/idempotent.kind Normal file
View File

@ -0,0 +1,6 @@
Nat.mod.idempotent(x: Nat, y: Nat, H: Nat.lte(y, x) == false): x == Nat.mod(x, y)
let H = mirror(H)
case H {
refl:
refl
}: Equal(Nat, x, Pair.snd(Nat,Nat,H.b((self) Pair(Nat,Nat),Nat.div_mod.go(y,1,Nat.sub(x,y)),Pair.new(Nat,Nat,0,x))))

6
base/Nat/mod/le_mod.kind
View File

@ -1,5 +1,7 @@
Nat.mod.le_mod(x : Nat, y : Nat, H : Nat.lte(Nat.succ(x), y) == true) : Nat.mod(x, y) == x
let simpl = refl :: Pair.snd(Nat,Nat,Nat.lte(y,x,(self) Pair(Nat,Nat),Nat.div_mod.go(y,1,Nat.sub(x,y)),Pair.new(Nat,Nat,0,x))) == Nat.mod(x, y)
Nat.mod.le_mod(
x: Nat, y: Nat, H: Nat.lte(Nat.succ(x), y) == true
): 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 {
refl :

5
base/Nat/mod/mod_one_equals_zero.kind
View File

@ -1,5 +0,0 @@
Nat.mod.mod_one_equals_zero(a: Nat): (a % 1) == 0
case a{
zero: refl
succ: Nat.mod.go_mod_one_equals_zero(a.pred)
}!

3
base/Nat/mod/one.kind Normal file
View File

@ -0,0 +1,3 @@
Nat.mod.one(n: Nat): Equal(Nat, Nat.mod(n, 1), 0)
let lemma = Nat.lte.comm.false(1, Nat.mod(n, 1), Nat.mod.small(n, 1, refl))
Nat.lte.zero_right(Nat.mod(n, 1), lemma)

2
base/Nat/mod/small.kind
View File

@ -3,7 +3,7 @@ Nat.mod.small(
m: Nat
Hyp: Equal<Bool>(Nat.lte(1, m), true)
): Equal<Bool>(Nat.lte(m, Nat.mod(n, m)), false)
Nat.mod.small.aux(m,0, n, Hyp)
Nat.mod.small.aux(m, 0, n, Hyp)
Nat.mod.small.aux(
n: Nat

1
base/Nat/mod/succ_left.kind Normal file
View File

@ -0,0 +1 @@
Nat.mod.succ_left(n: Nat, m: Nat)

2
base/Nat/mod/zero_left.kind Normal file
View File

@ -0,0 +1,2 @@
Nat.mod.zero_left(a: Nat): (0 % Nat.succ(a)) == 0
refl

2
base/Nat/mod/zero_mod_equals_zero.kind
View File

@ -1,2 +0,0 @@
Nat.mod.zero_mod_equals_zero(a: Nat): (0 % Nat.succ(a)) == 0
refl

26
base/Nat/pow/lte.kind Normal file
View File

@ -0,0 +1,26 @@
Nat.pow.lte(a: Nat, b: Nat): Equal(Bool, Nat.lte(Nat.pow(Nat.succ(a), b), 0), false)
case b {
zero:
refl
succ:
let remember = Equal.refl(Bool, Nat.lte(Nat.pow(Nat.succ(a), Nat.succ(b.pred)), 0))
def cond = Nat.lte(Nat.pow(Nat.succ(a), Nat.succ(b.pred)), 0)
case cond with remember: cond^ == cond {
true:
let either_zero = Nat.mul.equal_zero(
Nat.succ(a), Nat.pow(Nat.succ(a), b.pred)
Nat.lte.zero_right(Nat.pow(Nat.succ(a), Nat.succ(b.pred)) remember)
)
case either_zero {
left:
apply((n) Bool.not(Nat.is_zero(n)), either_zero.value)
right:
case either_zero.value {
refl:
Nat.pow.lte(a, b.pred)
}: Nat.lte(either_zero.value.b, 0) == false
}
false:
refl
}!
}!

7
base/Nat/to_word.kind
View File

@ -1,2 +1,7 @@
Nat.to_word(size: Nat, n: Nat): Word(size)
Nat.apply!(n, Word.inc!, Word.zero!)
case n {
zero:
Word.zero(size)
succ:
Word.inc(size, Nat.to_word(size, n.pred))
}!

9
base/Word/to_nat.kind
View File

@ -1,2 +1,9 @@
Word.to_nat<size: Nat>(word: Word(size)): Nat
Word.fold<(x) Nat, size>(0, <_> Nat.mul(2), <_> (x) Nat.succ(Nat.mul(2, x)), word)
case word {
e:
0
i:
Nat.succ(Nat.mul(2, Word.to_nat(word.size, word.pred)))
o:
Nat.mul(2, Word.to_nat(word.size, word.pred))
}

121
base/Word/to_nat/from_nat.kind Normal file
View File

@ -0,0 +1,121 @@
Word.size.zero(w: Word(0)): w((w, w.size) Type, Unit, (size, pred) Empty, (size, pred) Empty)
let contra = refl :: 0 == 0
(case w {
e:
(contra)
unit
o:
(contra)
Empty.absurd!(Nat.succ_neq_zero(w.size, contra))
i:
(contra)
Empty.absurd!(Nat.succ_neq_zero(w.size, contra))
}: (h: w.size == 0) -> w((k, k.size) Type, Unit, (size, pred) Empty, (size, pred) Empty))(contra)
Word.size.succ(n: Nat, w: Word(Nat.succ(n))): w((w, w.size) Type, Empty, (size, pred) Unit, (size, pred) Unit)
let contra = refl :: Nat.succ(n) == Nat.succ(n)
(case w {
e:
(contra)
Empty.absurd!(Nat.succ_neq_zero(n, contra))
o:
(contra)
unit
i:
(contra)
unit
}: (h: Nat.succ(n) == w.size) -> w((k, k.size) Type, Empty, (size, pred) Unit, (size, pred) Unit))(contra)
Word.to_nat.from_nat<size: Nat>(
n: Nat
): Word.to_nat(size, Nat.to_word(size, n)) == Nat.mod(n, Nat.pow(2, size))
case size {
zero:
let case_elim = Word.size.zero(Nat.to_word(0, n))
let qed =
case Nat.to_word(0, n) {
e:
(case_elim)
case refl :: 1 == Nat.pow(2, 0) {
refl:
case Nat.mod.one(n) {
refl:
refl
}: Equal(Nat, self.b, Nat.mod(n, 1))
}: Equal(Nat, 0, Nat.mod(n, self.b))
i:
(case_elim)
Empty.absurd!(case_elim)
o:
(case_elim)
Empty.absurd!(case_elim)
}: (case_elim: self((w, w.size) Type, Unit, (size, pred) Empty, (size, pred) Empty)) -> (Word.to_nat(self.size, self) == Nat.mod(n, Nat.pow(2, 0)))
qed(case_elim)
succ:
case n {
zero:
let lemma_right =
let contra = Nat.pow.lte(1, Nat.succ(size.pred))
(case Nat.pow(2,Nat.succ(size.pred)) {
zero:
(contra)
Empty.absurd!(Bool.true_neq_false(contra))
succ:
(contra)
refl
}: (contra: Nat.lte(self,0) == Bool.false) -> (0 == Nat.mod(0,self)))(contra)
let lemma_left = mirror(Word.to_nat.zero(Nat.succ(size.pred)))
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)))
}!
}!
// 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)
Word.to_nat.zero(size: Nat): 0 == Word.to_nat(size, Word.zero(size))
case size {
zero:
refl
succ:
case Word.to_nat.zero(size.pred) {
refl:
refl
}: 0 == Nat.mul(2, self.b)
}!

4
base/Word/to_nat/safe.kind Normal file
View File

@ -0,0 +1,4 @@
Word.to_nat.safe<size: Nat>(
n: Nat, H: Nat.lte(Nat.succ(n), Nat.pow(2, size)) == true
): Word.to_nat(Nat.to_word(size, n)) == n
?word.to_nat.safe