#lang pie

;; <=
(claim zero<=?
  (-> Nat Nat))
(define zero<=?
  (lambda (j)
    1))

(claim step-<=?
  (-> Nat (-> Nat Nat)
      (-> Nat Nat)))
(define step-<=?
  (lambda (n-1 n-1<=?)
    (lambda (j)
      (rec-Nat j
        0
        (lambda (j-1 almost_j-1)
          (n-1<=? j-1))))))


(claim <=? (-> Nat Nat Nat))
(define <=?
  (lambda (n j)
    ((rec-Nat n
       zero<=?
       step-<=?) j)))

;; insert :: Ord a => a -> [a] -> [a]
;; insert x [] = [x]
;; insert x (y:ys) 
;;         |  x < y = x:y:ys
;;         | otherwise = y : insert x ys

(claim step-insert
  (-> Nat Nat (List Nat) (List Nat)
      (List Nat)))
(define step-insert
  (lambda (x)
    (lambda (y ys result_ys)
      (which-Nat (<=? x y)
        (:: y result_ys)
        (lambda (_)
          (:: x (:: y ys) ) )))))

(claim insert
  (-> Nat (List Nat)
      (List Nat)))
(define insert
  (lambda (x list)
    (rec-List list
      (:: x nil)
      (step-insert x))))