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

History | View | Annotate | Download (18.1 KB)

1 |
Require Export Streams. |
---|---|

2 |
Require List. |

3 |
Require Import Setoid. |

4 |
Require Import Relation_Definitions. |

5 |
Require Import Program.Wf. |

6 |
Require Import Wf_nat. |

7 |
Require Import Wellfounded. |

8 | |

9 |
Definition mapT (F : Type -> Type) {A B} := (A -> B) -> (F A) -> (F B). |

10 | |

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

12 | |

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

14 |
fun f a => |

15 |
match f, a with |

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

17 |
| _ , _ => None |

18 |
end. |

19 | |

20 | |

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

22 | |

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

24 |
Proof. |

25 |
intros A P. |

26 |
cofix proof. |

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

28 |
intro H. |

29 |
apply HereAndFurther. |

30 |
exact H. |

31 | |

32 |
simpl. |

33 |
apply proof. |

34 |
inversion H. |

35 |
assumption. |

36 |
Qed. |

37 | |

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

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

40 |
Proof. |

41 |
induction 2. |

42 |
apply Here. |

43 |
inversion H. |

44 |
intuition. |

45 | |

46 |
apply Further. |

47 |
apply IHExists. |

48 |
inversion H. |

49 |
assumption. |

50 |
Qed. |

51 | |

52 |
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) := |

53 |
fun s always_p always_pq => |

54 |
match always_p, always_pq with |

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

56 |
end. |

57 | |

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

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

60 | |

61 |
Definition ForAll_reinforce {A} {P Q : (Stream A -> Prop)} : forall s, (ForAll (fun s => P s /\ Q s) s) -> (ForAll Q s). |

62 |
Proof. |

63 |
intros. |

64 |
eapply ForAll_apply. |

65 |
apply H. |

66 | |

67 |
apply necessitation. |

68 |
intuition. |

69 |
Defined. |

70 | |

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

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

73 | |

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

75 |
Proof. |

76 |
induction pfx. |

77 |
auto. |

78 | |

79 |
simpl. |

80 |
intros. |

81 |
apply IHpfx. |

82 |
apply eqst. |

83 |
reflexivity. |

84 | |

85 |
exact H. |

86 |
Qed. |

87 | |

88 |
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'. |

89 |
Proof. |

90 |
induction pfx. |

91 |
destruct pfx'. |

92 |
intuition. |

93 | |

94 |
discriminate. |

95 | |

96 |
destruct pfx'. |

97 |
discriminate. |

98 | |

99 |
simpl. |

100 |
intros. |

101 |
injection H. |

102 |
clear H; intro H. |

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

104 |
destruct 1. |

105 |
inversion H2. |

106 |
simpl in H3. |

107 |
simpl in H4. |

108 |
subst. |

109 |
intuition. |

110 |
Qed. |

111 | |

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

113 |
Proof. |

114 |
intros. |

115 |
apply Here. |

116 |
reflexivity. |

117 |
Qed. |

118 | |

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

120 |
Proof. |

121 |
induction p. |

122 |
trivial. |

123 | |

124 |
intros s H. |

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

126 |
apply Further. |

127 |
exact H. |

128 |
Qed. |

129 | |

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

131 |
Proof. |

132 |
induction p. |

133 |
trivial. |

134 | |

135 |
simpl. |

136 |
intros s H. |

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

138 |
intro H'. |

139 |
inversion H'. |

140 |
assumption. |

141 |
Qed. |

142 | |

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

144 | |

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

146 |
Proof. |

147 |
reflexivity. |

148 |
Qed. |

149 | |

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

151 |
Proof. |

152 |
reflexivity. |

153 |
Qed. |

154 | |

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

156 |
fun f a => |

157 |
match f, a with |

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

159 |
end. |

160 | |

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

162 |
Proof. |

163 |
destruct f; destruct a. |

164 |
reflexivity. |

165 |
Qed. |

166 | |

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

168 |
Proof. |

169 |
destruct f; destruct a. |

170 |
reflexivity. |

171 |
Qed. |

172 | |

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

174 |
Proof. |

175 |
intros. |

176 |
apply eqst. |

177 |
reflexivity. |

178 | |

179 |
apply EqSt_reflex. |

180 |
Qed. |

