정렬 된 목록의 연결 증명은 스테인리스의 정렬 된 목록입니다.

스테인리스 (이전에는 Leon이라고 함)에서 확인하려는 배열을 정렬하기위한 다음 코드가 있습니다.

import stainless.lang._
import stainless.collection._

object QuickSort {

  def isSorted(list: List[BigInt]): Boolean = list match {
    case Cons(x, xs @ Cons(y, _)) => x <= y && isSorted(xs)
    case _ => true
  }

  def quickSort(list: List[BigInt]): List[BigInt] = (list match {
        case Nil() => Nil[BigInt]()
        case Cons(x, xs) => par(x, Nil(), Nil(), xs)
  }) ensuring { res => isSorted(res) }


  def par(x: BigInt, l: List[BigInt], r: List[BigInt], ls: List[BigInt]): List[BigInt] = {
    require(l.forall(_ <= x) && r.forall(_ >= x))
    ls match {
      case Nil() => quickSort(l) ++ Cons(x, quickSort(r))
      case Cons(x2, xs2) => if (x2 <= x) par(x, Cons(x2, l), r, xs2) else par(x, l, Cons(x2, r), xs2)
    }
  } ensuring {res => isSorted(res)}
}

나는 여기에서 갈 방향이 많이 있지만 (확인에 성공하지 못하기 때문에) 제공된 힌트를 사용하여 확인이 성공해야한다고 생각하며 왜 그렇지 않은지 알고 싶습니다. 나는 나 자신을 설명한다.

분명히 par 함수를 확인하기 위해 두 경우가 isSorted 사후 조건을 개별적으로 의미한다는 것을 증명해야합니다. 이제 두 번째 경우에 재귀 호출이 포함되어 있으므로 사후 조건을 암시하는 것이 분명합니다. par의 첫 번째 경우에는 왼쪽 및 오른쪽 하위 배열이 정렬되고 전제 조건은 모든 요소가 피벗에 대해 정렬된다는 것을 알려줍니다.

이 마지막 부분은 연결 목록도 정렬되어 있음을 내 의견으로 암시해야합니다. 그렇다면 왜 확인되지 않습니까? 스테인리스에게이를 확인하도록 어떻게 지시 할 수 있습니까? 스테인리스 작업을 용이하게하기 위해 길이와 크기에 대한 힌트를 추가해야합니까?

편집하다:

def concatIsSorted(l1 : List[BigInt],l2 : List[BigInt],pivot : BigInt) : Boolean = {
    require(isSorted(l1) && isSorted(l2) && l1.forall(_ <= pivot) && l2.forall(_ >= pivot))
    isSorted(l1 ++ Cons(pivot,l2)) because{
      l1 match{
        case Nil() => isSorted(Cons(pivot,l2))
        case Cons(h,Nil()) => h <= pivot && isSorted(Cons(pivot,l2))
        case Cons(h,t) => h <= t.head && concatIsSorted(t,l2,pivot)
      }     
    }   
  }.holds