Mercurial > hg > Members > kono > Proof > category
changeset 337:203593ff1e60
add Tree example ( not yet worked )
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 24 Mar 2014 16:45:25 +0700 |
| parents | bda408a05c24 |
| children | 2f21eb997559 |
| files | system-f.agda |
| diffstat | 1 files changed, 36 insertions(+), 10 deletions(-) [+] |
line wrap: on
line diff
--- a/system-f.agda Sun Mar 23 07:31:20 2014 +0700 +++ b/system-f.agda Mon Mar 24 16:45:25 2014 +0700 @@ -101,7 +101,7 @@ Int : {l : Level } ( X : Set l ) → Set l -Int {l} X = X → ( X → X ) → X +Int X = X → ( X → X ) → X Zero : {l : Level } → { X : Set l } → Int X Zero {l} {X} = λ(x : X ) → λ(y : X → X ) → x @@ -128,7 +128,7 @@ lemma13 = refl It : {l : Level} {U : Set l} → U → ( U → U ) → Int U → U -It {l} {U} u f t = t u f +It u f t = t u f R : {l : Level} { U X : Set l} → U → ( U → Int X → U ) → Int _ → U R {l} {U} {X} u v t = π1 ( It {suc l} {U × Int X} (< u , Zero >) (λ (x : U × Int X) → < v (π1 x) (π2 x) , S (π2 x) > ) t ) @@ -139,6 +139,10 @@ -- RInt : {l : Level} { U X : Set l} → Int U → ( Int U → Int X → Int U ) → Int U → Int U -- RInt {l} {U} {X} u v t = π1 ( It {suc l} {Int U × Int X} (< u , Zero >) (λ (x : Int U × Int X) → < v (π1 x) (π2 x) , S (π2 x) > ) t ) +-- bad adder which modifies input type +add' : {l : Level} {X : Set l} → Int (Int X) → Int X → Int X +add' x y = It y S x + add : {l : Level} {X : Set l} → Int X → Int X → Int X add x y = λ z t → x (y z t) t @@ -186,11 +190,27 @@ l3 : {l : Level} {X X' : Set l} → List (Int X) (X') l3 = Cons n3 l2 -ListIt : {l : Level} {U W X : Set l} → W → ( U → W → W ) → List U W → W -ListIt w f t = t w f +ListIt : {l : Level} {U W : Set l} → (X : Set l) → W → ( U → W → W ) → List U W → W +ListIt _ w f t = t w f + +-- Car : {l : Level} {U : Set l} {X : Set l} → List U _ → U → U +-- Car x z = ListIt z ( λ u w → u ) x + +-- Cdr : {l : Level} {U : Set l} {X : Set l} → List U _ → List U X +-- Cdr w = λ x → λ y → w x (λ x y → y) + +-- lemma181 :{l : Level} {U : Set l} {X : Set l} → Car Zero l2 ≡ n2 +-- lemma181 = refl + +-- lemma182 :{l : Level} {U : Set l} {X : Set l} → Cdr l2 ≡ l1 +-- lemma182 = refl Nullp : {l : Level} {U : Set (suc l)} { X : Set (suc l)} → List U (Bool X) → Bool _ -Nullp {l} {U} {X} list = ListIt {suc l} {U} {Bool _} {X} (T X) (λ u w → (F X)) list +Nullp {_} {_} {X} list = ListIt X (T X) (λ u w → (F X)) list + +-- bad append +Append' : {l : Level} {U X : Set l} → List U (List U X) → List U X → List U X +Append' {_} {_} {X} x y = ListIt X y Cons x Append : {l : Level} {U : Set l} {X : Set l} → List U X → List U X → List U X Append x y = λ s t → x (y s t) t @@ -199,7 +219,7 @@ lemma18 = refl Reverse : {l : Level} {U : Set l} {X : Set l} → List U (List U X) → List U X -Reverse {l} {U} {X} x = ListIt {_} {U} {List U _} {X} Nil ( λ u w → Append w (Cons u Nil) ) x +Reverse {l} {U} {X} x = ListIt X Nil ( λ u w → Append w (Cons u Nil) ) x lemma19 :{l : Level} {U : Set l} {X : Set l} → Reverse {_} {Int U} {X} l3 ≡ Cons n1 (Cons n2 (Cons n3 Nil)) lemma19 = refl @@ -207,11 +227,17 @@ Tree : {l : Level} → Set l → Set l → Set l Tree {l} = λ( U X : Set l) → X → ( (U → X) → X ) → X -NilTree : {l : Level} (U : Set l) (X : Set l) → Tree U X -NilTree U X = λ(x : X) → λ(y : (U → X) → X) → x +NilTree : {l : Level} {U : Set l} {X : Set l} → Tree U X +NilTree {l} {U} {X} = λ(x : X) → λ(y : (U → X) → X) → x -Collect : {l : Level} (U : Set l) (X : Set l) → (U → X → ((U → X) → X) → X ) → Tree U X -Collect U X f = λ(x : X) → λ(y : (U → X) → X) → y (λ(z : U) → f z x y ) +Collect : {l : Level} {U : Set l} {X : Set l} → (U → Tree U X ) → Tree U X +Collect {l} {U} {X} f = λ(x : X) → λ(y : (U → X) → X) → y (λ(z : U) → f z x y ) TreeIt : {l : Level} {U W X : Set l} → W → ( (U → W) → W ) → Tree U W → W TreeIt w h t = t w h + +t0 : {l : Level} {X X' : Set l} → Tree (Bool X) X' +t0 {l} {X} {X'} = NilTree + +t1 : {l : Level} {X X' : Set l} → Tree (Bool X) X' +t1 {l} {X} {X'} = NilTree -- Collect (λ b → D b NilTree (λ c → Collect NilTree NilTree ))