181 | |

182 |
Lemma eqst_apply : forall {A B} {f f' : Stream (A -> B)} {a a' : Stream A}, |

183 |
EqSt f f' -> EqSt a a' -> EqSt (apply f a) (apply f' a'). |

184 |
Proof. |

185 |
intros A B. |

186 |
cofix proof. |

187 |
intros. |

188 |
inversion H. |

189 |
inversion H0. |

190 |
apply eqst. |

191 |
rewrite hd_apply. |

192 |
rewrite hd_apply. |

193 |
congruence. |

194 | |

195 |
rewrite tl_apply. |

196 |
rewrite tl_apply. |

197 |
apply proof. |

198 |
assumption. |

199 | |

200 |
assumption. |

201 |
Qed. |

202 | |

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

204 |
Proof. |

205 |
intros A B f P. |

206 |
cofix proof. |

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

208 |
intro H. |

209 |
inversion H. |

210 |
apply HereAndFurther. |

211 |
assumption. |

212 | |

213 |
simpl. |

214 |
apply proof. |

215 |
assumption. |

216 |
Qed. |

217 | |

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

219 |
Proof. |

220 |
intros A B f P. |

221 |
cofix proof. |

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

223 |
intro H. |

224 |
inversion H. |

225 |
apply HereAndFurther. |

226 |
assumption. |

227 | |

228 |
simpl. |

229 |
apply proof. |

230 |
assumption. |

231 |
Qed. |

232 | |

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

234 |
Proof. |

235 |
intros A B f P s. |

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

237 |
intro H. |

238 |
revert s Heqss. |

239 |
induction H. |

240 |
intros. |

241 |
apply Here. |

242 |
rewrite <- Heqss. |

243 |
exact H. |

244 | |

245 |
intros. |

246 |
apply Further. |

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

248 |
rewrite <- tl_lift. |

249 |
rewrite <- tl_apply. |

250 |
apply f_equal. |

251 |
exact Heqss. |

252 |
Qed. |

253 | |

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

255 |
Proof. |

256 |
intros A B f P s. |

257 |
intro H. |

258 |
induction H. |

259 |
apply Here. |

260 |
exact H. |

261 | |

262 |
apply Further. |

263 |
rewrite tl_apply. |

264 |
rewrite tl_lift. |

265 |
exact IHExists. |

266 |
Qed. |

267 | |

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

269 | |

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

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

272 |
Proof. |

273 |
intros A B. |

274 |
cofix proof. |

275 |
destruct s1; destruct s1'; destruct s2; destruct s2'. |

276 |
intro. |

277 |
inversion H. |

278 |
apply eqst. |

279 |
simpl in H0. |

280 |
simpl in H1. |

281 |
injection H0. |

282 |
intros. |

283 |
subst. |

284 |
reflexivity. |

285 | |

286 |
eapply proof. |

287 |
apply H1. |

288 |
Qed. |

289 | |

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

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

292 |
Proof. |

293 |
intros. |

294 |
apply eqst_eq. |

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

296 |
rewrite H. |

297 |
apply EqSt_reflex. |

298 |
Qed. |

299 | |

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

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

302 |
Proof. |

303 |
intros A B. |

304 |
cofix proof. |

305 |
destruct s1; destruct s1'; destruct s2; destruct s2'. |

306 |
intro. |

307 |
inversion H. |

308 |
apply eqst. |

309 |
simpl in H0. |

310 |
simpl in H1. |

311 |
injection H0. |

312 |
intros. |

313 |
subst. |

314 |
reflexivity. |

315 | |

316 |
eapply proof. |

317 |
apply H1. |

318 |
Qed. |

319 | |

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

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

322 |
Proof. |

323 |
intros. |

324 |
apply eqst_eq. |

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

326 |
rewrite H. |

327 |
apply EqSt_reflex. |

328 |
Qed. |

329 | |

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

331 | |

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

333 |
Proof. |

334 |
intros A B. |

335 |
cofix proof. |

336 |
destruct s1; destruct s2. |

337 |
apply eqst. |

338 |
reflexivity. |

339 | |

340 |
apply proof. |

341 |
Qed. |

342 | |

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

344 |
Proof. |

345 |
intros. |

346 |
apply eqst_eq. |

