Stream: Coq users

Topic: Simple proof with coinductive type


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Julin Shaji (Dec 06 2023 at 15:35):

Thanks! Rewriting with unfolding indeed solved it.

view this post on Zulip Pierre Castéran (Dec 06 2023 at 15:44):

You can find similar examples in section 13.4 of this chapter

view this post on Zulip 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:

view this post on Zulip 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: Oct 13 2024 at 01:02 UTC