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

History | View | Annotate | Download (22.6 KB)

1 |
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 ForAll_reinforce {A} {P Q : (Stream A -> Prop)} : forall s, (ForAll (fun s => P s /\ Q s) s) -> (ForAll Q s). |

57 |
Proof. |

58 |
intros. |

59 |
eapply ForAll_apply. |

60 |
apply H. |

61 | |

62 |
apply necessitation. |

63 |
intuition. |

64 |
Defined. |

65 | |

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

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

68 | |

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

70 |
Proof. |

71 |
induction pfx. |

72 |
auto. |

73 | |

74 |
simpl. |

75 |
intros. |

76 |
apply IHpfx. |

77 |
apply eqst. |

78 |
reflexivity. |

79 | |

80 |
exact H. |

81 |
Qed. |

82 | |

83 |
Theorem concat_eqst : forall {A} pfx pfx' (sfx sfx' : Stream A), List.length pfx = List.length pfx' -> EqSt (concat pfx sfx) (concat pfx' sfx') -> pfx = pfx' /\ EqSt sfx sfx'. |

84 |
Proof. |

85 |
induction pfx. |

86 |
destruct pfx'. |

87 |
intuition. |

88 | |

89 |
discriminate. |

90 | |

91 |
destruct pfx'. |

92 |
discriminate. |

93 | |

94 |
simpl. |

95 |
intros. |

96 |
injection H. |

97 |
clear H; intro H. |

98 |
generalize (IHpfx _ _ _ H H0). |

99 |
destruct 1. |

100 |
inversion H2. |

101 |
simpl in H3. |

102 |
simpl in H4. |

103 |
subst. |

104 |
intuition. |

105 |
Qed. |

106 | |

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

108 |
Proof. |

109 |
intros. |

110 |
apply Here. |

111 |
reflexivity. |

112 |
Qed. |

113 | |

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

115 |
Proof. |

116 |
induction p. |

117 |
trivial. |

118 | |

119 |
intros s H. |

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

121 |
apply Further. |

122 |
exact H. |

123 |
Qed. |

124 | |

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

126 |
Proof. |

127 |
induction p. |

128 |
trivial. |

129 | |

130 |
simpl. |

131 |
intros s H. |

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

133 |
intro H'. |

134 |
inversion H'. |

135 |
assumption. |

136 |
Qed. |

137 | |

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

139 | |

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

141 |
Proof. |

142 |
reflexivity. |

143 |
Qed. |

144 | |

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

146 |
Proof. |

147 |
reflexivity. |

148 |
Qed. |

149 | |

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

151 |
fun f a => |

152 |
match f, a with |

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

154 |
end. |

155 | |

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

157 |
Proof. |

158 |
destruct f; destruct a. |

159 |
reflexivity. |

160 |
Qed. |

161 | |

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

163 |
Proof. |

164 |
destruct f; destruct a. |

165 |
reflexivity. |

166 |
Qed. |

167 | |

168 |
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')). |

169 |
Proof. |

170 |
intros. |

171 |
apply eqst. |

172 |
reflexivity. |

173 | |

174 |
apply EqSt_reflex. |

175 |
Qed. |

176 | |

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

178 |
Proof. |

179 |
intros A B f P. |

180 |
cofix proof. |

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

182 |
intro H. |

183 |
inversion H. |

184 |
apply HereAndFurther. |

185 |
assumption. |

186 | |

187 |
simpl. |

188 |
apply proof. |

189 |
assumption. |

190 |
Qed. |

191 | |

192 |
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). |

193 |
Proof. |

194 |
intros A B f P. |

195 |
cofix proof. |

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

197 |
intro H. |

198 |
inversion H. |

199 |
apply HereAndFurther. |

200 |
assumption. |

201 | |

202 |
simpl. |

203 |
apply proof. |

204 |
assumption. |

205 |
Qed. |

206 | |

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

208 |
Proof. |

209 |
intros A B f P s. |

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

211 |
intro H. |

212 |
revert s Heqss. |

213 |
induction H. |

214 |
intros. |