347 |
apply fst_zip_eqst. |

348 |
Qed. |

349 | |

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

351 |
Proof. |

352 |
intros A B. |

353 |
cofix proof. |

354 |
destruct s1; destruct s2. |

355 |
apply eqst. |

356 |
reflexivity. |

357 | |

358 |
apply proof. |

359 |
Qed. |

360 | |

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

362 |
Proof. |

363 |
intros. |

364 |
apply eqst_eq. |

365 |
apply snd_zip_eqst. |

366 |
Qed. |

367 | |

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

369 |
Proof. |

370 |
intros A B. |

371 |
cofix proof. |

372 |
destruct s. |

373 |
apply eqst. |

374 |
simpl. |

375 |
destruct p. |

376 |
reflexivity. |

377 | |

378 |
simpl. |

379 |
apply proof. |

380 |
Qed. |

381 | |

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

383 |
Proof. |

384 |
intros. |

385 |
apply eqst_eq. |

386 |
apply zip_unzip_eqst. |

387 |
Qed. |

388 | |

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

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

391 |
Proof. |

392 |
intro A. |

393 |
cofix proof. |

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

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

396 |
intro H. |

397 |
inversion H. |

398 |
apply eqst. |

399 |
assumption. |

400 | |

401 |
apply proof. |

402 |
assumption. |

403 |
Qed. |

404 | |

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

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

407 |
Proof. |

408 |
intro A. |

409 |
cofix proof. |

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

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

412 |
intro H. |

413 |
inversion H. |

414 |
apply HereAndFurther. |

415 |
assumption. |

416 | |

417 |
apply proof. |

418 |
assumption. |

419 |
Qed. |

420 | |

421 | |

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

423 |
match s with |

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

425 |
end. |

426 | |

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

428 | |

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

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

431 |
Proof. |

432 |
intros A. |

433 |
cofix proof. |

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

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

436 |
intro H. |

437 |
inversion H. |

438 |
simpl in H0. |

439 |
rewrite H0. |

440 |
apply eqst. |

441 |
reflexivity. |

442 | |

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

444 |
assumption. |

445 |
Qed. |

446 | |

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

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

449 |
Proof. |

450 |
intros. |

451 |
apply eqst_history_rec. |

452 |
assumption. |

453 |
Qed. |

454 | |

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

456 |
Proof. |

457 |
intro A. |

458 |
cofix proof. |

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

460 |
apply eqst. |

461 |
reflexivity. |

462 | |

463 |
apply proof. |

464 |
Qed. |

465 | |

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

467 |
Proof. |

468 |
unfold history. |

469 |
intros. |

470 |
apply unzip_history_rec. |

471 |
Qed. |

472 | |

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

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

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

476 | |

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

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

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

480 |
Proof. |

481 |
intros. |

482 |
split. |

483 |
destruct s. |

484 |
reflexivity. |

485 | |

486 |
revert p s. |

487 |
cofix proof. |

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

489 |
apply HereAndFurther. |

490 |
split. |

491 |
simpl. |

492 |
destruct s'. |

493 |
reflexivity. |

494 | |

495 |
apply eqst_concat. |

496 |
apply unzip_history_rec. |

497 | |

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

499 |
Qed. |

500 | |

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

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

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

504 |
Proof. |

505 |
intros. |

506 |
generalize (history_rec_spec nil s). |

507 |
intuition. |

508 |
Qed. |

509 | |

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

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

512 |
Proof. |

513 |
intro A. |

514 |
cofix proof. |

515 |
intros. |

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

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

518 |
simpl in H. |

519 |
subst. |

520 |
inversion H0. |

521 |
unfold History_Spec in H. |

522 |
destruct H. |

523 |
simpl in H. |

524 |
apply eqst. |

525 |
simpl. |

526 |
intros. |

527 |
simpl in H. |

528 |
subst. |

529 |
inversion H0. |

530 |
unfold History_Spec in H. |

531 |
destruct H. |

532 |
simpl. |

533 |
simpl in H2. |

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

535 |
inversion H5. |

536 |
simpl in H6. |

537 |
subst. |

538 |
reflexivity. |

539 | |

540 |
simpl. |

541 |
apply proof. |

542 |
simpl in H2. |

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

