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

Add identitity proofs on bits cmp relation

Browse Source
This commit is contained in:
caotic123 2021-11-09 19:18:15 -03:00
parent 707041a334
commit c51fdc2d54
3 changed files with 62 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

31
base/Bits/cmp/identity_by_o.kind Normal file
View File

@ -0,0 +1,31 @@
Bits.cmp.identity_by_o.aux.left(y : Bits) : Bits.cmp.go(Bits.e,y,Cmp.ltn) == Cmp.ltn
case y {
e : refl
o : Bits.cmp.identity_by_o.aux.left(y.pred)
i : refl
}!
Bits.cmp.identity(x : Bits, y : Bits, j : Cmp, j2 : Cmp, H : Bits.cmp.go(x, y, j) == j2)
: Bits.cmp.go(Bits.trim.insert(x), y, j) == j2
case x with H {
o :
case y with H {
i : Bits.cmp.identity(x.pred, y.pred, Cmp.ltn, j2, H)
o : Bits.cmp.identity(x.pred, y.pred, j, j2, H)
e : Bits.cmp.identity(x.pred, Bits.e, j, j2, H)
}!
i : case y with H {
i : Bits.cmp.identity(x.pred, y.pred, j, j2, H)
o : Bits.cmp.identity(x.pred, y.pred, Cmp.gtn, j2, H)
e : H
}!
e : case y with H {
i :
let H = H :: Cmp.ltn == j2
case H {
refl : Bits.cmp.identity_by_o.aux.left(y.pred)
}!
o : H
e : H
}!
}!

9
base/Bits/trim.kind
View File

@ -6,4 +6,11 @@ Bits.trim(new_len: Nat, bits: Bits): Bits
o: Bits.o(Bits.trim(new_len.pred, bits.pred)),
i: Bits.i(Bits.trim(new_len.pred, bits.pred)),
}
}
}
Bits.trim.insert(bits: Bits): Bits
case bits {
e : Bits.o(Bits.e)
o : Bits.o(Bits.trim.insert(bits.pred))
i : Bits.i(Bits.trim.insert(bits.pred))
}

23
base/Bits/trim/identity.kind Normal file
View File

@ -0,0 +1,23 @@
Bits.trim.identity(bits : Bits) : Bits.trim(Bits.length(bits), bits) == bits
case bits {
e : refl
o :
let rec = Bits.trim.identity(bits.pred)
case refl :: Bits.length.go(bits.pred,1) == Bits.length(Bits.o(bits.pred)) {
refl :
let H = Bits.length.succ(bits.pred, 0)
case H {
refl : Equal.apply!!!!(Bits.o, rec)
}!
}!
i :
let rec = Bits.trim.identity(bits.pred)
case refl :: Bits.length.go(bits.pred,1) == Bits.length(Bits.i(bits.pred)) {
refl :
let H = Bits.length.succ(bits.pred, 0)
case H {
refl : Equal.apply!!!!(Bits.i, rec)
}!
}!
}!