Little typer notes

dev

#!/usr/bin/env bash

main () {
  local filename="the-little-typer.rkt"

  tmux \
    new-window   "nix-shell --run 'vim $filename'"\; \
    split-window "nix-shell --run 'entr -c racket $filename <<< $filename'"\; \
    select-layout even-horizontal\; \
    split-window -v "nix-shell --run 'racket -i'"
    select-layout even-vertical\;
}

main

setup

#!/usr/bin/env bash

set -exo pipefail

raco pkg install pie || raco pkg update pie

shell.nix

{ nixpkgs ? import <nixpkgs> {} }:
  nixpkgs.mkShell {
    name = "the-little-typer-notes";
    buildInputs = with nixpkgs; [
      entr
      racket
    ];
  }

the-little-typer.rkt

#lang pie

(claim one
  Nat)
(define one
  (add1 zero))

(claim vegetables
  (Pair Atom Atom))
(define vegetables
  (cons 'celery 'carrot))

; (claim forever
;   (-> Nat
;       Atom))
; (define forever
;   (lambda (and-ever)
;     (forever and-ever)))

(claim step-+
  (-> Nat
      Nat))
(define step-+
  (lambda (n-1)
    (add1 n-1)))

(claim +
  (-> Nat Nat
      Nat))
(define +
  (lambda (n j)
    (iter-Nat n
      j
      step-+)))

(claim Pear
  U)
(define Pear
  (Pair Nat Nat))

(claim Pear-maker
  U)
(define Pear-maker
  (-> Nat Nat
      Pear))

(claim elim-Pear
  (-> Pear Pear-maker
    Pear))
(define elim-Pear
  (lambda (pear maker)
    (maker (car pear) (cdr pear))))

(claim pearwise-+
  (-> Pear Pear
      Pear))
(define pearwise-+
  (lambda (anjou bosc)
    (elim-Pear anjou
      (lambda (a1 b1)
        (elim-Pear bosc
          (lambda (a2 b2)
            (cons
              (+ a1 a2)
              (+ b1 b2))))))))

(claim gauss
  (-> Nat Nat))
(define gauss
  (lambda (n)
    (rec-Nat n
      0
      (lambda (n-1 gaussn-1)
        (+ (add1 n-1) gaussn-1)))))

(claim step-*
  (-> Nat Nat Nat
      Nat))
(define step-*
  (lambda (j n-1 *n-1)
    (+ j *n-1)))

(claim *
  (-> Nat Nat
      Nat))
(define *
  (lambda (a b)
    (rec-Nat a
      0
      (step-* b))))

;(claim kar
;  (-> (Pair Nat Nat)
;      Nat))
;(define kar
;  (lambda (p)
;    (elim-Pair
;      Nat Nat
;      Nat
;      p
;      (lambda (a d)
;        a))))

;(claim kdr
;  (-> (Pair Nat nat)
;      Nat))
;(define kdr
;  (lambda (p)
;    (elim-Pair
;      Nat Nat
;      Nat
;      p
;      (lambda (a d)
;        d))))

;(claim swap
;  (-> (Pair Nat Atom)
;      (Pair Atom Nat)))
;(define swap
;  (lambda (p)
;    (elim-Pair
;      Nat Atom
;      (Pair Atom Nat)
;      p
;      (lambda (a d)
;        (cons d a)))))

(claim flip
  (Pi ((A U)
       (D U))
    (-> (Pair A D)
        (Pair D A))))
(define flip
  (lambda (A D)
    (lambda (p)
      (cons (cdr p) (car p)))))

(claim elim-Pair
  (Pi ((A U)
       (D U)
       (X U))
    (-> (Pair A D)
            (-> A D
              X)
            X)))
(define elim-Pair
  (lambda (A D X)
    (lambda (p f)
      (f (car p) (cdr p)))))

(claim twin
  (Pi ((A U))
    (-> A
        (Pair A A))))
(define twin
  (lambda (A a)
    (cons a a)))

(claim twin-Atom
  (-> Atom
      (Pair Atom Atom)))
(define twin-Atom
  (twin Atom))

(claim expectations
  (List Atom))
