search

snu-sf / paco

A Coq library for parametric coinduction
https://github.com/snu-sf/paco
Other
43 stars 10 forks source link

paco <= gpaco lemma? #35

Closed alxest closed 3 years ago

alxest commented 4 years ago

I found the following lemma useful during the proof. Maybe we can add it to the library?

  Lemma gpaco4_paco4
        clo r rg
    :
      paco4 gf r <4= gpaco4 gf clo r rg
  .
  Proof.
    intros.
    econstructor. econstructor. left.
    eapply paco4_mon; eauto.
    unfold Basics.compose.
    eapply paco4_mon_gen; eauto. intros.
    eapply gf_mon; eauto. intros. econstructor. eauto.
  Qed.
minkiminki commented 3 years ago

gpaco[N]_final is more strong.