1

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?

Bob
  • 1,713
  • 10
  • 23

1 Answers1

4

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.
Vilhelm Sjöberg
  • 503
  • 2
  • 5
  • By the way in the documentation's examples, they use `Require Import Parametricity` instead of `Declare ML Module "paramcoq"`. But Coq cannot find this library. Any idea? I have installed Paramcoq with Opam. – Bob Mar 12 '19 at 07:56
  • @Bob It would be awesome to let the maintainers know about this. Could you open an issue on GitHub? – Anton Trunov Mar 12 '19 at 08:32
  • @Bob there is a file Parametricity.v in the paramcoq test-suite director, and then the example.v file in the same directory includes it. – Vilhelm Sjöberg Mar 12 '19 at 18:31