215 |
apply Here. |

216 |
rewrite <- Heqss. |

217 |
exact H. |

218 | |

219 |
intros. |

220 |
apply Further. |

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

222 |
rewrite <- tl_lift. |

223 |
rewrite <- tl_apply. |

224 |
apply f_equal. |

225 |
exact Heqss. |

226 |
Qed. |

227 | |

228 |
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). |

229 |
Proof. |

230 |
intros A B f P s. |

231 |
intro H. |

232 |
induction H. |

233 |
apply Here. |

234 |
exact H. |

235 | |

236 |
apply Further. |

237 |
rewrite tl_apply. |

238 |
rewrite tl_lift. |

239 |
exact IHExists. |

240 |
Qed. |

241 | |

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

243 | |

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

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

246 |
Proof. |

247 |
intros A B. |

248 |
cofix proof. |

249 |
destruct s1; destruct s1'; destruct s2; destruct s2'. |

250 |
intro. |

251 |
inversion H. |

252 |
apply eqst. |

253 |
simpl in H0. |

254 |
simpl in H1. |

255 |
injection H0. |

256 |
intros. |

257 |
subst. |

258 |
reflexivity. |

259 | |

260 |
eapply proof. |

261 |
apply H1. |

262 |
Qed. |

263 | |

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

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

266 |
Proof. |

267 |
intros. |

268 |
apply eqst_eq. |

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

270 |
rewrite H. |

271 |
apply EqSt_reflex. |

272 |
Qed. |

273 | |

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

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

276 |
Proof. |

277 |
intros A B. |

278 |
cofix proof. |

279 |
destruct s1; destruct s1'; destruct s2; destruct s2'. |

280 |
intro. |

281 |
inversion H. |

282 |
apply eqst. |

283 |
simpl in H0. |

284 |
simpl in H1. |

285 |
injection H0. |

286 |
intros. |

287 |
subst. |

288 |
reflexivity. |

289 | |

290 |
eapply proof. |

291 |
apply H1. |

292 |
Qed. |

293 | |

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

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

296 |
Proof. |

297 |
intros. |

298 |
apply eqst_eq. |

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

300 |
rewrite H. |

301 |
apply EqSt_reflex. |

302 |
Qed. |

303 | |

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

305 | |

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

307 |
Proof. |

308 |
intros A B. |

309 |
cofix proof. |

310 |
destruct s1; destruct s2. |

311 |
apply eqst. |

312 |
reflexivity. |

313 | |

314 |
apply proof. |

315 |
Qed. |

316 | |

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

318 |
Proof. |

319 |
intros. |

320 |
apply eqst_eq. |

321 |
apply fst_zip_eqst. |

322 |
Qed. |

323 | |

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

325 |
Proof. |

326 |
intros A B. |

327 |
cofix proof. |

328 |
destruct s1; destruct s2. |

329 |
apply eqst. |

330 |
reflexivity. |

331 | |

332 |
apply proof. |

333 |
Qed. |

334 | |

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

336 |
Proof. |

337 |
intros. |

338 |
apply eqst_eq. |

339 |
apply snd_zip_eqst. |

340 |
Qed. |

341 | |

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

343 |
Proof. |

344 |
intros A B. |

345 |
cofix proof. |

346 |
destruct s. |

347 |
apply eqst. |

348 |
simpl. |

349 |
destruct p. |

350 |
reflexivity. |

351 | |

352 |
simpl. |

353 |
apply proof. |

354 |
Qed. |

355 | |

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

357 |
Proof. |

358 |
intros. |

359 |
apply eqst_eq. |

360 |
apply zip_unzip_eqst. |

361 |
Qed. |

362 | |

363 |
Theorem inv_eq_eqst : forall {A} (s s' : Stream A), |

364 |
ForAll (fun ss' => fst (hd ss') = snd (hd ss')) (zip (s, s')) -> EqSt s s'. |

365 |
Proof. |

366 |
intro A. |

367 |
cofix proof. |

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

