proofs/word_width.bend

stelliferous@0.0.2.0 · 19 lines · 2 definitions

1# Width transport changes the type index, never the stored bits.
2import Base
3
4def transport(-source: Nat,-target: Nat,value: Word(source),width: {source == target : Nat}) -> Word(target):
5  %width : Word(_)
6  value
7
8law transport_cons:
9  for +source: Nat
10  for +target: Nat
11  for +bit: Bool
12  for +tail: Word(source)
13  for width: {source == target : Nat}
14  {transport(1n+source,1n+target,WCon{bit,tail},Equal.cong(Nat,Nat,n => 1n+n,source,target,width)) == WCon{bit,transport(source,target,tail,
15        width)} : Word(1n+target)}
16
17def transport_cons(source,target,bit,tail,width):
18  %h@width : {transport(1n+source,1n+_,WCon{bit,tail},Equal.cong(Nat,Nat,n => 1n+n,source,_,h)) == WCon{bit,transport(source,_,tail,h)} : Word(1n+_)}
19  {==}