544 |
inversion H4. |

545 |
simpl in H5. |

546 |
subst. |

547 |
assumption. |

548 | |

549 |
assumption. |

550 |
Qed. |

551 | |

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

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

554 |
Proof. |

555 |
intros. |

556 |
apply history_rec_spec_complete. |

557 |
assumption. |

558 | |

559 |
assumption. |

560 |
Qed. |

561 | |

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

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

564 |
Proof. |

565 |
intros. |

566 |
apply inv_map. |

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

568 |
simpl. |

569 |
intro Hs. |

570 |
rewrite Hs. |

571 |
exact H. |

572 |
Qed. |

573 | |

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

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

576 |
Proof. |

577 |
intros. |

578 |
apply inv_snd_history_rec_intro. |

579 |
assumption. |

580 |
Qed. |

581 | |

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

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

584 |
Proof. |

585 |
intros. |

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

587 |
apply map_inv. |

588 |
exact H. |

589 |
Qed. |

590 | |

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

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

593 |
Proof. |

594 |
intros. |

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

596 |
assumption. |

597 |
Qed. |

598 | |

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

600 |
match k with |

601 |
| 0 => fun p => True |

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

603 |
match p with |

604 |
| List.nil => True |

605 |
| List.cons t q => |

606 |
match q with |

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

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

609 |
end |

610 |
end |

611 |
end. |

612 | |

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

614 |
Proof. |

615 |
induction k. |

616 |
simpl. |

617 |
trivial. |

618 | |

619 |
simpl. |

620 |
intuition. |

621 |
destruct p. |

622 |
trivial. |

623 | |

624 |
intuition. |

625 |
destruct p. |

626 |
intuition. |

627 | |

628 |
intuition. |

629 |
Qed. |

630 | |

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

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

633 |
Proof. |

634 |
intros A I I' T T'. |

635 |
induction k. |

636 |
trivial. |

637 | |

638 |
simpl. |

639 |
destruct p. |

640 |
trivial. |

641 | |

642 |
destruct p. |

643 |
intuition. |

644 | |

645 |
intuition. |

646 |
Qed. |

647 | |

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

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

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

651 |
Proof. |

652 |
intros. |

653 |
apply inv_snd_history_elim. |

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

655 |
apply |

656 |
@ForAll_apply |

657 |
with |

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

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

660 |
apply |

661 |
@ForAll_reinforce |

662 |
with |

