Project

General

Profile

Statistics
| Branch: | Revision:

corque / Lemmas_ElgotMonad.v @ 4806fe22

History | View | Annotate | Download (2.2 KB)

1
Add LoadPath "~/Schreibtisch/svnba/Elgot/Coq/".
2
Require Import biCCC.
3
Require Import Lemmas_biCCC.
4
Require Import ElgotMonad.
5
Require Import Coq_Steroids.
6
Open Scope c_scope.
7

    
8

    
9
Section Lemmas.
10
Context `(ElgotMonad).
11

    
12
(* Lemmas proven in the following:
13

    
14
map_id:
15
  map id (a:=x) = id
16

    
17
map_comp:
18
   map f ∘ map g = map (f ∘ g)
19

    
20
lifting_map:
21
  f * ∘ map g = (f ∘ g) *
22

    
23
map_unit:
24
  map f ∘ η = η ∘ f
25

    
26
map_lifting:
27
  map f ∘ g * = (map f ∘ g)*
28

    
29
mapinl_f_iter:
30
  (map inl ∘ f) † = f
31

    
32
map_naturality:
33
  map f ∘ u † = (map (f ⊕⊕ id) ∘ u) †
34

    
35
str_map :
36
  map (id ×× f) ∘ τ = τ ∘ (id (a:=z) ×× map f)
37

    
38
*)
39

    
40

    
41
Lemma map_id : forall
42
(x : Obj),
43
  map id (a:=x) = id.
44

    
45
Proof.
46
intros.
47
unfold map.
48
rewrite -> id_l, -> kl1.
49
trivial.
50
Qed.
51

    
52

    
53

    
54
Lemma map_comp : forall
55
(x y z : Obj) 
56
(f: y ~> z) 
57
(g: x ~> y),
58
  map f ∘ map g = map (f ∘ g).
59

    
60
Proof.
61
intros.
62
unfold map.
63
rewrite <- kl3.
64
rewrite -> comp_assoc, -> kl2, -> comp_assoc.
65
trivial.
66
Qed.
67

    
68

    
69

    
70
Lemma lifting_map : forall 
71
(x y z : Obj)
72
(f: y ~> T z)
73
(g: x ~> y),
74
  f * ∘ map g = (f ∘ g) *.
75

    
76
Proof.
77
intros.
78
unfold map.
79
rewrite <- kl3.
80
rewrite -> comp_assoc, -> kl2.
81
trivial.
82
Qed.
83

    
84

    
85

    
86
Lemma map_unit : forall
87
(x y : Obj)
88
(f: x ~> y),
89
  map f ∘ η = η ∘ f.
90

    
91
Proof.
92
intros.
93
unfold map.
94
rewrite -> kl2.
95
trivial.
96
Qed.
97

    
98

    
99

    
100
Lemma map_lifting : forall
101
(x y z : Obj)
102
(f: y ~> z)
103
(g: x ~> T y),
104
  map f ∘ g * = (map f ∘ g)*.
105

    
106
Proof.
107
intros.
108
unfold map.
109
rewrite <- kl3.
110
trivial.
111
Qed.
112

    
113

    
114

    
115
Lemma mapinl_f_iter : forall
116
(x y : Obj)
117
(f: x ~> T y),
118
  (map inl ∘ f) † = f.
119

    
120
Proof.
121
intros.
122
rewrite <- unfolding.
123
rewrite -> comp_assoc, -> lifting_map.
124
rewrite -> cpr_inl.
125
rewrite -> kl1, -> id_r.
126
trivial.
127
Qed.
128

    
129

    
130

    
131
Lemma map_naturality : forall 
132
(x y z : Obj)
133
(f: y ~> z)
134
(u : x ~> T (y ⊕ x)),
135
  map f ∘ u † = (map (f ⊕⊕ id) ∘ u) †.
136

    
137
Proof.
138
intros.
139
unfold map.
140
rewrite -> naturality.
141
rewrite -> comp_assoc, -> map_unit.
142
unfold coprodhom.
143
rewrite -> f_cpr, -> id_l, -> comp_assoc.
144
trivial.
145
Qed.
146

    
147

    
148

    
149
Lemma str_map : forall
150
(x y z : Obj)
151
(f: x ~> y),
152
  map (id ×× f) ∘ τ = τ ∘ (id (a:=z) ×× map f).
153

    
154
Proof.
155
intros.
156
unfold map.
157
rewrite <- str4.
158
rewrite <- id_l with (f':=id), <- prodhom_comp, -> id_l.
159
rewrite -> comp_assoc, -> str3.
160
trivial.
161
Qed.
162

    
163

    
164

    
165
End Lemmas.