# Splitting and Splicing Intervals (Part 2)

Previously, we saw how the principle of "making illegal states unrepresentable" allowed LH to easily enforce a key invariant in Joachim Breitner's library for representing sets of integers as sorted lists of intervals.

However, Hs-to-coq let Breitner specify and verify that his code properly implemented a set library. Today, lets see how LH's new "type-level computation" abilities let us reason about the sets of values corresponding to intervals, while using the SMT solver to greatly simplify the overhead of proof.

## Intervals¶

Recall that the key idea is to represent sets of integers like

``````{ 7, 1, 10, 3, 11, 2, 9, 12, 4}
``````

as ordered lists of intervals

``````[ (1, 5), (7, 8), (9, 13) ]
``````

where each pair `(i, j)` represents the set `{i, i+1,..., j-1}`.

To verify that the implementation correctly implements a set data type, we need a way to

1. Specify the set of values being described,
2. Establish some key properties of these sets.

## Range-Sets: Semantics of Intervals¶

We can describe the set of values corresponding to (i.e. "the semantics of") an interval `i, j` by importing the `Data.Set` library

```88: import qualified Data.Set as S
```

to write a function `rng i j` that defines the range-set `i..j`

```94: {-@ reflect rng @-}
95: {-@ rng :: i:Int -> j:Int -> S.Set Int / [j - i] @-}
96: Int -> Int -> (Set Int)rng Inti Intj
97:   | {v : Bool | v <=> i < j}i x1:Int -> x2:Int -> {v : Bool | v <=> x1 < x2}< j     = x1:(Set Int) -> x2:(Set Int) -> {v : (Set Int) | v == Set_cup x1 x2}S.union ({v : (Set Int) | v == Set_sng i}S.singleton i) (Int -> Int -> (Set Int)rng (Intix1:Int -> x2:Int -> {v : Int | v == x1 + x2}+1) j)
98:   | otherwise = S.empty
```

The `reflect rng` tells LH that we are going to want to work with the Haskell function `rng` at the refinement-type level.

## Equational Reasoning¶

To build up a little intuition about the above definition and how LH reasons about Sets, lets write some simple unit proofs. For example, lets check that `2` is indeed in the range-set `rng 1 3`, by writing a type signature

```116: {-@ test1 :: () -> { S.member 2 (rng 1 3) } @-}
```

Any implementation of the above type is a proof that `2` is indeed in `rng 1 3`. Notice that we can reuse the operators from `Data.Set` (here, `S.member`) to talk about set operations in the refinement logic. Lets write this proof in an equational style:

```126: () -> {VV : () | Set_mem 2 (RangeSet.rng 1 3)}test1 ()
127:   =   x1:Int -> x2:(Set Int) -> {v : Bool | v <=> Set_mem x1 x2}S.member 2 ({v : x1:Int -> x2:Int -> {v : (Set Int) | v == RangeSet.rng x1 x2
&& v == (if x1 < x2 then Set_cup (Set_sng x1) (RangeSet.rng (x1 + 1) x2) else Set_empty 0)} | v == RangeSet.rng}rng 1 3)
128:       -- by unfolding `rng 1 3`
129:   === x1:Int -> x2:(Set Int) -> {v : Bool | v <=> Set_mem x1 x2}S.member 2 (x1:(Set Int) -> x2:(Set Int) -> {v : (Set Int) | v == Set_cup x1 x2}S.union ((Set Int)S.singleton 1) ({v : x1:Int -> x2:Int -> {v : (Set Int) | v == RangeSet.rng x1 x2
&& v == (if x1 < x2 then Set_cup (Set_sng x1) (RangeSet.rng (x1 + 1) x2) else Set_empty 0)} | v == RangeSet.rng}rng 2 3))
130:       -- by unfolding `rng 2 3`
131:   === x1:Int -> x2:(Set Int) -> {v : Bool | v <=> Set_mem x1 x2}S.member 2 (x1:(Set Int) -> x2:(Set Int) -> {v : (Set Int) | v == Set_cup x1 x2}S.union ((Set Int)S.singleton 1)
132:                           (x1:(Set Int) -> x2:(Set Int) -> {v : (Set Int) | v == Set_cup x1 x2}S.union ((Set Int)S.singleton 2) ({v : x1:Int -> x2:Int -> {v : (Set Int) | v == RangeSet.rng x1 x2
&& v == (if x1 < x2 then Set_cup (Set_sng x1) (RangeSet.rng (x1 + 1) x2) else Set_empty 0)} | v == RangeSet.rng}rng 3 3)))
133:       -- by set-theory
134:   === True
135:   *** QED
```

