Повторное использование аксиомы с классами типов в Coq - PullRequest
Новая
       4

Повторное использование аксиомы с классами типов в Coq

0 голосов
/ 30 марта 2020

Я пытаюсь использовать классы типов для повторного использования кода, но я получаю сетоидные ошибки, применяя родительские аксиомы классов типов в теоремах дочерних классов типов. Я сделал MRE со следующими операциями равенства и сложения: 

Require Import Setoid.

(* Equality *)
Parameter CEq : forall A, A->A->Prop.
Arguments CEq [A] _ _.
Notation "x ¦ y" := (CEq x y) (at level 70, no associativity).
Axiom ceq_reflexivity: forall A, forall a:A, a¦a.
Axiom ceq_symmetry: forall A, forall a b:A, a¦b->b¦a.
Axiom ceq_transitivity: forall A, forall a b c:A, a¦b->b¦c->a¦c.
Add Parametric Relation A : (A) (@CEq A)
  reflexivity proved by (@ceq_reflexivity A)
  symmetry proved by (@ceq_symmetry A)
  transitivity proved by (@ceq_transitivity A)
  as ceq_rel.

(* Addition *)
Parameter CAdd: forall A, A->A->A.
Arguments CAdd [A] _ _.
Infix "±" := CAdd  (at level 50, left associativity).

Ниже перечислены родительские и дочерние классы: 

(* Parent Typeclass *)
Class CDiscT (CDisc: Set) := {
  O: forall CDisc, CDisc;
  cdisc_add_neutral:forall CDisc, forall x:CDisc, x±(O CDisc)¦x;
}.

(* Natural Set & Child Typeclass *)
Parameter CNat: Set.
Class CNatT `{CDiscT CNat} := {}.

А вот неверная теорема: 

(* Axiom inheritance test *)
Example test `{CNatT}: (O CNat)¦(O CNat)±(O CNat).
Proof.
  rewrite <- cdisc_add_neutral. (* Error *)
  reflexivity.
Qed.

Вот ошибка: 

Error:
Tactic failure: setoid rewrite failed: Unable to satisfy the following constraints:
In environment:
H : CDiscT CNat
H0 : CNatT

?s : "subrelation (CEq (A:=Prop)) (Basics.flip Basics.impl)"

Чего здесь не хватает, чтобы иметь возможность использовать аксиомы CDiscT внутри теорем CNatT? Есть ли лучший способ сделать это?

1 Ответ

1 голос
/ 30 марта 2020

Это может быть отчасти потому, что ваш пример слишком упрощен, но перезапись справа налево с помощью cdisc_add_neutral проблематично c, потому что правая часть x соответствует чему угодно и может иметь любой тип.

Ошибка, которую вы получаете, заключается в том, что Coq пытается переписать всю цель вместе с ней, но это будет использовать логическое значение impl, что, в свою очередь, требует, чтобы ваше отношение CEq было подчиненным отношением impl.

Вы можете избежать этого, немного специализировав лемму: 

  rewrite <- (cdisc_add_neutral CNat) at 1.

Вам нужен at 1, потому что теперь совпадающее подтерм является O CNat, но это происходит трижды в вашей цели , rewrite пытается переписать их все по умолчанию, что требует Proper экземпляров, которые здесь отсутствуют. (Вы можете получить их с помощью механизма Parametric Morphism, описанного в руководстве.)

Кроме того, вы можете переписать слева направо: 

rewrite cdisc_add_neutral
...