663 |
(P := ForAll |

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

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

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

667 |
apply |

668 |
@ForAll_reinforce |

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

670 |
eapply ForAll_coind. |

671 |
intro. |

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

673 | |

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

675 |
simpl. |

676 |
intuition. |

677 |
inversion H1. |

678 |
assumption. |

679 | |

680 |
inversion H0. |

681 |
assumption. |

682 | |

683 |
inversion H1. |

684 |
unfold History_Spec in H2. |

685 |
simpl in H2. |

686 |
destruct H2. |

687 |
rewrite H2. |

688 |
destruct k. |

689 |
simpl. |

690 |
trivial. |

691 | |

692 |
simpl. |

693 |
inversion H0. |

694 |
simpl in H6. |

695 |
destruct p0. |

696 |
intuition. |

697 | |

698 |
split. |

699 |
simpl in H3. |

700 |
apply H6. |

701 |
exact H3. |

702 | |

703 |
apply prefix_mono_k. |

704 |
exact H3. |

705 | |

706 |
simpl. |

707 |
intuition. |

708 |
generalize (history_spec s). |

709 |
intuition. |

710 | |

711 |
destruct s. |

712 |
simpl. |

713 |
destruct k. |

714 |
simpl. |

715 |
trivial. |

716 | |

717 |
simpl. |

718 |
trivial. |

719 | |

720 |
exact H. |

721 | |

722 |
apply necessitation. |

723 |
destruct s0. |

724 |
simpl. |

725 |
trivial. |

726 |
Qed. |

727 | |

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

729 |
fst (hd ps) = nil |

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

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

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

733 |
Proof. |

734 |
intros. |

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

736 |
eapply kinduction. |

737 |
apply H1. |

738 |
Qed. |

739 | |

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

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

742 |
forall k, |

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

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

745 |
Proof. |

746 |
intros A I T. |

747 |
cofix proof. |

748 |
intros. |

749 |
inversion H. |

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

751 |
apply HereAndFurther. |

752 |
assumption. |

753 | |

754 |
simpl. |

755 |
apply proof. |

756 |
assumption. |

757 | |

758 |
destruct k; simpl. |

759 |
trivial. |

760 | |

761 |
split. |

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

763 |
clear H; intro H. |

764 |
inversion H. |

765 |
assumption. |

766 | |

767 |
apply prefix_mono_k. |

768 |
assumption. |

769 |
Qed. |

770 | |

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

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

773 |
forall k, |

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

775 |
Proof. |

776 |
intros. |

777 |
apply inv_prefix_history_rec. |

778 |
assumption. |

779 | |

780 |
destruct k; simpl. |

781 |
trivial. |

782 | |

783 |
assumption. |

784 |
Qed. |

785 | |

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

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

788 |
forall k, |

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

790 |
Proof. |

791 |
intros. |

792 |
destruct k. |

793 |
apply necessitation. |

794 |
simpl. |

795 |
trivial. |

796 | |

797 |
eapply ForAll_apply. |

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

799 |
apply H. |

800 | |

801 |
apply H0. |

802 | |

803 |
apply necessitation. |

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

805 |
simpl. |

806 |
destruct p0. |

807 |
trivial. |

808 | |

809 |
intuition. |

810 |
Qed. |

811 | |

812 | |

813 |
Definition effective {A : Type} (r : relation A) := |

814 |
forall a1 a2, { r a1 a2 } + { ~ r a1 a2 }. |

815 | |

816 |
Definition lift_hd {A : Type} (r : relation A) : relation (Stream A) := |

817 |
fun s1 => fun s2 => r (hd s1) (hd s2). |

818 | |

819 |
Theorem lift_hd_effective : forall {A : Type} {r : relation A}, |

820 |
effective r -> effective (lift_hd r). |

821 |
Proof. |

822 |
unfold effective, lift_hd in |- *. |

823 |
intros A r H s1 s2. |

824 |
destruct s1; destruct s2. |

825 |
apply H. |

826 |
Defined. |

827 | |

828 |
Section FixedPoint. |

829 | |

830 |
Variable A : Type. |

831 | |

832 |
Variable union : A -> A -> A. |

833 | |

834 |
Variable le : relation A. |

835 | |

836 |
Hypothesis le_mono : forall x y, le x (union x y). |

837 | |

838 |
Hypothesis le_eff : effective le. |

839 | |

840 |
Definition gt x y := le y x /\ ~ le x y. |

841 | |

842 |
Hypothesis gt_wf : well_founded gt. |

843 | |

844 |
Program Fixpoint rec_hd (f : Stream A -> Stream A) (s : Stream A) { wf (lift_hd gt) s } : Stream A := |

845 |
let s' := apply (apply (lift union) s) (f s) in |

846 |
if (lift_hd_effective le_eff s' s) |

847 |
then s' |

848 |
else rec_hd f s'. |

849 | |

850 |
Obligation 1. |

851 |
Proof. |

852 |
unfold lift_hd. |

853 |
rewrite hd_apply. |

854 |
rewrite hd_apply. |

855 |
rewrite hd_lift. |

856 |
unfold gt. |

857 |
split. |

858 |
apply le_mono. |

859 | |

860 |
unfold lift_hd in H. |

861 |
rewrite hd_apply in H. |

862 |
rewrite hd_apply in H. |

863 |
rewrite hd_lift in H. |

864 |
exact H. |

865 |
Qed. |

866 | |

867 |
Obligation 2. |

868 |
Proof. |

869 |
unfold MR. |

870 |
apply wf_inverse_image. |

871 |
unfold lift_hd. |

872 |
apply wf_inverse_image. |

873 |
assumption. |

874 |
Defined. |

875 | |

876 |
CoFixpoint rec (f : Stream A -> Stream A) (s : Stream A) : Stream A := |

877 |
let s' := rec_hd f s in Cons (hd s') (rec f (tl s')). |

878 | |

879 |
End FixedPoint. |

880 | |

881 |
Arguments gt {A} _ _ _. |

882 | |

883 |
Arguments rec {A} _ _ _ _ _ _ _. |