Characterization of the type (forall a, ((a -> a) -> a) -> a) https://cstheory.stackexchange.com/questions/53855/can-we-use-relational-parametricity-to-simplify-the-type-forall-a-a-to-a

TUTUT.v

(* formalization attached to my answer to https://cstheory.stackexchange.com/questions/53855/can-we-use-relational-parametricity-to-simplify-the-type-forall-a-a-to-a *)
From Coq Require Import Lia.

Definition U : Type := forall A : Type, ((A -> A) -> A) -> A.

(* Try enumerating solutions by hand. After the initial [intros],
   we can either complete the term with [exact xi],
   or continue deeper with [apply f; intros xi]. *)
Goal U.
Proof.
  intros A f.
  apply f.
  intros x1.
  (* exact x1. *)
  apply f.
  intros x2.
  (* exact x1. *)
  (* exact x2. *)
  apply f.
  intros x3.
  (* etc. *)
Abort.

(* Examples *)
Definition f_0_0 : U := fun A f => f (fun x => x).
Definition f_0_1 : U := fun A f => f (fun x => f (fun _ => x)).
Definition f_1_0 : U := fun A f => f (fun _ => f (fun x => x)).
Definition f_0_2 : U := fun A f => f (fun x => f (fun _ => f (fun _ => x))).
Definition f_1_1 : U := fun A f => f (fun _ => f (fun x => f (fun _ => x))).
Definition f_2_0 : U := fun A f => f (fun _ => f (fun _ => f (fun x => x))).

(* A pair counting the number of "_" before and after the used variable. *)
Definition T : Type := (nat * nat).

(* Conjecture: U = T *)

(* Easy direction: T -> U *)

Definition fn {A : Type} (n : nat) (f : (A -> A) -> A) : A -> A :=
  Nat.iter n (fun y => f (fun _ => y)).

(* (Claim 2 in my SE post) *)
Definition T2U : T -> U := fun '(n, m) A f => fn n f (f (fun x => fn m f x)).

(* Hard direction: U -> T *)

(* Define (U -> T) by instantiating U with (A := A0): *)

Definition A0 : Type := nat -> T.
(* Use the [nat] to "count" the number/depth of nested calls to
   the function argument (f : (A -> A) -> A). *)

(* This encodes the variable x of the argument ((fun x => ...) : A -> A) of the argument (f : (A -> A) -> A).
   It gets passed the depth "n" of the current call to "f",
   and the successor "m" of the final depth of the last call to "f", and remembers them in a pair,
   storing the difference m-n-1 instead of m. *)
Definition x0 : nat -> A0 :=
  fun n m => (n, m - n - 1).

Definition f0 : (A0 -> A0) -> A0 :=
  fun g n => g (x0 n) (S n).

Definition U2T : U -> T := fun u => u A0 f0 0.

(* (Claim 1 in my SE post) *)
(* All terms of type U are (beta-equivalent) to some [T2U nm]. That means that
   [T2U] is surjective (in an external sense). Maybe there is a more general parametricity
   principle that implies this. *)
Parameter U2T2U : forall u, T2U (U2T u) = u.

(* (Claim 3 in my SE post) *)
(* U2T is surjective; T2U is injective *)

Theorem T2U2T : forall nm, U2T (T2U nm) = nm.
Proof.
  assert (H : forall n g i, fn n f0 g i = g (n + i)).
  { induction n; simpl.
    - reflexivity.
    - intros. unfold f0 at 1. rewrite IHn. rewrite plus_n_Sm. reflexivity. }
  intros [n m]. unfold U2T, T2U.
  rewrite H, <- plus_n_O. unfold f0 at 1. rewrite H. unfold x0. f_equal. lia.
Qed.