Skip to content

Instantly share code, notes, and snippets.

@Lysxia
Created April 11, 2024 00:27
Show Gist options
  • Save Lysxia/a2d73f3bbf2480b0d47c40d1304078a3 to your computer and use it in GitHub Desktop.
Save Lysxia/a2d73f3bbf2480b0d47c40d1304078a3 to your computer and use it in GitHub Desktop.
(* 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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment