In precept, we defined a relation between
two implementations of a range (ListRange
and LoHiPairRange):

let abs (lr:ListRange) (pr:LoHiPairRange) =
     (hd lr , hd (rev lr)) = pr

We also laid out the proof obligation for
showing that the relationship between the
module persists through their APIs:

Forall k:int:
       abs (L.singleton k) (P.singleton k) = true

Forall i,j:int:
       abs (L.range i j) (P.range i j) = true

Forall l:(int list), p:(int*int), k:int:
       if (L.inv l) and (P.inv p) and (abs l p) then
       abs (L.(+) l k) (P.(+) p k) = true

Forall l:(int list), p:(int*int), k:int:
       if (L.inv l) and (P.inv p) and (abs l p) then
       abs (L.(*) l k) (P.(*) p k) = true

Forall l1,l2:(int list), p1,p2:(int*int): 
       if (L.inv l1) and (L.inv l2) and (P.inv p1) and (P.inv p2)
          and (abs l1 p1) and (abs l2 p2) then
       (abs (L.bridge l1 l2) (P.bridge p1 p2)) = true

Forall l:(int list), p:(int*int):
       if (L.inv l) and (P.inv p) and (abs l p) then
       L.size l = P.size p

Forall l:(int list), p:(int*int), k:int:
	if (L.inv l) and (P.inv p) and (abs l p) then
        L.contains l k = P.contains p k

Forall l1,l2:(int list), p1,p2:(int*int): 
	if (L.inv l1) and (L.inv l2) and (P.inv p1) and (P.inv p2)
           and (abs l1 p1) and (abs l2 p2) then
	     L.(<) l1 l2 = None and P.(<) p1 p2 = None 
	      OR
	     L.(<) l1 l2 = Some b and P.(<) p1 p2 = Some b' and b=b'.

This week's exercise is to work through these proofs, but because of
the complicated implementation of ListRange, it may be more beneficial
to complete the proofs for a different implementation, such as
LoLenPairRange.

recall: let LHPR.inv = (lo <= hi)
and consider: let LLPR.inv = (len > 0)

let abs (llpr:LoLenPairRange) (lhpr:LoHiPairRange) =
    let (lo, len) = llpr in
    (lo, lo+len-1) = lhpr