Cleanup proofs
author Yasutaka Higa Tue, 03 Feb 2015 12:57:13 +0900 ac45d065cbf2 2412ccc94117 agda/delta.agda agda/delta/functor.agda agda/delta/monad.agda agda/deltaM/functor.agda agda/deltaM/monad.agda agda/laws.agda 6 files changed, 31 insertions(+), 120 deletions(-) [+]
line wrap: on
line diff
```--- 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))
-
-
{-
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 (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```
```--- 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
}```
```--- 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
-

tailDelta-is-nt : {l : Level} {A B : Set l} {n : Nat}
@@ -87,15 +86,15 @@

--- 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 = delta-association-law;
left-unity-law  = delta-left-unity-law ;
right-unity-law = \x -> (sym (delta-right-unity-law x)) }
```
```--- 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
}
-
-```
```--- 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)))
}
-
-
-
-```
```--- 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```