369 |
destruct 0 as (t0, t'). |

370 |
intro H. |

371 |
inversion H. |

372 |
apply eqst. |

373 |
assumption. |

374 | |

375 |
apply proof. |

376 |
assumption. |

377 |
Qed. |

378 | |

379 |
Theorem eqst_inv_eq : forall {A} (s s' : Stream A), |

380 |
EqSt s s' -> ForAll (fun ss' => fst (hd ss') = snd (hd ss')) (zip (s, s')). |

381 |
Proof. |

382 |
intro A. |

383 |
cofix proof. |

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

385 |
destruct 0 as (t0, t'). |

386 |
intro H. |

387 |
inversion H. |

388 |
apply HereAndFurther. |

389 |
assumption. |

390 | |

391 |
apply proof. |

392 |
assumption. |

393 |
Qed. |

394 | |

395 | |

396 | |

397 | |

398 | |

399 |
(* |

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

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

402 | |

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

404 |
match k with |

405 |
| 0 => fun s => True |

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

407 |
end. |

408 | |

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

410 |
Proof. |

411 |
destruct k. |

412 |
simpl. |

413 |
trivial. |

414 | |

415 |
simpl. |

416 |
left. |

417 |
trivial. |

418 |
Qed. |

419 | |

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

421 |
Proof. |

422 |
destruct k. |

423 |
simpl. |

424 |
trivial. |

425 | |

426 |
simpl. |

427 |
right. |

428 |
trivial. |

429 |
Qed. |

430 | |

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

432 |
Proof. |

433 | |

434 |
Qed. |

435 |
*) |

436 | |

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

438 |
match s with |

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

440 |
end. |

441 | |

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

443 | |

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

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

446 |
Proof. |

447 |
intros A. |

448 |
cofix proof. |

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

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

451 |
intro H. |

452 |
inversion H. |

453 |
simpl in H0. |

454 |
rewrite H0. |

455 |
apply eqst. |

456 |
reflexivity. |

457 | |

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

459 |
assumption. |

460 |
Qed. |

461 | |

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

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

464 |
Proof. |

465 |
intros. |

466 |
apply eqst_history_rec. |

467 |
assumption. |

468 |
Qed. |

469 | |

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

471 |
Proof. |

472 |
intro A. |

473 |
cofix proof. |

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

475 |
apply eqst. |

476 |
reflexivity. |

477 | |

478 |
apply proof. |

479 |
Qed. |

480 | |

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

482 |
Proof. |

483 |
unfold history. |

484 |
intros. |

485 |
apply unzip_history_rec. |

486 |
Qed. |

487 |
(* |

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

489 |
Proof. |

490 |
destruct s. |

491 |
reflexivity. |

492 |
Qed. |

493 | |

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

495 |
Proof. |

496 |
destruct s. |

497 |
reflexivity. |

498 |
Qed. |

499 | |

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

501 | |

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

503 |
Proof. |

504 |
intros. |

505 |
destruct s. |

506 |
reflexivity. |

507 |
Qed. |

508 | |

509 |
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))). |

510 |
Proof. |

511 |
intros. |

512 |
Qed. |

513 | |

514 |
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))). |

515 |
Proof. |

516 |
intros. |

517 |
Qed. |

518 |
*) |

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

520 |
match s with |

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

522 |
end. |

523 |
(* |

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

525 |
Proof. |

526 | |

527 |
intros A. |

528 |
cofix proof. |

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

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

531 |
intro H. |

532 |
inversion H. |

533 |
simpl in H0. |

534 |
rewrite H0. |

535 |
Qed. |

536 | |

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

538 |
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)). |

539 |
Proof. |

540 |
intro A. |

541 |
cofix proof. |

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

543 |
apply HereAndFurther. |

544 |
apply eqst_concat. |

545 |
apply unzip_history_rec. |

546 | |

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

548 |
Qed. |

549 | |

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

551 |
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)). |

552 |
Proof. |

553 |
intros. |

554 |
apply inv_history_rec. |

555 |
Qed. |

556 |
*) |

557 | |

558 |
Definition History_Spec {A} (s : Stream A) s' := |