the "proof" uses two library operators:

• `e1 === e2` is an implicit equality that checks `e1` is indeed equal to `e2` after unfolding functions at most once, and returns a term that equals `e1` and `e2`, and

• `e *** QED` converts any term `e` into a proof.

The first two steps of `test1`, simply unfold `rng` and the final step uses the SMT solver's decision procedure for sets to check equalities over set operations like `S.union`, `S.singleton` and `S.member`.

## Reusing Proofs¶

Next, lets check that:

```160: {-@ test2 :: () -> { S.member 2 (rng 0 3) } @-}
161: () -> {VV : () | Set_mem 2 (RangeSet.rng 0 3)}test2 ()
162:   =   x1:Int -> x2:(Set Int) -> {v : Bool | v <=> Set_mem x1 x2}S.member 2 ({v : x1:Int -> x2:Int -> {v : (Set Int) | v == RangeSet.rng x1 x2
&& v == (if x1 < x2 then Set_cup (Set_sng x1) (RangeSet.rng (x1 + 1) x2) else Set_empty 0)} | v == RangeSet.rng}rng 0 3)
163:       -- by unfolding and set-theory
164:   === (Bool2 x1:Integer -> x2:Integer -> {v : Bool | v <=> x1 == x2}== 0 {v : x1:Bool -> x2:Bool -> {v : Bool | v <=> x1
|| x2} | v == GHC.Classes.||}|| x1:Int -> x2:(Set Int) -> {v : Bool | v <=> Set_mem x1 x2}S.member 2 ({v : x1:Int -> x2:Int -> {v : (Set Int) | v == RangeSet.rng x1 x2
&& v == (if x1 < x2 then Set_cup (Set_sng x1) (RangeSet.rng (x1 + 1) x2) else Set_empty 0)} | v == RangeSet.rng}rng 1 3))
165:       -- by re-using test1 as a lemma
166:   ==? True ? {v : () -> {v : () | Set_mem 2 (RangeSet.rng 1 3)} | v == RangeSet.test1}test1 ()
167:   *** QED
```

We could do the proof by unfolding in the equational style. However, `test1` already establishes that `S.member 2 (rng 1 3)` and we can reuse this fact using:

• `e1 ==? e2 ? pf` an explicit equality which checks that `e1` equals `e2` because of the extra facts asserted by the `Proof` named `pf` (in addition to unfolding functions at most once) and returns a term that equals both `e1` and `e2`.

## Proof by Logical Evaluation¶

Equational proofs like `test1` and `test2` often have long chains of calculations that can be tedious to spell out. Fortunately, we taught LH a new trick called Proof by Logical Evaluation (PLE) that optionally shifts the burden of performing those calculations onto the machine. For example, PLE completely automates the above proofs:

```194: {-@ test1_ple :: () -> { S.member 2 (rng 1 3) } @-}
195: () -> {VV : () | Set_mem 2 (RangeSet.rng 1 3)}test1_ple () = ()
196:
197: {-@ test2_ple :: () -> { S.member 2 (rng 0 3) } @-}
198: () -> {VV : () | Set_mem 2 (RangeSet.rng 0 3)}test2_ple () = ()
```

Be Warned! While automation is cool, it can be very helpful to first write out all the steps of an equational proof, at least while building up intuition.

## Proof by Induction¶

At this point, we have enough tools to start proving some interesting facts about range-sets. For example, if `x` is outside the range `i..j` then it does not belong in `rng i j`:

```216: {-@ lem_mem :: i:_ -> j:_ -> x:{x < i || j <= x} ->
217:                  { not (S.member x (rng i j)) } / [j - i]
218:   @-}
```

We will prove the above "by induction". A confession: I always had trouble understanding what exactly proof by induction really meant. Why was it it ok to "do" induction on one thing but not another?

Induction is Recursion

Fortunately, with LH, induction is just recursion. That is,

1. We can recursively use the same theorem we are trying to prove, but

2. We must make sure that the recursive function/proof terminates.

The proof makes this clear:

