diff options
Diffstat (limited to 'test-suite/success/coindprim.v')
-rw-r--r-- | test-suite/success/coindprim.v | 85 |
1 files changed, 62 insertions, 23 deletions
diff --git a/test-suite/success/coindprim.v b/test-suite/success/coindprim.v index 4e0b7bf5..5b9265b6 100644 --- a/test-suite/success/coindprim.v +++ b/test-suite/success/coindprim.v @@ -1,36 +1,75 @@ +Require Import Program. + Set Primitive Projections. -CoInductive stream A := { hd : A; tl : stream A }. +CoInductive Stream (A : Type) := mkStream { hd : A; tl : Stream A}. -CoFixpoint ticks : stream unit := - {| hd := tt; tl := ticks |}. +Arguments mkStream [A] hd tl. +Arguments hd [A] s. +Arguments tl [A] s. -Arguments hd [ A ] s. -Arguments tl [ A ] s. +Definition eta {A} (s : Stream A) := {| hd := s.(hd); tl := s.(tl) |}. -CoInductive bisim {A} : stream A -> stream A -> Prop := - | bisims s s' : hd s = hd s' -> bisim (tl s) (tl s') -> bisim s s'. +CoFixpoint ones := {| hd := 1; tl := ones |}. +CoFixpoint ticks := {| hd := tt; tl := ticks |}. -Lemma bisim_refl {A} (s : stream A) : bisim s s. -Proof. - revert s. - cofix aux. intros. constructor. reflexivity. apply aux. -Defined. +CoInductive stream_equiv {A} {s : Stream A} {s' : Stream A} : Prop := + mkStreamEq { hdeq : s.(hd) = s'.(hd); tleq : stream_equiv _ s.(tl) s'.(tl) }. +Arguments stream_equiv {A} s s'. -Lemma constr : forall (A : Type) (s : stream A), - bisim s (Build_stream _ s.(hd) s.(tl)). -Proof. - intros. constructor. reflexivity. simpl. apply bisim_refl. -Defined. +Program CoFixpoint ones_eq : stream_equiv ones ones.(tl) := + {| hdeq := eq_refl; tleq := ones_eq |}. + +CoFixpoint stream_equiv_refl {A} (s : Stream A) : stream_equiv s s := + {| hdeq := eq_refl; tleq := stream_equiv_refl (tl s) |}. + +CoFixpoint stream_equiv_sym {A} (s s' : Stream A) (H : stream_equiv s s') : stream_equiv s' s := + {| hdeq := eq_sym H.(hdeq); tleq := stream_equiv_sym _ _ H.(tleq) |}. + +CoFixpoint stream_equiv_trans {A} {s s' s'' : Stream A} + (H : stream_equiv s s') (H' : stream_equiv s' s'') : stream_equiv s s'' := + {| hdeq := eq_trans H.(hdeq) H'.(hdeq); + tleq := stream_equiv_trans H.(tleq) H'.(tleq) |}. -Lemma constr' : forall (A : Type) (s : stream A), - s = Build_stream _ s.(hd) s.(tl). +Program Definition eta_eq {A} (s : Stream A) : stream_equiv s (eta s):= + {| hdeq := eq_refl; tleq := stream_equiv_refl (tl (eta s))|}. + +Section Parks. + Variable A : Type. + + Variable R : Stream A -> Stream A -> Prop. + Hypothesis bisim1 : forall s1 s2:Stream A, + R s1 s2 -> hd s1 = hd s2. + Hypothesis bisim2 : forall s1 s2:Stream A, + R s1 s2 -> R (tl s1) (tl s2). + CoFixpoint park_ppl : + forall s1 s2:Stream A, R s1 s2 -> stream_equiv s1 s2 := + fun s1 s2 (p : R s1 s2) => + mkStreamEq _ _ _ (bisim1 s1 s2 p) + (park_ppl (tl s1) + (tl s2) + (bisim2 s1 s2 p)). +End Parks. + +Program CoFixpoint iterate {A} (f : A -> A) (x : A) : Stream A := + {| hd := x; tl := iterate f (f x) |}. + +Program CoFixpoint map {A B} (f : A -> B) (s : Stream A) : Stream B := + {| hd := f s.(hd); tl := map f s.(tl) |}. + +Theorem map_iterate A (f : A -> A) (x : A) : stream_equiv (iterate f (f x)) + (map f (iterate f x)). Proof. - intros. - Fail destruct s. -Abort. +apply park_ppl with +(R:= fun s1 s2 => exists x : A, s1 = iterate f (f x) /\ + s2 = map f (iterate f x)). +now intros s1 s2 (x0,(->,->)). +intros s1 s2 (x0,(->,->)). +now exists (f x0). +now exists x. +Qed. -Eval compute in constr _ ticks. +Fail Check (fun A (s : Stream A) => eq_refl : s = eta s). Notation convertible x y := (eq_refl x : x = y). |