2
$\begingroup$

Suppose the following definition of an infinite stream in rocq:

CoFixpoint test x: traceinf :=
  Econsinf x (test x).

It seems that wanting to prove forall x, test x = Econsinf x (test x) is shooting to high. So instead I want to prove bisimilarity: forall x, traceinf_sim (test x) (Econsinf x (test x)). However, I do not manage to do it. (My goal is to unfold a single application of test).

Trying to destruct test just gives me test x = Econsinf e t without relating t and test, and unfolding test gives me a cofix expression that I am not able to use in any way.

So (how) can I show bisimilarity?

For completeness, it is

CoInductive traceinf : Type :=
  | Econsinf: nat -> traceinf -> traceinf.

CoInductive traceinf_sim: traceinf -> traceinf -> Prop :=
  | traceinf_sim_cons: forall e T1 T2,
      traceinf_sim T1 T2 ->
      traceinf_sim (Econsinf e T1) (Econsinf e T2).
Improve this question
$\endgroup$

1 Answer 1

Reset to default
2
$\begingroup$

I managed to prove full equality using a standard unfolding technique as described by Yves Bertot here:

Definition unfold_traceinf T := match T with Econsinf e T => Econsinf e T end.

Lemma unfold_spec: forall l,
  l = unfold_traceinf l.
Proof.
  intros. now destruct l.
Qed.

Lemma equal: forall x, test x = Econsinf x (test x).
Proof.
  intros. now rewrite (unfold_spec (test x)) at 1.
Qed.
Improve this answer
$\endgroup$
1
  • 2
    $\begingroup$ I believe this is the right approach to handle this sort of goals. $\endgroup$ Commented Nov 3 at 12:20

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.