proofs/ordered_ranges.bend

stelliferous@0.0.3.0 · 32 lines · 0 definitions

1# A finite half-open interval, represented as its consecutive positions.
2import Base
3import stelliferous@0.0.3.0/proofs/natural_addition.bend as Addition
4import stelliferous@0.0.3.0/ordered_matrix.bend as OrderedMatrix
5
6def range(n: Nat,+start: Nat) -> List<&2,Nat>:
7  match n:
8    case 0n:
9      []
10    case 1n+rest:
11      start <> range(rest,1n+start)
12
13def split(+a: Nat,+b: Nat,+start: Nat) -> {range(Nat.add(a,b),start) == OrderedMatrix.cat(Nat,range(a,start),range(b,Nat.add(start,
14        a))) : List<&2,Nat>}:
15  match a:
16    case 0n:
17      %Equal.sym(Nat,Nat.add(start,0n),start,Addition.zero_right(start)) : {range(b,start) == range(b,_) : List<&2,Nat>}
18      {==}
19    case 1n+ +p:
20      %Equal.sym(Nat,Nat.add(start,1n+p),1n+Nat.add(start,p),Addition.successor_right(start,p)) : {start <> range(Nat.add(p,b),
21          1n+start) == start <> OrderedMatrix.cat(Nat,range(p,1n+start),range(b,_)) : List<&2,Nat>}
22      %split(p,b,1n+start) : {start <> range(Nat.add(p,b),1n+start) == start <> _ : List<&2,Nat>}
23      {==}
24
25# [start, end) followed by [end, start + whole) is the whole interval.
26def join(+start: Nat,+left: Nat,+right: Nat,+end: Nat,+whole: Nat,end_exact: {end == Nat.add(start,left) : Nat},size_exact: {Nat.add(left,
27      right) == whole : Nat}) -> {OrderedMatrix.cat(Nat,range(left,start),range(right,end)) == range(whole,start) : List<&2,Nat>}:
28  %size_exact : {OrderedMatrix.cat(Nat,range(left,start),range(right,end)) == range(_,start) : List<&2,Nat>}
29  %Equal.sym(Nat,end,Nat.add(start,left),end_exact) : {OrderedMatrix.cat(Nat,range(left,start),range(right,_)) == range(Nat.add(left,right),
30      start) : List<&2,Nat>}
31  Equal.sym(List<&2,Nat>,range(Nat.add(left,right),start),OrderedMatrix.cat(Nat,range(left,start),range(right,Nat.add(start,left))),split(left,
32      right,start))