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

<code class="keyword">Definition</code> <a name="multiplicity"></a>multiplicity (m:<a href="Coq.Sets.Multiset.html#multiset">multiset</a>) (a:A) : <a href="Coq.Init.Datatypes.html#nat">nat</a> := let (f) := m in f a.

</code>

multiset equality

</td></tr></table>

<code>

<code class="keyword">Definition</code> <a name="meq"></a>meq (m1 m2:<a href="Coq.Sets.Multiset.html#multiset">multiset</a>) :=

forall a:A, <a href="Coq.Sets.Multiset.html#multiplicity">multiplicity</a> m1 a = <a href="Coq.Sets.Multiset.html#multiplicity">multiplicity</a> m2 a.

<code class="keyword">Hint</code> Unfold meq multiplicity.

<code class="keyword">Lemma</code> <a name="meq_refl"></a>meq_refl : forall x:<a href="Coq.Sets.Multiset.html#multiset">multiset</a>, <a href="Coq.Sets.Multiset.html#meq">meq</a> x x.

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

destruct x; auto.

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

<code class="keyword">Hint</code> Resolve <a href="Coq.Sets.Multiset.html#meq_refl">meq_refl</a>.

<code class="keyword">Lemma</code> <a name="meq_trans"></a>meq_trans : forall x y z:<a href="Coq.Sets.Multiset.html#multiset">multiset</a>, <a href="Coq.Sets.Multiset.html#meq">meq</a> x y -> <a href="Coq.Sets.Multiset.html#meq">meq</a> y z -> <a href="Coq.Sets.Multiset.html#meq">meq</a> x z.

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

unfold meq in |- *.

destruct x; destruct y; destruct z.

intros; rewrite H; auto.

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

<code class="keyword">Lemma</code> <a name="meq_sym"></a>meq_sym : forall x y:<a href="Coq.Sets.Multiset.html#multiset">multiset</a>, <a href="Coq.Sets.Multiset.html#meq">meq</a> x y -> <a href="Coq.Sets.Multiset.html#meq">meq</a> y x.

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

unfold meq in |- *.

destruct x; destruct y; auto.

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

<code class="keyword">Hint</code> <code class="keyword">Immediate</code> <a href="Coq.Sets.Multiset.html#meq_sym">meq_sym</a>.

</code>

multiset union

</td></tr></table>

<code>

<code class="keyword">Definition</code> <a name="munion"></a>munion (m1 m2:<a href="Coq.Sets.Multiset.html#multiset">multiset</a>) :=

<a href="Coq.Sets.Multiset.html#Bag">Bag</a> (fun a:A => <a href="Coq.Sets.Multiset.html#multiplicity">multiplicity</a> m1 a + <a href="Coq.Sets.Multiset.html#multiplicity">multiplicity</a> m2 a).

<code class="keyword">Lemma</code> <a name="munion_empty_left"></a>munion_empty_left : forall x:<a href="Coq.Sets.Multiset.html#multiset">multiset</a>, <a href="Coq.Sets.Multiset.html#meq">meq</a> x (<a href="Coq.Sets.Multiset.html#munion">munion</a> <a href="Coq.Sets.Multiset.html#EmptyBag">EmptyBag</a> x).

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

unfold meq in |- *; unfold munion in |- *; simpl in |- *; auto.

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

<code class="keyword">Hint</code> Resolve <a href="Coq.Sets.Multiset.html#munion_empty_left">munion_empty_left</a>.

<code class="keyword">Lemma</code> <a name="munion_empty_right"></a>munion_empty_right : forall x:<a href="Coq.Sets.Multiset.html#multiset">multiset</a>, <a href="Coq.Sets.Multiset.html#meq">meq</a> x (<a href="Coq.Sets.Multiset.html#munion">munion</a> x <a href="Coq.Sets.Multiset.html#EmptyBag">EmptyBag</a>).

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

unfold meq in |- *; unfold munion in |- *; simpl in |- *; auto.

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

<code class="keyword">Require</code> <code class="keyword">Import</code> Plus. <code class="keyword">Lemma</code> <a name="munion_comm"></a>munion_comm : forall x y:<a href="Coq.Sets.Multiset.html#multiset">multiset</a>, <a href="Coq.Sets.Multiset.html#meq">meq</a> (<a href="Coq.Sets.Multiset.html#munion">munion</a> x y) (<a href="Coq.Sets.Multiset.html#munion">munion</a> y x).

100

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

101

unfold meq in |- *; unfold multiplicity in |- *; unfold munion in |- *.

102

destruct x; destruct y; auto with arith.

103

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

104

<code class="keyword">Hint</code> Resolve <a href="Coq.Sets.Multiset.html#munion_comm">munion_comm</a>.

105

106

107

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

108

forall x y z:<a href="Coq.Sets.Multiset.html#multiset">multiset</a>, <a href="Coq.Sets.Multiset.html#meq">meq</a> (<a href="Coq.Sets.Multiset.html#munion">munion</a> (<a href="Coq.Sets.Multiset.html#munion">munion</a> x y) z) (<a href="Coq.Sets.Multiset.html#munion">munion</a> x (<a href="Coq.Sets.Multiset.html#munion">munion</a> y z)).

