Paramcoq：Coq 中的自由定理

Question

如何证明以下内容free theorem with the plugin Paramcoq？

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

如果不可能，那么这个插件的用途是什么？

Answer 1

插件可以为任何类型生成参数化声明。您仍然需要将其声明为公理或假设才能实际使用它：

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.