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

<code class="keyword">Definition</code> <a name="Zeven_odd_dec"></a>Zeven_odd_dec : forall z:<a href="Coq.ZArith.BinInt.html#Z">Z</a>, {<a href="Coq.ZArith.Zeven.html#Zeven">Zeven</a> z} + {<a href="Coq.ZArith.Zeven.html#Zodd">Zodd</a> z}.

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

intro z. case z;

  [ left; compute in |- *; trivial

| intro p; case p; intros;

(right; compute in |- *; exact I) || (left; compute in |- *; exact I)

| intro p; case p; intros;

(right; compute in |- *; exact I) || (left; compute in |- *; exact I) ].

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

<code class="keyword">Definition</code> <a name="Zeven_dec"></a>Zeven_dec : forall z:<a href="Coq.ZArith.BinInt.html#Z">Z</a>, {<a href="Coq.ZArith.Zeven.html#Zeven">Zeven</a> z} + {~ <a href="Coq.ZArith.Zeven.html#Zeven">Zeven</a> z}.

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

intro z. case z;

  [ left; compute in |- *; trivial

| intro p; case p; intros;

(left; compute in |- *; exact I) || (right; compute in |- *; trivial)

| intro p; case p; intros;

(left; compute in |- *; exact I) || (right; compute in |- *; trivial) ].

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

<code class="keyword">Definition</code> <a name="Zodd_dec"></a>Zodd_dec : forall z:<a href="Coq.ZArith.BinInt.html#Z">Z</a>, {<a href="Coq.ZArith.Zeven.html#Zodd">Zodd</a> z} + {~ <a href="Coq.ZArith.Zeven.html#Zodd">Zodd</a> z}.

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

intro z. case z;

  [ right; compute in |- *; trivial

| intro p; case p; intros;

(left; compute in |- *; exact I) || (right; compute in |- *; trivial)

| intro p; case p; intros;

(left; compute in |- *; exact I) || (right; compute in |- *; trivial) ].

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

100

<code class="keyword">Lemma</code> <a name="Zeven_not_Zodd"></a>Zeven_not_Zodd : forall n:<a href="Coq.ZArith.BinInt.html#Z">Z</a>, <a href="Coq.ZArith.Zeven.html#Zeven">Zeven</a> n -> ~ <a href="Coq.ZArith.Zeven.html#Zodd">Zodd</a> n.

101

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

102

intro z; destruct z; [ idtac | destruct p | destruct p ]; compute in |- *;

103

trivial.

104

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

105

106

107

<code class="keyword">Lemma</code> <a name="Zodd_not_Zeven"></a>Zodd_not_Zeven : forall n:<a href="Coq.ZArith.BinInt.html#Z">Z</a>, <a href="Coq.ZArith.Zeven.html#Zodd">Zodd</a> n -> ~ <a href="Coq.ZArith.Zeven.html#Zeven">Zeven</a> n.

108

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

109

intro z; destruct z; [ idtac | destruct p | destruct p ]; compute in |- *;

110

trivial.

111

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

112

113

114

<code class="keyword">Lemma</code> <a name="Zeven_Sn"></a>Zeven_Sn : forall n:<a href="Coq.ZArith.BinInt.html#Z">Z</a>, <a href="Coq.ZArith.Zeven.html#Zodd">Zodd</a> n -> <a href="Coq.ZArith.Zeven.html#Zeven">Zeven</a> (<a href="Coq.ZArith.BinInt.html#Zsucc">Zsucc</a> n).

115

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

116

intro z; destruct z; unfold Zsucc in |- *;

117

[ idtac | destruct p | destruct p ]; simpl in |- *;

118

trivial.

119

unfold Pdouble_minus_one in |- *; case p; simpl in |- *; auto.

120

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

121

122

123

<code class="keyword">Lemma</code> <a name="Zodd_Sn"></a>Zodd_Sn : forall n:<a href="Coq.ZArith.BinInt.html#Z">Z</a>, <a href="Coq.ZArith.Zeven.html#Zeven">Zeven</a> n -> <a href="Coq.ZArith.Zeven.html#Zodd">Zodd</a> (<a href="Coq.ZArith.BinInt.html#Zsucc">Zsucc</a> n).

124

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

125

intro z; destruct z; unfold Zsucc in |- *;

126

[ idtac | destruct p | destruct p ]; simpl in |- *;

127

trivial.

128

unfold Pdouble_minus_one in |- *; case p; simpl in |- *; auto.

129

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

130

131

132

<code class="keyword">Lemma</code> <a name="Zeven_pred"></a>Zeven_pred : forall n:<a href="Coq.ZArith.BinInt.html#Z">Z</a>, <a href="Coq.ZArith.Zeven.html#Zodd">Zodd</a> n -> <a href="Coq.ZArith.Zeven.html#Zeven">Zeven</a> (<a href="Coq.ZArith.BinInt.html#Zpred">Zpred</a> n).

133

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

134

intro z; destruct z; unfold Zpred in |- *;

