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 *)
```

@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:

- An obvious one is that without it,
`cbn`

gets really too aggressive. It is pleasant to have`_observe (bind t k)`

reduce in simple cases, but the primitive projection propagates all the way. So wrapping it controls reduction, letting you handle it by rewriting - Another one is that you sometimes want to rewrite under
`_observe`

, but cannot write proper instances for it: wrapping it solves this issue

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.

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.
```

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_.

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.

but if all uses of `_observe`

are *already* wrapped manually, how can Itree be affected by those corner cases when the compatibility constant disappears?

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

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).
```

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.
```

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...

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.

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 *)
```

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

work

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

but I guess you genuinely need to rewrite over a non-`eq`

relation on itrees?

right, we want to rewrite the record itself

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

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.

above others suggested that `Arguments f : simpl never`

would fix that?

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

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

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

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

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

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

does not match `_observe x`

.

or wasting time to think about that being possible

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).

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...

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.

@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)`

?

probably better add `Declare Instance : Equivalence aa.`

and `Declare Instance : Equivalence nn`

to the test.

Last updated: Jun 25 2024 at 18:02 UTC