The Coq mailing list

[Maximilian Wuttke <mwuttke97 AT posteo.de>]

Hi Dominique,

On 18/02/2021 23:48, Dominique Larchey-Wendling wrote:
> From your statement, only g = f (fun x => x) can satisfy your property
> Cannot you prove that this definition of g is enough ?
> 

Thanks for your answer. Unfortunately, this definition doesn't work.
Let's consider the easy case ϕ1=ϕ2=0 again (where I simplified `Vector.t
X 0` to unit):

> Goal
>   forall (f : forall {X}, (unit -> X) -> (unit -> X)),
>   exists g : unit -> unit,
>     forall (X : Type) (i : unit -> X) (ys : unit),
>       f i ys = i (g ys).
> Proof.
>   intros f.
>   exists (f _ (fun x => x)); intros X i []; cbn.
>   (* Goal: f X i tt = i (f unit (fun x : unit => x) tt) *)
>   Undo.
>   exists (fun x => x); intros X i []; cbn.
>   (* Goal: f X i tt = i tt <This one> *)
> Abort.

Basically, since f is parametric in X, all f can do is applying the
first argument to `tt`. That's why I've chosen `g := fun x : unit => x`.
I think <This one> goal holds but I don't think it can be proved.

In the general case, f could select/permute/insert/delete/etc. elements
from the second argument `ys : Vector.t nat ϕ2` and apply this to the
first argument of type `(Vector.t nat ϕ1) -> X`.

-- Maximilian