135

[ idtac | destruct p | destruct p ]; simpl in |- *;

136

trivial.

137

unfold Pdouble_minus_one in |- *; case p; simpl in |- *; auto.

138

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

139

140

141

<code class="keyword">Lemma</code> <a name="Zodd_pred"></a>Zodd_pred : forall n:<a href="Coq.ZArith.BinInt.html#Z">Z</a>, <a href="Coq.ZArith.Zeven.html#Zeven">Zeven</a> n -> <a href="Coq.ZArith.Zeven.html#Zodd">Zodd</a> (<a href="Coq.ZArith.BinInt.html#Zpred">Zpred</a> n).

142

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

143

intro z; destruct z; unfold Zpred in |- *;

144

[ idtac | destruct p | destruct p ]; simpl in |- *;

145

trivial.

146

unfold Pdouble_minus_one in |- *; case p; simpl in |- *; auto.

147

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

148

149

150

<code class="keyword">Hint</code> Unfold Zeven Zodd: zarith.

151

152

153

</code>

154

155

156

<code>Zdiv2</code> is defined on all <code>Z</code>, but notice that for odd negative

157

integers it is not the euclidean quotient: in that case we have <code>n =

158

2*(n/2)-1</code>

159

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

160

<code>

161

162

163

<code class="keyword">Definition</code> <a name="Zdiv2"></a>Zdiv2 (z:<a href="Coq.ZArith.BinInt.html#Z">Z</a>) :=

164

match z with

165

| <a href="Coq.ZArith.BinInt.html#Z0">Z0</a> => 0%Z

166

| <a href="Coq.ZArith.BinInt.html#Zpos">Zpos</a> <a href="Coq.NArith.BinPos.html#xH">xH</a> => 0%Z

167

| <a href="Coq.ZArith.BinInt.html#Zpos">Zpos</a> p => <a href="Coq.ZArith.BinInt.html#Zpos">Zpos</a> (<a href="Coq.NArith.BinPos.html#Pdiv2">Pdiv2</a> p)

168

| <a href="Coq.ZArith.BinInt.html#Zneg">Zneg</a> <a href="Coq.NArith.BinPos.html#xH">xH</a> => 0%Z

169

| <a href="Coq.ZArith.BinInt.html#Zneg">Zneg</a> p => <a href="Coq.ZArith.BinInt.html#Zneg">Zneg</a> (<a href="Coq.NArith.BinPos.html#Pdiv2">Pdiv2</a> p)

170

end.

171

172

173

<code class="keyword">Lemma</code> <a name="Zeven_div2"></a>Zeven_div2 : forall n:<a href="Coq.ZArith.BinInt.html#Z">Z</a>, <a href="Coq.ZArith.Zeven.html#Zeven">Zeven</a> n -> n = (2 * <a href="Coq.ZArith.Zeven.html#Zdiv2">Zdiv2</a> n)%Z.

174

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

175

intro x; destruct x.

176

auto with arith.

177

destruct p; auto with arith.

178

intros. absurd (<a href="Coq.ZArith.Zeven.html#Zeven">Zeven</a> (<a href="Coq.ZArith.BinInt.html#Zpos">Zpos</a> (<a href="Coq.NArith.BinPos.html#xI">xI</a> p))); red in |- *; auto with arith.

179

intros. absurd (<a href="Coq.ZArith.Zeven.html#Zeven">Zeven</a> 1); red in |- *; auto with arith.

180

destruct p; auto with arith.

181

intros. absurd (<a href="Coq.ZArith.Zeven.html#Zeven">Zeven</a> (<a href="Coq.ZArith.BinInt.html#Zneg">Zneg</a> (<a href="Coq.NArith.BinPos.html#xI">xI</a> p))); red in |- *; auto with arith.

182

intros. absurd (<a href="Coq.ZArith.Zeven.html#Zeven">Zeven</a> (-1)); red in |- *; auto with arith.

183

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

184

185

186

<code class="keyword">Lemma</code> <a name="Zodd_div2"></a>Zodd_div2 : forall n:<a href="Coq.ZArith.BinInt.html#Z">Z</a>, (n >= 0)%Z -> <a href="Coq.ZArith.Zeven.html#Zodd">Zodd</a> n -> n = (2 * <a href="Coq.ZArith.Zeven.html#Zdiv2">Zdiv2</a> n + 1)%Z.

187

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

188

intro x; destruct x.

189

intros. absurd (<a href="Coq.ZArith.Zeven.html#Zodd">Zodd</a> 0); red in |- *; auto with arith.

190

destruct p; auto with arith.

191

intros. absurd (<a href="Coq.ZArith.Zeven.html#Zodd">Zodd</a> (<a href="Coq.ZArith.BinInt.html#Zpos">Zpos</a> (<a href="Coq.NArith.BinPos.html#xO">xO</a> p))); red in |- *; auto with arith.

192

