PasteRack.org | ||
Paste # 17272 | ||
2019-02-17 10:58:59 | ||
Fork as a new paste. | ||
Paste viewed 95 times. | ||
Tweet | ||
Embed: | ||
#lang pie ;; Decidable (claim Dec (-> U U)) (define Dec (lambda (X) (Either X (-> X Absurd)))) ;; + (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-+))) ;; =consequence (claim =consequence (-> Nat Nat U)) (define =consequence (lambda (n j) (which-Nat n (which-Nat j Trivial (lambda (j-1) Absurd)) (lambda (n-1) (which-Nat j Absurd (lambda (j-1) (= Nat n-1 j-1))))))) ;; =consequence-same (claim =consequence-same (Pi ((n Nat)) (=consequence n n))) (define =consequence-same (lambda (n) (ind-Nat n (lambda (k) (=consequence k k)) sole (lambda (n-1 =consequence_n-1) (same n-1))))) ;; use-Nat= (claim use-Nat= (Pi ((n Nat) (j Nat)) (-> (= Nat n j) (=consequence n j)))) (define use-Nat= (lambda (n j) (lambda (n=j) (replace n=j (lambda (k) (=consequence n k)) (=consequence-same n))))) ;; zero-not-add1 (claim zero-not-add1 (Pi ((n Nat)) (-> (= Nat zero (add1 n)) Absurd))) (define zero-not-add1 (lambda (n) (use-Nat= zero (add1 n)))) ;; <= (claim <= (-> Nat Nat U)) (define <= (lambda (x y) (Sigma ((z Nat)) (= Nat (+ x z) y)))) ;; <=consequence (claim <=consequence (-> Nat Nat U)) (define <=consequence (lambda (n j) (which-Nat n Trivial (lambda (n-1) (which-Nat j Absurd (lambda (j-1) (<= n-1 j-1))))))) ;; use-Nat<= (claim mot-use-Nat<= (Pi ((n Nat) (k Nat)) U)) (define mot-use-Nat<= (lambda (n) (lambda (k) (Pi ((j Nat) (n<=j (<= n j))) (<=consequence k j))))) (claim step-use-Nat<= (Pi ((n Nat) (n-1 Nat)) (-> (mot-use-Nat<= n n-1) (mot-use-Nat<= n (add1 n-1))))) (define step-use-Nat<= (lambda (n) (lambda (n-1 use-Nat<=_n-1) (lambda (j n<=j) (ind-Nat j (lambda (k) (which-Nat k Absurd (lambda (j-1) (<= n-1 j-1)))) (use-Nat= (+ n (car n<=j)) j (cdr n<=j)) ; STUCK HERE: n>0 j-0 n<=j why use-Nat= can't use? TODO))) )) (claim use-Nat<= (Pi ((n Nat) (j Nat)) (-> (<= n j) (<=consequence n j)))) (define use-Nat<= (lambda (n j) (lambda (n<=j) ((ind-Nat n (mot-use-Nat<= n) (the (Pi ((j Nat) (n<=j (<= n j))) Trivial) (lambda (j n<=j) sole)) (step-use-Nat<= n)) j n<=j)))) ;; add1-not-<=zero (claim add1-not-<=zero (Pi ((n Nat)) (-> (<= (add1 n) zero) Absurd))) (define add1-not-<=zero (lambda (n) (use-Nat<= (add1 n) zero))) ;; nat<=? (claim mot-nat<=? (-> Nat U)) (define mot-nat<=? (lambda (k) (Pi ((j Nat)) (Dec (<= k j))))) (claim zero<=? (Pi ((j Nat)) (Dec (<= zero j)))) (define zero<=? (lambda (j) (left (cons j (same j))))) (claim step-nat<=? (Pi ((n-1 Nat)) (-> (mot-nat<=? n-1) (mot-nat<=? (add1 n-1))))) (define step-nat<=? (lambda (n-1 nat<=?_n-1) (lambda (j) (ind-Nat j (lambda (k) (Dec (<= (add1 n-1) k))) (right (add1-not-<=zero n-1)) ; embeded a (<= (add1 n-1) 0) -> Absurd TODO)))) (claim nat<=? (Pi ((n Nat) (j Nat)) (Dec (<= n j)))) (define nat<=? (lambda (n j) ((ind-Nat n mot-nat<=? zero<=? step-nat<=?) j)))