(define expectations
  (:: 'cooked
    (:: 'eaten
      (:: 'tried-cleaning
        (:: 'understood
          (:: 'slept nil))))))

(claim rugbrød
  (List Atom))
(define rugbrød
  (:: 'rye-flour
    (:: 'rye-kernels
      (:: 'water
        (:: 'sourdough
          (:: 'salt nil))))))

(claim toppings
  (List Atom))
(define toppings
  (:: 'potato
    (:: 'butter nil)))

(claim condiments
  (List Atom))
(define condiments
  (:: 'chives
    (:: 'mayonnaise nil)))

(claim step-length
  (Pi ((E U))
    (-> E (List E) Nat
        Nat)))
(define step-length
  (lambda (E e es length-es)
    (add1 length-es)))

(claim length
  (Pi ((E U))
    (-> (List E)
      Nat)))
(define length
  (lambda (E es)
    (rec-List es
      0
      (step-length E))))

(claim step-append
  (Pi ((E U))
    (-> E (List E) (List E)
          (List E))))
(define step-append
  (lambda (E e es res)
    (:: e res)))

(claim append
  (Pi ((E U))
    (-> (List E) (List E)
        (List E))))
(define append
  (lambda (E start end)
    (rec-List start
      end
      (step-append E))))

(claim snoc
  (Pi ((E U))
    (-> (List E) E
        (List E))))
(define snoc
  (lambda (E es e)
    (append E es (:: e nil))))

(claim step-concat
  (Pi ((E U))
    (-> E (List E) (List E)
        (List E))))
(define step-concat
  (lambda (E e es concat-es)
    (snoc E concat-es e)))

(claim concat
  (Pi ((E U))
    (-> (List E) (List E)
        (List E))))
(define concat
  (lambda (E start end)
    (rec-List end
      start
      (step-concat E))))

(claim step-reverse
  (Pi ((E U))
    (-> E (List E) (List E)
        (List E))))
(define step-reverse
  (lambda (E e es reverse-es)
    (snoc E reverse-es e)))

(claim reverse
  (Pi ((E U))
    (-> (List E)
        (List E))))
(define reverse
  (lambda (E es)
    (rec-List es
      (the (List E) nil)
      (step-reverse E))))

(claim kartoffelmad
  (List Atom))
(define kartoffelmad
  (append Atom
    (concat Atom
      toppings condiments)
    (reverse Atom
      (:: 'plate
        (:: 'rye-bread nil)))))

(claim first-of-one
  (Pi ((E U))
    (-> (Vec E 1)
        E)))
(define first-of-one
  (lambda (E es)
    (head es)))

(claim first-of-two
  (Pi ((E U))
    (-> (Vec E 2)
        E)))
(define first-of-two
  (lambda (E es)
    (head es)))

(claim first
  (Pi ((E U)
       (l Nat))
    (-> (Vec E (add1 l))
        E)))
(define first
  (lambda (E l es)
    (head es)))

(claim pi-only-first
  (Pi ((E U)
       (l Nat)
       (es (Vec E (add1 l))))
    E))

(claim rest
  (Pi ((E U)
       (l Nat)
       (es (Vec E (add1 l))))
    (Vec E l)))
(define rest
  (lambda (E l es)
    (tail es)))

(claim mot-peas
  (-> Nat
    U))
(define mot-peas
  (lambda (k)
    (Vec Atom k)))

(claim step-peas
  (Pi ((l-1 Nat))
    (-> (mot-peas l-1)
        (mot-peas (add1 l-1)))))
(define step-peas
  (lambda (l-1 peas-l-1)
    (vec:: 'pea peas-l-1)))

#| (claim peas |#
#|   (Pi ((how-many-peas Nat)) |#
#|     (Vec Atom how-many-peas))) |#
#| (define peas |#
#|   (lambda (how-many-peas) |#
#|     (ind-Nat how-many-peas |#
#|       mot-peas |#
#|       vecnil |#
#|       step-peas))) |#

(claim peas
  (Pi ((n Nat))
    (Vec Atom n)))
(define peas
  (lambda (n)
    (ind-Nat n
      (lambda (k)
        (Vec Atom k))
      vecnil
      (lambda (n-1 peas-n-1)
        (vec:: 'pea peas-n-1)))))

(claim also-rec-Nat
  (Pi ((X U))
    (-> Nat
        X
        (-> Nat X
            X)
        X)))
(define also-rec-Nat
  (lambda (X n x step)
    (ind-Nat n
      (lambda (k)
        X)
      x
      step)))

(claim base-last
  (Pi ((E U))
    (-> (Vec E 1)
        E)))
(define base-last
  (lambda (E es)
    (head es)))

(claim mot-last
  (-> U Nat
      U))
(define mot-last
  (lambda (E k)
    (-> (Vec E (+ 1 k))
        E)))

(claim step-last
  (Pi ((E U)
       (l-1 Nat))
    (-> (mot-last E l-1)
        (mot-last E (+ 1 l-1)))))
(define step-last
  (lambda (E l-1 lastl-1)
    (lambda (es)
      (lastl-1 (tail es)))))

(claim last
  (Pi ((E U)
       (l Nat))
    (-> (Vec E (+ 1 l))
        E)))
(define last
  (lambda (E l)
    (ind-Nat l
      (mot-last E)
      (base-last E)
      (step-last E))))

(claim base-drop-last
  (Pi ((E U))
      (-> (Vec E (+ 1 0))
          (Vec E 0))))
(define base-drop-last
  (lambda (E es)
    vecnil))

(claim mot-drop-last
  (-> U Nat
      U))
(define mot-drop-last
  (lambda (E k)
    (-> (Vec E (+ 1 k))
        (Vec E k))))

(claim step-drop-last
  (Pi ((E U)
       (l-1 Nat))
      (-> (mot-drop-last E l-1)
          (mot-drop-last E (+ 1 l-1)))))
(define step-drop-last
  (lambda (E l-1)
    (lambda (drop-lastl-1)
      (lambda (es)
        (vec:: (head es)
               (drop-lastl-1 (tail es)))))))

(claim drop-last
  (Pi ((E U)
       (l Nat))
      (-> (Vec E (+ 1 l))
          (Vec E l))))
(define drop-last
  (lambda (E l)
    (ind-Nat l
      (mot-drop-last E)
      (base-drop-last E)
      (step-drop-last E))))

; (drop-last Atom
;   (+ 1 (+ 1 0)))

; (ind-Nat (+ 1 (+ 1 0))
;   (mot-drop-last Atom)
;   (base-drop-last Atom)
;   (step-drop-last Atom))

; (ind-Nat (+ 1 (+ 1 0))
;  (lambda (k) (-> (Vec Atom (+ 1 k)) (Vec Atom k)))
;  (lambda (es) vecnil)
;  (lambda (l-1 drop-lastl-1)
;    (lambda (es)
;      (vec::
;        (head es)
;        (drop-lastl-1 (tail es))))))

;(lambda (es)
;  (vec::
;    (head es)
;    ((ind-Nat (+ 1 0)
;      (lambda (k) (-> (Vec Atom (+ 1 k)) (Vec Atom k)))
;      (lambda (es) vecnil)
;      (lambda (l-1 drop-lastl-1)
;        (lambda (es)
;          (vec::
;            (head es)
;            (drop-lastl-1 (tail es)))))) (tail es))))

;(lambda (es)
;  (vec::
;    (head es)
;    ((lambda (es)
;      (vec::
;        (head es)
;        (drop-lastl-1 (tail es)))) (tail es))))

;(lambda (es)
;  (vec::
;    (head es)
;    ((lambda (es)
;      (vec::
;        (head es)
;        ((ind-Nat 0
;          (lambda (k) (-> (Vec Atom (+ 1 k)) (Vec Atom k)))
;          (lambda (es) vecnil)
;          (lambda (l-1 drop-lastl-1)
;            (lambda (es)
;              (vec::
;                (head es)
;                (drop-lastl-1 (tail es)))))) (tail es)))) (tail es))))

;(lambda (es)
;  (vec::
;    (head es)
;    ((lambda (es)
;      (vec::
;        (head es)
;        ((lambda (es) vecnil) (tail es)))) (tail es))))

;(lambda (es)
;  (vec::
;    (head es)
;    (vec:: (head (tail es)) vecnil)))


; (+ 1)
; ((lambda (n j) (iter-Nat n j (lambda (n-1) (add1 n-1)))) 1)
; (lambda (j) (iter-Nat 1 j (lambda (n-1) (add1 n-1))))
; (lambda (j) ((lambda (n-1) (add1 n-1)) (iter-Nat 0 j (lambda (n-1) (add1 n-1)))))
; (lambda (j) ((lambda (n-1) (add1 n-1)) j))
; (lambda (j) (add1 j))

(claim incr
  (-> Nat
    Nat))
(define incr
  (lambda (n)
    (iter-Nat n
      1
      (+ 1))))

; (incr 0)
; ((lambda (n) (iter-Nat n 1 (+ 1))) 0)
; (iter-Nat 0 1 (+ 1))
; 1

; (incr 3)
; ((lambda (n) (iter-Nat n 1 (+ 1))) 3)
; (iter-Nat 3 1 (+ 1))
; (iter-Nat 3 1 (lambda (n-1) (add1 n-1)))
; (lambda (n-1) (add1 n-1)) (iter-Nat 2 1 (lambda (n-1) (add1 n-1)))
; ((lambda (n-1) (add1 n-1)) (lambda (n-1) (add1 n-1)) (iter-Nat 1 1 (lambda (n-1) (add1 n-1))))
; ((lambda (n-1) (add1 n-1)) ((lambda (n-1) (add1 n-1)) (lambda (n-1) (add1 n-1)) (iter-Nat 0 1 (lambda (n-1) (add1 n-1)))))
; ((lambda (n-1) (add1 n-1)) ((lambda (n-1) (add1 n-1)) (lambda (n-1) (add1 n-1)) 1))
; ((lambda (n-1) (add1 n-1)) ((lambda (n-1) (add1 n-1)) (add1 1)))
; ((lambda (n-1) (add1 n-1)) ((lambda (n-1) (add1 (add1 1)))))
; (add1 (add1 (add1 1)))

; "the-little-typer.rkt"> (the (-> Nat Nat) (lambda (n) (+ 1 n)))
; (the (→ Nat
;        Nat)
;   (λ (n)
;     (add1 n)))
; "the-little-typer.rkt"> (the (-> Nat Nat) (lambda (n) (+ n 1)))
; (the (→ Nat
;        Nat)
;   (λ (n)
;     (iter-Nat n
;        (the Nat 1)
;        (λ (n-1)
;          (add1 n-1)))))

; "the-little-typer.rkt"> (the (Pi ((n Nat)) (= Nat n (+ 0 n))) (lambda (n) (same n)))
; (the (Π ((n Nat))
;       (= Nat n n))
;   (λ (n)
;     (same n)))

(claim +1=add1
  (Pi ((n Nat))
    (= Nat (+ 1 n) (add1 n))))
(define +1=add1
  (lambda (n)
    (same (add1 n))))

(claim incr=add1
  (Pi ((n Nat))
    (= Nat (incr n) (add1 n))))
(define incr=add1
  (lambda (n)
    (ind-Nat n
      (lambda (n) (= Nat (incr n) (add1 n)))
      (same (incr 0))
      (lambda (n-1 incr=add1n-1)
        (cong incr=add1n-1
          (+ 1))))))
          ; OR
          ; (the (-> Nat Nat) (lambda (n) (add1 n))))))))
          ; But not?
          ; (the (-> Nat Nat) (lambda (n) (incr n))))))))

; (incr=add1 2)
; Let's just say '(incr 0)' = 1
; (ind-Nat 2 _ (same 1) (lambda (n-1 incr=add1n-1) (cong incr=add1n-1 (+ 1))))
; (cong (ind-Nat 1 _ (same 1) (lambda (n-1 incr=add1n-1) (cong incr=add1n-1 (+ 1)))) (+ 1))
; (cong (cong (ind-Nat 0 _ (same 1) (lambda (n-1 incr=add1n-1) (cong incr=add1n-1 (+ 1)))) (+ 1)) (+ 1))
; (cong (cong (same 1) (+ 1)) (+ 1))
; (cong (same (+ 1 1)) (+ 1))
; (same (+ 1 (+ 1 1)))
; (same (+ 1 2))
; (same 3)

(claim +-right-identity
  (Pi ((n Nat))
    (= Nat n (+ n 0))))
(define +-right-identity
  (lambda (n)
    (ind-Nat n
      (lambda (n-1) (= Nat n-1 (+ n-1 0)))
      (same 0)
      (lambda (n-1 +-right-identity_n-1)
        (cong +-right-identity_n-1 (+ 1))))))

(claim +-left-identity
  (Pi ((n Nat))
    (= Nat n (+ 0 n))))
(define +-left-identity
  (lambda (n)
    (ind-Nat n
      (lambda (n-1) (= Nat n-1 (+ 0 n-1)))
      (same 0)
      (lambda (n-1 +-left-identity_n-1)
        (cong +-left-identity_n-1 (+ 1))))))

#| (claim +-commutative |#
#|   (Pi ((n Nat) (m Nat)) |#
#|     (= Nat (+ n m) (+ m n)))) |#
#| (define +-commutative |#
#|   (lambda (n m) |#
#|     (ind-Nat n |#
#|       (lambda (n-1) (= Nat (+ n-1 m) (+ m n-1))) |#
#|       (+-right-identity m) |#
#|       (lambda (n-1 +-commutative_n-1) |#
#|         (cong +-commutative_n-1 (+ 1)))))) |#

#| Results in: |#
#| Expected |#
#|   (= Nat |#
#|     (add1 (iter-Nat n-1 |#
#|              (the Nat m) |#
#|              (λ (n-1₁) |#
#|                (add1 n-1₁)))) |#
#|     (iter-Nat m |#
#|        (the Nat |#
#|          (add1 n-1)) |#
#|        (λ (n-1₁) |#
#|          (add1 n-1₁)))) |#
#| but given |#
#|   (= Nat |#
#|     (add1 (iter-Nat n-1 |#
#|              (the Nat m) |#
#|              (λ (n-1₁) |#
#|                (add1 n-1₁)))) |#
#|     (add1 (iter-Nat m |#
#|              (the Nat n-1) |#
#|              (λ (n-1₁) |#
#|                (add1 n-1₁))))) |#

#| I'm missing something here. Moving on for now ... |#

(claim mot-incr=add1
  (-> Nat Nat
      U))
(define mot-incr=add1
  (lambda (n-1 n)
    (= Nat (add1 (incr n-1)) (add1 n))))

(claim step-incr=add1
  (Pi ((n-1 Nat))
    (-> (= Nat
           (incr n-1)
           (add1 n-1))
      (= Nat
         (add1 (incr n-1))
         (add1 (add1 n-1))))))
(define step-incr=add1
  (lambda (n-1)
    (lambda (incr=add1_n-1)
      (replace incr=add1_n-1
        (mot-incr=add1 n-1)
        (same (add1 (incr n-1)))))))

(claim double
  (-> Nat
    Nat))
(define double
  (lambda (n)
    (iter-Nat n
      0
      (lambda (n-1) (add1 (add1 n-1))))))

(claim twice
  (-> Nat
    Nat))
(define twice
  (lambda (n)
    (+ n n)))

(claim mot-add1+=+add1
  (-> Nat Nat U))
(define mot-add1+=+add1
  (lambda (j n-1)
    (= Nat (add1 (+ n-1 j)) (+ n-1 (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 add1+=+add1_n-1)
    (cong add1+=+add1_n-1
      (+ 1))))

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

(claim mot-twice=double
  (-> Nat
      U))
(define mot-twice=double
  (lambda (n)
    (= Nat (twice n) (double n))))

(claim mot-step-twice=double
  (-> Nat Nat
      U))
(define mot-step-twice=double
  (lambda (n-1 n)
    (= Nat
       (add1 n)
       (add1 (add1 (double n-1))))))

(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 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)))

(claim mot-double-Vec
  (-> U Nat
      U))
(define mot-double-Vec
  (lambda (E l-1)
    (-> (Vec E l-1)
      (Vec E (double l-1)))))

(claim base-double-Vec
  (Pi ((E U))
    (-> (Vec E 0)
      (Vec E (double 0)))))
(define base-double-Vec
  (lambda (E v0)
    vecnil))

(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 (vec)
        (vec::
          (head vec)
          (vec::
            (head vec)
            (double-Vec_l-1 (tail vec))))))))

(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))))

(claim twice-Vec
  (Pi ((E U)
       (l Nat))
  (-> (Vec E l)
      (Vec E (twice l)))))
(define twice-Vec
  (lambda (E l)
    (lambda (vec)
      (replace (symm (twice=double l))
        (lambda (n) (Vec E n))
        (double-Vec E l vec)))))

(claim more-expectations
  (Vec Atom 3))
(define more-expectations
  (vec:: 'need-induction
    (vec:: 'understood-induction
      (vec:: 'built-function vecnil))))

(claim mot-list->vec
  (Pi ((E U))
    (-> (List E) U)))
(define mot-list->vec
  (lambda (E)
    (lambda (mot-list->vec_es)
      (Vec E (length E mot-list->vec_es)))))

(claim step-list->vec
  (Pi ((E U) (e E) (es (List E)))
    (-> (Vec E (length E es))
      (Vec E (+ 1 (length E es))))))
(define step-list->vec
  (lambda (E)
    (lambda (e es step-list->vec_es)
      (vec:: e step-list->vec_es))))

(claim list->vec
  (Pi ((E U) (es (List E)))
    (Vec E (length E es))))
(define list->vec
  (lambda (E es)
    (ind-List es
      (mot-list->vec E)
      vecnil
      (step-list->vec E))))

(claim mot-replicate
  (-> U Nat
      U))
(define mot-replicate
  (lambda (E n) (Vec E n)))

(claim step-replicate
  (Pi ((E U) (e E) (n-1 Nat))
    (-> (Vec E n-1)
        (Vec E (+ 1 n-1)))))
(define step-replicate
  (lambda (E e n-1)
    (lambda (step-replicate_n-1)
      (vec:: e step-replicate_n-1))))

(claim replicate
  (Pi ((E U) (n Nat))
      (-> E
          (Vec E n))))
(define replicate
  (lambda (E n)
    (lambda (e)
      (ind-Nat n
        (mot-replicate E)
        vecnil
        (step-replicate E e)))))

(claim mot-vec-append
  (Pi ((E U) (m Nat) (k Nat))
    (-> (Vec E k)
      U)))
(define mot-vec-append
  (lambda (E m)
    (lambda (k es)
      (Vec E (+ k m)))))

(claim step-vec-append
  (Pi ((E U) (m Nat) (k Nat) (h E) (t (Vec E k)))
    (-> (mot-vec-append E m k t)
      (mot-vec-append E m (+ 1 k) (vec:: h t)))))
(define step-vec-append
  (lambda (E m)
    (lambda (k h t)
      (lambda (step-vec-append_t)
        (vec:: h step-vec-append_t)))))

(claim vec-append
  (Pi ((E U) (l Nat) (m Nat))
    (-> (Vec E l) (Vec E m)
      (Vec E (+ l m)))))
(define vec-append
  (lambda (E l m)
    (lambda (es end)
      (ind-Vec l es
        (mot-vec-append E m)
        end
        (step-vec-append E m)))))

(claim mot-vec->list
  (Pi ((E U) (l Nat))
    (-> (Vec E l)
      U)))
(define mot-vec->list
  (lambda (E l)
    (lambda (es)
      (List E))))

(claim step-vec->list
  (Pi ((E U) (k Nat))
    (-> E (Vec E k) (List E)
      (List E))))
(define step-vec->list
  (lambda (E k)
    (lambda (e es step-vec->list_es)
      (:: e step-vec->list_es))))

(claim vec->list
  (Pi ((E U) (l Nat))
    (-> (Vec E l)
      (List E))))
(define vec->list
  (lambda (E l)
    (lambda (es)
      (ind-Vec l es
        (mot-vec->list E)
        nil
        (step-vec->list E)))))

(claim mot-list->vec->list=
  (Pi ((E U))
    (-> (List E)
      U)))
(define mot-list->vec->list=
  (lambda (E)
    (lambda (es)
      (= (List E)
        es
        (vec->list E
          (length E es)
          (list->vec E es))))))

(claim step-list->vec->list=
  (Pi ((E U) (e E) (es (List E)))
    (-> (mot-list->vec->list= E es)
      (mot-list->vec->list= E (:: e es)))))
(define step-list->vec->list=
  (lambda (E e es step-list->vec->list=_es)
    (cong
      step-list->vec->list=_es
      (the (-> (List E) (List E)) (lambda (es) (:: e es))))))

(claim list->vec->list=
  (Pi ((E U) (es (List E)))
    (= (List E)
      es
      (vec->list E
        (length E es)
        (list->vec E es)))))
(define list->vec->list=
  (lambda (E es)
    (ind-List es
      (mot-list->vec->list= E)
      (same nil)
      (step-list->vec->list= E))))