twice-vec.rkt

#lang pie

; "imports"
;
(claim + (-> Nat Nat Nat))

(define +
  (lambda (n j)
    (iter-Nat n
      j
      (lambda (n-1)
        (add1 n-1)))))


(claim twice (-> Nat Nat))

(define twice
  (lambda (n)
    (+ n n)))


(claim double (-> Nat Nat))

(define double
  (lambda (n)
    (iter-Nat n
      0
      (+ 2))))

(claim mot-twice=double
  (-> Nat U))

(define mot-twice=double
  (lambda (k)
    (= Nat
      (twice k)
      (double k))))

(claim mot-step-twice=double
  (-> Nat Nat
    U))

(define mot-step-twice=double
   (lambda (n-1)
    (lambda (k)
     (= Nat
      (add1 k)
      (add1 (add1 (double n-1)))))))

(claim add1+=+add1
       (Pi ((n Nat)
            (j Nat))
           (= Nat
              (add1 (+ n j))
              (+ n (add1 j)))))

(claim mot-add1+=+add1
       (-> Nat Nat U))

(define mot-add1+=+add1
  (lambda (j k)
    (= Nat
       (add1 (+ k j))
       (+ k (add1 j)))))

(claim step-add1+=+add1
       (Pi ((j Nat)
            (n-1 Nat))
           (-> (mot-add1+=+add1 j n-1)
               (mot-add1+=+add1 j (add1 n-1)))))

(define step-add1+=+add1
  (lambda (j n-1)
    (lambda (add1+=+add1-n-1)
      (cong add1+=+add1-n-1 (+ 1)))))

(define add1+=+add1
  (lambda (n j)
    (ind-Nat n
             (mot-add1+=+add1 j)
             (same (add1 j))
             (step-add1+=+add1 j))))

(claim step-twice=double
  (Pi ((n-1 Nat))
       (-> (mot-twice=double n-1)
         (mot-twice=double (add1 n-1)))))

(define step-twice=double
  (lambda (n-1)
    (lambda (twice=double-n-1)
      (replace (add1+=+add1 n-1 n-1)
        (mot-step-twice=double n-1)
        (cong twice=double-n-1 (+ 2))))))

(claim twice=double
       (Pi ((n Nat))
            (= Nat (twice n) (double n))))

(define twice=double
  (lambda (n)
    (ind-Nat n
      mot-twice=double
      (same 0)
      step-twice=double)))

;; Exercise
;;

(claim base-double-Vec
  (Pi ((E U))
      (-> (Vec E zero)
          (Vec E (double zero)))))

(define base-double-Vec
  (lambda (E)
    (lambda (es)
      vecnil)))

(claim mot-double-Vec
       (-> U Nat
           U))

(define mot-double-Vec
  (lambda (E k)
    (-> (Vec E k)
        (Vec E (double k)))))

(claim step-double-Vec
       (Pi ((E U)
            (l-1 Nat))
           (-> (-> (Vec E l-1)
                   (Vec E (double l-1)))
               (-> (Vec E (add1 l-1))
                   (Vec E (double (add1 l-1)))))))

(define step-double-Vec
  (lambda (E l-1)
    (lambda (double-Vec-l-1)
      (lambda (es)
        (vec:: (head es)
               (vec:: (head es)
                      (double-Vec-l-1 (tail es))))))))


(claim double-Vec
  (Pi ((E U)
       (l Nat))
      (-> (Vec E l)
          (Vec E (double l)))))

(define double-Vec
  (lambda (E l)
    (ind-Nat l
             (mot-double-Vec E)
             (base-double-Vec E)
             (step-double-Vec E))))


;; using twice, the hard one
;;
(claim twice-Vec
  (Pi ((E U)
       (l Nat))
      (-> (Vec E l)
          (Vec E (twice l)))))

(define twice-Vec
  (lambda (E l)
    (lambda (es)
      (replace (symm (twice=double l))
               (lambda (k)
                 (Vec E k))
               (double-Vec E l es)))))