109

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

110

unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *.

111

destruct x; destruct y; destruct z; auto with arith.

112

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

113

<code class="keyword">Hint</code> Resolve <a href="Coq.Sets.Multiset.html#munion_ass">munion_ass</a>.

114

115

116

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

117

forall x y z:<a href="Coq.Sets.Multiset.html#multiset">multiset</a>, <a href="Coq.Sets.Multiset.html#meq">meq</a> x y -> <a href="Coq.Sets.Multiset.html#meq">meq</a> (<a href="Coq.Sets.Multiset.html#munion">munion</a> x z) (<a href="Coq.Sets.Multiset.html#munion">munion</a> y z).

118

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

119

unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *.

120

destruct x; destruct y; destruct z.

121

intros; elim H; auto with arith.

122

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

123

<code class="keyword">Hint</code> Resolve <a href="Coq.Sets.Multiset.html#meq_left">meq_left</a>.

124

125

126

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

127

forall x y z:<a href="Coq.Sets.Multiset.html#multiset">multiset</a>, <a href="Coq.Sets.Multiset.html#meq">meq</a> x y -> <a href="Coq.Sets.Multiset.html#meq">meq</a> (<a href="Coq.Sets.Multiset.html#munion">munion</a> z x) (<a href="Coq.Sets.Multiset.html#munion">munion</a> z y).

128

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

129

unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *.

130

destruct x; destruct y; destruct z.

131

intros; elim H; auto.

132

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

133

<code class="keyword">Hint</code> Resolve <a href="Coq.Sets.Multiset.html#meq_right">meq_right</a>.

134

135

136

</code>

137

138

139

Here we should make multiset an abstract datatype, by hiding <code>Bag</code>,

140

<code>munion</code>, <code>multiplicity</code>; all further properties are proved abstractly

141

</td></tr></table>

142

<code>

143

144

145

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

146

forall x y z:<a href="Coq.Sets.Multiset.html#multiset">multiset</a>, <a href="Coq.Sets.Multiset.html#meq">meq</a> (<a href="Coq.Sets.Multiset.html#munion">munion</a> x (<a href="Coq.Sets.Multiset.html#munion">munion</a> y z)) (<a href="Coq.Sets.Multiset.html#munion">munion</a> z (<a href="Coq.Sets.Multiset.html#munion">munion</a> x y)).

147

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

148

intros; apply (<a href="Coq.Sets.Permut.html#op_rotate">op_rotate</a> <a href="Coq.Sets.Multiset.html#multiset">multiset</a> <a href="Coq.Sets.Multiset.html#munion">munion</a> <a href="Coq.Sets.Multiset.html#meq">meq</a>); auto.

149

exact <a href="Coq.Sets.Multiset.html#meq_trans">meq_trans</a>.

150

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

151

152

153

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

154

forall x y z t:<a href="Coq.Sets.Multiset.html#multiset">multiset</a>, <a href="Coq.Sets.Multiset.html#meq">meq</a> x y -> <a href="Coq.Sets.Multiset.html#meq">meq</a> z t -> <a href="Coq.Sets.Multiset.html#meq">meq</a> (<a href="Coq.Sets.Multiset.html#munion">munion</a> x z) (<a href="Coq.Sets.Multiset.html#munion">munion</a> y t).

155

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

156

intros; apply (<a href="Coq.Sets.Permut.html#cong_congr">cong_congr</a> <a href="Coq.Sets.Multiset.html#multiset">multiset</a> <a href="Coq.Sets.Multiset.html#munion">munion</a> <a href="Coq.Sets.Multiset.html#meq">meq</a>); auto.

157

exact <a href="Coq.Sets.Multiset.html#meq_trans">meq_trans</a>.

158

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

159

160

161

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

162

forall x y z:<a href="Coq.Sets.Multiset.html#multiset">multiset</a>, <a href="Coq.Sets.Multiset.html#meq">meq</a> (<a href="Coq.Sets.Multiset.html#munion">munion</a> x (<a href="Coq.Sets.Multiset.html#munion">munion</a> y z)) (<a href="Coq.Sets.Multiset.html#munion">munion</a> y (<a href="Coq.Sets.Multiset.html#munion">munion</a> x z)).

163

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

164

intros; apply (<a href="Coq.Sets.Permut.html#perm_left">perm_left</a> <a href="Coq.Sets.Multiset.html#multiset">multiset</a> <a href="Coq.Sets.Multiset.html#munion">munion</a> <a href="Coq.Sets.Multiset.html#meq">meq</a>); auto.

165

exact <a href="Coq.Sets.Multiset.html#meq_trans">meq_trans</a>.

166

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

167

168

169

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

170

forall x y z t:<a href="Coq.Sets.Multiset.html#multiset">multiset</a>,

171

