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

Bits.to_nat identity proof

Browse Source
This commit is contained in:
MaiaVictor 2021-11-09 01:24:50 -03:00
parent 5cdf4a052e
commit 5fef08ca79
6 changed files with 45 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
base/Bits/to_nat.kind
View File

@ -1,6 +1,6 @@
Bits.to_nat(b: Bits): Nat
case b {
e: 0,
o: Nat.mul(2, Bits.to_nat(b.pred)),
i: Nat.succ(Nat.mul(2, Bits.to_nat(b.pred)))
}
e: Nat.zero
o: Nat.double(Bits.to_nat(b.pred))
i: Nat.succ(Nat.double(Bits.to_nat(b.pred)))
}

22
base/Bits/to_nat/identity.kind Normal file
View File

@ -0,0 +1,22 @@
Bits.to_nat.identity.aux0(x: Bits): Bits.to_nat(Bits.inc(x)) == Nat.succ(Bits.to_nat(x))
case x {
e: refl
o: refl
i: apply(Nat.double, Bits.to_nat.identity.aux0(x.pred))
}!
Bits.to_nat.identity.aux1(x: Nat): Nat.to_bits(Nat.succ(x)) == Bits.inc(Nat.to_bits(x))
case x {
zero: refl
succ: apply(Bits.inc, Bits.to_nat.identity.aux1(x.pred))
}!
Bits.to_nat.identity(n: Nat): Equal<Nat, n, Bits.to_nat(Nat.to_bits(n))>
case n {
zero:
refl
succ:
rewrite X in Nat.succ(n.pred) == Bits.to_nat(X) with Bits.to_nat.identity.aux1(n.pred)
rewrite X in Nat.succ(n.pred) == X with Bits.to_nat.identity.aux0(Nat.to_bits(n.pred))
apply(Nat.succ, Bits.to_nat.identity(n.pred))
}!

18
bin/js/package-lock.json generated
View File

@ -1,24 +1,24 @@
{
"name": "kind-lang",
"version": "1.0.108",
"version": "1.0.109",
"lockfileVersion": 2,
"requires": true,
"packages": {
"": {
"name": "kind-lang",
"version": "1.0.108",
"version": "1.0.109",
"license": "MIT",
"dependencies": {
"formcore-js": "^0.1.93"
"formcore-js": "^0.1.94"
},
"bin": {
"kind": "src/main.js"
}
},
"node_modules/formcore-js": {
"version": "0.1.93",
"resolved": "https://registry.npmjs.org/formcore-js/-/formcore-js-0.1.93.tgz",
"integrity": "sha512-Rkt2eBR/qaDguj01lW8P8jKFExl0+uxJV402Di9rSOnD2YhT64Pd8qFqGx7CqzR83iAnFhQseAgrLkS1Fz85bQ==",
"version": "0.1.94",
"resolved": "https://registry.npmjs.org/formcore-js/-/formcore-js-0.1.94.tgz",
"integrity": "sha512-lZP1eGDTlxk4ku8IcbwLIlZkYhgA5FB1Ypt52ciTuYbOU03sqQSDT+VE5betCJ6xQ3746EOUiVmNQX1SxQEhkg==",
"bin": {
"fmc": "main.js"
}
@ -26,9 +26,9 @@
},
"dependencies": {
"formcore-js": {
"version": "0.1.93",
"resolved": "https://registry.npmjs.org/formcore-js/-/formcore-js-0.1.93.tgz",
"integrity": "sha512-Rkt2eBR/qaDguj01lW8P8jKFExl0+uxJV402Di9rSOnD2YhT64Pd8qFqGx7CqzR83iAnFhQseAgrLkS1Fz85bQ=="
"version": "0.1.94",
"resolved": "https://registry.npmjs.org/formcore-js/-/formcore-js-0.1.94.tgz",
"integrity": "sha512-lZP1eGDTlxk4ku8IcbwLIlZkYhgA5FB1Ypt52ciTuYbOU03sqQSDT+VE5betCJ6xQ3746EOUiVmNQX1SxQEhkg=="
}
}
}

4
bin/js/package.json
View File

@ -1,6 +1,6 @@
{
"name": "kind-lang",
"version": "1.0.109",
"version": "1.0.110",
"description": "Kind-Lang in JavaScript",
"main": "src/kind.js",
"scripts": {
@ -20,6 +20,6 @@
},
"homepage": "https://github.com/uwu-tech/kind#readme",
"dependencies": {
"formcore-js": "^0.1.93"
"formcore-js": "^0.1.94"
}
}

14
bin/package-lock.json generated
View File

@ -9,13 +9,13 @@
"version": "0.1.0",
"license": "MIT",
"dependencies": {
"formcore-js": "^0.1.93"
"formcore-js": "^0.1.94"
}
},
"node_modules/formcore-js": {
"version": "0.1.93",
"resolved": "https://registry.npmjs.org/formcore-js/-/formcore-js-0.1.93.tgz",
"integrity": "sha512-Rkt2eBR/qaDguj01lW8P8jKFExl0+uxJV402Di9rSOnD2YhT64Pd8qFqGx7CqzR83iAnFhQseAgrLkS1Fz85bQ==",
"version": "0.1.94",
"resolved": "https://registry.npmjs.org/formcore-js/-/formcore-js-0.1.94.tgz",
"integrity": "sha512-lZP1eGDTlxk4ku8IcbwLIlZkYhgA5FB1Ypt52ciTuYbOU03sqQSDT+VE5betCJ6xQ3746EOUiVmNQX1SxQEhkg==",
"bin": {
"fmc": "main.js"
}
@ -23,9 +23,9 @@
},
"dependencies": {
"formcore-js": {
"version": "0.1.93",
"resolved": "https://registry.npmjs.org/formcore-js/-/formcore-js-0.1.93.tgz",
"integrity": "sha512-Rkt2eBR/qaDguj01lW8P8jKFExl0+uxJV402Di9rSOnD2YhT64Pd8qFqGx7CqzR83iAnFhQseAgrLkS1Fz85bQ=="
"version": "0.1.94",
"resolved": "https://registry.npmjs.org/formcore-js/-/formcore-js-0.1.94.tgz",
"integrity": "sha512-lZP1eGDTlxk4ku8IcbwLIlZkYhgA5FB1Ypt52ciTuYbOU03sqQSDT+VE5betCJ6xQ3746EOUiVmNQX1SxQEhkg=="
}
}
}

2
bin/package.json
View File

@ -9,6 +9,6 @@
"author": "",
"license": "MIT",
"dependencies": {
"formcore-js": "^0.1.93"
"formcore-js": "^0.1.94"
}
}