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


781

