Mercurial > hg > Members > kono > Proof > category
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) ∎