#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                                    
; =========================