```239: x1:Int -> x2:Int -> x3:{v : Int | v < x1
|| x2 <= v} -> {VV : () | not (Set_mem x3 (RangeSet.rng x1 x2))}lem_mem Inti Intj {v : Int | v < i
|| j <= v}x
240:   | {v : Bool | v <=> i >= j}i x1:Int -> x2:Int -> {v : Bool | v <=> x1 >= x2}>= j
241:       -- BASE CASE
242:   =   {v : x1:Bool -> {v : Bool | v <=> not x1} | v == GHC.Classes.not}not (x1:Int -> x2:(Set Int) -> {v : Bool | v <=> Set_mem x1 x2}S.member x ({v : x1:Int -> x2:Int -> {v : (Set Int) | v == RangeSet.rng x1 x2
&& v == (if x1 < x2 then Set_cup (Set_sng x1) (RangeSet.rng (x1 + 1) x2) else Set_empty 0)} | v == RangeSet.rng}rng i j))
243:       -- by unfolding
244:   === {v : x1:Bool -> {v : Bool | v <=> not x1} | v == GHC.Classes.not}not (x1:Int -> x2:(Set Int) -> {v : Bool | v <=> Set_mem x1 x2}S.member x S.empty)
245:       -- by set-theory
246:   === True *** QED
247:
248:   | {v : Bool | v <=> i < j}i x1:Int -> x2:Int -> {v : Bool | v <=> x1 < x2}< j
249:       -- INDUCTIVE CASE
250:   =   {v : x1:Bool -> {v : Bool | v <=> not x1} | v == GHC.Classes.not}not (x1:Int -> x2:(Set Int) -> {v : Bool | v <=> Set_mem x1 x2}S.member x ({v : x1:Int -> x2:Int -> {v : (Set Int) | v == RangeSet.rng x1 x2
&& v == (if x1 < x2 then Set_cup (Set_sng x1) (RangeSet.rng (x1 + 1) x2) else Set_empty 0)} | v == RangeSet.rng}rng i j))
251:       -- by unfolding
252:   === {v : x1:Bool -> {v : Bool | v <=> not x1} | v == GHC.Classes.not}not (x1:Int -> x2:(Set Int) -> {v : Bool | v <=> Set_mem x1 x2}S.member x (x1:(Set Int) -> x2:(Set Int) -> {v : (Set Int) | v == Set_cup x1 x2}S.union ({v : (Set Int) | v == Set_sng i}S.singleton i) ({v : x1:Int -> x2:Int -> {v : (Set Int) | v == RangeSet.rng x1 x2
&& v == (if x1 < x2 then Set_cup (Set_sng x1) (RangeSet.rng (x1 + 1) x2) else Set_empty 0)} | v == RangeSet.rng}rng (Intix1:Int -> x2:Int -> {v : Int | v == x1 + x2}+1) j)))
253:       -- by set-theory
254:   === {v : x1:Bool -> {v : Bool | v <=> not x1} | v == GHC.Classes.not}not (x1:Int -> x2:(Set Int) -> {v : Bool | v <=> Set_mem x1 x2}S.member x ({v : x1:Int -> x2:Int -> {v : (Set Int) | v == RangeSet.rng x1 x2
&& v == (if x1 < x2 then Set_cup (Set_sng x1) (RangeSet.rng (x1 + 1) x2) else Set_empty 0)} | v == RangeSet.rng}rng (Intix1:Int -> x2:Int -> {v : Int | v == x1 + x2}+1) j))
255:       -- by "induction hypothesis"
256:   ==? True ? x1:Int -> x2:Int -> x3:{v : Int | v < x1
|| x2 <= v} -> {VV : () | not (Set_mem x3 (RangeSet.rng x1 x2))}lem_mem (Inti x1:Int -> x2:Int -> {v : Int | v == x1 + x2}+ 1) j x *** QED
```

There are two cases.

• Base Case: As `i >= j`, we know `rng i j` is empty, so `x` cannot be in it.

• Inductive Case As `i < j` we can unfold `rng i j` and then recursively call `lem_mem (i+1) j` to obtain the fact that `x` cannot be in `i+1..j` to complete the proof.

LH automatically checks that the proof:

1. Accounts for all cases, as otherwise the function is not total i.e. like the `head` function which is only defined on non-empty lists. (Try deleting a case at the demo to see what happens.)

2. Terminates, as otherwise the induction is bogus, or in math-speak, not well-founded. We use the explicit termination metric `/ [j-i]` as a hint to tell LH that in each recursive call, the size of the interval `j-i` shrinks and is always non-negative. LH checks that is indeed the case, ensuring that we have a legit proof by induction.

Proof by Evaluation

Once you get the hang of the above style, you get tired of spelling out all the details. Logical evaluation lets us eliminate all the boring calculational steps, leaving the essential bits: the recursive (inductive) skeleton