intros. absurd (<a href="Coq.ZArith.BinInt.html#Zneg">Zneg</a> p >= 0)%Z; red in |- *; auto with arith.

193

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

194

195

196

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

197

forall n:<a href="Coq.ZArith.BinInt.html#Z">Z</a>, (n <= 0)%Z -> <a href="Coq.ZArith.Zeven.html#Zodd">Zodd</a> n -> n = (2 * <a href="Coq.ZArith.Zeven.html#Zdiv2">Zdiv2</a> n - 1)%Z.

198

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

199

intro x; destruct x.

200

intros. absurd (<a href="Coq.ZArith.Zeven.html#Zodd">Zodd</a> 0); red in |- *; auto with arith.

201

intros. absurd (<a href="Coq.ZArith.BinInt.html#Zneg">Zneg</a> p >= 0)%Z; red in |- *; auto with arith.

202

destruct p; auto with arith.

203

intros. absurd (<a href="Coq.ZArith.Zeven.html#Zodd">Zodd</a> (<a href="Coq.ZArith.BinInt.html#Zneg">Zneg</a> (<a href="Coq.NArith.BinPos.html#xO">xO</a> p))); red in |- *; auto with arith.

204

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

205

206

207

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

208

forall n:<a href="Coq.ZArith.BinInt.html#Z">Z</a>, {y : <a href="Coq.ZArith.BinInt.html#Z">Z</a> | n = (2 * y)%Z} + {y : <a href="Coq.ZArith.BinInt.html#Z">Z</a> | n = (2 * y + 1)%Z}.

209

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

210

intros x.

211

elim (<a href="Coq.ZArith.Zeven.html#Zeven_odd_dec">Zeven_odd_dec</a> x); intro.

212

left. split with (<a href="Coq.ZArith.Zeven.html#Zdiv2">Zdiv2</a> x). exact (<a href="Coq.ZArith.Zeven.html#Zeven_div2">Zeven_div2</a> x a).

213

right. generalize b; clear b; case x.

214

intro b; inversion b.

215

intro p; split with (<a href="Coq.ZArith.Zeven.html#Zdiv2">Zdiv2</a> (<a href="Coq.ZArith.BinInt.html#Zpos">Zpos</a> p)). apply (<a href="Coq.ZArith.Zeven.html#Zodd_div2">Zodd_div2</a> (<a href="Coq.ZArith.BinInt.html#Zpos">Zpos</a> p)); trivial.

216

unfold Zge, Zcompare in |- *; simpl in |- *; discriminate.

217

intro p; split with (<a href="Coq.ZArith.Zeven.html#Zdiv2">Zdiv2</a> (<a href="Coq.ZArith.BinInt.html#Zpred">Zpred</a> (<a href="Coq.ZArith.BinInt.html#Zneg">Zneg</a> p))).

218

pattern (<a href="Coq.ZArith.BinInt.html#Zneg">Zneg</a> p) at 1 in |- *; rewrite (<a href="Coq.ZArith.BinInt.html#Zsucc_pred">Zsucc_pred</a> (<a href="Coq.ZArith.BinInt.html#Zneg">Zneg</a> p)).

219

pattern (<a href="Coq.ZArith.BinInt.html#Zpred">Zpred</a> (<a href="Coq.ZArith.BinInt.html#Zneg">Zneg</a> p)) at 1 in |- *; rewrite (<a href="Coq.ZArith.Zeven.html#Zeven_div2">Zeven_div2</a> (<a href="Coq.ZArith.BinInt.html#Zpred">Zpred</a> (<a href="Coq.ZArith.BinInt.html#Zneg">Zneg</a> p))).

220

reflexivity.

221

apply <a href="Coq.ZArith.Zeven.html#Zeven_pred">Zeven_pred</a>; assumption.

222

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

223

224

225

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

226

forall n:<a href="Coq.ZArith.BinInt.html#Z">Z</a>,

227

{p : <a href="Coq.ZArith.BinInt.html#Z">Z</a> * <a href="Coq.ZArith.BinInt.html#Z">Z</a> |

228

let (x1, x2) := p in n = (x1 + x2)%Z /\ (x1 = x2 \/ x2 = (x1 + 1)%Z)}.

229

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

230

intros x.

231

elim (<a href="Coq.ZArith.Zeven.html#Z_modulo_2">Z_modulo_2</a> x); intros [y Hy]; rewrite <a href="Coq.ZArith.BinInt.html#Zmult_comm">Zmult_comm</a> in Hy;

232

rewrite <- <a href="Coq.ZArith.BinInt.html#Zplus_diag_eq_mult_2">Zplus_diag_eq_mult_2</a> in Hy.

233

exists (y, y); split.

234

assumption.

235

left; reflexivity.

236

exists (y, (y + 1)%Z); split.

237

rewrite <a href="Coq.ZArith.BinInt.html#Zplus_assoc">Zplus_assoc</a>; assumption.

238

right; reflexivity.

239

240

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

241

</body>

242

</html>

b'\\ No newline at end of file'

Older »