Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: coindprim.v Sprache: Coq

Original von: Coq^©

Require Import Program.

Set Primitive Projections.

CoInductive Stream (A : Type) := mkStream { hd : A; tl : Stream A}.

Arguments mkStream [A] hd tl.
Arguments hd [A] s.
Arguments tl [A] s.

Definition eta {A} (s : Stream A) := {| hd := s.(hd); tl := s.(tl) |}.

CoFixpoint ones := {| hd := 1; tl := ones |}.
CoFixpoint ticks := {| hd := tt; tl := ticks |}.

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 hdeq {A} {s} {s'}.
Arguments tleq {A} {s} {s'}.

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

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

Fail Check (fun A (s : Stream A) => eq_refl : s = eta s).

Notation convertible x y := (eq_refl x : x = y).

Fail Check convertible ticks {| hd := hd ticks; tl := tl ticks |}.

CoInductive U := inU
{ outU : U }.

CoFixpoint u : U :=
  inU u.

CoFixpoint force (u : U) : U :=
  inU (outU u).

Lemma eq (x : U) : x = force x.
Proof.
  Fail destruct x.
Abort.
  (* Impossible *)

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.