```291: {-@ lem_mem_ple :: i:_ -> j:_ -> x:{x < i || j <= x} ->
292:                      {not (S.member x (rng i j))} / [j-i]
293:   @-}
294: x1:Int -> x2:Int -> x3:{v : Int | v < x1
|| x2 <= v} -> {VV : () | not (Set_mem x3 (RangeSet.rng x1 x2))}lem_mem_ple Inti Intj {v : Int | v < i
|| j <= v}x
295:   | {v : Bool | v <=> i >= j}i x1:Int -> x2:Int -> {v : Bool | v <=> x1 >= x2}>= j =  ()
296:   | {v : Bool | v <=> i < j}i x1:Int -> x2:Int -> {v : Bool | v <=> x1 < x2}< j  =  x1:Int -> x2:Int -> x3:{v : Int | v < x1
|| x2 <= v} -> {VV : () | not (Set_mem x3 (RangeSet.rng x1 x2))}lem_mem_ple (Inti x1:Int -> x2:Int -> {v : Int | v == x1 + x2}+ 1) j x
```

The above is just `lem_mem` sans the (PLE-synthesized) intermediate equalities.

## Disjointness¶

We say that two sets are disjoint if their `intersection` is `empty`:

```309: {-@ inline disjoint @-}
310: disjoint :: S.Set Int -> S.Set Int -> Bool
311: x1:(Set Int) -> x2:(Set Int) -> {VV : Bool | VV <=> Set_cap x1 x2 == Set_empty 0}disjoint (Set Int)a (Set Int)b = x1:(Set Int) -> x2:(Set Int) -> {v : (Set Int) | v == Set_cap x1 x2}S.intersection a b x1:(Set Int) -> x2:(Set Int) -> {v : Bool | v <=> x1 == x2}== S.empty
```

Lets prove that two intervals are disjoint if the first ends before the second begins:

```318: {-@ lem_disj :: i1:_ -> j1:_ -> i2:{j1 <= i2} -> j2:_ ->
319:                   {disjoint (rng i1 j1) (rng i2 j2)} / [j2-i2]
320:   @-}
```

This proof goes "by induction" on the size of the second interval, i.e. `j2-i2`:

```327: x1:Int -> x2:Int -> x3:{i2 : Int | x2 <= i2} -> x4:Int -> {VV : () | Set_cap (RangeSet.rng x1 x2) (RangeSet.rng x3 x4) == Set_empty 0}lem_disj Inti1 Intj1 {i2 : Int | j1 <= i2}i2 Intj2
328:   | {v : Bool | v <=> i2 >= j2}i2 x1:Int -> x2:Int -> {v : Bool | v <=> x1 >= x2}>= j2
329:       -- Base CASE
330:   =   {v : x1:(Set Int) -> x2:(Set Int) -> {v : Bool | v <=> Set_cap x1 x2 == Set_empty 0} | v == RangeSet.disjoint}disjoint ({v : x1:Int -> x2:Int -> {v : (Set Int) | v == RangeSet.rng x1 x2
&& v == (if x1 < x2 then Set_cup (Set_sng x1) (RangeSet.rng (x1 + 1) x2) else Set_empty 0)} | v == RangeSet.rng}rng i1 j1) ({v : x1:Int -> x2:Int -> {v : (Set Int) | v == RangeSet.rng x1 x2
&& v == (if x1 < x2 then Set_cup (Set_sng x1) (RangeSet.rng (x1 + 1) x2) else Set_empty 0)} | v == RangeSet.rng}rng i2 j2)
331:       -- by unfolding
332:   === {v : x1:(Set Int) -> x2:(Set Int) -> {v : Bool | v <=> Set_cap x1 x2 == Set_empty 0} | v == RangeSet.disjoint}disjoint ({v : x1:Int -> x2:Int -> {v : (Set Int) | v == RangeSet.rng x1 x2
&& v == (if x1 < x2 then Set_cup (Set_sng x1) (RangeSet.rng (x1 + 1) x2) else Set_empty 0)} | v == RangeSet.rng}rng i1 j1) S.empty
333:       -- by set-theory
334:   === True
335:   *** QED
336:
337:   | {v : Bool | v <=> i2 < j2}i2 x1:Int -> x2:Int -> {v : Bool | v <=> x1 < x2}< j2
338:       -- Inductive CASE
339:   =   {v : x1:(Set Int) -> x2:(Set Int) -> {v : Bool | v <=> Set_cap x1 x2 == Set_empty 0} | v == RangeSet.disjoint}disjoint ({v : x1:Int -> x2:Int -> {v : (Set Int) | v == RangeSet.rng x1 x2
&& v == (if x1 < x2 then Set_cup (Set_sng x1) (RangeSet.rng (x1 + 1) x2) else Set_empty 0)} | v == RangeSet.rng}rng i1 j1) ({v : x1:Int -> x2:Int -> {v : (Set Int) | v == RangeSet.rng x1 x2
&& v == (if x1 < x2 then Set_cup (Set_sng x1) (RangeSet.rng (x1 + 1) x2) else Set_empty 0)} | v == RangeSet.rng}rng i2 j2)
340:       -- by unfolding
341:   === {v : x1:(Set Int) -> x2:(Set Int) -> {v : Bool | v <=> Set_cap x1 x2 == Set_empty 0} | v == RangeSet.disjoint}disjoint ({v : x1:Int -> x2:Int -> {v : (Set Int) | v == RangeSet.rng x1 x2
&& v == (if x1 < x2 then Set_cup (Set_sng x1) (RangeSet.rng (x1 + 1) x2) else Set_empty 0)} | v == RangeSet.rng}rng i1 j1) (x1:(Set Int) -> x2:(Set Int) -> {v : (Set Int) | v == Set_cup x1 x2}S.union ({v : (Set Int) | v == Set_sng i2}S.singleton i2) ({v : x1:Int -> x2:Int -> {v : (Set Int) | v == RangeSet.rng x1 x2
&& v == (if x1 < x2 then Set_cup (Set_sng x1) (RangeSet.rng (x1 + 1) x2) else Set_empty 0)} | v == RangeSet.rng}rng (Inti2x1:Int -> x2:Int -> {v : Int | v == x1 + x2}+1) j2))
342:       -- by induction and lem_mem
343:   ==? True ? ({v : x1:Int -> x2:Int -> x3:{v : Int | v < x1
|| x2 <= v} -> {v : () | not (Set_mem x3 (RangeSet.rng x1 x2))} | v == RangeSet.lem_mem}lem_mem i1 j1 i2 {v : () -> () -> () | v == Language.Haskell.Liquid.NewProofCombinators.&&&}&&& x1:Int -> x2:Int -> x3:{i2 : Int | x2 <= i2} -> x4:Int -> {VV : () | Set_cap (RangeSet.rng x1 x2) (RangeSet.rng x3 x4) == Set_empty 0}lem_disj i1 j1 (Inti2x1:Int -> x2:Int -> {v : Int | v == x1 + x2}+1) j2)
344:   *** QED
```

