Paramcoq: свободные теоремы в Coq

Question

Paramcoq: свободные теоремы в Coq

Как я могу доказать следующую бесплатную теорему с плагином Paramcoq?

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

Если это невозможно, то какова цель этого плагина?

1

coq parametric-polymorphism coq-plugin free-theorem

Источник

user3780931 11 мар '19 в 22:46

1 ответ

Решение

Другие вопросы по тегам coq parametric-polymorphism coq-plugin free-theorem

user8378768 12 мар '19 в 02:36 2019-03-12 02:36 · Accepted Answer · 2019-03-12 02:36

Плагин может сгенерировать параметр параметричности для любого типа. Вам все равно нужно будет объявить его как аксиому или предположение, чтобы фактически использовать его:

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.