#lang pie ; ========================= ; Methoden-Definitionen ; ========================= (claim + (-> Nat Nat Nat)) (define + (lambda (x y) (iter-Nat x y (lambda (y-1) (add1 y-1))))) (claim incr (-> Nat Nat)) (define incr (lambda (x) (iter-Nat x 1 (+ 1)))) ; ========================= ; incr=add1 ; ========================= ; step-incr=add1 mit cong (claim base-incr=add1 (= Nat (incr zero) (add1 zero))) (define base-incr=add1 (same (add1 zero))) (claim mot-incr=add1 (-> Nat U)) (define mot-incr=add1 (lambda (n) (= Nat (incr n) (add1 n)))) (claim step-incr=add1 (Pi ((n-1 Nat)) (-> (= Nat (incr n-1) (add1 n-1)) (= Nat (incr (add1 n-1)) (add1 (add1 n-1)))))) ;-------------------------------------------------------- (define step-incr=add1 (lambda (n-1) (lambda (incr=add1n-1) ; IV (cong incr=add1n-1 (+ 1))))) (claim incr=add1 (Pi ((n Nat)) (= Nat (incr n) (add1 n)))) (define incr=add1 (lambda (n) (ind-Nat n mot-incr=add1 base-incr=add1 step-incr=add1))) (claim step-replace_incr=add1 (Pi ((n-1 Nat)) (-> (= Nat (incr n-1) (add1 n-1)) (= Nat (add1 (incr n-1)) (add1 (add1 n-1)))))) (claim mot-replace_incr=add1 (-> Nat Nat U)) (define mot-replace_incr=add1 (lambda (n-1 k) (= Nat (add1 (incr n-1)) (add1 k)))) (define step-replace_incr=add1 (lambda (n-1) (lambda (incr=add1) (replace incr=add1 (mot-replace_incr=add1 n-1) (same (add1 (incr n-1))))))) (claim replace_incr=add1 (Pi ((n Nat)) (= Nat (incr n) (add1 n)))) (define replace_incr=add1 (lambda (n) (ind-Nat n mot-incr=add1 base-incr=add1 step-replace_incr=add1))) ; ========================= ; twice=double ; ========================= (claim twice (-> Nat Nat)) (define twice (lambda (n) (+ n n))) (claim double (-> Nat Nat)) (define double (lambda (n) (iter-Nat n 0 (+ 2)))) (claim twice=double (Pi ((n Nat)) (= Nat (twice n) (double n)))) (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) (cong add1+=+add1 (+ 1))))) (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 (k) (= Nat (twice k) (double k)))) (claim step-twice=double (Pi ((n-1 Nat)) (-> (mot-twice=double n-1) (mot-twice=double (add1 n-1))))) (claim mot-step-twice=double (-> Nat Nat U)) (define mot-step-twice=double (lambda (n-1 k) (= Nat (add1 k) (add1 (add1 (double n-1)))))) (define step-twice=double (lambda (n-1) (lambda (twice=double) (replace (add1+=+add1 n-1 n-1) (mot-step-twice=double n-1) (cong twice=double (+ 2)))))) (define twice=double (lambda (n) (ind-Nat n mot-twice=double (same zero) step-twice=double))) ; ========================= ; double-Vec und twice-Vec ; ========================= (claim double-Vec (Pi ((E U) (l Nat)) (-> (Vec E l) (Vec E (double l))))) (claim mot-double-Vec (-> U Nat U)) (define mot-double-Vec (lambda (E k) (-> (Vec E k) (Vec E (double k))))) (claim base-double-Vec (Pi ((E U)) (-> (Vec E zero) (Vec E (double zero))))) (define base-double-Vec (lambda (E) (lambda (es) 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) (lambda (es) (vec:: (head es) (vec:: (head es) (double-Vec (tail es)))))))) (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 (es) (replace (symm (twice=double l)) (lambda (k) (Vec E k)) (double-Vec E l es))))) ; ========================= ; THE END ; =========================