Here, the operator `pf1 &&& pf2` conjoins the two facts asserted by `pf1` and `pf2`.

Again, we can get PLE to do the boring calculations:

```353: {-@ lem_disj_ple :: i1:_ -> j1:_ -> i2:{j1 <= i2} -> j2:_ ->
354:                       {disjoint (rng i1 j1) (rng i2 j2)} / [j2-i2]
355:   @-}
356: x1:Int -> x2:Int -> x3:{i2 : Int | x2 <= i2} -> x4:Int -> {VV : () | Set_cap (RangeSet.rng x1 x2) (RangeSet.rng x3 x4) == Set_empty 0}lem_disj_ple Inti1 Intj1 {i2 : Int | j1 <= i2}i2 Intj2
357:   | {v : Bool | v <=> i2 >= j2}i2 x1:Int -> x2:Int -> {v : Bool | v <=> x1 >= x2}>= j2 = ()
358:   | {v : Bool | v <=> i2 < j2}i2 x1:Int -> x2:Int -> {v : Bool | v <=> x1 < x2}<  j2 = {v : x1:Int -> x2:Int -> x3:{v : Int | v < x1
|| x2 <= v} -> {v : () | not (Set_mem x3 (RangeSet.rng x1 x2))} | v == RangeSet.lem_mem}lem_mem i1 j1 i2 {v : () -> () -> () | v == Language.Haskell.Liquid.NewProofCombinators.&&&}&&& x1:Int -> x2:Int -> x3:{i2 : Int | x2 <= i2} -> x4:Int -> {VV : () | Set_cap (RangeSet.rng x1 x2) (RangeSet.rng x3 x4) == Set_empty 0}lem_disj_ple i1 j1 (Inti2x1:Int -> x2:Int -> {v : Int | v == x1 + x2}+1) j2
```

## Splitting Intervals¶

Finally, we can establish the splitting property of an interval `i..j`, that is, given some `x` that lies between `i` and `j` we can split `i..j` into `i..x` and `x..j`. We define a predicate that a set `s` can be split into `a` and `b` as:

