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?

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

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

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

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.

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`

?

Like below?

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

Yes! Thanks.

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

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: Jun 15 2024 at 08:01 UTC