## lustrec / optim / oversampling / streams2_lus.v @ 6a93d814

History | View | Annotate | Download (17.8 KB)

1 | 6a93d814 | xthirioux | Definition mapT (F : Type -> Type) {A B} := (A -> B) -> (F A) -> (F B). |
---|---|---|---|

2 | |||

3 | Definition applyT (F : Type -> Type) {A B} := (F (A -> B)) -> (F A) -> (F B). |
||

4 | |||

5 | Definition option_apply {A B} : @applyT option A B := |
||

6 | fun f a => |
||

7 | match f, a with |
||

8 | | Some f, Some a => Some (f a) |
||

9 | | _ , _ => None |
||

10 | end. |
||

11 | |||

12 | Require Import Streams. |
||

13 | Require List. |
||

14 | Require Import Setoid. |
||

15 | |||

16 | Axiom eqst_eq : forall {A} (s s' : Stream A), EqSt s s' -> s = s'. |
||

17 | |||

18 | Theorem inv_inv : forall {A} (P : Stream A -> Prop) (s : Stream A), ForAll P s -> ForAll (fun s' => ForAll P s') s. |
||

19 | Proof. |
||

20 | intros A P. |
||

21 | cofix proof. |
||

22 | destruct s as (s0, s'). |
||

23 | intro H. |
||

24 | apply HereAndFurther. |
||

25 | exact H. |
||

26 | |||

27 | simpl. |
||

28 | apply proof. |
||

29 | inversion H. |
||

30 | assumption. |
||

31 | Qed. |
||

32 | |||

33 | Theorem evt_inv : forall {A} (P Q : Stream A -> Prop) (s : Stream A), |
||

34 | ForAll P s -> Exists Q s -> Exists (fun s' => P s' /\ Q s') s. |
||

35 | Proof. |
||

36 | induction 2. |
||

37 | apply Here. |
||

38 | inversion H. |
||

39 | intuition. |
||

40 | |||

41 | apply Further. |
||

42 | apply IHExists. |
||

43 | inversion H. |
||

44 | assumption. |
||

45 | Qed. |
||

46 | |||

47 | CoFixpoint ForAll_apply {A} {P Q : (Stream A -> Prop)} : forall s, (ForAll P s) -> (ForAll (fun s => P s -> Q s) s) -> (ForAll Q s) := |
||

48 | fun s always_p always_pq => |
||

49 | match always_p, always_pq with |
||

50 | | (HereAndFurther p_s always_p'), (HereAndFurther pq_s always_pq') => HereAndFurther s (pq_s p_s) (ForAll_apply (tl s) always_p' always_pq') |
||

51 | end. |
||

52 | |||

53 | CoFixpoint necessitation {A} {P : Stream A -> Prop} (I : forall s, P s) s : ForAll P s := |
||

54 | HereAndFurther s (I s) (necessitation I (tl s)). |
||

55 | |||

56 | Definition concat {A} (prefix : list A) (suffix : Stream A) : Stream A := |
||

57 | List.fold_left (fun q t => Cons t q) prefix suffix. |
||

58 | |||

59 | Theorem eqst_concat : forall {A} pfx (sfx sfx' : Stream A), EqSt sfx sfx' -> EqSt (concat pfx sfx) (concat pfx sfx'). |
||

60 | Proof. |
||

61 | induction pfx. |
||

62 | auto. |
||

63 | |||

64 | simpl. |
||

65 | intros. |
||

66 | apply IHpfx. |
||

67 | apply eqst. |
||

68 | reflexivity. |
||

69 | |||

70 | exact H. |
||

71 | Qed. |
||

72 | |||

73 | Theorem evt_id : forall {A} (s : Stream A), Exists (fun s' => s = s') s. |
||

74 | Proof. |
||

75 | intros. |
||

76 | apply Here. |
||

77 | reflexivity. |
||

78 | Qed. |
||

79 | |||

80 | Theorem evt_concat : forall {A} (P : Stream A -> Prop) p (s : Stream A), Exists P s -> Exists P (concat p s). |
||

81 | Proof. |
||

82 | induction p. |
||

83 | trivial. |
||

84 | |||

85 | intros s H. |
||

86 | apply (IHp (Cons a s)). |
||

87 | apply Further. |
||

88 | exact H. |
||

89 | Qed. |
||

90 | |||

91 | Theorem inv_concat : forall {A} (P : Stream A -> Prop) p (s : Stream A), ForAll P (concat p s) -> ForAll P s. |
||

92 | Proof. |
||

93 | induction p. |
||

94 | trivial. |
||

95 | |||

96 | simpl. |
||

97 | intros s H. |
||

98 | generalize (IHp (Cons a s) H). |
||

99 | intro H'. |
||

100 | inversion H'. |
||

101 | assumption. |
||

102 | Qed. |
||

103 | |||

104 | |||

105 | CoFixpoint lift {A} (v : A) := Cons v (lift v). |
||

106 | |||

107 | Lemma hd_lift : forall {A} {v : A}, hd (lift v) = v. |
||

108 | Proof. |
||

109 | reflexivity. |
||

110 | Qed. |
||

111 | |||

112 | Lemma tl_lift : forall {A} {v : A}, tl (lift v) = lift v. |
||

113 | Proof. |
||

114 | reflexivity. |
||

115 | Qed. |
||

116 | |||

117 | CoFixpoint apply {A B} : @applyT Stream A B := |
||

118 | fun f a => |
||

119 | match f, a with |
||

120 | | (Cons f0 f'), (Cons a0 a') => Cons (f0 a0) (apply f' a') |
||

121 | end. |
||

122 | |||

123 | Lemma hd_apply : forall {A B} {f : Stream (A -> B)} {a : Stream A}, hd (apply f a) = (hd f) (hd a). |
||

124 | Proof. |
||

125 | destruct f; destruct a. |
||

126 | reflexivity. |
||

127 | Qed. |
||

128 | |||

129 | Lemma tl_apply : forall {A B} {f : Stream (A -> B)} {a : Stream A}, tl (apply f a) = apply (tl f) (tl a). |
||

130 | Proof. |
||

131 | destruct f; destruct a. |
||

132 | reflexivity. |
||

133 | Qed. |
||

134 | |||

135 | Lemma cons_apply : forall {A B} {f0 : A -> B} {f' : Stream (A -> B)} {a0 : A} {a' : Stream A}, EqSt (apply (Cons f0 f') (Cons a0 a')) (Cons (f0 a0) (apply f' a')). |
||

136 | Proof. |
||

137 | intros. |
||

138 | apply eqst. |
||

139 | reflexivity. |
||

140 | |||

141 | apply EqSt_reflex. |
||

142 | Qed. |
||

143 | |||

144 | Theorem inv_map : forall {A B} (f : A -> B) P (s : Stream A), ForAll P (apply (lift f) s) -> ForAll (fun s' => P (apply (lift f) s')) s. |
||

145 | Proof. |
||

146 | intros A B f P. |
||

147 | cofix proof. |
||

148 | destruct s as (s0, s'). |
||

149 | intro H. |
||

150 | inversion H. |
||

151 | apply HereAndFurther. |
||

152 | assumption. |
||

153 | |||

154 | simpl. |
||

155 | apply proof. |
||

156 | assumption. |
||

157 | Qed. |
||

158 | |||

159 | Theorem map_inv : forall {A B} (f : A -> B) P (s : Stream A), ForAll (fun s' => P (apply (lift f) s')) s -> ForAll P (apply (lift f) s). |
||

160 | Proof. |
||

161 | intros A B f P. |
||

162 | cofix proof. |
||

163 | destruct s as (s0, s'). |
||

164 | intro H. |
||

165 | inversion H. |
||

166 | apply HereAndFurther. |
||

167 | assumption. |
||

168 | |||

169 | simpl. |
||

170 | apply proof. |
||

171 | assumption. |
||

172 | Qed. |
||

173 | |||

174 | Theorem evt_map : forall {A B} (f : A -> B) P (s : Stream A), Exists P (apply (lift f) s) -> Exists (fun s' => P (apply (lift f) s')) s. |
||

175 | Proof. |
||

176 | intros A B f P s. |
||

177 | remember (apply (lift f) s) as ss. |
||

178 | intro H. |
||

179 | revert s Heqss. |
||

180 | induction H. |
||

181 | intros. |
||

182 | apply Here. |
||

183 | rewrite <- Heqss. |
||

184 | exact H. |
||

185 | |||

186 | intros. |
||

187 | apply Further. |
||

188 | apply (IHExists (tl s)). |
||

189 | rewrite <- tl_lift. |
||

190 | rewrite <- tl_apply. |
||

191 | apply f_equal. |
||

192 | exact Heqss. |
||

193 | Qed. |
||

194 | |||

195 | Theorem map_evt : forall {A B} (f : A -> B) P (s : Stream A), Exists (fun s' => P (apply (lift f) s')) s -> Exists P (apply (lift f) s). |
||

196 | Proof. |
||

197 | intros A B f P s. |
||

198 | intro H. |
||

199 | induction H. |
||

200 | apply Here. |
||

201 | exact H. |
||

202 | |||

203 | apply Further. |
||

204 | rewrite tl_apply. |
||

205 | rewrite tl_lift. |
||

206 | exact IHExists. |
||

207 | Qed. |
||

208 | |||

209 | Definition zip {A B} (s : Stream A * Stream B) := apply (apply (lift (fun a b => (a, b))) (fst s)) (snd s). |
||

210 | |||

211 | Lemma zip_fst_eqst : forall {A B}, forall (s1 s1' : Stream A) (s2 s2' : Stream B), |
||

212 | EqSt (zip (s1, s2)) (zip (s1', s2')) -> EqSt s1 s1'. |
||

213 | Proof. |
||

214 | intros A B. |
||

215 | cofix proof. |
||

216 | destruct s1; destruct s1'; destruct s2; destruct s2'. |
||

217 | intro. |
||

218 | inversion H. |
||

219 | apply eqst. |
||

220 | simpl in H0. |
||

221 | simpl in H1. |
||

222 | injection H0. |
||

223 | intros. |
||

224 | subst. |
||

225 | reflexivity. |
||

226 | |||

227 | eapply proof. |
||

228 | apply H1. |
||

229 | Qed. |
||

230 | |||

231 | Lemma zip_fst : forall {A B}, forall (s1 s1' : Stream A) (s2 s2' : Stream B), |
||

232 | zip (s1, s2) = zip (s1', s2') -> s1 = s1'. |
||

233 | Proof. |
||

234 | intros. |
||

235 | apply eqst_eq. |
||

236 | apply (zip_fst_eqst s1 s1' s2 s2'). |
||

237 | rewrite H. |
||

238 | apply EqSt_reflex. |
||

239 | Qed. |
||

240 | |||

241 | Lemma zip_snd_eqst : forall {A B}, forall (s1 s1' : Stream A) (s2 s2' : Stream B), |
||

242 | EqSt (zip (s1, s2)) (zip (s1', s2')) -> EqSt s2 s2'. |
||

243 | Proof. |
||

244 | intros A B. |
||

245 | cofix proof. |
||

246 | destruct s1; destruct s1'; destruct s2; destruct s2'. |
||

247 | intro. |
||

248 | inversion H. |
||

249 | apply eqst. |
||

250 | simpl in H0. |
||

251 | simpl in H1. |
||

252 | injection H0. |
||

253 | intros. |
||

254 | subst. |
||

255 | reflexivity. |
||

256 | |||

257 | eapply proof. |
||

258 | apply H1. |
||

259 | Qed. |
||

260 | |||

261 | Lemma zip_snd : forall {A B}, forall (s1 s1' : Stream A) (s2 s2' : Stream B), |
||

262 | zip (s1, s2) = zip (s1', s2') -> s2 = s2'. |
||

263 | Proof. |
||

264 | intros. |
||

265 | apply eqst_eq. |
||

266 | apply (zip_snd_eqst s1 s1' s2 s2'). |
||

267 | rewrite H. |
||

268 | apply EqSt_reflex. |
||

269 | Qed. |
||

270 | |||

271 | Definition unzip {A B} (s : Stream (A*B)) := (apply (lift (@fst _ _)) s, apply (lift (@snd _ _)) s). |
||

272 | |||

273 | Lemma fst_zip_eqst : forall {A B} (s1 : Stream A) (s2 : Stream B), EqSt (apply (lift (@fst _ _)) (zip (s1, s2))) s1. |
||

274 | Proof. |
||

275 | intros A B. |
||

276 | cofix proof. |
||

277 | destruct s1; destruct s2. |
||

278 | apply eqst. |
||

279 | reflexivity. |
||

280 | |||

281 | apply proof. |
||

282 | Qed. |
||

283 | |||

284 | Lemma fst_zip : forall {A B} (s1 : Stream A) (s2 : Stream B), apply (lift (@fst _ _)) (zip (s1, s2)) = s1. |
||

285 | Proof. |
||

286 | intros. |
||

287 | apply eqst_eq. |
||

288 | apply fst_zip_eqst. |
||

289 | Qed. |
||

290 | |||

291 | Lemma snd_zip_eqst : forall {A B} (s1 : Stream A) (s2 : Stream B), EqSt (apply (lift (@snd _ _)) (zip (s1, s2))) s2. |
||

292 | Proof. |
||

293 | intros A B. |
||

294 | cofix proof. |
||

295 | destruct s1; destruct s2. |
||

296 | apply eqst. |
||

297 | reflexivity. |
||

298 | |||

299 | apply proof. |
||

300 | Qed. |
||

301 | |||

302 | Lemma snd_zip : forall {A B} (s1 : Stream A) (s2 : Stream B), apply (lift (@snd _ _)) (zip (s1, s2)) = s2. |
||

303 | Proof. |
||

304 | intros. |
||

305 | apply eqst_eq. |
||

306 | apply snd_zip_eqst. |
||

307 | Qed. |
||

308 | |||

309 | Lemma zip_unzip_eqst : forall {A B} (s : Stream (A*B)), EqSt (zip (unzip s)) s. |
||

310 | Proof. |
||

311 | intros A B. |
||

312 | cofix proof. |
||

313 | destruct s. |
||

314 | apply eqst. |
||

315 | simpl. |
||

316 | destruct p. |
||

317 | reflexivity. |
||

318 | |||

319 | simpl. |
||

320 | apply proof. |
||

321 | Qed. |
||

322 | |||

323 | Lemma zip_unzip : forall {A B} (s : Stream (A*B)), zip (unzip s) = s. |
||

324 | Proof. |
||

325 | intros. |
||

326 | apply eqst_eq. |
||

327 | apply zip_unzip_eqst. |
||

328 | Qed. |
||

329 | |||

330 | (* |
||

331 | CoInductive transition {A} (T : A -> A -> Prop) : Stream A -> Prop := |
||

332 | | Tick : forall a0 a1 s'', T a0 a1 -> transition T (Cons a1 s'') -> transition T (Cons a0 (Cons a1 s'')). |
||

333 | |||

334 | Fixpoint prefix {A} (I : A -> Prop) (T : A -> A -> Prop) (k : nat) : Stream A -> Prop := |
||

335 | match k with |
||

336 | | 0 => fun s => True |
||

337 | | S k' => fun s => (I (hd s) \/ (T (hd s) (hd (tl s)) /\ prefix I T k' (tl s))) |
||

338 | end. |
||

339 | |||

340 | Lemma I_prefix : forall {A} (I : A -> Prop) (T : A -> A -> Prop) k (s : Stream A), I (hd s) -> prefix I T k s. |
||

341 | Proof. |
||

342 | destruct k. |
||

343 | simpl. |
||

344 | trivial. |
||

345 | |||

346 | simpl. |
||

347 | left. |
||

348 | trivial. |
||

349 | Qed. |
||

350 | |||

351 | Lemma T_prefix : forall {A} (I : A -> Prop) (T : A -> A -> Prop) k (s : Stream A), T (hd s) (hd (tl s)) -> prefix I T k (tl s) -> prefix I T k s. |
||

352 | Proof. |
||

353 | destruct k. |
||

354 | simpl. |
||

355 | trivial. |
||

356 | |||

357 | simpl. |
||

358 | right. |
||

359 | trivial. |
||

360 | Qed. |
||

361 | |||

362 | Lemma prefix_mono_k : forall {A} I T k (s : Stream A), prefix I T (S k) s -> prefix I T k s. |
||

363 | Proof. |
||

364 | |||

365 | Qed. |
||

366 | *) |
||

367 | |||

368 | CoFixpoint history_rec {A} (past : list A) (s : Stream A) : Stream (list A * A) := |
||

369 | match s with |
||

370 | | Cons s0 s' => Cons (past, s0) (history_rec (cons s0 past) s') |
||

