List-Compress, must break up spec

[michaelbjames]

Consider this program specification:

compress ::
  -- The output is always shorter or equal to the input
  (xs: List Int -> {List Int | ((len _v < len xs) || (_v == xs)) && elems _v == elems xs}) ^

  -- If it's empty list, then it should produce nothing
  (xs: {List Int | len _v == 0} -> {List Int | _v == Nil}) ^

  -- A couple base cases
  (xs: {List Int | _v == (Cons 1 Nil) || _v == (Cons 1 (Cons 1 Nil))} -> {List Int | _v == (Cons 1 Nil)}) ^

  -- QUESTIONABLE
  (xs: {List Int | _v == Cons 2 (Cons 1 Nil) || _v == (Cons 3 (Cons 2 (Cons 1 Nil))) } -> {List Int | _v == xs})
compress = \xs .  -- defn Taken from synquid-verified PLDI16 solutions
  match xs with
    Nil -> Nil
    Cons x3 x4 ->
      match compress x4 with
        Nil -> Cons x3 Nil
        Cons x10 x11 ->
          if x3 == x10
            then compress x4
            else Cons x3 (Cons x10 x11)

It fails to check that compress satisfies the last refinement intersection with the error:

  Cannot find sufficiently strong refinements
  when checking
  x4 :: {PList Int <True>|(_v == (Cons 2 ((Cons 1 (Nil)))) || _v == (Cons 3 ((Cons 2 ((Cons 1 (Nil))))))) && (len _v >= 0 && len _v < len xs)}
  in
  \xs . 
    match xs with
      Cons x3 x4 -> 
        match compress x4 with

Confusingly, to me, this program checks if I change the last spec. Instead of: (xs: {List Int | _v == Cons 2 (Cons 1 Nil) || _v == (Cons 3 (Cons 2 (Cons 1 Nil))) } -> {List Int | _v == xs}) I break it in two, to:

  (xs: {List Int | _v == Cons 2 (Cons 1 Nil)} -> {List Int | _v == xs}) ^
  (xs: {List Int | _v == Cons 3 (Cons 2 (Cons 1 Nil))} -> {List Int | _v == xs})

The whole program and refinement passes.

I'm not sure why this is.

[michaelbjames]

The program will also check if that "questionable" spec is expanded to be entirely inductive: (xs: {List Int | _v == Nil || _v == (Cons 1 Nil) || _v == Cons 2 (Cons 1 Nil) || _v == (Cons 3 (Cons 2 (Cons 1 Nil))) } -> {List Int | _v == xs})

This raises the question if we would want a normalization process to prevent this kind of spec problem.