# HG changeset patch # User Yasutaka Higa # Date 1422935833 -32400 # Node ID d205ff1e406f905168bce67b3b69dec7a63fddae # Parent ac45d065cbf260e948f084ee0d4283532139a68d Cleanup proofs diff -r ac45d065cbf2 -r d205ff1e406f agda/delta.agda --- a/agda/delta.agda Tue Feb 03 12:46:20 2015 +0900 +++ b/agda/delta.agda Tue Feb 03 12:57:13 2015 +0900 @@ -1,12 +1,12 @@ +open import Level +open import Relation.Binary.PropositionalEquality +open ≡-Reasoning + open import list open import basic open import nat open import laws -open import Level -open import Relation.Binary.PropositionalEquality -open ≡-Reasoning - module delta where data Delta {l : Level} (A : Set l) : (Nat -> (Set l)) where @@ -38,9 +38,6 @@ delta-eta {n = O} x = mono x delta-eta {n = (S n)} x = delta x (delta-eta {n = n} x) - - - delta-mu : {l : Level} {A : Set l} {n : Nat} -> (Delta (Delta A (S n)) (S n)) -> Delta A (S n) delta-mu (mono x) = x delta-mu (delta x d) = delta (headDelta x) (delta-mu (delta-fmap tailDelta d)) @@ -48,10 +45,6 @@ delta-bind : {l : Level} {A B : Set l} {n : Nat} -> (Delta A (S n)) -> (A -> Delta B (S n)) -> Delta B (S n) delta-bind d f = delta-mu (delta-fmap f d) ---delta-bind (mono x) f = f x ---delta-bind (delta x d) f = delta (headDelta (f x)) (tailDelta (f x)) - - {- -- Monad (Haskell) delta-return : {l : Level} {A : Set l} -> A -> Delta A (S O) @@ -61,67 +54,4 @@ (x : Delta A n) -> (f : A -> (Delta B n)) -> (Delta B n) d >>= f = delta-bind d f --} - -{- --- proofs - --- sub-proofs - -n-tail-plus : {l : Level} {A : Set l} -> (n : Nat) -> ((n-tail {l} {A} n) ∙ tailDelta) ≡ n-tail (S n) -n-tail-plus O = refl -n-tail-plus (S n) = begin - n-tail (S n) ∙ tailDelta ≡⟨ refl ⟩ - (tailDelta ∙ (n-tail n)) ∙ tailDelta ≡⟨ refl ⟩ - tailDelta ∙ ((n-tail n) ∙ tailDelta) ≡⟨ cong (\t -> tailDelta ∙ t) (n-tail-plus n) ⟩ - n-tail (S (S n)) - ∎ - -n-tail-add : {l : Level} {A : Set l} {d : Delta A} -> (n m : Nat) -> (n-tail {l} {A} n) ∙ (n-tail m) ≡ n-tail (n + m) -n-tail-add O m = refl -n-tail-add (S n) O = begin - n-tail (S n) ∙ n-tail O ≡⟨ refl ⟩ - n-tail (S n) ≡⟨ cong (\n -> n-tail n) (nat-add-right-zero (S n))⟩ - n-tail (S n + O) - ∎ -n-tail-add {l} {A} {d} (S n) (S m) = begin - n-tail (S n) ∙ n-tail (S m) ≡⟨ refl ⟩ - (tailDelta ∙ (n-tail n)) ∙ n-tail (S m) ≡⟨ refl ⟩ - tailDelta ∙ ((n-tail n) ∙ n-tail (S m)) ≡⟨ cong (\t -> tailDelta ∙ t) (n-tail-add {l} {A} {d} n (S m)) ⟩ - tailDelta ∙ (n-tail (n + (S m))) ≡⟨ refl ⟩ - n-tail (S (n + S m)) ≡⟨ refl ⟩ - n-tail (S n + S m) ∎ - -tail-delta-to-mono : {l : Level} {A : Set l} -> (n : Nat) -> (x : A) -> - (n-tail n) (mono x) ≡ (mono x) -tail-delta-to-mono O x = refl -tail-delta-to-mono (S n) x = begin - n-tail (S n) (mono x) ≡⟨ refl ⟩ - tailDelta (n-tail n (mono x)) ≡⟨ refl ⟩ - tailDelta (n-tail n (mono x)) ≡⟨ cong (\t -> tailDelta t) (tail-delta-to-mono n x) ⟩ - tailDelta (mono x) ≡⟨ refl ⟩ - mono x ∎ - -head-delta-natural-transformation : {l : Level} {A B : Set l} - -> (f : A -> B) -> (d : Delta A) -> headDelta (delta-fmap f d) ≡ f (headDelta d) -head-delta-natural-transformation f (mono x) = refl -head-delta-natural-transformation f (delta x d) = refl - -n-tail-natural-transformation : {l : Level} {A B : Set l} - -> (n : Nat) -> (f : A -> B) -> (d : Delta A) -> n-tail n (delta-fmap f d) ≡ delta-fmap f (n-tail n d) -n-tail-natural-transformation O f d = refl -n-tail-natural-transformation (S n) f (mono x) = begin - n-tail (S n) (delta-fmap f (mono x)) ≡⟨ refl ⟩ - n-tail (S n) (mono (f x)) ≡⟨ tail-delta-to-mono (S n) (f x) ⟩ - (mono (f x)) ≡⟨ refl ⟩ - delta-fmap f (mono x) ≡⟨ cong (\d -> delta-fmap f d) (sym (tail-delta-to-mono (S n) x)) ⟩ - delta-fmap f (n-tail (S n) (mono x)) ∎ -n-tail-natural-transformation (S n) f (delta x d) = begin - n-tail (S n) (delta-fmap f (delta x d)) ≡⟨ refl ⟩ - n-tail (S n) (delta (f x) (delta-fmap f d)) ≡⟨ cong (\t -> t (delta (f x) (delta-fmap f d))) (sym (n-tail-plus n)) ⟩ - ((n-tail n) ∙ tailDelta) (delta (f x) (delta-fmap f d)) ≡⟨ refl ⟩ - n-tail n (delta-fmap f d) ≡⟨ n-tail-natural-transformation n f d ⟩ - delta-fmap f (n-tail n d) ≡⟨ refl ⟩ - delta-fmap f (((n-tail n) ∙ tailDelta) (delta x d)) ≡⟨ cong (\t -> delta-fmap f (t (delta x d))) (n-tail-plus n) ⟩ - delta-fmap f (n-tail (S n) (delta x d)) ∎ --} +-} \ No newline at end of file diff -r ac45d065cbf2 -r d205ff1e406f agda/delta/functor.agda --- a/agda/delta/functor.agda Tue Feb 03 12:46:20 2015 +0900 +++ b/agda/delta/functor.agda Tue Feb 03 12:57:13 2015 +0900 @@ -11,20 +11,21 @@ -- Functor-laws --- Functor-law-1 : T(id) = id' -functor-law-1 : {l : Level} {A : Set l} {n : Nat} -> (d : Delta A (S n)) -> (delta-fmap id) d ≡ id d -functor-law-1 (mono x) = refl -functor-law-1 (delta x d) = cong (delta x) (functor-law-1 d) +-- functor-law 1 : T(id) = id' +delta-preserve-id : {l : Level} {A : Set l} {n : Nat} -> (d : Delta A (S n)) -> (delta-fmap id) d ≡ id d +delta-preserve-id (mono x) = refl +delta-preserve-id (delta x d) = cong (delta x) (delta-preserve-id d) --- Functor-law-2 : T(f . g) = T(f) . T(g) -functor-law-2 : {l : Level} {n : Nat} {A B C : Set l} -> + +-- functor-law 2 : T(f . g) = T(f) . T(g) +delta-covariant : {l : Level} {n : Nat} {A B C : Set l} -> (f : B -> C) -> (g : A -> B) -> (d : Delta A (S n)) -> (delta-fmap (f ∙ g)) d ≡ ((delta-fmap f) ∙ (delta-fmap g)) d -functor-law-2 f g (mono x) = refl -functor-law-2 f g (delta x d) = cong (delta (f (g x))) (functor-law-2 f g d) +delta-covariant f g (mono x) = refl +delta-covariant f g (delta x d) = cong (delta (f (g x))) (delta-covariant f g d) -delta-fmap-equiv : {l : Level} {A B : Set l} {n : Nat} {f g : A -> B} +delta-fmap-equiv : {l : Level} {A B : Set l} {n : Nat} {f g : A -> B} (eq : (x : A) -> f x ≡ g x) -> (d : Delta A (S n)) -> delta-fmap f d ≡ delta-fmap g d delta-fmap-equiv {l} {A} {B} {O} {f} {g} eq (mono x) = begin @@ -41,7 +42,7 @@ delta-is-functor : {l : Level} {n : Nat} -> Functor {l} (\A -> Delta A (S n)) delta-is-functor = record { fmap = delta-fmap - ;preserve-id = functor-law-1 - ; covariant = \f g -> functor-law-2 g f + ; preserve-id = delta-preserve-id + ; covariant = \f g -> delta-covariant g f ; fmap-equiv = delta-fmap-equiv } diff -r ac45d065cbf2 -r d205ff1e406f agda/delta/monad.agda --- a/agda/delta/monad.agda Tue Feb 03 12:46:20 2015 +0900 +++ b/agda/delta/monad.agda Tue Feb 03 12:57:13 2015 +0900 @@ -1,14 +1,13 @@ +open import Level +open import Relation.Binary.PropositionalEquality +open ≡-Reasoning + open import basic open import delta open import delta.functor open import nat open import laws - -open import Level -open import Relation.Binary.PropositionalEquality -open ≡-Reasoning - module delta.monad where tailDelta-is-nt : {l : Level} {A B : Set l} {n : Nat} @@ -87,15 +86,15 @@ -- Monad-laws (Category) --- monad-law-1 : join . delta-fmap join = join . join -monad-law-1 : {l : Level} {A : Set l} {n : Nat} (d : Delta (Delta (Delta A (S n)) (S n)) (S n)) -> +-- association-law : join . delta-fmap join = join . join +delta-association-law : {l : Level} {A : Set l} {n : Nat} (d : Delta (Delta (Delta A (S n)) (S n)) (S n)) -> ((delta-mu ∙ (delta-fmap delta-mu)) d) ≡ ((delta-mu ∙ delta-mu) d) -monad-law-1 {n = O} (mono d) = refl -monad-law-1 {n = S n} (delta (delta (delta x d) dd) ds) = begin +delta-association-law {n = O} (mono d) = refl +delta-association-law {n = S n} (delta (delta (delta x d) dd) ds) = begin delta x (delta-mu (delta-fmap tailDelta (delta-fmap delta-mu ds))) ≡⟨ cong (\de -> delta x (delta-mu de)) (delta-fmap-mu-to-tail n n ds) ⟩ delta x (delta-mu (delta-fmap delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds)))) - ≡⟨ cong (\de -> delta x de) (monad-law-1 (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))) ⟩ + ≡⟨ cong (\de -> delta x de) (delta-association-law (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))) ⟩ delta x (delta-mu (delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds)))) ≡⟨ cong (\de -> delta x (delta-mu de)) (delta-mu-is-nt tailDelta (delta-fmap tailDelta ds) ) ⟩ delta x (delta-mu (delta-fmap tailDelta (delta-mu (delta-fmap tailDelta ds)))) @@ -133,7 +132,7 @@ delta-mu (delta (delta-eta x) (delta-fmap delta-eta d)) ≡⟨ refl ⟩ delta (headDelta {n = S n} (delta-eta x)) (delta-mu (delta-fmap tailDelta (delta-fmap delta-eta d))) ≡⟨ refl ⟩ delta x (delta-mu (delta-fmap tailDelta (delta-fmap delta-eta d))) - ≡⟨ cong (\de -> delta x (delta-mu de)) (sym (functor-law-2 tailDelta delta-eta d)) ⟩ + ≡⟨ cong (\de -> delta x (delta-mu de)) (sym (delta-covariant tailDelta delta-eta d)) ⟩ delta x (delta-mu (delta-fmap (tailDelta ∙ delta-eta {n = S n}) d)) ≡⟨ refl ⟩ delta x (delta-mu (delta-fmap (delta-eta {n = n}) d)) ≡⟨ cong (\de -> delta x de) (delta-left-unity-law d) ⟩ delta x d ≡⟨ refl ⟩ @@ -146,7 +145,7 @@ mu = delta-mu; eta-is-nt = delta-eta-is-nt; mu-is-nt = delta-mu-is-nt; - association-law = monad-law-1; + association-law = delta-association-law; left-unity-law = delta-left-unity-law ; right-unity-law = \x -> (sym (delta-right-unity-law x)) } diff -r ac45d065cbf2 -r d205ff1e406f agda/deltaM/functor.agda --- a/agda/deltaM/functor.agda Tue Feb 03 12:46:20 2015 +0900 +++ b/agda/deltaM/functor.agda Tue Feb 03 12:57:13 2015 +0900 @@ -75,7 +75,7 @@ (deltaM-fmap f ∙ deltaM-fmap g) (deltaM (delta x d)) ∎ -deltaM-fmap-equiv : {l : Level} {A B : Set l} {n : Nat} +deltaM-fmap-equiv : {l : Level} {A B : Set l} {n : Nat} {T : Set l -> Set l} {F : Functor T} {M : Monad T F} {f g : A -> B} (eq : (x : A) -> f x ≡ g x) -> (d : DeltaM M A (S n)) -> @@ -104,5 +104,3 @@ ; covariant = (\f g -> deltaM-covariant {F = F} g f) ; fmap-equiv = deltaM-fmap-equiv } - - diff -r ac45d065cbf2 -r d205ff1e406f agda/deltaM/monad.agda --- a/agda/deltaM/monad.agda Tue Feb 03 12:46:20 2015 +0900 +++ b/agda/deltaM/monad.agda Tue Feb 03 12:57:13 2015 +0900 @@ -32,6 +32,7 @@ headDeltaM-with-f {n = O} f (deltaM (mono x)) = refl headDeltaM-with-f {n = S n} f (deltaM (delta x d)) = refl + tailDeltaM-with-f : {l : Level} {A B : Set l} {n : Nat} {T : Set l -> Set l} {F : Functor T} {M : Monad T F} (f : A -> B) -> (d : (DeltaM M A (S (S n)))) -> @@ -39,21 +40,6 @@ tailDeltaM-with-f {n = O} f (deltaM (delta x d)) = refl tailDeltaM-with-f {n = S n} f (deltaM (delta x d)) = refl -headDeltaM-with-deltaM-eta : {l : Level} {A : Set l} {n : Nat} - {T : Set l -> Set l} {F : Functor T} {M : Monad T F} -> - (x : DeltaM M A (S n)) -> - ((headDeltaM {n = n} {M = M}) ∙ deltaM-eta) x ≡ eta M x -headDeltaM-with-deltaM-eta {n = O} (deltaM (mono x)) = refl -headDeltaM-with-deltaM-eta {n = S n} (deltaM (delta x d)) = refl - - -fmap-tailDeltaM-with-deltaM-eta : {l : Level} {A : Set l} {n : Nat} - {T : Set l -> Set l} {F : Functor T} {M : Monad T F} -> - (d : DeltaM M A (S n)) -> - deltaM-fmap ((tailDeltaM {n = n} {M = M} ) ∙ deltaM-eta) d ≡ deltaM-fmap (deltaM-eta) d -fmap-tailDeltaM-with-deltaM-eta {n = O} d = refl -fmap-tailDeltaM-with-deltaM-eta {n = S n} d = refl - fmap-headDeltaM-with-deltaM-mu : {l : Level} {A : Set l} {n : Nat} @@ -455,7 +441,3 @@ ; left-unity-law = deltaM-left-unity-law ; right-unity-law = (\x -> (sym (deltaM-right-unity-law x))) } - - - - diff -r ac45d065cbf2 -r d205ff1e406f agda/laws.agda --- a/agda/laws.agda Tue Feb 03 12:46:20 2015 +0900 +++ b/agda/laws.agda Tue Feb 03 12:57:13 2015 +0900 @@ -1,5 +1,6 @@ open import Relation.Binary.PropositionalEquality open import Level + open import basic module laws where