559 |
fst (hd (tl s')) = cons (snd (hd s')) (fst (hd s')) |

560 |
/\ EqSt (concat (fst (hd s')) (apply (lift (@snd _ _)) s')) s. |

561 | |

562 |
Theorem history_rec_spec : forall {A} p (s : Stream A), |

563 |
fst (hd (history_rec p s)) = p |

564 |
/\ ForAll (fun s' => History_Spec (concat p s) s') (history_rec p s). |

565 |
Proof. |

566 |
intros. |

567 |
split. |

568 |
destruct s. |

569 |
reflexivity. |

570 | |

571 |
revert p s. |

572 |
cofix proof. |

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

574 |
apply HereAndFurther. |

575 |
split. |

576 |
simpl. |

577 |
destruct s'. |

578 |
reflexivity. |

579 | |

580 |
apply eqst_concat. |

581 |
apply unzip_history_rec. |

582 | |

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

584 |
Qed. |

585 | |

586 |
Theorem history_spec : forall {A} (s : Stream A), |

587 |
fst (hd (history s)) = nil |

588 |
/\ ForAll (fun s' => History_Spec s s') (history s). |

589 |
Proof. |

590 |
intros. |

591 |
generalize (history_rec_spec nil s). |

592 |
intuition. |

593 |
Qed. |

594 | |

595 |
Theorem history_rec_spec_complete : forall {A} p (s : Stream A) ps, |

596 |
fst (hd ps) = p -> ForAll (fun s' => History_Spec (concat p s) s') ps -> EqSt ps (history_rec p s). |

597 |
Proof. |

598 |
intro A. |

599 |
cofix proof. |

600 |
intros. |

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

602 |
destruct ps as ((p_ps0, s_ps0), ps'). |

603 |
simpl in H. |

604 |
subst. |

605 |
inversion H0. |

606 |
unfold History_Spec in H. |

607 |
destruct H. |

608 |
simpl in H. |

609 |
apply eqst. |

610 |
simpl. |

611 |
intros. |

612 |
simpl in H. |

613 |
subst. |

614 |
inversion H0. |

615 |
unfold History_Spec in H. |

616 |
destruct H. |

617 |
simpl. |

618 |
simpl in H2. |

619 |
destruct (concat_eqst _ _ _ _ refl_equal H2). |

620 |
inversion H5. |

621 |
simpl in H6. |

622 |
subst. |

623 |
reflexivity. |

624 | |

625 |
simpl. |

626 |
apply proof. |

627 |
simpl in H2. |

628 |
destruct (concat_eqst _ _ _ _ refl_equal H2). |

629 |
inversion H4. |

630 |
simpl in H5. |

631 |
subst. |

632 |
assumption. |

633 | |

634 |
assumption. |

635 |
Qed. |

636 | |

637 |
Theorem history_spec_complete : forall {A} (s : Stream A) ps, |

638 |
fst (hd ps) = nil -> ForAll (fun s' => History_Spec s s') ps -> EqSt ps (history s). |

639 |
Proof. |

640 |
intros. |

641 |
apply history_rec_spec_complete. |

642 |
assumption. |

643 | |

644 |
assumption. |

645 |
Qed. |

646 | |

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

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

649 |
Proof. |

650 |
intros. |

651 |
apply inv_map. |

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

653 |
simpl. |

654 |
intro Hs. |

655 |
rewrite Hs. |

656 |
exact H. |

657 |
Qed. |

658 | |

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

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

661 |
Proof. |

662 |
intros. |

663 |
apply inv_snd_history_rec_intro. |

664 |
assumption. |

665 |
Qed. |

666 | |

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

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

669 |
Proof. |

670 |
intros. |

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

672 |
apply map_inv. |

673 |
exact H. |

674 |
Qed. |

675 | |

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

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

678 |
Proof. |

679 |
intros. |

680 |
apply inv_snd_history_rec_elim with (p := nil). |

681 |
assumption. |

682 |
Qed. |

683 | |

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

685 |
match k with |

686 |
| 0 => fun p => True |

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

688 |
match p with |

689 |
| List.nil => True |

690 |
| List.cons t q => |

691 |
match q with |

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

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

694 |
end |

695 |
end |

696 |
end. |

697 | |

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

699 |
Proof. |

700 |
induction k. |

701 |
simpl. |

702 |
trivial. |

703 | |

704 |
simpl. |

705 |
intuition. |

706 |
destruct p. |

707 |
trivial. |

708 | |

709 |
intuition. |

710 |
destruct p. |

711 |
intuition. |

712 | |

713 |
intuition. |

714 |
Qed. |

715 | |

716 |
Theorem prefix_apply : forall {A} (I I' : A -> Prop) (T T' : A -> A -> Prop) k (p : list A), |

717 |
prefix I T k p -> prefix (fun s => I s -> I' s) (fun s s' => T s s' -> T' s s') k p -> prefix I' T' k p. |

718 |
Proof. |

719 |
intros A I I' T T'. |

720 |
induction k. |

721 |
trivial. |

722 | |

723 |
simpl. |

724 |
destruct p. |

725 |
trivial. |

726 | |

727 |
destruct p. |

728 |
intuition. |

729 | |

730 |
intuition. |

731 |
Qed. |

732 | |

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

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

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

736 |
Proof. |

737 |
intros. |

738 |
apply inv_snd_history_elim. |

739 |
apply @ForAll_apply with (P := fun s' => P (snd (hd s'))). |

740 |
apply |

741 |
@ForAll_apply |

742 |
with |

743 |
(P := fun s' => |

744 |
prefix (fun st => P st) (fun st st' => P st') k (fst (hd s'))). |

745 |
apply |

746 |
@ForAll_reinforce |

747 |
with |

748 |
(P := ForAll |

749 |
(fun s' : Stream (list A * A) => |

750 |
prefix (fun st : A => P st) (fun _ st' : A => P st') k |

751 |
(fst (hd s')) -> P (snd (hd s')))). |

752 |
apply |

753 |
@ForAll_reinforce |

754 |
with (P := ForAll (fun s' : Stream (list A * A) => History_Spec s s')). |

755 |
eapply ForAll_coind. |

756 |
intro. |

757 |
exact (fun x => x). |

758 | |

759 |
destruct x as ((p0, s0), ((p1, s1), x'')). |

760 |
simpl. |

761 |
intuition. |

762 |
inversion H1. |

763 |
assumption. |

764 | |

765 |
inversion H0. |

766 |
assumption. |

767 | |

768 |
inversion H1. |

769 |
unfold History_Spec in H2. |

770 |
simpl in H2. |

771 |
destruct H2. |

772 |
rewrite H2. |

773 |
destruct k. |

774 |
simpl. |

775 |
trivial. |

776 | |

777 |
simpl. |

778 |
inversion H0. |

779 |
simpl in H6. |

780 |
destruct p0. |

781 |
intuition. |

782 | |

783 |
split. |

784 |
simpl in H3. |

785 |
apply H6. |

786 |
exact H3. |

787 | |

788 |
apply prefix_mono_k. |

789 |
exact H3. |

790 | |

791 |
simpl. |

792 |
intuition. |

793 |
generalize (history_spec s). |

794 |
intuition. |

795 | |

796 |
destruct s. |

797 |
simpl. |

798 |
destruct k. |

799 |
simpl. |

800 |
trivial. |

801 | |

802 |
simpl. |

803 |
trivial. |

804 | |

805 |
exact H. |

806 | |

807 |
apply necessitation. |

808 |
destruct s0. |

809 |
simpl. |

810 |
trivial. |

811 |
Qed. |

812 | |

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

814 |
fst (hd ps) = nil |

815 |
-> ForAll (fun s' => History_Spec s s') ps |

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

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

818 |
Proof. |

819 |
intros. |

820 |
rewrite (eqst_eq _ _ (history_spec_complete _ _ H H0)) in H1. |

821 |
eapply kinduction. |

822 |
apply H1. |

823 |
Qed. |

824 | |

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

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

827 |
forall k, |

828 |
prefix I T k (cons (hd s) p) -> |

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

830 |
Proof. |

831 |
intros A I T. |

832 |
cofix proof. |

833 |
intros. |

834 |
inversion H. |

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

836 |
apply HereAndFurther. |

837 |
assumption. |

838 | |

839 |
simpl. |

840 |
apply proof. |

841 |
assumption. |

842 | |

843 |
destruct k; simpl. |

844 |
trivial. |

845 | |

846 |
split. |

847 |
generalize (inv_concat _ _ _ H). |

848 |
clear H; intro H. |

849 |
inversion H. |

850 |
assumption. |

851 | |

852 |
apply prefix_mono_k. |

853 |
assumption. |

854 |
Qed. |

855 | |

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

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

858 |
forall k, |

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

860 |
Proof. |

861 |
intros. |

862 |
apply inv_prefix_history_rec. |

863 |
assumption. |

864 | |

865 |
destruct k; simpl. |

866 |
trivial. |

867 | |

868 |
assumption. |

869 |
Qed. |

870 | |

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

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

873 |
forall k, |

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

875 |
Proof. |

876 |
intros. |

877 |
destruct k. |

878 |
apply necessitation. |

879 |
simpl. |

880 |
trivial. |

881 | |

882 |
eapply ForAll_apply. |

883 |
apply (fun i n => inv_prefix_history I T s i n (S (S k))). |

884 |
apply H. |

885 | |

886 |
apply H0. |

887 | |

888 |
apply necessitation. |

889 |
destruct s0 as ((p0, s0), s'). |

890 |
simpl. |

891 |
destruct p0. |

892 |
trivial. |

893 | |

894 |
intuition. |

895 |
Qed. |

896 | |

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

898 | |

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

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

901 | |

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

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

904 |
Proof. |

905 |
destruct c; destruct t; destruct e. |

906 |
reflexivity. |

907 |
Qed. |

908 | |

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

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

911 |
Proof. |

912 |
destruct c; destruct t; destruct e. |

913 |
reflexivity. |

914 |
Qed. |

915 | |

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

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

918 |
Proof. |

919 |
intros. |

920 |
apply eqst_apply. |

921 |
apply eqst_apply. |

922 |
apply eqst_apply. |

923 |
apply EqSt_reflex. |

924 | |

925 |
assumption. |

926 | |

927 |
assumption. |

928 | |

929 |
assumption. |

930 |
Qed. |

931 | |

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

933 | |

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

935 | |

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

937 | |

938 |
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). |

939 | |

940 | |

941 |
Require Import Bool. |

942 | |

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

944 | |

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

946 | |

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

948 | |

949 |
Require Import ZArith. |

950 | |

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

952 | |

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

954 | |

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

956 | |

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

958 | |

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

960 | |

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

962 | |

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

964 | |

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

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

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

968 | |

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

970 | |

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

972 | |

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

974 | |

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

976 | |

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

978 | |

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

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

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

982 |
/\ (ni_2 mem_out) = false |

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

984 | |

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

986 |
match s, s' with |

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

988 |
end. |

989 | |

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

991 |
Proof. |

992 |
intros. |

993 |
injection H. |

994 |
intuition. |

995 |
Qed. |

996 | |

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

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

999 |
-> |

1000 |
denot_f x cpt y. |

1001 |
Proof. |

1002 |
intros. |

1003 |
apply zip_pair. |

1004 |
revert x cpt y mem H. |

1005 |
cofix proof. |

1006 |
intros. |

1007 | |

1008 | |

1009 | |

1010 |
intros. |

1011 |
split. |

1012 |
revert x cpt y mem H. |

1013 |
cofix proof. |

1014 |
intros. |

1015 |
destruct H. |

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

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

1018 |
inversion H0. |

1019 |
apply eqst. |

1020 |
simpl. |

1021 |
unfold zip in H1. |

1022 |
simpl in H1. |

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

1024 |
simpl. |

1025 |
intro. |

1026 |
subst. |

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

1028 |
simpl. |

1029 | |

1030 |
Qed. |

1031 | |

1032 |