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: Oct 13 2024 at 01:02 UTC