Stream: Coq users

Topic: Primitive projection wrapping


view this post on Zulip Karl Palmskog (Feb 06 2023 at 19:47):

According to the Coq manual, primitive projections are always applied, even if there was no explicit record defined to apply them to. Seemingly for this reason, the Interaction Trees library always wraps its primitive projection(s) in a function, which is then what is passed around. Are there any examples of what might happen when using unwrapped projections everywhere? The Interaction Trees code comments talk about that this can be confusing, but doesn't state any specifics.

CoInductive itree : Type := go { _observe : itreeF itree }.
(* .... *)
Definition observe {E R} (t : itree E R) : itree' E R := @_observe E R t.
(* observe and _observe have the same type *)

view this post on Zulip Yannick Zakowski (Feb 06 2023 at 22:19):

@Li-yao is the one that crafted that at the time, so he might have more insights! But he told me essentially of two motivations:

view this post on Zulip Paolo Giarrusso (Feb 06 2023 at 23:58):

Another one is that you sometimes want to rewrite under _observe, but cannot write proper instances for it: wrapping it solves this issue

That sounds super-surprising! Among other reasons, Karl's summary isn't quite complete, because Coq _already_ wraps primitive projections into constants.

view this post on Zulip Paolo Giarrusso (Feb 07 2023 at 00:02):

I wondered if somehow coinductives were difference? But not AFAIK:

Section foo.
Context (E R : Type).
Definition itreeF (X : Type) : Type := E * R * X.
CoInductive itree : Type := go { _observe : itreeF itree }.
End foo.
(* .... *)
Definition observe := @_observe.

view this post on Zulip Paolo Giarrusso (Feb 07 2023 at 00:03):

for extra fun, everything the manual says _is_ true:

Primitive projections extend the Calculus of Inductive Constructions with a new binary term constructor r.(p) representing a primitive projection p applied to a record object r (i.e., primitive projections are always applied).

That is, it _is_ true that the _primitive projection_ _observe cannot be partially applied. But _observe also refers to a wrapper — a _compatibility constant_.

view this post on Zulip Paolo Giarrusso (Feb 07 2023 at 00:05):

However, this wrapping was intended to be transparent, but it isn't in some corner cases, so there are plans to _drop_ these compatibility constant. When that happens, hopefully itree will mostly keep working as-is — except when those corner cases are relevant.

view this post on Zulip Karl Palmskog (Feb 07 2023 at 07:20):

but if all uses of _observe are already wrapped manually, how can Itree be affected by those corner cases when the compatibility constant disappears?

view this post on Zulip Karl Palmskog (Feb 07 2023 at 07:33):

it seems like the wrapping could then be motivated as a defense against future changes in Coq.

view this post on Zulip Yannick Zakowski (Feb 07 2023 at 09:38):

Mmmh the remark on Proper indeed seems incorrect, I must have misunderstood/be misremembering.
On the reduction side though here is a minimal illustration on the delay monad of the concern:

Set Primitive Projections.
Variant delayF (X : Type) (rec : Type) : Type :=
| NowF (x : X)
| LaterF (d : rec).
CoInductive delay X : Type := go { _observe : delayF X (delay X) }.
Arguments NowF {_ _}.
Arguments LaterF {_ _}.
Arguments _observe {_}.
Arguments go {_}.
Notation Now x := (go (NowF x)).
Notation Later t := (go (LaterF t)).

Definition subst {X Y} (k : X -> delay Y) : delay X -> delay Y :=
  cofix F (c : delay X) : delay Y :=
    match _observe c with
    | NowF x => k x
    | LaterF d => Later (F d)
    end.

Definition bind {X Y} (c : delay X) (k : X -> delay Y) := subst k c.

Definition iter {Acc Res : Type} (body : Acc -> delay (Acc + Res)) : Acc -> delay Res :=
  cofix F acc :=
    bind
      (body acc)
      (fun x =>
         match x with
         | inl acc' => Later (F acc')
         | inr res  => Now res
         end
      ).

Variable (body : nat -> delay (nat + nat)).
Variable (k : nat -> delay bool).
(* Undesired reduction behavior, the wrapping blocks it *)
Eval cbn in _observe (bind (iter body 0) k).

view this post on Zulip MackieLoeffel (Feb 07 2023 at 11:29):

Did you experiment with controlling the reduction behavior of _observe directly? E.g. via one of the following? These seem to fix at least this example.

Arguments _observe {_} !_.
Arguments _observe {_} : simpl never.

view this post on Zulip Paolo Giarrusso (Feb 07 2023 at 21:23):

Does Arguments _observe {_} !_ /. work? I avoid Arguments _observe {_} !_. like the pest because cbn and simpl interpret it differently sometimes. This time I haven't memorized the exact bug reports so I don't know if they would apply here...

view this post on Zulip Brandon Moore (Feb 07 2023 at 23:24):

In @Yannick Zakowski's example code Eval simpl in _observe (bind (iter body 0) k). doesn't over-reduce, even with any Arguments. Any of @Paolo Giarrusso's suggestions also work to make cbn leave _observe (bind (iter body 0) k) alone.

