Paramcoq: свободные теоремы в Coq - PullRequest
Новая
       73

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

1 голос
/ 12 марта 2019

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

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

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

1 Ответ

4 голосов
/ 12 марта 2019

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

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.
...