> module Project3B(justify)
>  where
>  import SequenceUtilities(multiplex, reps)
>  import IOutilities(spaces)

justify delivers a string constructed by concatenating the strings
in its second argument, inserting at least one space between each
pair of adjacent strings and with enough extra spaces (uniformly
distributed across the gaps between strings, as nearly as possible)
to make the length of the delivered string equal the number specified
in the first argument
Exception: justify n ws = unwords ws, if length(unwords ws) > n
examples:
  justify 12 ["The", "purpose"] = "The  purpose"
  justify 12 ["of", "computing"] = "of computing"
  justify 6 ["is"] = "is    "
  justify 6 ["insight,"] = "insight,"

>  justify :: Int -> [String] -> String
>  justify lineLength ws =
>    (concat . multiplex) [ws, uniformFill, extraFill]
>    where
>    numChars = (length . concat) ws
>    numGaps = max 0 (length(ws) - 1)
>    uniformFill = reps numGaps (spaces spacesPerGap)
>    extraFill = reps numExtras " "
>    numSpacesNeeded =
>      numGaps + max 0 (lineLength - numGaps - numChars)
>    spacesPerGap = numSpacesNeeded `div` numGaps
>    numExtras = numSpacesNeeded - sum(reps numGaps spacesPerGap)
>      -- note: numGaps*spacesPerGap would fail when numGaps is zero
>      --       if it were computed (because spacesPerGap would fail)

Theorem J (a property of the function justify):
  if ws::[String] and length(unwords ws) <= n,
  then length(justify n ws) = n

proof:
  The following namings (mostly abbreviations of terms in the
  definition of justify) make proof more compact: 
    c  = numChars = length(concat ws)
    g  = numGaps  = max 0 (length ws - 1)
    sn = numSpacesNeeded = g + max 0 (n - g - c)
    sg = spacesPerGap = sn `div` g
    ne = numExtras = sn - sum(reps g sg)
    uf = uniformFill
    ef = extraFill
    e  = length(concat ef)
    u  = length(concat uf)
  Note: In this context, Theorem U says length(unwords ws) = g + c.
        So, the hypothesis length(unwords ws) <= n means n >= g + c.

  length(justify n ws)
   = length(concat(multiplex[ws, uf, ef]))            -- def justify
   = sum[length w | w <- multiplex[ws, uf, ef]]       -- Thm C
   = sum[length w | w <- p(concat[ws, uf, ef])]
         -- where p permutes the sequence delivered by concat (Thm M)
   = sum[length w | w <- concat[ws, uf, ef]]
                               -- order of addends doesn't affect sum
   = sum[length w | w <- ws ++ uf ++ ef]                -- def concat
   = length(concat(ws ++ uf ++ ef))                     -- Thm C
   = length(concat(ws) ++ concat(uf) ++ concat(ef))     -- Thm D-concat
   = length(concat ws) + length(concat uf) +
                         length(concat ef)              -- Thm D-length
   = c + length(concat(reps g (spaces sg))) +           -- defs uf,
         length(concat(reps ne " "))                            ef

Now consder two cases: (1) length(ws) <= 1; (2) length(ws) > 1

Case 1: length(ws) <= 1 (hence, g = max 0 (length(ws) - 1) = 0)
Continuing with the above sequence of equaliites:
   = c + length(concat(reps 0 (spaces sg))) +           -- sub 0 for g,
         length(concat(reps (sn - sum(reps 0 sg)) " "))    def ne
   = c + length(concat([ ])) +                          -- def reps,
         length(concat(reps sn " "))                           sum
   = c + 0 +                                            -- def concat,
         sum[length ss | ss <- reps sn " "]                Thm C
   = c + sum[1 | ss <- reps sn " "]                     -- length " "
   = c + 1*sn                                           -- def reps
   = c + 1*(g + max 0 (n - g - c))                      -- def sn
   = c + 1*(0 + max 0 (n - 0 - c))                      -- 0 for g
   = c + 1*(0 + (n - 0 - c))                            -- n >= c + g
   = n                                                  -- algebra
                                                      QED Case 1
Case 2: length(ws) > 1 (hence, g = max 0 (length(ws) - 1) > 0)
Continuing with the sequence of equaliites prior to Case 1:
   = c + sum[length ss | ss <- reps g (spaces sg)] +
         sum[length ss | ss <- reps (sn - sum(reps g sg)) " "] --def ne
   = c + sum[sg | ss <- reps g (spaces sg)]             -- def spaces,
       + sum[ 1 | ss <- reps (sn - sum(reps g sg)) " "]        reps
   = c + sg*g + 1*(sn - g*sg)                           -- def reps
   = c + sn                                             -- algebra
   = c + g + max 0 (n - g - c)                          -- def sn
   = c + g + (n - g - c)                                -- n >= c + g
   = n                                                  -- algebra
                                                      QED