```372: {-@ inline split @-}
373: split :: S.Set Int -> S.Set Int -> S.Set Int -> Bool
374: x1:(Set Int) -> x2:(Set Int) -> x3:(Set Int) -> {VV : Bool | VV <=> x1 == Set_cup x2 x3
&& Set_cap x2 x3 == Set_empty 0}split (Set Int)s (Set Int)a (Set Int)b = Bools x1:(Set Int) -> x2:(Set Int) -> {v : Bool | v <=> x1 == x2}== x1:(Set Int) -> x2:(Set Int) -> {v : (Set Int) | v == Set_cup x1 x2}S.union a b {v : x1:Bool -> x2:Bool -> {v : Bool | v <=> x1
&& x2} | v == GHC.Classes.&&}&& {v : x1:(Set Int) -> x2:(Set Int) -> {v : Bool | v <=> Set_cap x1 x2 == Set_empty 0} | v == RangeSet.disjoint}disjoint a b
```

We can now state and prove the splitting property as:

```380: {-@ lem_split :: i:_ -> x:{i <= x} -> j:{x <= j} ->
381:                    {split (rng i j) (rng i x) (rng x j)} / [x-i]
382:   @-}
383: x1:Int -> x2:{v : Int | x1 <= v} -> x3:{j : Int | x2 <= j} -> {VV : () | RangeSet.rng x1 x3 == Set_cup (RangeSet.rng x1 x2) (RangeSet.rng x2 x3)
&& Set_cap (RangeSet.rng x1 x2) (RangeSet.rng x2 x3) == Set_empty 0}lem_split Inti {v : Int | i <= v}x {j : Int | x <= j}t
384:   | {v : Bool | v <=> i == x}i x1:Int -> x2:Int -> {v : Bool | v <=> x1 == x2}== x = ()
385:   | {v : Bool | v <=> i < x}i x1:Int -> x2:Int -> {v : Bool | v <=> x1 < x2}<  x = x1:Int -> x2:{v : Int | x1 <= v} -> x3:{j : Int | x2 <= j} -> {VV : () | RangeSet.rng x1 x3 == Set_cup (RangeSet.rng x1 x2) (RangeSet.rng x2 x3)
&& Set_cap (RangeSet.rng x1 x2) (RangeSet.rng x2 x3) == Set_empty 0}lem_split (Inti x1:Int -> x2:Int -> {v : Int | v == x1 + x2}+ 1) x t {v : () -> () -> () | v == Language.Haskell.Liquid.NewProofCombinators.&&&}&&& {v : x1:Int -> x2:Int -> x3:{v : Int | v < x1
|| x2 <= v} -> {v : () | not (Set_mem x3 (RangeSet.rng x1 x2))} | v == RangeSet.lem_mem}lem_mem x t i
```

