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

move definition

Browse Source
This commit is contained in:
Rígille S. B. Menezes 2021-11-16 15:52:08 -03:00
parent 978bf75b8a
commit b94f4770c6
2 changed files with 14 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
base/RLP/encode_identity.kind
View File

@ -1,3 +1,16 @@
RlP.new_aux.list_length_1_identity(A : Type,
x : List<A>,
y : A,
H : Nat.eql(List.length(A,x),1) == Bool.true) :
List.cons(A, List.head_with_default(A ,y,x), List.nil(A)) == x
case x with H {
nil : Empty.absurd!(Bool.false_neq_true(H))
cons : case x.tail as X with H : Nat.eql(List.length(A,List.cons(A,x.head,X)),1) == Bool.true {
nil : refl
cons : Empty.absurd!(Bool.false_neq_true(H))
} : List.cons(A,List.head_with_default(A,y,List.cons(A,x.head, X)),List.nil(A)) == List.cons(A,x.head, X)
}!
RLP.encode_identity(rlp: RLP): RLP.decode(RLP.encode(rlp)) == rlp
case rlp {
data :
@ -11,7 +24,7 @@ RLP.encode_identity(rlp: RLP): RLP.decode(RLP.encode(rlp)) == rlp
let ensure_non_empty = RLP.aux.12(rlp.value, break_and1)
replace X with mirror(ensure_non_empty) in Maybe.default(RLP,List.head(RLP,X((bytes) List(RLP),List.nil(RLP),(bytes.head) (bytes.tail) U8.ltn(bytes.head,Nat.to_u8(128),() List(RLP),List.cons(RLP,RLP.data(List.cons(U8,bytes.head,List.nil(U8))),RLP.decode.many(bytes.tail)),U8.ltn(bytes.head,Nat.to_u8(192),() List(RLP),RLP.split.length(128,rlp.value,() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))),RLP.split.length(192,rlp.value,() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail))))))),RLP.data(List.nil(U8))) == RLP.data(rlp.value)
replace X with mirror(break_and2) in Maybe.default(RLP,List.head(RLP,X(() List(RLP),List.cons(RLP,RLP.data(List.cons(U8,List.head_with_default(U8,Nat.to_u8(0),rlp.value),List.nil(U8))),RLP.decode.many(List.nil(U8))),U8.ltn(List.head_with_default(U8,Nat.to_u8(0),rlp.value),Nat.to_u8(192),() List(RLP),RLP.split.length(128,rlp.value,() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))),RLP.split.length(192,rlp.value,() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail)))))),RLP.data(List.nil(U8))) == RLP.data(rlp.value)
let list_length_1 = Rlp.new_aux.list_length_1_identity(U8, rlp.value, Nat.to_u8(0), break_and1)
let list_length_1 = RlP.new_aux.list_length_1_identity(U8, rlp.value, Nat.to_u8(0), break_and1)
replace X with mirror(list_length_1) in RLP.data(X) == RLP.data(rlp.value)
refl
false :

17
base/RLP/new_aux.kind
View File

@ -1,17 +0,0 @@
// forall A x,
// Nat.eql(List.length(U8,rlp.value),1) == Bool.true ->
// List.head_with_default(A ,Nat.to_u8(0),x) :: [] == x
Rlp.new_aux.list_length_1_identity(A : Type,
x : List<A>,
y : A,
H : Nat.eql(List.length(A,x),1) == Bool.true) :
List.cons(A, List.head_with_default(A ,y,x), List.nil(A)) == x
case x with H {
nil : Empty.absurd!(Bool.false_neq_true(H))
cons : case x.tail as X with H : Nat.eql(List.length(A,List.cons(A,x.head,X)),1) == Bool.true {
nil : refl
cons : Empty.absurd!(Bool.false_neq_true(H))
} : List.cons(A,List.head_with_default(A,y,List.cons(A,x.head, X)),List.nil(A)) == List.cons(A,x.head, X)
}!