Paramcoq: Free theorems in Coq

292 views Asked by At

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?

1

There are 1 answers

3
Vilhelm Sjöberg On BEST ANSWER

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.