(We're using PLE here quite aggressively, can you work out the equational proof?)

## Set Operations¶

The splitting abstraction is a wonderful hammer that lets us break higher-level proofs into the bite sized pieces suitable for the SMT solver's decision procedures.

Subset

An interval `i1..j1` is enclosed by `i2..j2` if `i2 <= i1 < j1 <= j2`. Lets verify that the range-set of an interval is contained in that of an enclosing one.

```406: {-@ lem_sub :: i1:_ -> j1:{i1 < j1} ->
407:                i2:_ -> j2:{i2 < j2 && i2 <= i1 && j1 <= j2 } ->
408:                  { S.isSubsetOf (rng i1 j1) (rng i2 j2) }
409:   @-}
```

Here's a "proof-by-picture". We can split the larger interval `i2..j2` into smaller pieces, `i2..i1`, `i1..j1` and `j1..j2` one of which is the `i1..j1`, thereby completing the proof:

![`lem_sub` a proof by picture](../static/img/lem_sub.png "lem_sub proof by picture")

The intuition represented by the picture can distilled into the following proof, that invokes `lem_split` to carve `i2..j2` into the relevant sub-intervals:

```432: x1:Int -> x2:{j1 : Int | x1 < j1} -> x3:Int -> x4:{j2 : Int | x3 < j2
&& x3 <= x1
&& x2 <= j2} -> {VV : () | Set_sub (RangeSet.rng x1 x2) (RangeSet.rng x3 x4)}lem_sub Inti1 {j1 : Int | i1 < j1}j1 Inti2 {j2 : Int | i2 < j2
&& i2 <= i1
&& j1 <= j2}j2 = {v : x1:Int -> x2:{v : Int | x1 <= v} -> x3:{v : Int | x2 <= v} -> {v : () | RangeSet.rng x1 x3 == Set_cup (RangeSet.rng x1 x2) (RangeSet.rng x2 x3)
&& Set_cap (RangeSet.rng x1 x2) (RangeSet.rng x2 x3) == Set_empty 0} | v == RangeSet.lem_split}lem_split i2 i1 j2 {v : () -> () -> () | v == Language.Haskell.Liquid.NewProofCombinators.&&&}&&& {v : x1:Int -> x2:{v : Int | x1 <= v} -> x3:{v : Int | x2 <= v} -> {v : () | RangeSet.rng x1 x3 == Set_cup (RangeSet.rng x1 x2) (RangeSet.rng x2 x3)
&& Set_cap (RangeSet.rng x1 x2) (RangeSet.rng x2 x3) == Set_empty 0} | v == RangeSet.lem_split}lem_split i1 j1 j2
```

Union

An interval `i1..j1` overlaps `i2..j2` if `i1 <= j2 <= i2`, that is, if the latter ends somewhere inside the former. The same splitting hammer lets us compute the union of two overlapping intervals simply by picking the interval defined by the endpoints.

```446: {-@ lem_union ::
447:       i1:_ -> j1:{i1 < j1} ->
448:       i2:_ -> j2:{i2 < j2 && i1 <= j2 && j2 <= j1 } ->
449:         { rng (min i1 i2) j1 = S.union (rng i1 j1) (rng i2 j2) }
450:   @-}
```

![`lem_union` a proof by picture](../static/img/lem_union.png "lem_union proof by picture")

The pictorial proof illustrates the two cases:

1. `i1..j1` encloses `i2..j2`; here the union is just `i1..j1`,

2. `i1..j1` only overlaps `i1..j1`; here the union is `i2..j1` which can be split into `i2..i1`, `i1..j2` and `j2..j1` which are exactly the union of the intervals `i1..j1` and `i2..j2`.

Again, we render the picture into a formal proof as:

```474: x1:Int -> x2:{j1 : Int | x1 < j1} -> x3:Int -> x4:{j2 : Int | x3 < j2
&& x1 <= j2
&& j2 <= x2} -> {VV : () | RangeSet.rng (RangeSet.min x1 x3) x2 == Set_cup (RangeSet.rng x1 x2) (RangeSet.rng x3 x4)}lem_union Inti1 {j1 : Int | i1 < j1}j1 Inti2 {j2 : Int | i2 < j2
&& i1 <= j2
&& j2 <= j1}j2
475:   -- i1..j1 encloses i2..j2
476:   | {v : Bool | v <=> i1 < i2}i1 x1:Int -> x2:Int -> {v : Bool | v <=> x1 < x2}< i2   = {v : x1:Int -> x2:{v : Int | x1 < v} -> x3:Int -> x4:{v : Int | x3 < v
&& x3 <= x1
&& x2 <= v} -> {v : () | Set_sub (RangeSet.rng x1 x2) (RangeSet.rng x3 x4)} | v == RangeSet.lem_sub}lem_sub i2 j2 i1 j1
477:   -- i1..j1 overlaps i2..j2
478:   | otherwise = {v : x1:Int -> x2:{v : Int | x1 <= v} -> x3:{v : Int | x2 <= v} -> {v : () | RangeSet.rng x1 x3 == Set_cup (RangeSet.rng x1 x2) (RangeSet.rng x2 x3)
&& Set_cap (RangeSet.rng x1 x2) (RangeSet.rng x2 x3) == Set_empty 0} | v == RangeSet.lem_split}lem_split i2 i1 j1
479:             {v : () -> () -> () | v == Language.Haskell.Liquid.NewProofCombinators.&&&}&&& {v : x1:Int -> x2:{v : Int | x1 <= v} -> x3:{v : Int | x2 <= v} -> {v : () | RangeSet.rng x1 x3 == Set_cup (RangeSet.rng x1 x2) (RangeSet.rng x2 x3)
&& Set_cap (RangeSet.rng x1 x2) (RangeSet.rng x2 x3) == Set_empty 0} | v == RangeSet.lem_split}lem_split i1 j2 j1
480:             {v : () -> () -> () | v == Language.Haskell.Liquid.NewProofCombinators.&&&}&&& {v : x1:Int -> x2:{v : Int | x1 <= v} -> x3:{v : Int | x2 <= v} -> {v : () | RangeSet.rng x1 x3 == Set_cup (RangeSet.rng x1 x2) (RangeSet.rng x2 x3)
&& Set_cap (RangeSet.rng x1 x2) (RangeSet.rng x2 x3) == Set_empty 0} | v == RangeSet.lem_split}lem_split i2 i1 j2
```

Intersection

Finally, we check that the intersection of two overlapping intervals is given by their inner-points.

```489: {-@ lem_intersect ::
490:       i1:_ -> j1:{i1 < j1} ->
491:       i2:_ -> j2:{i2 < j2 && i1 <= j2 && j2 <= j1 } ->
492:         {rng (max i1 i2) j2 = S.intersection (rng i1 j1) (rng i2 j2)}
493:   @-}
```

![`lem_intersect` a proof by picture](../static/img/lem_intersect.png "lem_intersect proof by picture")

We have the same two cases as for `lem_union`

1. `i1..j1` encloses `i2..j2`; here the intersection is just `i2..j2`,

2. `i1..j1` only overlaps `i1..j1`; here the intersection is the middle segment `i1..j2`, which we obtain by (a) splitting `i1..j1` at `j2`, (b) splitting `i2..j2` at `i1`, (c) discarding the end segments which do not belong in the intersection.

```517: x1:Int -> x2:{j1 : Int | x1 < j1} -> x3:Int -> x4:{j2 : Int | x3 < j2
&& x1 <= j2
&& j2 <= x2} -> {VV : () | RangeSet.rng (RangeSet.max x1 x3) x4 == Set_cap (RangeSet.rng x1 x2) (RangeSet.rng x3 x4)}lem_intersect Inti1 {j1 : Int | i1 < j1}j1 Inti2 {j2 : Int | i2 < j2
&& i1 <= j2
&& j2 <= j1}j2
518:   -- i1..j1 encloses i2..j2
519:   | {v : Bool | v <=> i1 < i2}i1 x1:Int -> x2:Int -> {v : Bool | v <=> x1 < x2}< i2   = {v : x1:Int -> x2:{v : Int | x1 < v} -> x3:Int -> x4:{v : Int | x3 < v
&& x3 <= x1
&& x2 <= v} -> {v : () | Set_sub (RangeSet.rng x1 x2) (RangeSet.rng x3 x4)} | v == RangeSet.lem_sub}lem_sub i2 j2 i1 j1
520:   -- i1..j1 overlaps i2..j2
521:   | otherwise = {v : x1:Int -> x2:{v : Int | x1 <= v} -> x3:{v : Int | x2 <= v} -> {v : () | RangeSet.rng x1 x3 == Set_cup (RangeSet.rng x1 x2) (RangeSet.rng x2 x3)
&& Set_cap (RangeSet.rng x1 x2) (RangeSet.rng x2 x3) == Set_empty 0} | v == RangeSet.lem_split}lem_split i1 j2 j1
522:             {v : () -> () -> () | v == Language.Haskell.Liquid.NewProofCombinators.&&&}&&& {v : x1:Int -> x2:{v : Int | x1 <= v} -> x3:{v : Int | x2 <= v} -> {v : () | RangeSet.rng x1 x3 == Set_cup (RangeSet.rng x1 x2) (RangeSet.rng x2 x3)
&& Set_cap (RangeSet.rng x1 x2) (RangeSet.rng x2 x3) == Set_empty 0} | v == RangeSet.lem_split}lem_split i2 i1 j2
523:             {v : () -> () -> () | v == Language.Haskell.Liquid.NewProofCombinators.&&&}&&& {v : x1:Int -> x2:Int -> x3:{v : Int | x2 <= v} -> x4:Int -> {v : () | Set_cap (RangeSet.rng x1 x2) (RangeSet.rng x3 x4) == Set_empty 0} | v == RangeSet.lem_disj}lem_disj  i2 i1 i1 j1     -- discard i2..i1
524:             {v : () -> () -> () | v == Language.Haskell.Liquid.NewProofCombinators.&&&}&&& {v : x1:Int -> x2:Int -> x3:{v : Int | x2 <= v} -> x4:Int -> {v : () | Set_cap (RangeSet.rng x1 x2) (RangeSet.rng x3 x4) == Set_empty 0} | v == RangeSet.lem_disj}lem_disj  i2 j2 j2 j1     -- discard j2..j1
```

## Conclusions¶

Whew. That turned out a lot longer than I'd expected!

On the bright side, we saw how to:

1. Specify the semantics of range-sets,
2. Write equational proofs using plain Haskell code,
3. Avoid boring proof steps using PLE,
4. Verify key properties of operations on range-sets.

Next time we'll finish the series by showing how to use the above lemmas to specify and verify the correctness of Breitner's implementation.

Ranjit Jhala
2017-12-24