SsrReflect и переписывание сетоидов - PullRequest
Новая
       72

SsrReflect и переписывание сетоидов

1 голос
/ 02 февраля 2020

Я не могу использовать переписывание Ssreflect с сетоидами. Хотя я не думаю, что эта информация имеет отношение к решению проблемы, я использую эту формулировку теории категорий в coq: https://github.com/jwiegley/category-theory.

Насколько я знаю, Ssreflect's при переписывании могут использоваться определяемые пользователем отношения эквивалентности, если может быть разрешен подходящий RewriteRelation экземпляр класса типов. 

Context { x y : obj[C]}.

About RewriteRelation.
(* ∀ A : Type, crelation A → Prop *)

Instance equivrw : (@RewriteRelation (x ~> y) (@equiv (x ~> y) (homset x y))) := {}. (* defined and correctly type-checked *)
About equivrw.
(* RewriteRelation equiv (coq omits implicit arguments) *)

Lemma test_rwrel (a b c : x ~> y) : (@equiv (x ~> y) (homset x y) a b) -> (@equiv (x ~> y) (homset x y)  b c) -> (@equiv (x ~> y) (homset x y) a c).
Proof.
    move => ->.
    (* Fails: not a rewritable relation: (a ≈ b) in rule __top_assumption_ *)

Вместо этого работает перезапись по умолчанию tacti c (даже без ручного объявления экземпляра, поскольку что-то похожее уже объявлено в библиотеке).

Что-то смешное: 

Instance equivrw : (@RewriteRelation False equiv) := {}.
Lemma test_rwrel (a b c : False) : (equiv a b) -> (equiv b c) -> (equiv a c).
Proof.
    move => ->.
    by []. 
Qed.

Это прекрасно работает.

Почему SSReflect не использует экземпляр RewriteRelation, который я объявил вручную переписать по пользовательской эквивалентности? Заранее спасибо.

РЕДАКТИРОВАТЬ: Я выяснил, почему Ssreflect не видит мои отношения. По-видимому, вы можете добавить отношения, которые будут использоваться с перезаписью Ssreflect, только с Add Parametric Relation, что задокументировано в руководстве, и экземпляры RewriteRelation ничего не изменят. Я попытался создать поддельное отношение, используя аксиомы и добавив его с Add Parametric Relation и rewriting, работает правильно. Но теперь я снова в беде. Отношение, которое я хочу использовать, имеет тип crelation (x ~> y) (который (x ~> y) -> (x ~> y) -> Type), но для использования Add Parametric Relation мне нужен термин с типом relation (x ~> y) (который (x ~> y) -> (x ~> y) -> Prop. Почему два разных вида отношения (relation и crelation) были определены в стандартной библиотеке? Как я могу преобразовать crelation в relation без ошибок несоответствия юниверса? И я до сих пор не могу понять, почему приведенный выше пример с False работы.

1 Ответ

2 голосов
/ 03 февраля 2020

Недостаточно и не нужно объявлять отношение как RewriteRelation. Вы должны доказать свойства, обеспечивающие логическую корректность перезаписи, наиболее распространенной из которых является транзитивность (но вам часто требуется и рефлексивность, и даже симметрия).

Как вы уже заметили, плагин для переписывания setoid на самом деле состоит из двух систем-близнецов, одна для отношений в Prop, а другая для отношений в Type (имена модулей имеют префикс C). Обычно вы используете только одно или другое, в зависимости от вида ваших отношений.

Я не уверен, что SSReflect меняет ситуацию, но вот пример использования переписывания setoid без него:

  1. Require Setoid. для активации плагина.
  2. Require Import CEquivalence., если вы используете Type отношения, или Require Import Equivalence., если вы используете Prop отношения.
  3. Реализация экземпляров для свойства отношений эквивалентности (любые из Reflexive, Symmetric, Transitive или Equivalence для всех 3).
  4. Вам также может потребоваться доказать Proper лемм, если термины, которые вы переписываете не находятся на верхнем уровне цели.

Обратите внимание, что на шаге 3, если вы не можете / не можете доказать все три свойства, вам не разрешат переписывать во всех направлениях.

Насколько мне известно, такие команды, как Add Parametric Relation, которые вы можете найти в документации, являются просто образцом, который предназначен для этих случаев. Но, по моему мнению, как пользователь, они добавляют ненужный слой косвенности; прямое объявление экземпляров делает вещи более понятными (особенно если вы уже знакомы с классами типов). 

Require Setoid. (* 1 *)
Require Import CMorphisms. (* 2 *)

Axiom obj : Type.
Axiom equiv : obj -> obj -> Type.
Axiom cat : forall a b c, equiv a b -> equiv b c -> equiv a c.

(* 3 *)
Instance Transitive_equiv : Transitive equiv.
Proof.
  exact cat.
Qed.

(* Example usage *)
Goal forall a b c,
    equiv a b -> equiv b c -> equiv a c.
Proof.
  intros a b c H1 H2.
  rewrite H1.
  (* or,
  rewrite H2
  *)
...