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} _ _ _ _ _ _ _.
