proofs/nat_interval.bend

stelliferous@0.0.2.0 · 38 lines · 5 definitions

1import Base
2import stelliferous@0.0.2.0/proofs/nat_order.bend as Order
3import stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend as Bounds
4import stelliferous@0.0.2.0/proofs/natural_addition.bend as Addition
5import stelliferous@0.0.2.0/proofs/nat_extrema.bend as Extrema
6
7def shifted_inside(+begin: Nat,+end: Nat,+query: Nat,+lower: {Nat.is_le(begin,query) == True{} : Bool},+upper: {Nat.is_lt(query,end) == True{} : Bool}) ->
8  {Nat.is_lt(Nat.sub(query,begin),Nat.sub(end,begin)) == True{} : Bool}:
9  +ordered = Bounds.strict_le(begin,end,Order.le_lt_trans(begin,query,end,lower,upper))
10  Order.cancel_offset_lt(begin,Nat.sub(query,begin),Nat.sub(end,begin),
11    %Equal.sym(Nat,Nat.add(begin,Nat.sub(query,begin)),query,Order.restore_shift(begin,query,lower)) : {Nat.is_lt(_,Nat.add(begin,Nat.sub(end,begin))) == True{} : Bool}
12    %Equal.sym(Nat,Nat.add(begin,Nat.sub(end,begin)),end,Order.restore_shift(begin,end,ordered)) : {Nat.is_lt(query,_) == True{} : Bool} upper)
13
14def shifted_span(+first: Nat,+rows: Nat,+begin: Nat,+end: Nat,lower: {Nat.is_le(first,begin) == True{} : Bool},
15  ordered: {Nat.is_le(begin,end) == True{} : Bool},upper: {Nat.is_le(end,Nat.add(first,rows)) == True{} : Bool}) ->
16  {Nat.is_le(Nat.add(Nat.sub(begin,first),Nat.sub(end,begin)),rows) == True{} : Bool}:
17  Order.cancel_offset_le(first,Nat.add(Nat.sub(begin,first),Nat.sub(end,begin)),rows,
18    %Addition.associative(first,Nat.sub(begin,first),Nat.sub(end,begin)) : {Nat.is_le(_,Nat.add(first,rows)) == True{} : Bool}
19    %Equal.sym(Nat,Nat.add(first,Nat.sub(begin,first)),begin,Order.restore_shift(first,begin,lower)) : {Nat.is_le(Nat.add(_,Nat.sub(end,begin)),Nat.add(first,rows)) == True{} : Bool}
20    %Equal.sym(Nat,Nat.add(begin,Nat.sub(end,begin)),end,Order.restore_shift(begin,end,ordered)) : {Nat.is_le(_,Nat.add(first,rows)) == True{} : Bool} upper)
21
22# A query lies strictly before or at/after the end of a half-open interval.
23type Outside<-start: Nat,-length: Nat,-query: Nat> is Data:
24  Before{bound: {Nat.is_lt(query,start) == True{} : Bool}}
25  After{bound: {Nat.is_le(Nat.add(start,length),query) == True{} : Bool}}
26
27def outside_head(+start: Nat,+remaining: Nat,+query: Nat,outside: Outside<start,1n+remaining,query>) ->
28  {Nat.is_eq(query,start) == False{} : Bool}:
29  match outside:
30    case Before{bound}: Order.less_not_equal(query,start,bound)
31    case After{bound}:
32      %Equal.sym(Bool,Nat.is_eq(query,start),Nat.is_eq(start,query),Order.equal_symmetric(query,start)) : {_ == False{} : Bool}
33      Order.less_not_equal(start,query,Order.room_index(start,remaining,query,bound))
34
35def outside_tail(+start: Nat,+remaining: Nat,+query: Nat,outside: Outside<start,1n+remaining,query>) -> Outside<1n+start,remaining,query>:
36  match outside:
37    case Before{bound}: Before{Order.lt_succ(query,start,Bounds.strict_le(query,start,bound))}
38    case After{bound}: After{Order.advance_room(start,remaining,query,bound)}