mirror of
https://github.com/HigherOrderCO/Kind1.git
synced 2024-09-11 08:45:32 +03:00
move tiago's lemma to Nat lib
This commit is contained in:
parent
5f7e58366e
commit
28e6ab48bc
19
base/Nat/ltn/sub_right.kind
Normal file
19
base/Nat/ltn/sub_right.kind
Normal file
@ -0,0 +1,19 @@
|
||||
Nat.ltn.sub_right(
|
||||
x: Nat, y: Nat, z: Nat
|
||||
H: Equal(Bool, Nat.ltn(y, Nat.sub(z, x)), true)
|
||||
): Equal(Bool, Nat.lte(Nat.add(x y), z), true)
|
||||
case x with H {
|
||||
succ:
|
||||
case z with H {
|
||||
succ:
|
||||
let H = H :: rewrite X in Nat.lte(Nat.succ(y), X) == Bool.true with (Nat.sub.succ_both(z.pred,x.pred))
|
||||
let rec = Nat.ltn.sub_right(x.pred, y, z.pred, H)
|
||||
rec
|
||||
zero:
|
||||
let H = H :: Nat.lte(Nat.succ(y),0) == Bool.true
|
||||
Empty.absurd!(Bool.false_neq_true(H))
|
||||
}!
|
||||
zero:
|
||||
let H = H :: Nat.lte(Nat.succ(y), z) == Bool.true
|
||||
Nat.lte.succ_left!!(H)
|
||||
}!
|
@ -5,7 +5,7 @@ RLP.aux.split.0(
|
||||
H: Equal<Bool>(Nat.lte(List.length!(payload), 55), true)
|
||||
): Pair.new(Bytes, Bytes, payload, tail) == RLP.split.length(128, Nat.to_u8(Nat.add(128, List.length!(payload))) & payload ++ tail)
|
||||
let chain = Nat.Order.chain(List.length(U8,payload), 55, 126, H, refl)
|
||||
let H0 = RLP.new_aux.Nat.lte.max_add(128, List.length(U8,payload), 255, chain)
|
||||
let H0 = Nat.ltn.sub_right(128, List.length(U8,payload), 255, chain)
|
||||
let H1 = Nat.to_u8.safe_conversion(Nat.add(128,List.length(U8,payload)), H0)
|
||||
replace X with H1 in Pair.new(Bytes,Bytes,payload,tail) == Nat.lte(Nat.sub(X,128),55,() Pair(Bytes,Bytes),Bytes.split(List.concat(U8,payload,tail),Nat.sub(U8.to_nat(Nat.to_u8(Nat.add(128,List.length(U8,payload)))),128)),Bytes.split(List.concat(U8,payload,tail),Nat.sub(Nat.sub(U8.to_nat(Nat.to_u8(Nat.add(128,List.length(U8,payload)))),128),56),() Pair(Bytes,Bytes),(length) (tail) Bytes.split(tail,Bytes.to_nat(length))))
|
||||
let H2 = Nat.sub.add.left(128, List.length(U8,payload)) :: rewrite X in Nat.sub(X,128) == List.length(U8,payload) with Nat.add.comm(List.length(U8,payload),128)
|
||||
@ -52,7 +52,7 @@ RLP.aux.split.2(
|
||||
H: Equal<Bool>(Nat.lte(List.length!(payload), 55), true)
|
||||
): Pair.new(Bytes, Bytes, payload, tail) == RLP.split.length(192, Nat.to_u8(Nat.add(192, List.length!(payload))) & payload ++ tail)
|
||||
let chain = Nat.Order.chain(List.length(U8,payload), 55, 62, H, refl)
|
||||
let H0 = RLP.new_aux.Nat.lte.max_add(192, List.length(U8,payload), 255, chain)
|
||||
let H0 = Nat.ltn.sub_right(192, List.length(U8,payload), 255, chain)
|
||||
let H1 = Nat.to_u8.safe_conversion(Nat.add(192,List.length(U8,payload)), H0)
|
||||
replace X with H1 in Pair.new(Bytes,Bytes,payload,tail) == Nat.lte(Nat.sub(X,192),55,() Pair(Bytes,Bytes),Bytes.split(List.concat(U8,payload,tail),Nat.sub(X,192)),Bytes.split(List.concat(U8,payload,tail),Nat.sub(Nat.sub(X,192),56),() Pair(Bytes,Bytes),(length) (tail) Bytes.split(tail,Bytes.to_nat(length))))
|
||||
let H2 = Nat.sub.add.left(192, List.length(U8,payload)) :: rewrite X in Nat.sub(X,192) == List.length(U8,payload) with Nat.add.comm(List.length(U8,payload),192)
|
||||
|
@ -1,16 +0,0 @@
|
||||
RLP.new_aux.Nat.lte.max_add(x : Nat, y : Nat, z : Nat, H : Nat.lte(Nat.succ(y), z - x) == true)
|
||||
: Nat.lte(Nat.add(x y), z) == true
|
||||
case x with H {
|
||||
succ : case z with H {
|
||||
succ :
|
||||
let H = H :: rewrite X in Nat.lte(Nat.succ(y), X) == Bool.true with (Nat.sub.succ_both(z.pred,x.pred))
|
||||
let rec = RLP.new_aux.Nat.lte.max_add(x.pred, y, z.pred, H)
|
||||
rec
|
||||
zero :
|
||||
let H = H :: Nat.lte(Nat.succ(y),0) == Bool.true
|
||||
Empty.absurd!(Bool.false_neq_true(H))
|
||||
}!
|
||||
zero :
|
||||
let H = H :: Nat.lte(Nat.succ(y), z) == Bool.true
|
||||
Nat.lte.succ_left!!(H)
|
||||
}!
|
Loading…
Reference in New Issue
Block a user