371 | end. |
||

372 | |||

373 | Definition history {A} (s : Stream A) : Stream (list A * A) := history_rec nil s. |
||

374 | |||

375 | Theorem eqst_history_rec : forall {A} (pfx : list A) (sfx sfx' : Stream A), |
||

376 | EqSt sfx sfx' -> EqSt (history_rec pfx sfx) (history_rec pfx sfx'). |
||

377 | Proof. |
||

378 | intros A. |
||

379 | cofix proof. |
||

380 | destruct sfx as (sfx0, sfxq). |
||

381 | destruct sfx' as (sfx0', sfxq'). |
||

382 | intro H. |
||

383 | inversion H. |
||

384 | simpl in H0. |
||

385 | rewrite H0. |
||

386 | apply eqst. |
||

387 | reflexivity. |
||

388 | |||

389 | apply (proof _ sfxq sfxq'). |
||

390 | assumption. |
||

391 | Qed. |
||

392 | |||

393 | Theorem eqst_history : forall {A} (sfx sfx' : Stream A), |
||

394 | EqSt sfx sfx' -> EqSt (history sfx) (history sfx'). |
||

395 | Proof. |
||

396 | intros. |
||

397 | apply eqst_history_rec. |
||

398 | assumption. |
||

399 | Qed. |
||

400 | |||

401 | Theorem unzip_history_rec : forall {A} (pfx : list A) (sfx : Stream A), EqSt (snd (unzip (history_rec pfx sfx))) sfx. |
||

402 | Proof. |
||

403 | intro A. |
||

404 | cofix proof. |
||

405 | destruct sfx as (sfx0, sfx'). |
||

406 | apply eqst. |
||

407 | reflexivity. |
||

408 | |||

409 | apply proof. |
||

410 | Qed. |
||

411 | |||

412 | Theorem unzip_history : forall {A} (s : Stream A), EqSt (snd (unzip (history s))) s. |
||

413 | Proof. |
||

414 | unfold history. |
||

415 | intros. |
||

416 | apply unzip_history_rec. |
||

417 | Qed. |
||

418 | |||

419 | Theorem hd_history_rec : forall {A} p (s : Stream A), hd (history_rec p s) = (p, hd s). |
||

420 | Proof. |
||

421 | destruct s. |
||

422 | reflexivity. |
||

423 | Qed. |
||

424 | |||

425 | Theorem hd_history : forall {A} (s : Stream A), hd (history s) = (nil, hd s). |
||

426 | Proof. |
||

427 | destruct s. |
||

428 | reflexivity. |
||

429 | Qed. |
||

430 | |||

431 | Definition snoc {A} (a : A) (l : list A) := app l (cons a nil). |
||

432 | |||

433 | Theorem tl_history_rec : forall {A} p (s : Stream A), tl (history_rec p s) = history_rec (cons (hd s) p) (tl s). |
||

434 | Proof. |
||

435 | intros. |
||

436 | destruct s. |
||

437 | reflexivity. |
||

438 | Qed. |
||

439 | |||

440 | Theorem tl_history_rec : forall {A} p (s : Stream A), EqSt (tl (history_rec p s)) (apply (lift (fun pfx_sfx => (app (fst pfx_sfx) (cons (hd s) p), (snd pfx_sfx)))) (history_rec p (tl s))). |
||

441 | Proof. |
||

442 | intros. |
||

443 | Qed. |
||

444 | |||

445 | Theorem tl_history : forall {A} (s : Stream A), EqSt (tl (history s)) (apply (lift (fun pfx_sfx => (snoc (hd s) (fst pfx_sfx), (snd pfx_sfx)))) (history (tl s))). |
||

446 | Proof. |
||

447 | intros. |
||

448 | Qed. |
||

449 | |||

450 | CoFixpoint cojoin {A} (s : Stream A) : Stream (Stream A) := |
||

451 | match s with |
||

452 | | Cons _ s' => Cons s (cojoin s') |
||

453 | end. |
||

454 | (* |
||

455 | Theorem eqst_cojoin : forall {A} (s s' : Stream A), EqSt s s' -> EqSt (cojoin s) (cojoin s'). |
||

456 | Proof. |
||

457 | |||

458 | intros A. |
||

459 | cofix proof. |
||

460 | destruct s as (s0, sq). |
||

461 | destruct s' as (s0', sq'). |
||

462 | intro H. |
||

463 | inversion H. |
||

464 | simpl in H0. |
||

465 | rewrite H0. |
||

466 | Qed. |
||

467 | |||

468 | Theorem inv_history_rec : forall {A} p (s : Stream A), |
||

469 | let (fst_s, snd_s) := unzip (history_rec p s) in ForAll (fun s' => EqSt (hd s') (concat p s)) (apply (apply (lift concat) fst_s) (cojoin snd_s)). |
||

470 | Proof. |
||

471 | intro A. |
||

472 | cofix proof. |
||

473 | destruct s as (s0, s'). |
||

474 | apply HereAndFurther. |
||

475 | apply eqst_concat. |
||

476 | apply unzip_history_rec. |
||

477 | |||

478 | apply (proof (cons s0 p) s'). |
||

479 | Qed. |
||

480 | |||

481 | Theorem inv_history : forall {A} (s : Stream A), |
||

482 | let (fst_s, snd_s) := unzip (history s) in ForAll (fun s' => EqSt (hd s') s) (apply (apply (lift concat) fst_s) (cojoin snd_s)). |
||

483 | Proof. |
||

484 | intros. |
||

485 | apply inv_history_rec. |
||

486 | Qed. |
||

487 | *) |
||

488 | |||

489 | Theorem inv_history_rec : forall {A} p (s : Stream A), |
||

490 | ForAll (fun s' => EqSt (concat (fst (hd s')) (apply (lift (@snd _ _)) s')) (concat p s)) (history_rec p s). |
||

491 | Proof. |
||

492 | intro A. |
||

493 | cofix proof. |
||

494 | destruct s as (s0, s'). |
||

495 | apply HereAndFurther. |
||

496 | apply eqst_concat. |
||

497 | apply unzip_history_rec. |
||

498 | |||

499 | apply (proof (cons s0 p) s'). |
||

500 | Qed. |
||

501 | |||

502 | Theorem inv_history : forall {A} (s : Stream A), |
||

503 | ForAll (fun s' => EqSt (concat (fst (hd s')) (apply (lift (@snd _ _)) s')) s) (history s). |
||

504 | Proof. |
||

505 | intros. |
||

506 | assert (s = concat nil s). |
||

507 | reflexivity. |
||

508 | |||

509 | rewrite H. |
||

510 | rewrite <- H in |- * at 1. |
||

511 | apply inv_history_rec. |
||

512 | Qed. |
||

513 | |||

514 | Theorem inv_mono_history_rec : forall {A} (P : Stream A -> Prop) p (s : Stream A), |
||

515 | ForAll P s -> ForAll (fun s' => P (apply (lift (@snd _ _)) s')) (history_rec p s). |
||

516 | Proof. |
||

517 | intros. |
||

518 | apply inv_map. |
||

519 | generalize (eqst_eq _ _ (unzip_history_rec p s)). |
||

520 | simpl. |
||

521 | intro Hs. |
||

522 | rewrite Hs. |
||

523 | exact H. |
||

524 | Qed. |
||

525 | |||

526 | Theorem inv_mono_history : forall {A} (P : Stream A -> Prop) (s : Stream A), |
||

527 | ForAll P s -> ForAll (fun s' => P (apply (lift (@snd _ _)) s')) (history s). |
||

528 | Proof. |
||

529 | intros. |
||

530 | apply inv_mono_history_rec. |
||

531 | assumption. |
||

532 | Qed. |
||

533 | |||

534 | Theorem history_rec_mono_inv : forall {A} (P : Stream A -> Prop) p (s : Stream A), |
||

535 | ForAll (fun s' => P (apply (lift (@snd _ _)) s')) (history_rec p s) -> ForAll P s. |
||

536 | Proof. |
||

537 | intros. |
||

538 | rewrite <- (eqst_eq _ _ (unzip_history_rec p s)). |
||

539 | apply map_inv. |
||

540 | exact H. |
||

541 | Qed. |
||

542 | |||

543 | Theorem history_mono_inv : forall {A} (P : Stream A -> Prop) (s : Stream A), |
||

544 | ForAll (fun s' => P (apply (lift (@snd _ _)) s')) (history s) -> ForAll P s. |
||

545 | Proof. |
||

546 | intros. |
||

547 | apply history_rec_mono_inv with (p := nil). |
||

548 | assumption. |
||

549 | Qed. |
||

550 | |||

551 | Fixpoint prefix {A} (I : A -> Prop) (T : A -> A -> Prop) (k : nat) : list A -> Prop := |
||

552 | match k with |
||

553 | | 0 => fun p => True |
||

554 | | S k' => fun p => |
||

555 | match p with |
||

556 | | List.nil => True |
||

557 | | List.cons t q => |
||

558 | match q with |
||

559 | | List.nil => (I t) |
||

560 | | List.cons t' q' => (T t' t) /\ (prefix I T k' q) |
||

561 | end |
||

562 | end |
||

563 | end. |
||

564 | |||

565 | Theorem prefix_mono_k : forall {A} I T k (p : list A), prefix I T (S k) p -> prefix I T k p. |
||

566 | Proof. |
||

567 | induction k. |
||

568 | simpl. |
||

569 | trivial. |
||

570 | |||

571 | simpl. |
||

572 | intuition. |
||

573 | destruct p. |
||

574 | trivial. |
||

575 | |||

576 | intuition. |
||

577 | destruct p. |
||

578 | intuition. |
||

579 | |||

580 | intuition. |
||

581 | Qed. |
||

582 | |||

583 | Theorem prefix_mono : forall {A} (I I' : A -> Prop) (T T' : A -> A -> Prop) k (p : list A), (forall s, I s -> I' s) -> (forall s s', T s s' -> T' s s') -> prefix I T k p -> prefix I' T' k p. |
||

584 | Proof. |
||

585 | induction k. |
||

586 | trivial. |
||

587 | |||

588 | simpl. |
||

589 | destruct p. |
||

590 | trivial. |
||

591 | |||

592 | intros. |
||

593 | destruct p. |
||

594 | intuition. |
||

595 | |||

596 | intuition. |
||

597 | Qed. |
||

598 | |||

599 | Theorem kinduction : forall {A} (P : A -> Prop) k (s : Stream A), |
||

600 | ForAll (fun s' => prefix (fun st => P st) (fun st st' => P st') k (fst (hd s')) -> P (snd (hd s'))) (history s) |
||

601 | -> ForAll (fun s' => P (hd s')) s. |
||

602 | Proof. |
||

603 | induction k. |
||

604 | simpl. |
||

605 | intros. |
||

606 | apply history_mono_inv. |
||

607 | eapply ForAll_apply. |
||

608 | apply H. |
||

609 | |||

610 | apply necessitation. |
||

611 | intros. |
||

612 | rewrite hd_apply. |
||

613 | rewrite hd_lift. |
||

614 | intuition. |
||

615 | |||

616 | intros. |
||

617 | apply IHk. |
||

618 | eapply ForAll_apply. |
||

619 | apply H. |
||

620 | |||

621 | apply necessitation. |
||

622 | intros. |
||

623 | apply H0. |
||

624 | simpl. |
||

625 | Qed. |
||

626 | |||

627 | Theorem inv_prefix_history_rec : forall {A} (I : A -> Prop) (T : A -> A -> Prop) (s : Stream A), |
||

628 | I (hd s) -> ForAll (fun s' => T (hd s') (hd (tl s'))) (concat p s) -> |
||

629 | forall k, |
||

630 | ForAll (fun s' => prefix I T k (fst (hd s'))) (history_rec p s). |
||

631 | Proof. |
||

632 | |||

633 | Qed. |
||

634 | |||

635 | Theorem inv_prefix_history : forall {A} (I : A -> Prop) (T : A -> A -> Prop) (s : Stream A), |
||

636 | I (hd s) -> ForAll (fun s' => T (hd s') (hd (tl s'))) s -> |
||

637 | forall k, |
||

638 | ForAll (fun s' => prefix I T k (fst (hd s'))) (history s). |
||

639 | Proof. |
||

640 | intros A I T. |
||

641 | cofix proof. |
||

642 | intros. |
||

643 | Qed. |
||

644 | |||

645 | |||

646 | Definition _arrow := Cons true (lift false). |
||

647 | |||

648 | Definition ite {A} (s_if : Stream bool) (s_then s_else : Stream A) := |
||

649 | apply (apply (apply (lift (fun (c : bool) (t e : A) => if c then t else e)) s_if) s_then) s_else. |
||

650 | |||

651 | Lemma hd_ite : forall {A}, forall (c : Stream bool) (t e : Stream A), |
||

652 | hd (ite c t e) = if (hd c) then (hd t) else (hd e). |
||

653 | Proof. |
||

654 | destruct c; destruct t; destruct e. |
||

655 | reflexivity. |
||

656 | Qed. |
||

657 | |||

658 | Lemma tl_ite : forall {A}, forall (c : Stream bool) (t e : Stream A), |
||

659 | tl (ite c t e) = ite (tl c) (tl t) (tl e). |
||

660 | Proof. |
||

661 | destruct c; destruct t; destruct e. |
||

662 | reflexivity. |
||

663 | Qed. |
||

664 | |||

665 | Theorem eqst_ite : forall {A}, forall (c1 c2 : Stream bool) (t1 t2 e1 e2 : Stream A), |
||

666 | EqSt c1 c2 -> EqSt t1 t2 -> EqSt e1 e2 -> EqSt (ite c1 t1 e1) (ite c2 t2 e2). |
||

667 | Proof. |
||

668 | intros. |
||

669 | apply eqst_apply. |
||

670 | apply eqst_apply. |
||

671 | apply eqst_apply. |
||

672 | apply EqSt_reflex. |
||

673 | |||

674 | assumption. |
||

675 | |||

676 | assumption. |
||

677 | |||

678 | assumption. |
||

679 | Qed. |
||

680 | |||

681 | Variable pre : forall {A}, Stream A -> Stream A. |
||

682 | |||

683 | Axiom pre_spec : forall {A}, forall (s : Stream A), EqSt (tl (pre s)) s. |
||

684 | |||

685 | Variable when : forall {A}, Stream bool -> Stream A -> Stream A. |
||

686 | |||

687 | Axiom when_spec : forall {A}, forall (c : Stream bool) (s : Stream A), forall n, hd (Str_nth_tl n c) = true -> hd (Str_nth_tl n (when c s)) = hd (Str_nth_tl n s). |
||

688 | |||

689 | |||

690 | Require Import Bool. |
||

691 | |||

692 | Definition bnot (s : Stream bool) := apply (lift negb) s. |
||

693 | |||

694 | Definition band (s1 s2 : Stream bool) := apply (apply (lift andb) s1) s2. |
||

695 | |||

696 | Definition bor (s1 s2 : Stream bool) := apply (apply (lift orb) s1) s2. |
||

697 | |||

698 | Require Import ZArith. |
||

699 | |||

700 | Definition iplus (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => (i1 + i2)%Z)) s1) s2. |
||

