The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Hi,

Well what I meant was that the existence of g
is just a property of f in reality (see below).
Maybe this parametricity property is not provable though.

D.

From Coq.Vectors Require Import Vector.

Section exists_g_property_f.

  Notation vec := Vector.t.

  Variables (ϕ1 ϕ2 : _) (f : forall {X}, ((vec nat ϕ1) -> X) -> ((vec nat ϕ2) 
-> X)).

  Definition g_spec g := forall (X : Type) (i : _ -> X) ys, f i ys = i (g ys).

  Theorem exists_g : (exists g, g_spec g) <-> forall X (i : _ -> X) ys, f i 
ys = i (f (fun v => v) ys).
  Proof.
    split.
    + intros (g & Hg) X i ys.
      rewrite (Hg _ (fun v => v)); apply Hg.
    + intros H; exists (f (fun v => v)); exact H.
  Qed. 

End exists_g_property_f.


----- Mail original -----
> De: "Maximilian Wuttke" <mwuttke97 AT posteo.de>
> À: "coq-club" <coq-club AT inria.fr>
> Envoyé: Vendredi 19 Février 2021 00:18:29
> Objet: Re: [Coq-Club] Parametricity Axiom

> 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