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?
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.
Thanks! Rewriting with unfolding indeed solved it.
You can find similar examples in section 13.4 of this chapter
Yeah, I was reading that. That's when I got here. I wasn't sure how to use the unfolding lemma.. :sweat_smile:
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