changeset 16:228147b118d6

sss
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 09 Jul 2013 10:42:36 +0900
parents 730a4a59a7bd
children 03d39cabebb7
files list-nat.agda
diffstat 1 files changed, 16 insertions(+), 45 deletions(-) [+]
line wrap: on
line diff
--- a/list-nat.agda	Tue Jul 09 10:36:20 2013 +0900
+++ b/list-nat.agda	Tue Jul 09 10:42:36 2013 +0900
@@ -1,6 +1,4 @@
-module list-nat where
-                                                                        
-open import Level
+module category where
 
 
 postulate a : Set
@@ -26,10 +24,9 @@
 
 infixr 20  _==_
 
-data _==_ {n} {A : Set n} :  List A -> List A -> Set n where
+data _==_ {A : Set} :  List A -> List A -> Set where
       reflection  : {x : List A} -> x == x
       eq-cons : {x y : List A} { a : A } -> x ==  y -> ( a :: x ) == ( a :: y )
-      trans-list : {x y z : List A} { a : A } -> x ==  y -> y == z -> x == z
 --      eq-nil  : [] == []
 
 list-id-l : { A : Set } -> { x : List A} ->  [] ++ x == x
@@ -50,57 +47,31 @@
 
 
 
---open  import  Relation.Binary.PropositionalEquality
---open ≡-Reasoning
-
-cong1 : ∀{a} {A : Set a } {b} { B : Set b } ->
-   ( f : A -> B ) -> {x : A } -> {y : A} -> x == y -> f x == f y
-cong1 f refl = refl
+open  import  Relation.Binary.PropositionalEquality
+open ≡-Reasoning
 
-module ==-Reasoning {n} (A : Set n) where
-
-
-  infixr  2 _∎
-  infixr 2 _==⟨_⟩_
-  infix  1 begin_
+cong1 : {A : Set } { B : Set } ->
+   ( f : A -> B ) -> {x : A } -> {y : A} -> x ≡ y -> f x ≡ f y
+cong1 f refl = refl
 
 
-  data _IsRelatedTo_ {a} {A1 : Set a} (x : A1) {b} {B : Set b} (y : B) :
-                     Set where
-    relTo : (x≈y : x == y  ) → x IsRelatedTo y
-
-  begin_ : ∀ {a} {A1 : Set a} {x : A1} {b} {B : Set b} {y : B} →
-           x IsRelatedTo y →  x == y 
-  begin relTo x≈y = x≈y
-
-  _==⟨_⟩_ : ∀ {a} {A1 : Set a} (x : A1) {b} {B : Set b} {y : B}
-             {c} {C : Set c} {z : C} →
-            x == y  → y IsRelatedTo z → x IsRelatedTo z
-  _ ==⟨ x≈y ⟩ relTo y≈z = relTo (trans-list x≈y y≈z)
-
-  _∎ : ∀ {a} {A1 : Set a} (x : A1) → x IsRelatedTo x
-  _∎ _ = relTo reflection
-
-++-assoc : {A : Set} ( xs ys zs : List A ) -> (xs ++ ys) ++ zs == xs ++ (ys ++ zs)
-++-assoc [] ys zs = {A : Set} -> let open ==-Reasoning A in
-  begin -- to prove ([] ++ ys) ++ zs == [] ++ (ys ++ zs)
+++-assoc : {A : Set} ( xs ys zs : List A ) -> (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
+++-assoc [] ys zs = begin -- to prove ([] ++ ys) ++ zs ≡ [] ++ (ys ++ zs)
    ( [] ++ ys ) ++ zs
-  ==⟨ reflection ⟩
+  ≡⟨ refl ⟩
     ys ++ zs
-  ==⟨ reflection ⟩
+  ≡⟨ refl ⟩
     [] ++ ( ys ++ zs )

-  
-++-assoc (x :: xs) ys zs = {A : Set} -> let open  ==-Reasoning A in
-  begin -- to prove ((x :: xs) ++ ys) ++ zs ≡ (x :: xs) ++ (ys ++ zs)
+++-assoc (x :: xs) ys zs = begin -- to prove ((x :: xs) ++ ys) ++ zs ≡ (x :: xs) ++ (ys ++ zs)
     ((x :: xs) ++ ys) ++ zs
-  ==⟨ reflection ⟩
+  ≡⟨ refl ⟩
      (x :: (xs ++ ys)) ++ zs
-  ==⟨ reflection ⟩
+  ≡⟨ refl ⟩
     x :: ((xs ++ ys) ++ zs)
-  ==⟨ cong1 (_::_ x) (++-assoc xs ys zs) ⟩ 
+  ≡⟨ cong1 (_::_ x) (++-assoc xs ys zs) ⟩ 
     x :: (xs ++ (ys ++ zs))
-  ==⟨ reflection ⟩
+  ≡⟨ refl ⟩
     (x :: xs) ++ (ys ++ zs)