Commit 37fca919 authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

[dk_monads] enforce monadic laws by rewriting

parent 33a1e36e
......@@ -58,39 +58,28 @@ comp :
(; monadic laws ;)
monad_neutral_left :
M : (cc.uT -> cc.uT) ->
A : cc.uT ->
B : cc.uT ->
a : cc.eT A ->
f : (cc.eT A -> cc.eT (M B)) ->
istrue (equal (M B)
(bind M A B (return M A a) f)
(f a)).
monad_neutral_right :
M : (cc.uT -> cc.uT) ->
A : cc.uT ->
m : cc.eT (M A) ->
istrue (equal (M A)
(bind M A A m (return M A))
m).
monad_bind_comp :
M : (cc.uT -> cc.uT) ->
A : cc.uT ->
B : cc.uT ->
C : cc.uT ->
f : (cc.eT A -> cc.eT (M B)) ->
g : (cc.eT B -> cc.eT (M C)) ->
m : cc.eT (M A) ->
istrue (equal (M C)
(bind M B C (bind M A B m f) g)
(bind M A C m (comp M A B C f g))).
[ M : (cc.uT -> cc.uT) ,
A : cc.uT ,
B : cc.uT ,
a : cc.eT A ,
f : (cc.eT A -> cc.eT (M B)) ]
bind M A B (return _ _ a) f --> f a.
[ M : (cc.uT -> cc.uT),
A : cc.uT,
m : cc.eT (M A) ]
bind M _ _ m (return M A) --> m.
[ M : (cc.uT -> cc.uT),
A : cc.uT,
B : cc.uT,
C : cc.uT,
f : (cc.eT A -> cc.eT (M B)),
g : (cc.eT B -> cc.eT (M C)),
m : cc.eT (M A) ]
bind M B C (bind _ A _ m f) g
-->
bind M A C m (comp M A B C f g).
(; option type ;)
......@@ -98,38 +87,6 @@ option : cc.uT -> cc.uT.
None : A : cc.uT -> cc.eT (option A).
Some : A : cc.uT -> cc.eT A -> cc.eT (option A).
option_dep_case :
A : cc.uT ->
RET : (cc.eT (option A) -> cc.uT) ->
None_case : cc.eT (RET (None A)) ->
Some_case : (a : cc.eT A -> cc.eT (RET (Some A a))) ->
m : cc.eT (option A) ->
cc.eT (RET m).
[A : cc.uT,
RET : cc.eT (option A) -> cc.uT,
None_case : cc.eT (RET (None A)),
Some_case : a : cc.eT A -> cc.eT (RET (Some A a))]
option_dep_case A RET None_case Some_case (None _) --> None_case
[A : cc.uT,
RET : cc.eT (option A) -> cc.uT,
None_case : cc.eT (RET (None A)),
Some_case : a : cc.eT A -> cc.eT (RET (Some A a)),
a : cc.eT A]
option_dep_case A RET None_case Some_case (Some _ a) --> Some_case a.
option_case :
RET : cc.uT ->
A : cc.uT ->
None_case : cc.eT RET ->
Some_case : (cc.eT A -> cc.eT RET) ->
cc.eT (option A) ->
cc.eT RET
:=
RET : cc.uT =>
A : cc.uT =>
option_dep_case A (m : cc.eT (option A) => RET).
(; the option monad ;)
[] return option --> Some.
......@@ -141,76 +98,12 @@ option_case :
B : cc.uT, f : cc.eT A -> cc.eT (option B)]
bind option A B (Some _ a) f --> f a.
(; Alternative definition of bind option leading to the same proofs :
[A : cc.uT, m : cc.eT (option A),
B : cc.uT, f : cc.eT A -> cc.eT (option B)]
bind option A B m f -->
option_case (option B) A (None B) f m.
;)
[A : cc.uT, B : cc.uT, a : cc.eT A, f : cc.eT A -> cc.eT (option B)]
monad_neutral_left option A B a f --> refl (option B) (f a).
[A : cc.uT, m : cc.eT (option A)]
monad_neutral_right option A m -->
option_dep_case
A
(m : cc.eT (option A) =>
istruetype (equal (option A)
(bind option A A m (return option A))
m))
(refl (option A) (None A))
(a : cc.eT A => refl (option A) (Some A a))
m.
[A : cc.uT,
B : cc.uT,
C : cc.uT,
f : (cc.eT A -> cc.eT (option B)),
g : (cc.eT B -> cc.eT (option C)),
m : cc.eT (option A)]
monad_bind_comp option A B C f g m -->
option_dep_case
A
(m : cc.eT (option A) =>
istruetype (equal (option C)
(bind option B C (bind option A B m f) g)
(bind option A C m (comp option A B C f g))))
(refl (option C) (None C))
(a : cc.eT A => refl (option C) (bind option B C (f a) g))
m.
(; list type ;)
list : cc.uT -> cc.uT.
Nil : A : cc.uT -> cc.eT (list A).
Cons : A : cc.uT -> cc.eT A -> cc.eT (list A) -> cc.eT (list A).
list_dep_case :
A : cc.uT ->
RET : (cc.eT (list A) -> cc.uT) ->
Nil_case : cc.eT (RET (Nil A)) ->
Cons_case : (a : cc.eT A -> l : cc.eT (list A) -> cc.eT (RET (Cons A a l))) ->
l : cc.eT (list A) ->
cc.eT (RET l).
[A : cc.uT,
RET : cc.eT (list A) -> cc.uT,
Nil_case : cc.eT (RET (Nil A)),
Cons_case : a : cc.eT A -> l : cc.eT (list A) -> cc.eT (RET (Cons A a l))]
list_dep_case A RET Nil_case Cons_case (Nil _) --> Nil_case
[A : cc.uT,
RET : cc.eT (list A) -> cc.uT,
Nil_case : cc.eT (RET (Nil A)),
Cons_case : a : cc.eT A -> l : cc.eT (list A) -> cc.eT (RET (Cons A a l)),
a : cc.eT A, l : cc.eT (list A)]
list_dep_case A RET Nil_case Cons_case (Cons _ a l) --> Cons_case a l.
append : A : cc.uT -> cc.eT (list A) -> cc.eT (list A) -> cc.eT (list A).
[A : cc.uT, l2 : cc.eT (list A)]
append A (Nil _) l2 --> l2
......@@ -220,14 +113,6 @@ append : A : cc.uT -> cc.eT (list A) -> cc.eT (list A) -> cc.eT (list A).
[A : cc.uT, l1 : cc.eT (list A)]
append A l1 (Nil _) --> l1.
[A : cc.uT,
a1 : cc.eT A, a2 : cc.eT A,
l1 : cc.eT (list A), l2 : cc.eT (list A)]
istruetype (equal (list A) (Cons _ a1 l1) (Cons _ a2 l2)) -->
dk_tuple.Tuple
(istruetype (equal A a1 a2))
(istruetype (equal (list A) l1 l2)).
(; the list monad ;)
[] return list --> A : cc.uT => a : cc.eT A => Cons A a (Nil A).
......@@ -238,51 +123,3 @@ append : A : cc.uT -> cc.eT (list A) -> cc.eT (list A) -> cc.eT (list A).
[A : cc.uT, a : cc.eT A, l : cc.eT (list A),
B : cc.uT, f : cc.eT A -> cc.eT (list B)]
bind list A B (Cons _ a l) f --> append B (f a) (bind list A B l f).
[A : cc.uT, B : cc.uT, a : cc.eT A, f : cc.eT A -> cc.eT (list B)]
monad_neutral_left list A B a f --> refl (list B) (f a).
(; This recursive proof does not terminate
if reduction under lambda is allowed ;)
[A : cc.uT, m : cc.eT (list A)]
monad_neutral_right list A m -->
list_dep_case
A
(m : cc.eT (list A) =>
istruetype (equal (list A)
(bind list A A m (return list A))
m))
(refl (list A) (Nil A))
(a : cc.eT A =>
l : cc.eT (list A) =>
dk_tuple.cpl
(istruetype (equal A a a))
(istruetype (equal
(list A)
(bind list A A
l
(a2 : cc.eT A => Cons A a2 (Nil A)))
l))
(refl A a)
(monad_neutral_right list A l))
m.
[A : cc.uT,
B : cc.uT,
C : cc.uT,
f : (cc.eT A -> cc.eT (list B)),
g : (cc.eT B -> cc.eT (list C)),
m : cc.eT (list A)]
monad_bind_comp list A B C f g m -->
list_dep_case
A
(m : cc.eT (list A) =>
istruetype (equal (list C)
(bind list B C (bind list A B m f) g)
(bind list A C m (comp list A B C f g))))
(refl (list C) (Nil C))
(a : cc.eT A =>
l : cc.eT (list A) =>
refl (list C) (bind list B C (append B (f a) (bind list A B l f)) g))
m.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment