Stream: Coq users

Topic: Using Streams.Exists


view this post on Zulip Julin S (Oct 02 2022 at 05:20):

I got a stream like:

Require Import Streams.

CoFixpoint const3 : Stream nat := Cons 3 const3.

Now, I wanted to say that at some point in the stream const3, the value is 3 using Streams.Exists.

How can that be done?

Streams.Exists is like:

Exists
     : forall {A : Type}, (Stream A -> Prop) -> Stream A -> Prop

But how can we make a value of type Stream A -> Prop for this?

Check Streams.Exists _ const3.

How can the hole here be filled?

view this post on Zulip Pierre Castéran (Oct 02 2022 at 06:31):

Is the following example OK ?

Lemma stm_unfold {A: Type} (s: Stream A) :
  s = match s with Cons a s' => Cons a s' end.
Proof.
  now destruct s.
Qed.

Inductive starts_with {A: Type} (a:A): Stream A -> Prop :=
      starts_hd : forall s, starts_with a (Cons a s).

Goal Streams.Exists (starts_with 3) const3.
  left; rewrite (stm_unfold const3); split.
Qed.

Goal Streams.Exists (starts_with 3) (Cons 4 const3).
  right;  left. rewrite (stm_unfold const3). split.
Qed.

view this post on Zulip Julin S (Oct 06 2022 at 07:17):

Thanks. Sorry for the very late reply.. :grimacing:

view this post on Zulip Julin S (Oct 06 2022 at 07:18):

Should all predicates involving a coinductive type made an inductive type? Is there a way to skip doing that in this case?

view this post on Zulip Julin S (Oct 06 2022 at 07:54):

Could do a ForAll example like:

Goal
  Streams.ForAll (starts_with 3) const3.
Proof.
  cofix const3.
  split.
  - rewrite (sUnfold att4.const3).  (* TODO: FILENAME!!! *)
    constructor.
  - unfold tl.
    simpl.
    exact const3.
Qed.

But that too involved proposition made as an inductive type.

view this post on Zulip Julin S (Oct 06 2022 at 07:57):

Could it be possible to have the propostion as a function or something?

Like: fun x:Stream nat => Streams.hd x == 3 or something in lieu of startswith?

view this post on Zulip Pierre Castéran (Oct 06 2022 at 08:22):

Like below?

Goal Streams.ForAll (fun s => Streams.hd s = 3) const3.
cofix always3.
 rewrite (stm_unfold const3) ; split.
 - reflexivity.
 - cbn; apply always3.
Qed.

view this post on Zulip Julin S (Oct 06 2022 at 09:03):

Yes! Thanks.

view this post on Zulip Julin S (Oct 06 2022 at 09:04):

Is there any advantage in using separate inductive types to represent propositions though?

view this post on Zulip Karl Palmskog (Oct 06 2022 at 09:12):

if you're going to express that something happens eventually in an infinite Stream, how'd you do it without regular inductive propositions? At least in the Streams library, this is how the game is played. You could of course reason about infinite streams in some deeply embedded logic with its separately defined semantics.


Last updated: Jan 29 2023 at 06:02 UTC