701 | |||

702 | Definition iminus (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => (i1 - i2)%Z)) s1) s2. |
||

703 | |||

704 | Definition imult (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => (i1 * i2)%Z)) s1) s2. |
||

705 | |||

706 | Definition idiv (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => (i1 / i2)%Z)) s1) s2. |
||

707 | |||

708 | Definition imod (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => Zmod i1 i2)) s1) s2. |
||

709 | |||

710 | Definition ieq (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => match (i1 ?= i2)%Z with Eq => true | _ => false end)) s1) s2. |
||

711 | |||

712 | Definition ilt (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => match (i1 ?= i2)%Z with Lt => true | _ => false end)) s1) s2. |
||

713 | |||

714 | (* sémantique dénotationnelle de f *) |
||

715 | Definition denot_f (x cpt y : Stream Z) := |
||

716 | (EqSt y (iplus x (lift 1%Z))) /\ (EqSt cpt (iplus (ite _arrow (lift 0%Z) (pre cpt)) (lift 1%Z))). |
||

717 | |||

718 | (* sémantique axiomatique de f, simplifiée *) |
||

719 | |||

720 | Definition mem_f := (bool * Z)%type. |
||

721 | |||

722 | Definition ni_2 (mem : mem_f) := fst mem. |
||

