~ubuntu-branches/ubuntu/hardy/coq-doc/hardy

<a href="Coq.IntMap.Mapaxioms.html#eqmap">eqmap</a> A m m' -> <a href="Coq.IntMap.Mapiter.html#MapFold">MapFold</a> _ _ neutral op f m = <a href="Coq.IntMap.Mapiter.html#MapFold">MapFold</a> _ _ neutral op f m'.

<code class="keyword">Proof</code>.

intros. rewrite (<a href="Coq.IntMap.Mapiter.html#MapFold_as_fold">MapFold_as_fold</a> A M neutral op assoc nleft nright f m).

rewrite (<a href="Coq.IntMap.Mapiter.html#MapFold_as_fold">MapFold_as_fold</a> A M neutral op assoc nleft nright f m').

cut (<a href="Coq.IntMap.Mapiter.html#alist_of_Map">alist_of_Map</a> A m = <a href="Coq.IntMap.Mapiter.html#alist_of_Map">alist_of_Map</a> A m'). intro. rewrite H0. reflexivity.

apply <a href="Coq.IntMap.Lsort.html#alist_canonical">alist_canonical</a>. unfold eqmap in H. apply <a href="Coq.IntMap.Mapaxioms.html#eqm_trans">eqm_trans</a> with (f':= <a href="Coq.IntMap.Map.html#MapGet">MapGet</a> A m).

apply <a href="Coq.IntMap.Mapaxioms.html#eqm_sym">eqm_sym</a>. apply <a href="Coq.IntMap.Mapiter.html#alist_of_Map_semantics">alist_of_Map_semantics</a>.

apply <a href="Coq.IntMap.Mapaxioms.html#eqm_trans">eqm_trans</a> with (f':= <a href="Coq.IntMap.Map.html#MapGet">MapGet</a> A m'). assumption.

apply <a href="Coq.IntMap.Mapiter.html#alist_of_Map_semantics">alist_of_Map_semantics</a>.

apply <a href="Coq.IntMap.Lsort.html#alist_of_Map_sorts2">alist_of_Map_sorts2</a>.

<code class="keyword">Qed</code>.

<code class="keyword">Lemma</code> <a name="MapFold_ext_f_1"></a>MapFold_ext_f_1 :

forall (m:<a href="Coq.IntMap.Map.html#Map">Map</a> A) (f g:<a href="Coq.IntMap.Addr.html#ad">ad</a> -> A -> M) (pf:<a href="Coq.IntMap.Addr.html#ad">ad</a> -> <a href="Coq.IntMap.Addr.html#ad">ad</a>),

(forall (a:<a href="Coq.IntMap.Addr.html#ad">ad</a>) (y:A), <a href="Coq.IntMap.Map.html#MapGet">MapGet</a> _ m a = <a href="Coq.IntMap.Map.html#SOME">SOME</a> _ y -> f (pf a) y = g (pf a) y) ->

<a href="Coq.IntMap.Mapiter.html#MapFold1">MapFold1</a> _ _ neutral op f pf m = <a href="Coq.IntMap.Mapiter.html#MapFold1">MapFold1</a> _ _ neutral op g pf m.

<code class="keyword">Proof</code>.

simple induction m. trivial.

simpl in |- *. intros. apply H. rewrite (<a href="Coq.IntMap.Addec.html#ad_eq_correct">ad_eq_correct</a> a). reflexivity.

intros. simpl in |- *. rewrite (H f g (fun a0:<a href="Coq.IntMap.Addr.html#ad">ad</a> => pf (<a href="Coq.IntMap.Addr.html#ad_double">ad_double</a> a0))).

rewrite (H0 f g (fun a0:<a href="Coq.IntMap.Addr.html#ad">ad</a> => pf (<a href="Coq.IntMap.Addr.html#ad_double_plus_un">ad_double_plus_un</a> a0))). reflexivity.

intros. apply H1. rewrite <a href="Coq.IntMap.Map.html#MapGet_M2_bit_0_1">MapGet_M2_bit_0_1</a>. rewrite <a href="Coq.IntMap.Addr.html#ad_double_plus_un_div_2">ad_double_plus_un_div_2</a>. assumption.

apply <a href="Coq.IntMap.Addr.html#ad_double_plus_un_bit_0">ad_double_plus_un_bit_0</a>.

intros. apply H1. rewrite <a href="Coq.IntMap.Map.html#MapGet_M2_bit_0_0">MapGet_M2_bit_0_0</a>. rewrite <a href="Coq.IntMap.Addr.html#ad_double_div_2">ad_double_div_2</a>. assumption.

apply <a href="Coq.IntMap.Addr.html#ad_double_bit_0">ad_double_bit_0</a>.

<code class="keyword">Qed</code>.

<code class="keyword">Lemma</code> <a name="MapFold_ext_f"></a>MapFold_ext_f :

forall (f g:<a href="Coq.IntMap.Addr.html#ad">ad</a> -> A -> M) (m:<a href="Coq.IntMap.Map.html#Map">Map</a> A),

(forall (a:<a href="Coq.IntMap.Addr.html#ad">ad</a>) (y:A), <a href="Coq.IntMap.Map.html#MapGet">MapGet</a> _ m a = <a href="Coq.IntMap.Map.html#SOME">SOME</a> _ y -> f a y = g a y) ->

<a href="Coq.IntMap.Mapiter.html#MapFold">MapFold</a> _ _ neutral op f m = <a href="Coq.IntMap.Mapiter.html#MapFold">MapFold</a> _ _ neutral op g m.

<code class="keyword">Proof</code>.

intros. exact (<a href="Coq.IntMap.Mapfold.html#MapFold_ext_f_1">MapFold_ext_f_1</a> m f g (fun a0:<a href="Coq.IntMap.Addr.html#ad">ad</a> => a0) H).

<code class="keyword">Qed</code>.

<code class="keyword">Lemma</code> <a name="MapFold1_as_Fold_1"></a>MapFold1_as_Fold_1 :

forall (m:<a href="Coq.IntMap.Map.html#Map">Map</a> A) (f f':<a href="Coq.IntMap.Addr.html#ad">ad</a> -> A -> M) (pf pf':<a href="Coq.IntMap.Addr.html#ad">ad</a> -> <a href="Coq.IntMap.Addr.html#ad">ad</a>),

(forall (a:<a href="Coq.IntMap.Addr.html#ad">ad</a>) (y:A), f (pf a) y = f' (pf' a) y) ->

<a href="Coq.IntMap.Mapiter.html#MapFold1">MapFold1</a> _ _ neutral op f pf m = <a href="Coq.IntMap.Mapiter.html#MapFold1">MapFold1</a> _ _ neutral op f' pf' m.

<code class="keyword">Proof</code>.

simple induction m. trivial.

intros. simpl in |- *. apply H.

intros. simpl in |- *.

rewrite

(H f f' (fun a0:<a href="Coq.IntMap.Addr.html#ad">ad</a> => pf (<a href="Coq.IntMap.Addr.html#ad_double">ad_double</a> a0))

(fun a0:<a href="Coq.IntMap.Addr.html#ad">ad</a> => pf' (<a href="Coq.IntMap.Addr.html#ad_double">ad_double</a> a0))).

rewrite

(H0 f f' (fun a0:<a href="Coq.IntMap.Addr.html#ad">ad</a> => pf (<a href="Coq.IntMap.Addr.html#ad_double_plus_un">ad_double_plus_un</a> a0))

(fun a0:<a href="Coq.IntMap.Addr.html#ad">ad</a> => pf' (<a href="Coq.IntMap.Addr.html#ad_double_plus_un">ad_double_plus_un</a> a0))).

reflexivity.

intros. apply H1.

100

<code class="keyword">Qed</code>.

101

102

103

<code class="keyword">Lemma</code> <a name="MapFold1_as_Fold"></a>MapFold1_as_Fold :

104

forall (f:<a href="Coq.IntMap.Addr.html#ad">ad</a> -> A -> M) (pf:<a href="Coq.IntMap.Addr.html#ad">ad</a> -> <a href="Coq.IntMap.Addr.html#ad">ad</a>) (m:<a href="Coq.IntMap.Map.html#Map">Map</a> A),

105

<a href="Coq.IntMap.Mapiter.html#MapFold1">MapFold1</a> _ _ neutral op f pf m =

106

<a href="Coq.IntMap.Mapiter.html#MapFold">MapFold</a> _ _ neutral op (fun (a:<a href="Coq.IntMap.Addr.html#ad">ad</a>) (y:A) => f (pf a) y) m.

107

<code class="keyword">Proof</code>.

108

intros. unfold MapFold in |- *. apply <a href="Coq.IntMap.Mapfold.html#MapFold1_as_Fold_1">MapFold1_as_Fold_1</a>. trivial.

109

<code class="keyword">Qed</code>.

110

111

112

<code class="keyword">Lemma</code> <a name="MapFold1_ext"></a>MapFold1_ext :

113

forall (f:<a href="Coq.IntMap.Addr.html#ad">ad</a> -> A -> M) (m m':<a href="Coq.IntMap.Map.html#Map">Map</a> A),

114

<a href="Coq.IntMap.Mapaxioms.html#eqmap">eqmap</a> A m m' ->

115

forall pf:<a href="Coq.IntMap.Addr.html#ad">ad</a> -> <a href="Coq.IntMap.Addr.html#ad">ad</a>,

116

<a href="Coq.IntMap.Mapiter.html#MapFold1">MapFold1</a> _ _ neutral op f pf m = <a href="Coq.IntMap.Mapiter.html#MapFold1">MapFold1</a> _ _ neutral op f pf m'.

117

<code class="keyword">Proof</code>.

118

intros. rewrite <a href="Coq.IntMap.Mapfold.html#MapFold1_as_Fold">MapFold1_as_Fold</a>. rewrite <a href="Coq.IntMap.Mapfold.html#MapFold1_as_Fold">MapFold1_as_Fold</a>. apply <a href="Coq.IntMap.Mapfold.html#MapFold_ext">MapFold_ext</a>. assumption.

119

<code class="keyword">Qed</code>.

120

121

122

<code class="keyword">Variable</code> comm : forall a b:M, op a b = op b a.

123

124

125

<code class="keyword">Lemma</code> <a name="MapFold_Put_disjoint_1"></a>MapFold_Put_disjoint_1 :

126

forall (p:<a href="Coq.NArith.BinPos.html#positive">positive</a>) (f:<a href="Coq.IntMap.Addr.html#ad">ad</a> -> A -> M) (pf:<a href="Coq.IntMap.Addr.html#ad">ad</a> -> <a href="Coq.IntMap.Addr.html#ad">ad</a>)

127

(a1 a2:<a href="Coq.IntMap.Addr.html#ad">ad</a>) (y1 y2:A),

128

129

<a href="Coq.IntMap.Mapiter.html#MapFold1">MapFold1</a> A M neutral op f pf (<a href="Coq.IntMap.Map.html#MapPut1">MapPut1</a> A a1 y1 a2 y2 p) =

130

op (f (pf a1) y1) (f (pf a2) y2).

131

<code class="keyword">Proof</code>.

132

simple induction p. intros. simpl in |- *. elim (<a href="Coq.Bool.Sumbool.html#sumbool_of_bool">sumbool_of_bool</a> (<a href="Coq.IntMap.Addr.html#ad_bit_0">ad_bit_0</a> a1)). intro H1. rewrite H1.

133

simpl in |- *. rewrite <a href="Coq.IntMap.Addr.html#ad_div_2_double_plus_un">ad_div_2_double_plus_un</a>. rewrite <a href="Coq.IntMap.Addr.html#ad_div_2_double">ad_div_2_double</a>. apply comm.

134

change (<a href="Coq.IntMap.Addr.html#ad_bit_0">ad_bit_0</a> a2 = <a href="Coq.Bool.Bool.html#negb">negb</a> <a href="Coq.Init.Datatypes.html#true">true</a>) in |- *. rewrite <- H1. rewrite (<a href="Coq.IntMap.Addr.html#ad_neg_bit_0_2">ad_neg_bit_0_2</a> _ _ _ H0).

135

rewrite <a href="Coq.Bool.Bool.html#negb_elim">negb_elim</a>. reflexivity.

136

assumption.

137

intro H1. rewrite H1. simpl in |- *. rewrite <a href="Coq.IntMap.Addr.html#ad_div_2_double">ad_div_2_double</a>. rewrite <a href="Coq.IntMap.Addr.html#ad_div_2_double_plus_un">ad_div_2_double_plus_un</a>.

138

reflexivity.

139

change (<a href="Coq.IntMap.Addr.html#ad_bit_0">ad_bit_0</a> a2 = <a href="Coq.Bool.Bool.html#negb">negb</a> <a href="Coq.Init.Datatypes.html#false">false</a>) in |- *. rewrite <- H1. rewrite (<a href="Coq.IntMap.Addr.html#ad_neg_bit_0_2">ad_neg_bit_0_2</a> _ _ _ H0).

140

rewrite <a href="Coq.Bool.Bool.html#negb_elim">negb_elim</a>. reflexivity.

141

assumption.

142

simpl in |- *. intros. elim (<a href="Coq.Bool.Sumbool.html#sumbool_of_bool">sumbool_of_bool</a> (<a href="Coq.IntMap.Addr.html#ad_bit_0">ad_bit_0</a> a1)). intro H1. rewrite H1. simpl in |- *.

143

rewrite nleft.

144

rewrite

145

(H f (fun a0:<a href="Coq.IntMap.Addr.html#ad">ad</a> => pf (<a href="Coq.IntMap.Addr.html#ad_double_plus_un">ad_double_plus_un</a> a0)) (

146

<a href="Coq.IntMap.Addr.html#ad_div_2">ad_div_2</a> a1) (<a href="Coq.IntMap.Addr.html#ad_div_2">ad_div_2</a> a2) y1 y2).

147

rewrite <a href="Coq.IntMap.Addr.html#ad_div_2_double_plus_un">ad_div_2_double_plus_un</a>. rewrite <a href="Coq.IntMap.Addr.html#ad_div_2_double_plus_un">ad_div_2_double_plus_un</a>. reflexivity.

148

rewrite <- (<a href="Coq.IntMap.Addr.html#ad_same_bit_0">ad_same_bit_0</a> _ _ _ H0). assumption.

149

assumption.

150

rewrite <- <a href="Coq.IntMap.Addr.html#ad_xor_div_2">ad_xor_div_2</a>. rewrite H0. reflexivity.

151

intro H1. rewrite H1. simpl in |- *. rewrite nright.

152

rewrite

153

(H f (fun a0:<a href="Coq.IntMap.Addr.html#ad">ad</a> => pf (<a href="Coq.IntMap.Addr.html#ad_double">ad_double</a> a0)) (<a href="Coq.IntMap.Addr.html#ad_div_2">ad_div_2</a> a1) (<a href="Coq.IntMap.Addr.html#ad_div_2">ad_div_2</a> a2) y1 y2)

154

.

155

rewrite <a href="Coq.IntMap.Addr.html#ad_div_2_double">ad_div_2_double</a>. rewrite <a href="Coq.IntMap.Addr.html#ad_div_2_double">ad_div_2_double</a>. reflexivity.

156

rewrite <- (<a href="Coq.IntMap.Addr.html#ad_same_bit_0">ad_same_bit_0</a> _ _ _ H0). assumption.

157

assumption.

158

rewrite <- <a href="Coq.IntMap.Addr.html#ad_xor_div_2">ad_xor_div_2</a>. rewrite H0. reflexivity.

159

intros. simpl in |- *. elim (<a href="Coq.Bool.Sumbool.html#sumbool_of_bool">sumbool_of_bool</a> (<a href="Coq.IntMap.Addr.html#ad_bit_0">ad_bit_0</a> a1)). intro H0. rewrite H0. simpl in |- *.

160

rewrite <a href="Coq.IntMap.Addr.html#ad_div_2_double">ad_div_2_double</a>. rewrite <a href="Coq.IntMap.Addr.html#ad_div_2_double_plus_un">ad_div_2_double_plus_un</a>. apply comm.

161

assumption.

162

change (<a href="Coq.IntMap.Addr.html#ad_bit_0">ad_bit_0</a> a2 = <a href="Coq.Bool.Bool.html#negb">negb</a> <a href="Coq.Init.Datatypes.html#true">true</a>) in |- *. rewrite <- H0. rewrite (<a href="Coq.IntMap.Addr.html#ad_neg_bit_0_1">ad_neg_bit_0_1</a> _ _ H).

163

rewrite <a href="Coq.Bool.Bool.html#negb_elim">negb_elim</a>. reflexivity.

164

intro H0. rewrite H0. simpl in |- *. rewrite <a href="Coq.IntMap.Addr.html#ad_div_2_double">ad_div_2_double</a>. rewrite <a href="Coq.IntMap.Addr.html#ad_div_2_double_plus_un">ad_div_2_double_plus_un</a>.

165

reflexivity.

166

change (<a href="Coq.IntMap.Addr.html#ad_bit_0">ad_bit_0</a> a2 = <a href="Coq.Bool.Bool.html#negb">negb</a> <a href="Coq.Init.Datatypes.html#false">false</a>) in |- *. rewrite <- H0. rewrite (<a href="Coq.IntMap.Addr.html#ad_neg_bit_0_1">ad_neg_bit_0_1</a> _ _ H).

167

rewrite <a href="Coq.Bool.Bool.html#negb_elim">negb_elim</a>. reflexivity.

168

assumption.

169

<code class="keyword">Qed</code>.

170

171

172

<code class="keyword">Lemma</code> <a name="MapFold_Put_disjoint_2"></a>MapFold_Put_disjoint_2 :

173

forall (f:<a href="Coq.IntMap.Addr.html#ad">ad</a> -> A -> M) (m:<a href="Coq.IntMap.Map.html#Map">Map</a> A) (a:<a href="Coq.IntMap.Addr.html#ad">ad</a>) (y:A) (pf:<a href="Coq.IntMap.Addr.html#ad">ad</a> -> <a href="Coq.IntMap.Addr.html#ad">ad</a>),

174

<a href="Coq.IntMap.Map.html#MapGet">MapGet</a> A m a = <a href="Coq.IntMap.Map.html#NONE">NONE</a> A ->

175

<a href="Coq.IntMap.Mapiter.html#MapFold1">MapFold1</a> A M neutral op f pf (<a href="Coq.IntMap.Map.html#MapPut">MapPut</a> A m a y) =

176

op (f (pf a) y) (<a href="Coq.IntMap.Mapiter.html#MapFold1">MapFold1</a> A M neutral op f pf m).

177

<code class="keyword">Proof</code>.

178

simple induction m. intros. simpl in |- *. rewrite (nright (f (pf a) y)). reflexivity.

179

intros a1 y1 a2 y2 pf H. simpl in |- *. elim (<a href="Coq.IntMap.Addr.html#ad_sum">ad_sum</a> (<a href="Coq.IntMap.Addr.html#ad_xor">ad_xor</a> a1 a2)). intro H0. elim H0.

180

intros p H1. rewrite H1. rewrite comm. exact (<a href="Coq.IntMap.Mapfold.html#MapFold_Put_disjoint_1">MapFold_Put_disjoint_1</a> p f pf a1 a2 y1 y2 H1).

181

intro H0. rewrite (<a href="Coq.IntMap.Addec.html#ad_eq_complete">ad_eq_complete</a> _ _ (<a href="Coq.IntMap.Addec.html#ad_xor_eq_true">ad_xor_eq_true</a> _ _ H0)) in H.

182

rewrite (<a href="Coq.IntMap.Map.html#M1_semantics_1">M1_semantics_1</a> A a2 y1) in H. discriminate H.

183

intros. elim (<a href="Coq.Bool.Sumbool.html#sumbool_of_bool">sumbool_of_bool</a> (<a href="Coq.IntMap.Addr.html#ad_bit_0">ad_bit_0</a> a)). intro H2.

184

cut (<a href="Coq.IntMap.Map.html#MapPut">MapPut</a> A (<a href="Coq.IntMap.Map.html#M2">M2</a> A m0 m1) a y = <a href="Coq.IntMap.Map.html#M2">M2</a> A m0 (<a href="Coq.IntMap.Map.html#MapPut">MapPut</a> A m1 (<a href="Coq.IntMap.Addr.html#ad_div_2">ad_div_2</a> a) y)). intro.

185

rewrite H3. simpl in |- *. rewrite (H0 (<a href="Coq.IntMap.Addr.html#ad_div_2">ad_div_2</a> a) y (fun a0:<a href="Coq.IntMap.Addr.html#ad">ad</a> => pf (<a href="Coq.IntMap.Addr.html#ad_double_plus_un">ad_double_plus_un</a> a0))).

186

rewrite <a href="Coq.IntMap.Addr.html#ad_div_2_double_plus_un">ad_div_2_double_plus_un</a>. rewrite <- assoc.

187

rewrite

188

(comm (<a href="Coq.IntMap.Mapiter.html#MapFold1">MapFold1</a> A M neutral op f (fun a0:<a href="Coq.IntMap.Addr.html#ad">ad</a> => pf (<a href="Coq.IntMap.Addr.html#ad_double">ad_double</a> a0)) m0)

189

(f (pf a) y)).

190

rewrite assoc. reflexivity.

191

assumption.

192

rewrite (<a href="Coq.IntMap.Map.html#MapGet_M2_bit_0_1">MapGet_M2_bit_0_1</a> A a H2 m0 m1) in H1. assumption.

193

simpl in |- *. elim (<a href="Coq.IntMap.Addr.html#ad_sum">ad_sum</a> a). intro H3. elim H3. intro p. elim p. intros p0 H4 H5. rewrite H5.

194

reflexivity.

195

intros p0 H4 H5. rewrite H5 in H2. discriminate H2.

196

intro H4. rewrite H4. reflexivity.

197

intro H3. rewrite H3 in H2. discriminate H2.

198

intro H2. cut (<a href="Coq.IntMap.Map.html#MapPut">MapPut</a> A (<a href="Coq.IntMap.Map.html#M2">M2</a> A m0 m1) a y = <a href="Coq.IntMap.Map.html#M2">M2</a> A (<a href="Coq.IntMap.Map.html#MapPut">MapPut</a> A m0 (<a href="Coq.IntMap.Addr.html#ad_div_2">ad_div_2</a> a) y) m1).

199

intro. rewrite H3. simpl in |- *. rewrite (H (<a href="Coq.IntMap.Addr.html#ad_div_2">ad_div_2</a> a) y (fun a0:<a href="Coq.IntMap.Addr.html#ad">ad</a> => pf (<a href="Coq.IntMap.Addr.html#ad_double">ad_double</a> a0))).

200

rewrite <a href="Coq.IntMap.Addr.html#ad_div_2_double">ad_div_2_double</a>. rewrite <- assoc. reflexivity.

201

assumption.

202

rewrite (<a href="Coq.IntMap.Map.html#MapGet_M2_bit_0_0">MapGet_M2_bit_0_0</a> A a H2 m0 m1) in H1. assumption.

203

simpl in |- *. elim (<a href="Coq.IntMap.Addr.html#ad_sum">ad_sum</a> a). intro H3. elim H3. intro p. elim p. intros p0 H4 H5. rewrite H5 in H2.

204

discriminate H2.

205

intros p0 H4 H5. rewrite H5. reflexivity.

206

intro H4. rewrite H4 in H2. discriminate H2.

207

intro H3. rewrite H3. reflexivity.

208

<code class="keyword">Qed</code>.

209

210

211

<code class="keyword">Lemma</code> <a name="MapFold_Put_disjoint"></a>MapFold_Put_disjoint :

212

forall (f:<a href="Coq.IntMap.Addr.html#ad">ad</a> -> A -> M) (m:<a href="Coq.IntMap.Map.html#Map">Map</a> A) (a:<a href="Coq.IntMap.Addr.html#ad">ad</a>) (y:A),

213

<a href="Coq.IntMap.Map.html#MapGet">MapGet</a> A m a = <a href="Coq.IntMap.Map.html#NONE">NONE</a> A ->

214

<a href="Coq.IntMap.Mapiter.html#MapFold">MapFold</a> A M neutral op f (<a href="Coq.IntMap.Map.html#MapPut">MapPut</a> A m a y) =

215

op (f a y) (<a href="Coq.IntMap.Mapiter.html#MapFold">MapFold</a> A M neutral op f m).

216

<code class="keyword">Proof</code>.

217

intros. exact (<a href="Coq.IntMap.Mapfold.html#MapFold_Put_disjoint_2">MapFold_Put_disjoint_2</a> f m a y (fun a0:<a href="Coq.IntMap.Addr.html#ad">ad</a> => a0) H).

218

<code class="keyword">Qed</code>.

219

220

221

<code class="keyword">Lemma</code> <a name="MapFold_Put_behind_disjoint_2"></a>MapFold_Put_behind_disjoint_2 :

222

223

<a href="Coq.IntMap.Map.html#MapGet">MapGet</a> A m a = <a href="Coq.IntMap.Map.html#NONE">NONE</a> A ->

224

<a href="Coq.IntMap.Mapiter.html#MapFold1">MapFold1</a> A M neutral op f pf (<a href="Coq.IntMap.Map.html#MapPut_behind">MapPut_behind</a> A m a y) =

225

op (f (pf a) y) (<a href="Coq.IntMap.Mapiter.html#MapFold1">MapFold1</a> A M neutral op f pf m).

226

<code class="keyword">Proof</code>.

227

intros. cut (<a href="Coq.IntMap.Mapaxioms.html#eqmap">eqmap</a> A (<a href="Coq.IntMap.Map.html#MapPut_behind">MapPut_behind</a> A m a y) (<a href="Coq.IntMap.Map.html#MapPut">MapPut</a> A m a y)). intro.

228

rewrite (<a href="Coq.IntMap.Mapfold.html#MapFold1_ext">MapFold1_ext</a> f _ _ H0 pf). apply <a href="Coq.IntMap.Mapfold.html#MapFold_Put_disjoint_2">MapFold_Put_disjoint_2</a>. assumption.

229

apply <a href="Coq.IntMap.Mapaxioms.html#eqmap_trans">eqmap_trans</a> with (m':= <a href="Coq.IntMap.Map.html#MapMerge">MapMerge</a> A (<a href="Coq.IntMap.Map.html#M1">M1</a> A a y) m). apply <a href="Coq.IntMap.Mapaxioms.html#MapPut_behind_as_Merge">MapPut_behind_as_Merge</a>.

230

apply <a href="Coq.IntMap.Mapaxioms.html#eqmap_trans">eqmap_trans</a> with (m':= <a href="Coq.IntMap.Map.html#MapMerge">MapMerge</a> A m (<a href="Coq.IntMap.Map.html#M1">M1</a> A a y)).

231

apply <a href="Coq.IntMap.Mapaxioms.html#eqmap_trans">eqmap_trans</a> with (m':= <a href="Coq.IntMap.Map.html#MapDelta">MapDelta</a> A (<a href="Coq.IntMap.Map.html#M1">M1</a> A a y) m). apply <a href="Coq.IntMap.Mapaxioms.html#eqmap_sym">eqmap_sym</a>. apply <a href="Coq.IntMap.Mapsubset.html#MapDelta_disjoint">MapDelta_disjoint</a>.

232

unfold MapDisjoint in |- *. unfold in_dom in |- *. simpl in |- *. intros. elim (<a href="Coq.Bool.Sumbool.html#sumbool_of_bool">sumbool_of_bool</a> (<a href="Coq.IntMap.Addec.html#ad_eq">ad_eq</a> a a0)).

233

intro H2. rewrite (<a href="Coq.IntMap.Addec.html#ad_eq_complete">ad_eq_complete</a> _ _ H2) in H. rewrite H in H1. discriminate H1.

234

intro H2. rewrite H2 in H0. discriminate H0.

235

apply <a href="Coq.IntMap.Mapaxioms.html#eqmap_trans">eqmap_trans</a> with (m':= <a href="Coq.IntMap.Map.html#MapDelta">MapDelta</a> A m (<a href="Coq.IntMap.Map.html#M1">M1</a> A a y)). apply <a href="Coq.IntMap.Mapaxioms.html#MapDelta_sym">MapDelta_sym</a>.

236

apply <a href="Coq.IntMap.Mapsubset.html#MapDelta_disjoint">MapDelta_disjoint</a>. unfold MapDisjoint in |- *. unfold in_dom in |- *. simpl in |- *. intros.

237

elim (<a href="Coq.Bool.Sumbool.html#sumbool_of_bool">sumbool_of_bool</a> (<a href="Coq.IntMap.Addec.html#ad_eq">ad_eq</a> a a0)). intro H2. rewrite (<a href="Coq.IntMap.Addec.html#ad_eq_complete">ad_eq_complete</a> _ _ H2) in H.

238

rewrite H in H0. discriminate H0.

239

intro H2. rewrite H2 in H1. discriminate H1.

240

apply <a href="Coq.IntMap.Mapaxioms.html#eqmap_sym">eqmap_sym</a>. apply <a href="Coq.IntMap.Mapaxioms.html#MapPut_as_Merge">MapPut_as_Merge</a>.

241

<code class="keyword">Qed</code>.

242

243

244

<code class="keyword">Lemma</code> <a name="MapFold_Put_behind_disjoint"></a>MapFold_Put_behind_disjoint :

245

forall (f:<a href="Coq.IntMap.Addr.html#ad">ad</a> -> A -> M) (m:<a href="Coq.IntMap.Map.html#Map">Map</a> A) (a:<a href="Coq.IntMap.Addr.html#ad">ad</a>) (y:A),

246

<a href="Coq.IntMap.Map.html#MapGet">MapGet</a> A m a = <a href="Coq.IntMap.Map.html#NONE">NONE</a> A ->

247

<a href="Coq.IntMap.Mapiter.html#MapFold">MapFold</a> A M neutral op f (<a href="Coq.IntMap.Map.html#MapPut_behind">MapPut_behind</a> A m a y) =

248

op (f a y) (<a href="Coq.IntMap.Mapiter.html#MapFold">MapFold</a> A M neutral op f m).

249

<code class="keyword">Proof</code>.

250

intros. exact (<a href="Coq.IntMap.Mapfold.html#MapFold_Put_behind_disjoint_2">MapFold_Put_behind_disjoint_2</a> f m a y (fun a0:<a href="Coq.IntMap.Addr.html#ad">ad</a> => a0) H).

251

<code class="keyword">Qed</code>.

252

253

254

<code class="keyword">Lemma</code> <a name="MapFold_Merge_disjoint_1"></a>MapFold_Merge_disjoint_1 :

255

forall (f:<a href="Coq.IntMap.Addr.html#ad">ad</a> -> A -> M) (m1 m2:<a href="Coq.IntMap.Map.html#Map">Map</a> A) (pf:<a href="Coq.IntMap.Addr.html#ad">ad</a> -> <a href="Coq.IntMap.Addr.html#ad">ad</a>),

256

<a href="Coq.IntMap.Mapsubset.html#MapDisjoint">MapDisjoint</a> A A m1 m2 ->

257

<a href="Coq.IntMap.Mapiter.html#MapFold1">MapFold1</a> A M neutral op f pf (<a href="Coq.IntMap.Map.html#MapMerge">MapMerge</a> A m1 m2) =

258

op (<a href="Coq.IntMap.Mapiter.html#MapFold1">MapFold1</a> A M neutral op f pf m1) (<a href="Coq.IntMap.Mapiter.html#MapFold1">MapFold1</a> A M neutral op f pf m2).

259

<code class="keyword">Proof</code>.

260

simple induction m1. simpl in |- *. intros. rewrite nleft. reflexivity.

261

intros. unfold MapMerge in |- *. apply (<a href="Coq.IntMap.Mapfold.html#MapFold_Put_behind_disjoint_2">MapFold_Put_behind_disjoint_2</a> f m2 a a0 pf).

262

apply <a href="Coq.IntMap.Fset.html#in_dom_none">in_dom_none</a>. exact (<a href="Coq.IntMap.Mapsubset.html#MapDisjoint_M1_l">MapDisjoint_M1_l</a> _ _ m2 a a0 H).

263

simple induction m2. intros. simpl in |- *. rewrite nright. reflexivity.

264

intros. unfold MapMerge in |- *. rewrite (<a href="Coq.IntMap.Mapfold.html#MapFold_Put_disjoint_2">MapFold_Put_disjoint_2</a> f (<a href="Coq.IntMap.Map.html#M2">M2</a> A m m0) a a0 pf). apply comm.

265

apply <a href="Coq.IntMap.Fset.html#in_dom_none">in_dom_none</a>. exact (<a href="Coq.IntMap.Mapsubset.html#MapDisjoint_M1_r">MapDisjoint_M1_r</a> _ _ (<a href="Coq.IntMap.Map.html#M2">M2</a> A m m0) a a0 H1).

266

intros. simpl in |- *. rewrite (H m3 (fun a0:<a href="Coq.IntMap.Addr.html#ad">ad</a> => pf (<a href="Coq.IntMap.Addr.html#ad_double">ad_double</a> a0))).

267

rewrite (H0 m4 (fun a0:<a href="Coq.IntMap.Addr.html#ad">ad</a> => pf (<a href="Coq.IntMap.Addr.html#ad_double_plus_un">ad_double_plus_un</a> a0))).

268

cut (forall a b c d:M, op (op a b) (op c d) = op (op a c) (op b d)). intro. apply H4.

269

intros. rewrite assoc. rewrite <- (assoc b c d). rewrite (comm b c). rewrite (assoc c b d).

270

rewrite assoc. reflexivity.

271

exact (<a href="Coq.IntMap.Mapsubset.html#MapDisjoint_M2_r">MapDisjoint_M2_r</a> _ _ _ _ _ _ H3).

272

exact (<a href="Coq.IntMap.Mapsubset.html#MapDisjoint_M2_l">MapDisjoint_M2_l</a> _ _ _ _ _ _ H3).

273

<code class="keyword">Qed</code>.

274

275

276

<code class="keyword">Lemma</code> <a name="MapFold_Merge_disjoint"></a>MapFold_Merge_disjoint :

277

forall (f:<a href="Coq.IntMap.Addr.html#ad">ad</a> -> A -> M) (m1 m2:<a href="Coq.IntMap.Map.html#Map">Map</a> A),

278

<a href="Coq.IntMap.Mapsubset.html#MapDisjoint">MapDisjoint</a> A A m1 m2 ->

279

<a href="Coq.IntMap.Mapiter.html#MapFold">MapFold</a> A M neutral op f (<a href="Coq.IntMap.Map.html#MapMerge">MapMerge</a> A m1 m2) =

280

op (<a href="Coq.IntMap.Mapiter.html#MapFold">MapFold</a> A M neutral op f m1) (<a href="Coq.IntMap.Mapiter.html#MapFold">MapFold</a> A M neutral op f m2).

281

<code class="keyword">Proof</code>.

282

intros. exact (<a href="Coq.IntMap.Mapfold.html#MapFold_Merge_disjoint_1">MapFold_Merge_disjoint_1</a> f m1 m2 (fun a0:<a href="Coq.IntMap.Addr.html#ad">ad</a> => a0) H).

283

<code class="keyword">Qed</code>.

284

285

<code class="keyword">End</code> MapFoldResults.

286

287

288

<code class="keyword">Section</code> MapFoldDistr.

289

290

291

<code class="keyword">Variable</code> A : Set.

292

293

294

<code class="keyword">Variable</code> M : Set.

295

<code class="keyword">Variable</code> neutral : M.

296

<code class="keyword">Variable</code> op : M -> M -> M.

297

298

299

<code class="keyword">Variable</code> M' : Set.

300

<code class="keyword">Variable</code> neutral' : M'.

301

<code class="keyword">Variable</code> op' : M' -> M' -> M'.

302

303

304

<code class="keyword">Variable</code> N : Set.

305

306

307

<code class="keyword">Variable</code> times : M -> N -> M'.

308

309

310

<code class="keyword">Variable</code> absorb : forall c:N, times neutral c = neutral'.

311

<code class="keyword">Variable</code>

312

distr :

313

forall (a b:M) (c:N), times (op a b) c = op' (times a c) (times b c).

314

315

316

<code class="keyword">Lemma</code> <a name="MapFold_distr_r_1"></a>MapFold_distr_r_1 :

317

forall (f:<a href="Coq.IntMap.Addr.html#ad">ad</a> -> A -> M) (m:<a href="Coq.IntMap.Map.html#Map">Map</a> A) (c:N) (pf:<a href="Coq.IntMap.Addr.html#ad">ad</a> -> <a href="Coq.IntMap.Addr.html#ad">ad</a>),

318

times (<a href="Coq.IntMap.Mapiter.html#MapFold1">MapFold1</a> A M neutral op f pf m) c =

319

<a href="Coq.IntMap.Mapiter.html#MapFold1">MapFold1</a> A M' neutral' op' (fun (a:<a href="Coq.IntMap.Addr.html#ad">ad</a>) (y:A) => times (f a y) c) pf m.

320

<code class="keyword">Proof</code>.

321

simple induction m. intros. exact (absorb c).

322

trivial.

323

intros. simpl in |- *. rewrite distr. rewrite H. rewrite H0. reflexivity.

324

<code class="keyword">Qed</code>.

325

326

327

<code class="keyword">Lemma</code> <a name="MapFold_distr_r"></a>MapFold_distr_r :

328

forall (f:<a href="Coq.IntMap.Addr.html#ad">ad</a> -> A -> M) (m:<a href="Coq.IntMap.Map.html#Map">Map</a> A) (c:N),

329

times (<a href="Coq.IntMap.Mapiter.html#MapFold">MapFold</a> A M neutral op f m) c =

330

<a href="Coq.IntMap.Mapiter.html#MapFold">MapFold</a> A M' neutral' op' (fun (a:<a href="Coq.IntMap.Addr.html#ad">ad</a>) (y:A) => times (f a y) c) m.

331

<code class="keyword">Proof</code>.

332

intros. exact (<a href="Coq.IntMap.Mapfold.html#MapFold_distr_r_1">MapFold_distr_r_1</a> f m c (fun a:<a href="Coq.IntMap.Addr.html#ad">ad</a> => a)).

333

<code class="keyword">Qed</code>.

334

335

336

<code class="keyword">End</code> MapFoldDistr.

337

338

339

<code class="keyword">Section</code> MapFoldDistrL.

340

341

342

<code class="keyword">Variable</code> A : Set.

343

344

345

<code class="keyword">Variable</code> M : Set.

346

<code class="keyword">Variable</code> neutral : M.

347

<code class="keyword">Variable</code> op : M -> M -> M.

348

349

350

<code class="keyword">Variable</code> M' : Set.

351

<code class="keyword">Variable</code> neutral' : M'.

352

<code class="keyword">Variable</code> op' : M' -> M' -> M'.

353

354

355

<code class="keyword">Variable</code> N : Set.

356

357

358

<code class="keyword">Variable</code> times : N -> M -> M'.

359

360

361

<code class="keyword">Variable</code> absorb : forall c:N, times c neutral = neutral'.

362

<code class="keyword">Variable</code>

363

distr :

364

forall (a b:M) (c:N), times c (op a b) = op' (times c a) (times c b).

365

366

367

<code class="keyword">Lemma</code> <a name="MapFold_distr_l"></a>MapFold_distr_l :

368

forall (f:<a href="Coq.IntMap.Addr.html#ad">ad</a> -> A -> M) (m:<a href="Coq.IntMap.Map.html#Map">Map</a> A) (c:N),

369

times c (<a href="Coq.IntMap.Mapiter.html#MapFold">MapFold</a> A M neutral op f m) =

370

<a href="Coq.IntMap.Mapiter.html#MapFold">MapFold</a> A M' neutral' op' (fun (a:<a href="Coq.IntMap.Addr.html#ad">ad</a>) (y:A) => times c (f a y)) m.

371

<code class="keyword">Proof</code>.

372

intros. apply <a href="Coq.IntMap.Mapfold.html#MapFold_distr_r">MapFold_distr_r</a> with (times:= fun (a:M) (b:N) => times b a);

373

assumption.

374

<code class="keyword">Qed</code>.

375

376

377

<code class="keyword">End</code> MapFoldDistrL.

378

379

380

<code class="keyword">Section</code> MapFoldExists.

381

382

383

<code class="keyword">Variable</code> A : Set.

384

385

386

<code class="keyword">Lemma</code> <a name="MapFold_orb_1"></a>MapFold_orb_1 :

387

forall (f:<a href="Coq.IntMap.Addr.html#ad">ad</a> -> A -> <a href="Coq.Init.Datatypes.html#bool">bool</a>) (m:<a href="Coq.IntMap.Map.html#Map">Map</a> A) (pf:<a href="Coq.IntMap.Addr.html#ad">ad</a> -> <a href="Coq.IntMap.Addr.html#ad">ad</a>),

388

<a href="Coq.IntMap.Mapiter.html#MapFold1">MapFold1</a> A <a href="Coq.Init.Datatypes.html#bool">bool</a> <a href="Coq.Init.Datatypes.html#false">false</a> <a href="Coq.Bool.Bool.html#orb">orb</a> f pf m =

389

match <a href="Coq.IntMap.Mapiter.html#MapSweep1">MapSweep1</a> A f pf m with

390

| <a href="Coq.IntMap.Map.html#SOME">SOME</a> _ => <a href="Coq.Init.Datatypes.html#true">true</a>

391

| _ => <a href="Coq.Init.Datatypes.html#false">false</a>

392

end.

393

<code class="keyword">Proof</code>.

394

simple induction m. trivial.

395

intros a y pf. simpl in |- *. unfold MapSweep2 in |- *. case (f (pf a) y); reflexivity.

396

intros. simpl in |- *. rewrite (H (fun a0:<a href="Coq.IntMap.Addr.html#ad">ad</a> => pf (<a href="Coq.IntMap.Addr.html#ad_double">ad_double</a> a0))).

397

rewrite (H0 (fun a0:<a href="Coq.IntMap.Addr.html#ad">ad</a> => pf (<a href="Coq.IntMap.Addr.html#ad_double_plus_un">ad_double_plus_un</a> a0))).

398

case (<a href="Coq.IntMap.Mapiter.html#MapSweep1">MapSweep1</a> A f (fun a0:<a href="Coq.IntMap.Addr.html#ad">ad</a> => pf (<a href="Coq.IntMap.Addr.html#ad_double">ad_double</a> a0)) m0); reflexivity.

399

<code class="keyword">Qed</code>.

400

401

402

<code class="keyword">Lemma</code> <a name="MapFold_orb"></a>MapFold_orb :

403

forall (f:<a href="Coq.IntMap.Addr.html#ad">ad</a> -> A -> <a href="Coq.Init.Datatypes.html#bool">bool</a>) (m:<a href="Coq.IntMap.Map.html#Map">Map</a> A),

404

<a href="Coq.IntMap.Mapiter.html#MapFold">MapFold</a> A <a href="Coq.Init.Datatypes.html#bool">bool</a> <a href="Coq.Init.Datatypes.html#false">false</a> <a href="Coq.Bool.Bool.html#orb">orb</a> f m =

405

match <a href="Coq.IntMap.Mapiter.html#MapSweep">MapSweep</a> A f m with

406

| <a href="Coq.IntMap.Map.html#SOME">SOME</a> _ => <a href="Coq.Init.Datatypes.html#true">true</a>

407

| _ => <a href="Coq.Init.Datatypes.html#false">false</a>

408

end.

409

<code class="keyword">Proof</code>.

410

intros. exact (<a href="Coq.IntMap.Mapfold.html#MapFold_orb_1">MapFold_orb_1</a> f m (fun a:<a href="Coq.IntMap.Addr.html#ad">ad</a> => a)).

411

<code class="keyword">Qed</code>.

412

413

414

<code class="keyword">End</code> MapFoldExists.

415

416

417

<code class="keyword">Section</code> DMergeDef.

418

419

420

<code class="keyword">Variable</code> A : Set.

421

422

423

<code class="keyword">Definition</code> <a name="DMerge"></a>DMerge :=

424

<a href="Coq.IntMap.Mapiter.html#MapFold">MapFold</a> (<a href="Coq.IntMap.Map.html#Map">Map</a> A) (<a href="Coq.IntMap.Map.html#Map">Map</a> A) (<a href="Coq.IntMap.Map.html#M0">M0</a> A) (<a href="Coq.IntMap.Map.html#MapMerge">MapMerge</a> A) (fun (_:<a href="Coq.IntMap.Addr.html#ad">ad</a>) (m:<a href="Coq.IntMap.Map.html#Map">Map</a> A) => m).

425

426

427

<code class="keyword">Lemma</code> <a name="in_dom_DMerge_1"></a>in_dom_DMerge_1 :

428

forall (m:<a href="Coq.IntMap.Map.html#Map">Map</a> (<a href="Coq.IntMap.Map.html#Map">Map</a> A)) (a:<a href="Coq.IntMap.Addr.html#ad">ad</a>),

429

<a href="Coq.IntMap.Fset.html#in_dom">in_dom</a> A a (<a href="Coq.IntMap.Mapfold.html#DMerge">DMerge</a> m) =

430

match <a href="Coq.IntMap.Mapiter.html#MapSweep">MapSweep</a> _ (fun (_:<a href="Coq.IntMap.Addr.html#ad">ad</a>) (m0:<a href="Coq.IntMap.Map.html#Map">Map</a> A) => <a href="Coq.IntMap.Fset.html#in_dom">in_dom</a> A a m0) m with

431

| <a href="Coq.IntMap.Map.html#SOME">SOME</a> _ => <a href="Coq.Init.Datatypes.html#true">true</a>

432

| _ => <a href="Coq.Init.Datatypes.html#false">false</a>

433

end.

434

<code class="keyword">Proof</code>.

435

unfold DMerge in |- *. intros.

436

rewrite

437

(<a href="Coq.IntMap.Mapfold.html#MapFold_distr_l">MapFold_distr_l</a> (<a href="Coq.IntMap.Map.html#Map">Map</a> A) (<a href="Coq.IntMap.Map.html#Map">Map</a> A) (<a href="Coq.IntMap.Map.html#M0">M0</a> A) (<a href="Coq.IntMap.Map.html#MapMerge">MapMerge</a> A) <a href="Coq.Init.Datatypes.html#bool">bool</a> <a href="Coq.Init.Datatypes.html#false">false</a> <a href="Coq.Bool.Bool.html#orb">orb</a> <a href="Coq.IntMap.Addr.html#ad">ad</a>

438

(<a href="Coq.IntMap.Fset.html#in_dom">in_dom</a> A) (fun c:<a href="Coq.IntMap.Addr.html#ad">ad</a> => <a href="Coq.Init.Logic.html#refl_equal">refl_equal</a> _) (<a href="Coq.IntMap.Fset.html#in_dom_merge">in_dom_merge</a> A))

439

.

440

apply <a href="Coq.IntMap.Mapfold.html#MapFold_orb">MapFold_orb</a>.

441

<code class="keyword">Qed</code>.

442

443

444

<code class="keyword">Lemma</code> <a name="in_dom_DMerge_2"></a>in_dom_DMerge_2 :

445

forall (m:<a href="Coq.IntMap.Map.html#Map">Map</a> (<a href="Coq.IntMap.Map.html#Map">Map</a> A)) (a:<a href="Coq.IntMap.Addr.html#ad">ad</a>),

446

<a href="Coq.IntMap.Fset.html#in_dom">in_dom</a> A a (<a href="Coq.IntMap.Mapfold.html#DMerge">DMerge</a> m) = <a href="Coq.Init.Datatypes.html#true">true</a> ->

447

{b : <a href="Coq.IntMap.Addr.html#ad">ad</a> &

448

{m0 : <a href="Coq.IntMap.Map.html#Map">Map</a> A | <a href="Coq.IntMap.Map.html#MapGet">MapGet</a> _ m b = <a href="Coq.IntMap.Map.html#SOME">SOME</a> _ m0 /\ <a href="Coq.IntMap.Fset.html#in_dom">in_dom</a> A a m0 = <a href="Coq.Init.Datatypes.html#true">true</a>}}.

449

<code class="keyword">Proof</code>.

450

intros m a. rewrite <a href="Coq.IntMap.Mapfold.html#in_dom_DMerge_1">in_dom_DMerge_1</a>.

451

elim

452

(<a href="Coq.IntMap.Map.html#option_sum">option_sum</a> _

453

(<a href="Coq.IntMap.Mapiter.html#MapSweep">MapSweep</a> (<a href="Coq.IntMap.Map.html#Map">Map</a> A) (fun (_:<a href="Coq.IntMap.Addr.html#ad">ad</a>) (m0:<a href="Coq.IntMap.Map.html#Map">Map</a> A) => <a href="Coq.IntMap.Fset.html#in_dom">in_dom</a> A a m0) m)).

454

intro H. elim H. intro r. elim r. intros b m0 H0. intro. split with b. split with m0.

455

split. exact (<a href="Coq.IntMap.Mapiter.html#MapSweep_semantics_2">MapSweep_semantics_2</a> _ _ _ _ _ H0).

456

exact (<a href="Coq.IntMap.Mapiter.html#MapSweep_semantics_1">MapSweep_semantics_1</a> _ _ _ _ _ H0).

457

intro H. rewrite H. intro. discriminate H0.

458

<code class="keyword">Qed</code>.

459

460

461

<code class="keyword">Lemma</code> <a name="in_dom_DMerge_3"></a>in_dom_DMerge_3 :

462

forall (m:<a href="Coq.IntMap.Map.html#Map">Map</a> (<a href="Coq.IntMap.Map.html#Map">Map</a> A)) (a b:<a href="Coq.IntMap.Addr.html#ad">ad</a>) (m0:<a href="Coq.IntMap.Map.html#Map">Map</a> A),

463

<a href="Coq.IntMap.Map.html#MapGet">MapGet</a> _ m a = <a href="Coq.IntMap.Map.html#SOME">SOME</a> _ m0 ->

464

<a href="Coq.IntMap.Fset.html#in_dom">in_dom</a> A b m0 = <a href="Coq.Init.Datatypes.html#true">true</a> -> <a href="Coq.IntMap.Fset.html#in_dom">in_dom</a> A b (<a href="Coq.IntMap.Mapfold.html#DMerge">DMerge</a> m) = <a href="Coq.Init.Datatypes.html#true">true</a>.

465

<code class="keyword">Proof</code>.

466

intros m a b m0 H H0. rewrite <a href="Coq.IntMap.Mapfold.html#in_dom_DMerge_1">in_dom_DMerge_1</a>.

467

elim

468

(<a href="Coq.IntMap.Mapiter.html#MapSweep_semantics_4">MapSweep_semantics_4</a> _ (fun (_:<a href="Coq.IntMap.Addr.html#ad">ad</a>) (m'0:<a href="Coq.IntMap.Map.html#Map">Map</a> A) => <a href="Coq.IntMap.Fset.html#in_dom">in_dom</a> A b m'0) _ _ _

469

H H0).

470

intros a' H1. elim H1. intros m'0 H2. rewrite H2. reflexivity.

471

<code class="keyword">Qed</code>.

472

473

474

<code class="keyword">End</code> DMergeDef.</code>

475

<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://www.lri.fr/~filliatr/coqdoc/">coqdoc</a>

476

</body>

477

</html>

b'\\ No newline at end of file'

Older »