<a href="Coq.Sets.Multiset.html#meq">meq</a> (<a href="Coq.Sets.Multiset.html#munion">munion</a> x (<a href="Coq.Sets.Multiset.html#munion">munion</a> (<a href="Coq.Sets.Multiset.html#munion">munion</a> y z) t)) (<a href="Coq.Sets.Multiset.html#munion">munion</a> (<a href="Coq.Sets.Multiset.html#munion">munion</a> y (<a href="Coq.Sets.Multiset.html#munion">munion</a> x t)) z).

172

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

173

intros; apply (<a href="Coq.Sets.Permut.html#twist">twist</a> <a href="Coq.Sets.Multiset.html#multiset">multiset</a> <a href="Coq.Sets.Multiset.html#munion">munion</a> <a href="Coq.Sets.Multiset.html#meq">meq</a>); auto.

174

exact <a href="Coq.Sets.Multiset.html#meq_trans">meq_trans</a>.

175

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

176

177

178

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

179

forall x y z t:<a href="Coq.Sets.Multiset.html#multiset">multiset</a>,

180

181

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

182

intros; apply <a href="Coq.Sets.Multiset.html#meq_trans">meq_trans</a> with (<a href="Coq.Sets.Multiset.html#munion">munion</a> (<a href="Coq.Sets.Multiset.html#munion">munion</a> x (<a href="Coq.Sets.Multiset.html#munion">munion</a> y z)) t).

183

apply <a href="Coq.Sets.Multiset.html#meq_sym">meq_sym</a>; apply <a href="Coq.Sets.Multiset.html#munion_ass">munion_ass</a>.

184

apply <a href="Coq.Sets.Multiset.html#meq_left">meq_left</a>; apply <a href="Coq.Sets.Multiset.html#munion_perm_left">munion_perm_left</a>.

185

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

186

187

188

</code>

189

190

191

specific for treesort

192

</td></tr></table>

193

<code>

194

195

196

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

197

forall x y z t u:<a href="Coq.Sets.Multiset.html#multiset">multiset</a>,

198

<a href="Coq.Sets.Multiset.html#meq">meq</a> u (<a href="Coq.Sets.Multiset.html#munion">munion</a> y z) ->

199

<a href="Coq.Sets.Multiset.html#meq">meq</a> (<a href="Coq.Sets.Multiset.html#munion">munion</a> x (<a href="Coq.Sets.Multiset.html#munion">munion</a> u t)) (<a href="Coq.Sets.Multiset.html#munion">munion</a> (<a href="Coq.Sets.Multiset.html#munion">munion</a> y (<a href="Coq.Sets.Multiset.html#munion">munion</a> x t)) z).

200

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

201

intros; apply <a href="Coq.Sets.Multiset.html#meq_trans">meq_trans</a> with (<a href="Coq.Sets.Multiset.html#munion">munion</a> x (<a href="Coq.Sets.Multiset.html#munion">munion</a> (<a href="Coq.Sets.Multiset.html#munion">munion</a> y z) t)).

202

apply <a href="Coq.Sets.Multiset.html#meq_right">meq_right</a>; apply <a href="Coq.Sets.Multiset.html#meq_left">meq_left</a>; trivial.

203

apply <a href="Coq.Sets.Multiset.html#multiset_twist1">multiset_twist1</a>.

204

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

205

206

207

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

208

forall x y z t u:<a href="Coq.Sets.Multiset.html#multiset">multiset</a>,

209

<a href="Coq.Sets.Multiset.html#meq">meq</a> u (<a href="Coq.Sets.Multiset.html#munion">munion</a> y z) ->

210

211

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

212

213

apply <a href="Coq.Sets.Multiset.html#meq_right">meq_right</a>; apply <a href="Coq.Sets.Multiset.html#meq_left">meq_left</a>; trivial.

214

apply <a href="Coq.Sets.Multiset.html#multiset_twist2">multiset_twist2</a>.

215

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

216

217

218

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

219

220

221

<code class="keyword">Unset</code> <code class="keyword">Implicit</code> Arguments.

222

223

224

<code class="keyword">Hint</code> Unfold meq multiplicity: v62 datatypes.

225

<code class="keyword">Hint</code> Resolve <a href="Coq.Sets.Multiset.html#munion_empty_right">munion_empty_right</a> <a href="Coq.Sets.Multiset.html#munion_comm">munion_comm</a> <a href="Coq.Sets.Multiset.html#munion_ass">munion_ass</a> <a href="Coq.Sets.Multiset.html#meq_left">meq_left</a> <a href="Coq.Sets.Multiset.html#meq_right">meq_right</a>

226

<a href="Coq.Sets.Multiset.html#munion_empty_left">munion_empty_left</a>: v62 datatypes.

227

<code class="keyword">Hint</code> <code class="keyword">Immediate</code> <a href="Coq.Sets.Multiset.html#meq_sym">meq_sym</a>: v62 datatypes.</code>

228

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

229

</body>

230

</html>

b'\\ No newline at end of file'

Older »