723 | |||

724 | Definition __f_2 (mem : mem_f) := snd mem. |
||

725 | |||

726 | Definition init_f (mem : mem_f) := ni_2 mem = true. |
||

727 | |||

728 | Definition trans_f (x cpt y : Z) (mem_in mem_out : mem_f) := |
||

729 | (cpt = ((if bool_dec (ni_2 mem_in) true then 0 else (__f_2 mem_in)) + 1)%Z) |
||

730 | /\ (y = (x + 1)%Z) |
||

731 | /\ (ni_2 mem_out) = false |
||

732 | /\ (__f_2 mem_out) = cpt. |
||

733 | |||

734 | Definition trans_f' (s s' : (Z * (Z * Z)) * mem_f) := |
||

735 | match s, s' with |
||

736 | | ((x, (cpt, y)), mem), ((x', (cpt', y')), mem') => trans_f x cpt y mem mem' |
||

737 | end. |
||

738 | |||

739 | Lemma Cons_inj : forall {A}, forall a a' (s s' : Stream A), Cons a s = Cons a' s' -> a = a' /\ s = s'. |
||

740 | Proof. |
||

741 | intros. |
||

742 | injection H. |
||

743 | intuition. |
||

744 | Qed. |
||

745 | |||

746 | Theorem raffinement : forall (x cpt y : Stream Z) (mem : Stream mem_f), |
||

747 | (init_f (hd mem) /\ transition trans_f' (zip ((zip (x, (zip (cpt, y)))), mem))) |
||

748 | -> |
||

749 | denot_f x cpt y. |
||

750 | Proof. |
||

751 | intros. |
||

752 | apply zip_pair. |
||

753 | revert x cpt y mem H. |
||

754 | cofix proof. |
||

755 | intros. |
||

756 | |||

757 | |||

758 | |||

759 | intros. |
||

760 | split. |
||

761 | revert x cpt y mem H. |
||

762 | cofix proof. |
||

763 | intros. |
||

764 | destruct H. |
||

765 | destruct x as (x0, x'); destruct cpt as (cpt0, cpt'); destruct y as (y0, y'). |
||

766 | destruct mem as (mem0, mem'). |
||

767 | inversion H0. |
||

768 | apply eqst. |
||

769 | simpl. |
||

770 | unfold zip in H1. |
||

771 | simpl in H1. |
||

772 | generalize (f_equal (@hd _) H1). |
||

773 | simpl. |
||

774 | intro. |
||

775 | subst. |
||

776 | generalize (f_equal (@tl _) H1). |
||

777 | simpl. |
||

778 | |||

779 | Qed. |
||

780 |