view this post on Zulip Li-yao (Feb 08 2023 at 00:32):

You can declare a Proper instance for the wrapper, but it does not let you rewrite under the unwrapped projection.

From Coq Require Import Setoid Morphisms.
Set Primitive Projections.

Record a : Type := { f : nat }.

Parameter aa : a -> a -> Prop.
Parameter nn : nat -> nat -> Prop.

#[global] Instance Proper_f : Proper (aa ==> nn) f.
Admitted.

Theorem w : forall x y : a, aa x y -> nn (f x) (f y).
Proof.
  intros x y H. rewrite H. (* fails *)

view this post on Zulip Paolo Giarrusso (Feb 08 2023 at 00:35):

I'm used to having Record a : Type := { f : nat -> nat }. #[global] Instance Proper_f a : Proper (nn ==> nn) (f a). work

view this post on Zulip Paolo Giarrusso (Feb 08 2023 at 00:37):

examples are robust enough to be all over Iris https://gitlab.mpi-sws.org/Blaisorblade/iris/-/blob/master/iris/bi/interface.v#L310-311

view this post on Zulip Paolo Giarrusso (Feb 08 2023 at 00:38):

but I guess you genuinely need to rewrite over a non-eq relation on itrees?

view this post on Zulip Li-yao (Feb 08 2023 at 00:39):

right, we want to rewrite the record itself

view this post on Zulip Paolo Giarrusso (Feb 08 2023 at 00:39):

so you give up on the term-size advantages of prim. projections — is the only point to get eta?

view this post on Zulip Li-yao (Feb 08 2023 at 00:46):

you can write r = {| f := f r |} with the projection if you want but then the issue is that cbn will force all of your cofix.

view this post on Zulip Paolo Giarrusso (Feb 08 2023 at 00:49):

above others suggested that Arguments f : simpl never would fix that?

view this post on Zulip Paolo Giarrusso (Feb 08 2023 at 00:51):

but mostly, I'm asking why you bother enabling primitive projections?

view this post on Zulip Paolo Giarrusso (Feb 08 2023 at 00:52):

because always using your wrappers removes the main performance advantage of prim. projs — omitting indexes E R from the actual syntax of applications, making the real term smaller

view this post on Zulip Paolo Giarrusso (Feb 08 2023 at 00:53):

then having definitional eta-equality (not just propositional) is the only remaining upside

view this post on Zulip Li-yao (Feb 08 2023 at 00:53):

cuz that's how coinductive records ought to be :)

view this post on Zulip Paolo Giarrusso (Feb 08 2023 at 00:54):

fair, all my experience is with inductive records :-)

view this post on Zulip Li-yao (Feb 08 2023 at 00:57):

The other part of it is to not find myself in a situation where _observe x does not match _observe x.

view this post on Zulip Li-yao (Feb 08 2023 at 00:58):

or wasting time to think about that being possible

view this post on Zulip Li-yao (Feb 08 2023 at 01:02):

As another way to avoid that, we could also be forbidden from writing unapplied projections, whether by being forced to write (fun x => _observe x) or by distinguishing x.(_observe) (projection) from _observe x (wrapper).

view this post on Zulip Paolo Giarrusso (Feb 08 2023 at 01:19):

The last version is interesting... There have been plans to drop the compatibility layer, but that might be a way to preserve a reasonable amount of compatibility. But it's maybe annoying that in a sense that "defaults" to the expensive variant...

view this post on Zulip Li-yao (Feb 08 2023 at 01:28):

And another goal of itree is to hide those representation details, so I just made some maybe-more-ideological-than-practical decisions knowing that it doesn't matter at the level of abstraction I cared about.

view this post on Zulip Wojciech Kołowski (Feb 08 2023 at 13:28):

@Li-yao Rewriting with the wrapper doesn't work either (at least for your example) or I'm doing something wrong.

From Coq Require Import Setoid Morphisms.
Set Primitive Projections.

Record a : Type := { f : nat }.

Parameter aa : a -> a -> Prop.
Parameter nn : nat -> nat -> Prop.

#[global] Instance Proper_f : Proper (aa ==> nn) f.
Admitted.

Theorem w : forall x y : a, aa x y -> nn (f x) (f y).
Proof.
  intros x y H.
  Fail rewrite H.
  (* Tactic failure: Nothing to rewrite. *)
Abort.

Definition f' (x : a) : nat := f x.

#[global] Instance Proper_f' : Proper (aa ==> nn) f'.
Admitted.

Theorem w : forall x y : a, aa x y -> nn (f' x) (f' y).
Proof.
  intros x y H.
  Fail rewrite H.
  (* Tactic failure: setoid rewrite failed: Unable to satisfy the following constraints: *)
Abort.

Can you give an example of a situation in which _observe x does not match _observe x (I guess you mean that they are not computationally equal)?

Also, is there any way other than convention to force primitive projections to be written as .(p)?

view this post on Zulip Paolo Giarrusso (Feb 08 2023 at 13:32):

probably better add Declare Instance : Equivalence aa. and Declare Instance : Equivalence nn to the test.


Last updated: Jun 25 2024 at 18:02 UTC