search

snu-sf / paco

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

pcofix works while gcofix doesn't? #37

Closed alxest closed 3 years ago

alxest commented 3 years ago

In the example below, pcofix tactic works while gcofix doesn't.

Require Import Coq.Relations.Relation_Definitions.
From Paco Require Import paco.
Let __add_constraint__: relation (rel2 unit (fun _ => unit)) := bot2.
Variable f: (forall R, relation R -> Prop) -> (forall R, relation R -> Prop).
Goal forall R (RR: relation R), (paco2 f bot2 R RR). Proof. pcofix CIH. Abort.
Goal forall R (RR: relation R), (gpaco2 f (cpn2 f) bot2 bot2 R RR). Proof. Fail gcofix CIH. Abort.

It seems like gcofix is somewhat universe-sensitive while pcofix isn't. Related issue: https://github.com/DeepSpec/InteractionTrees/issues/193

gilhur commented 3 years ago

I just checked it. It is a simple bug of gcofix. I will fix it soon.

gilhur commented 3 years ago

I pushed the fix for this bug. @minkiminki, can you update the opam package?

alxest commented 3 years ago

Thanks for your effort!