## Stream: Coq users

### Topic: Simple proof with coinductive type

#### Julin Shaji (Dec 06 2023 at 11:47):

Hi. I had been trying a small proof with a coinductive type.

``````CoInductive stream (A: Type): Type :=
| SNil: stream A
| SCons: A -> stream A -> stream A.
Arguments SNil {A}.
Arguments SCons {A}.

CoFixpoint sapp {A: Type} (a b: stream A): stream A :=
match a with
| SNil => b
| SCons x a' => SCons x (sapp a' b)
end.

Lemma sappSNil: forall (A: Type) (s: stream A),
sapp SNil s = s.
Proof.
intros A s.
(*
1 subgoal

A : Type
s : stream A

========================= (1 / 1)

sapp SNil s = s
*)
``````

How can we get this proof done?

Goal sort of directly follows from the definition.

Unfolding didn't help either?

#### Pierre Castéran (Dec 06 2023 at 15:10):

A possible trick (among others?) is to prove and apply "unfolding lemmas"

``````Definition decompose {A} (a: stream A) :=
match a with
SNil => SNil
| SCons x b => SCons x b
end.

Lemma unfold_lemma {A} (a: stream A): a = decompose a.
Proof.
destruct a; reflexivity.
Qed.

Goal forall {A} (a: stream A), sapp SNil a = a.
Proof.
intros; rewrite (unfold_lemma (sapp SNil a)).
destruct a;  reflexivity.
Qed.
``````

#### Julin Shaji (Dec 06 2023 at 15:35):

Thanks! Rewriting with unfolding indeed solved it.

#### Pierre Castéran (Dec 06 2023 at 15:44):

You can find similar examples in section 13.4 of this chapter

#### Julin Shaji (Dec 06 2023 at 15:55):

Yeah, I was reading that. That's when I got here. I wasn't sure how to use the unfolding lemma.. :sweat_smile:

#### Julin Shaji (Dec 06 2023 at 15:56):

No, I hadn't read 13.4. Had jumped directly to see how ltl was formalized.. I better have a look at the earlier sections.

Last updated: Jun 22 2024 at 16:02 UTC