## 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. |