Search code examples
coqparametric-polymorphismcoq-pluginfree-theorem

Paramcoq: Free theorems in Coq

How can I prove the following free theorem with the plugin Paramcoq?

Lemma id_free (f : forall A : Type, A -> A) (X : Type) (x : X), f X x = x.

If it is not possible, then what is the purpose of this plugin?

Solution

  • The plugin can generate the statement of parametricity for any type. You will still need to then declare it as an axiom or an assumption to actually use it:

    Declare ML Module "paramcoq".

Definition idt := forall A:Type, A -> A.
Parametricity idt arity 1.
(* ^^^ This command defines the constant idt_P. *)

Axiom param_idt : forall f, idt_P f.

Lemma id_free (f : forall A : Type, A -> A) (X : Type) (x : X) : f X x = x.
Proof.
  intros. 
  apply (param_idt f X (fun y => y = x) x).
  reflexivity.
Qed.