1
$\begingroup$

It might be a very silly question for the logic gurus but less so for me. First I generally describe the issue, than I provide a proper example with code.

Assume three streams of nats: xs, ys, zs. Using paco, I want to prove the bisimilarity of xs & ys, where seq' is the bisimilarity relation:

Lemma xs_ys:
 seq' xs ys.
Proof.
 pcofix coIH.
 (* get heads out *)
 pfold; constructor; right.
 (* Now I need to show "r xs' ys'" *)

My lemma was stated not generally enough, so I cannot use coIH. I could use coIH to show: r xs' zs and I also have previously proved seq' ys' zs, so I hoped to use coIH as an argument to some form of transitivity.

Using paco I could not figure a way to do it, since there are different types (seq' vs r), using basic cofix I could, but I could not Qed.

My question is

a) Does it break any coinduction principle?

b) If not, is it still somehow possible in paco manipulating seq' vs r relationship.

Below is a simplified updated reproducible example.

Require Import Arith Bool List.
Require Import Setoid Program.
Require Import Paco.paco.
(*****************)
(***** SETUP *****)
(*****************)
CoInductive stream (V : Type) : Type :=
| Cons : V -> stream V -> stream V.

Inductive seq_gen seq : stream nat -> stream nat -> Prop :=
  | _seq_gen : forall n s1 s2 (R : seq s1 s2 : Prop), seq_gen seq (Cons nat n s1) (Cons nat n s2).
#[export] Hint Constructors seq_gen : core.

CoInductive seq : stream nat -> stream nat -> Prop :=
| seq_fold : forall s1 s2, seq_gen seq s1 s2 -> seq s1 s2.
Definition seq' s1 s2 := paco2 seq_gen bot2 s1 s2.
#[export] Hint Unfold seq' : core.
Lemma seq_gen_mon: monotone2 seq_gen. Proof. pmonauto. Qed.
#[export] Hint Resolve seq_gen_mon : paco.

Theorem seq'_cons : forall n1 n2 s1 s2 (SEQ : seq' (Cons nat n1 s1) (Cons nat n2 s2)),
  n1 = n2 /\ seq' s1 s2.
Proof.
  intros.
  punfold SEQ.
  inversion_clear SEQ.
  pclearbot.
  auto.
Qed.

Definition stream_decompose (V : Type) (s : stream V) :=
  match s with
  | Cons _ v s' =>
    Cons V v s'
  end.

Theorem stream_decomposition :
  forall (V : Type)
         (s : stream V),
    s = stream_decompose V s.
Proof.
  intros V [v s'].
  unfold stream_decompose.
  reflexivity.
Qed.

Ltac unfold_and_fold f :=
  unfold stream_decompose;
  unfold f; fold f.


Lemma seq'_is_transitive :
  forall xs ys zs : stream nat,
    seq' xs ys ->
    seq' ys zs ->
    seq' xs zs.
Proof.
  pcofix coIH.
  intros [x xs'] [y ys'] [z zs'] seq'_xs_ys seq'_ys_zs.

  destruct (seq'_cons x y xs' ys' seq'_xs_ys) as [eq_x_y seq'_xs'_ys']; clear seq'_xs_ys.
  destruct (seq'_cons y z ys' zs' seq'_ys_zs) as [eq_y_z seq'_ys'_zs']; clear seq'_ys_zs.

  rewrite -> eq_x_y, eq_y_z.

  pfold; constructor; right.

  exact (coIH xs' ys' zs' seq'_xs'_ys' seq'_ys'_zs').
Qed. 

(**********************)
(***** MAIN POINT / EXAMPLE *****)
(**********************)

Fixpoint sum (n x : nat) : nat :=
  match n with
  | O => 0
  | S n' => x + (sum n' x)
  end.


CoFixpoint nats_v0_aux (n : nat) : stream nat :=
  Cons nat n (nats_v0_aux (S n)).

Definition nats_v0 : stream nat :=
  nats_v0_aux 0.

CoFixpoint nats_v1_aux (n : nat) : stream nat :=
  Cons nat (sum n 1) (nats_v1_aux (S n)).

Definition nats_v1 : stream nat :=
  nats_v1_aux 0.

Lemma about_sum :
  forall (j : nat),
    sum j 1 = j.
Proof.
  induction j as [ | j' IHj'].
  - simpl; reflexivity.
  - simpl; rewrite IHj'; reflexivity.
Qed.

Lemma seq'_ys_zs :
  forall (i : nat),
    seq' (nats_v0_aux (S i)) (nats_v0_aux (S i)).
Proof.
  pcofix coIH.
  intro i.
  rewrite -> (stream_decomposition nat (nats_v0_aux (S i))).
  unfold_and_fold nats_v0_aux.
  pfold; constructor; right.
  exact (coIH (S i)).
Qed.
  
Theorem seq'_nats_v0_nats_v1 :
  forall (i : nat),
    seq' (nats_v0_aux i) (nats_v1_aux i).
Proof.
  pcofix xs_ys.
  intro i.
  rewrite -> (stream_decomposition nat (nats_v0_aux i)).
  rewrite -> (stream_decomposition nat (nats_v1_aux i)).
  unfold_and_fold nats_v0_aux.
  unfold_and_fold nats_v1_aux.
  rewrite about_sum.
  pfold; constructor; right.
  (* I could easily use xs_ys here *)
  (* But this is not the point of the example *)
  (* Instead, I want to either
     a) rewrite 
        nats_v0_aux (S i) with
        nats_v0_aux (S i) using
        seq'_ys_zs
        and then 
        exact xs_ys
     b) use transitivity to show
        xs_ys -> seq'_ys_zs -> my goal.
   *)
Abort.
$\endgroup$
1
  • $\begingroup$ You need to establish a stronger fact than transitivity of seq': validity of seq_gen bisimulation up-to seq_gen. I will write down a detailed answer tonight, but your code is not quite compiling, you are missing notably stream_decomposiiton and ones. Can you fix it to ease answering please? $\endgroup$ Feb 27 at 16:24

1 Answer 1

0
$\begingroup$

I am slightly unsure about your question as your code does not compile but seems to only require the reflexivity of seq', but your question seems to ask whether you can, in the middle of a proof by coinduction, rewrite by a previously established seq' equation.

I will therefore try to answer the latter question, first from a theoretical standpoint, then using paco.

Normal coinduction principle for νb (here, b == seq_gen):

First, recall that what you have access by default is essentially the basic coinduction principle from Knaster Tarski, i.e.:

 x <= y /\ y <= by
-----------------
     x <= νb

So the core of the proof consistes in proving "y <= by" for a well chosen candidate y. For a binary relation, that looks like that in the middle of a proof:

   y a b
  --------
  b y a b

Making things a bit more concrete, in the case at hand, a and b are streams, b is seq_gen, and y the parameter r paco introduced. In your proof, you know some structure about y, and therefore about a and b, allowing you to prove they have the same head and therefore "step through b". You have now as a goal:

   y a b
  --------
  y a' b'

for some particular a' and b'. If you had chosen y wisely, i.e., if y was indeed a valid coinduction candidate, you must have fallen back into it and can conclude.

Up-to principle

What you ask (I think) is: what if I missed, but not by much? I.e., in particular here, what if the pair (a',b') is not in y, but y contains a pair (a',b') such that seq a a' and seq b' b. Surely that should be fair to conclude even if I didn't really pick a coinductively stable set?

Well, it can be fair (as in sound) or it may be unsound depending on [b]: you are asking what is referred to in the literature whether b-bisimulation up-to b-bisimilarity is a valid principle. Famously, it is valid when considering strong bisimilarity, but not when considering weak bisimilarity: see chapter 4 of Sangiorgi's "Introduction to Bisimulation and Coinduction" for a detailed and gentle explanation.

Now in your case, it absolutely is valid! But we need to prove it. Luckily, paco (as well as Pous's coq-coinduction library) provide tools to do so.

Before jumping into the code, let's rephrase what we are aiming to prove, i.e., that the following principle is valid:

    x <= y /\ y <= bfy
  -----------------
       x <= νb

That is: after stepping through b, we don't have to fall back exactly into y, but can fall into something slightly bigger, some (f y) for a well chosen f. Libraries like paco provide a sufficient condition to establish this principle, and some support to use it smoothly.

With that in mind, we start by defining the specific f of interest, i.e. the one that allows us to look for bisimilar (seq-related) pairs in our set. We call it [seqTC] for seq_transitive_closure.

Based on your definitions, you can use the following code to implement the ideas described above.

(* UPDATED CODE 02/28 following OP's edit *)

(* BEGIN NEW CODE *)
Variant seqTC (r : stream nat -> stream nat -> Prop)
  : stream nat -> stream nat -> Prop :=
| seqTC_intro s1 s1' s2 s2'
      (EQl: seq' s1 s1')
      (EQr: seq' s2 s2')
      (REL: r s1' s2')
  : seqTC r s1 s2
.

(* It must be monotone, and we inform paco of this fact *)
Lemma seqTC_mon r1 r2 s1 s2
      (IN: seqTC r1 s1 s2)
      (LE: r1 <2= r2):
  seqTC r2 s1 s2.
Proof.
  destruct IN. econstructor; eauto.
Qed.
Hint Resolve seqTC_mon : paco.

(* Now here is the crucial proof obligation: compatibility is a sufficient condition to establish the validity of our up-to principle!
  I would recommend for instance Pous's «CoInduction All The Way Up» for more details on this sufficient condition.
 *)
Lemma seqTC_compat:
  compatible2 seq_gen seqTC.
Proof.
  econstructor; eauto with paco.
  intros ? s1 s2 H.
  inversion_clear H.
  punfold EQl; inversion EQl.
  punfold EQr; inversion EQr.
  inversion REL.
  subst.
  inversion H3; inversion H4; subst.
  constructor.
  pclearbot.
  econstructor; eauto.
Qed.
(* For technical reasons, paco let you establish something slightly weaker than compatibility.
  We hence derive trivially this alternative, and inform paco of this fact.
*)
Lemma seqTC_wcompat:
  wcompatible2 seq_gen seqTC.
Proof.
  apply compat2_wcompat; eauto with paco; apply seqTC_compat.
Qed.
Hint Resolve seqTC_wcompat : paco.

(* Up-to reflexivity is always true *)
#[global] Instance Reflexive_seq_gen f (r rg: stream nat -> stream nat -> Prop) :
  Reflexive (gpaco2 seq_gen f r rg).
Proof.
  gcofix CIH. gstep; intros.
  destruct x; constructor.
  eauto with paco.
Qed.

(* So in particular seq is reflexive *)
#[global] Instance Reflexive_seq :
  Reflexive seq'.
Proof.
  intro.
  ginit.
  apply Reflexive_seq_gen.
Qed.

From Coq Require Import Morphisms.
(* So in particular seq is reflexive *)
#[global] Instance seq_seq_gen (r rg: stream nat -> stream nat -> Prop) :
  Proper (seq' ==> seq' ==> flip impl) (gpaco2 seq_gen seqTC r rg).
Proof.
  intros ?? EQ1 ?? EQ2 EQ3.
  gclo; econstructor; eauto.
Qed.

(* END NEW CODE *)

(* BEGIN EXAMPLE *)
Theorem seq'_nats_v0_nats_v1 :
  forall (i : nat),
    seq' (nats_v0_aux i) (nats_v1_aux i).
Proof.
  (* YOUR CODE *)
  pcofix xs_ys.
  intro i.
  rewrite -> (stream_decomposition nat (nats_v0_aux i)).
  rewrite -> (stream_decomposition nat (nats_v1_aux i)).
  unfold_and_fold nats_v0_aux.
  unfold_and_fold nats_v1_aux.
  rewrite about_sum.
  pfold; constructor.
  (* You have stepped, as you say you can conclude by *)
  right; exact (xs_ys (S i)).
  (* But this is not the point of the example *)
  Restart.
  (* a. and b. are essentially the same, one explicit the other implicit.
     Let's do b. first, the explicit use of transitivity *)
  (* We move to the generalized world. Note that it picks up automatically [seqTC] in doing so *)
  (* We follow the same step with the renaming:
     pcofix -> gcofix
     pfold/pstep -> gstep
   *)
  ginit.
  gcofix xs_ys.
  intro i.
  rewrite -> (stream_decomposition nat (nats_v0_aux i)).
  rewrite -> (stream_decomposition nat (nats_v1_aux i)).
  unfold_and_fold nats_v0_aux.
  unfold_and_fold nats_v1_aux.
  rewrite about_sum.
  gstep; constructor.
  (* You have stepped, again, could conclude, but let's illustrate b.
     We invoke the closure
   *)
  gclo.
  econstructor.
  (* We can use transitivity on each side. We use [seq'_ys_zs] on the left, reflexivity on the right *)
  apply seq'_ys_zs.
  reflexivity.
  (* Of course this is a bit silly as we just rewrote [x ≡ x], but we did it nonetheless! We can conclude *)
  gbase.
  exact (xs_ys (S i)).
  Restart.
  (* and finally option (a), amounts to the same but wrapped in typeclass extravaganza *)
   ginit.
  gcofix xs_ys.
  intro i.
  rewrite -> (stream_decomposition nat (nats_v0_aux i)).
  rewrite -> (stream_decomposition nat (nats_v1_aux i)).
  unfold_and_fold nats_v0_aux.
  unfold_and_fold nats_v1_aux.
  rewrite about_sum.
  gstep; constructor.
  (* You have stepped, again, could conclude, but let's illustrate a.
     Thanks to seq_seq_gen, you can simply rewrite.
     Well you could, except that coq complain it fails to progress as
     the equation is of the shape [x ≡ x], but as far as paco and seq' is concerned,
     you can!
   *)
  Fail rewrite seq'_ys_zs.
Abort.
$\endgroup$
5
  • $\begingroup$ Dear Yannick, thank you so much for this detailed answer. Sorry for the late update, living in a very different timezone. Let me address some of the points: 1. I have updated the code section to make sure it compiles. I also replaced the example of 'ones' with a little more comprehensible one. 2. The last theorem there explains that I do know that I could prove this example in a very simple way, but that is not the point. The point would be for a more general case, where my coIH can fit s1 but cannot fit s2, and instead it can show s1~s3, where I have previously shown s2~s3. $\endgroup$ Feb 28 at 5:32
  • $\begingroup$ 3. An important note is that s1 and s2 refer to the tails of the original streams as you can see in the example. Assume I do not have a theorem s2_original ~ s3, but specifically s2~s3. Hence, I need to unfold the original streams. 4. I will be jumping into "Introduction to Bisimulation and Coinduction" in a bit, and I also read the paper behind paco, but I am still catching up with the definitions you provided above. Do you mind showing Lemma foo s1 s2 in the context of what I provided (Theorem seq'_nats_v0_nats_v1 )? $\endgroup$ Feb 28 at 5:41
  • $\begingroup$ Hello! It does feel like you are indeed looking for what I have described in my answer. I have updated the code to use the one from your edit. As you can see in your example I can either explicitly use the closure to "transit" via seq'_ys_zs, or could directly rewrite with it if it was not a trivial equation. $\endgroup$ Feb 28 at 10:41
  • $\begingroup$ You may also be interested in the paper we had written about gpaco: arxiv.org/abs/2001.02659 $\endgroup$ Feb 28 at 10:41
  • $\begingroup$ Thank you so much! It answers my question precisely. Just some readings left to do for me. $\endgroup$ Feb 28 at 11:34

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.