Как установить неявные параметры для конструктора - PullRequest
Новая
       22

Как установить неявные параметры для конструктора

1 голос
/ 02 июля 2019

Играя с упражнениями ностаттера, я обнаружил еще одно странное поведение.Вот код: 

Inductive nostutter {X:Type} : list X -> Prop :=
| ns_nil : nostutter []
| ns_one : forall (x : X), nostutter [x]
| ns_cons: forall (x : X) (h : X) (t : list X), nostutter (h::t) -> x <> h -> nostutter (x::h::t).

Example test_nostutter_manual: not (nostutter [3;1;1;4]).
Proof.
  intro.
  inversion_clear H.
  inversion_clear H0.
  unfold not in H2.
  (* We are here *)
  specialize (H2 eq_refl).
  apply H2.
Qed.

Состояние после развёртывания выглядит следующим образом: 

1 subgoal (ID 229)

H1 : 3 <> 1
H : nostutter [1; 4]
H2 : 1 = 1 -> False
============================
False

Когда я запускаю specialize (H2 eq_refl). внутри IndProp.v, который загружает другие файлы логических оснований, он работает.Каким-то образом он понимает, что ему нужно поставить «1» в качестве параметра.Заголовок IndProp.v такой: 

Set Warnings "-notation-overridden,-parsing".
From LF Require Export Logic.
Require Import String.
Require Coq.omega.Omega.

Когда я перемещаю код в другой файл "nostutter.v", этот же код выдает ожидаемую ошибку:

Термин«eq_refl» имеет тип «RelationClasses.Reflexive Logic.eq», в то время как ожидается, что он будет иметь тип «1 = 1».

Заголовок nostutter.v: 

Set Warnings "-notation-overridden,-parsing".
Require Import List.
Import ListNotations.
Require Import PeanoNat.
Import Nat.
Local Open Scope nat_scope.

Я должен явно добавить параметр в eq_refl: specialize (H2 (eq_refl 1)).

Я думаю, что он не имеет отношения к специализации.Что это?Как исправить?

1 Ответ

3 голосов
/ 02 июля 2019

Проблема импортируется PeanoNat.Nat.

При импорте PeanoNat тип модуля Nat входит в область действия, поэтому при импорте Nat вводится PeanoNat.Nat. Если вы намеревались импортировать Coq.Init.Nat, вам придется либо импортировать его перед импортом PeanoNat, либо импортировать его с Import Init.Nat..

Почему импорт PeanoNat.Nat вызывает проблемы в этом случае?

Arith / PeanoNat.v ( статическая ссылка ) содержит модуль 1 Nat. Внутри этого модуля мы находим 2 необычно выглядящую линию 

Include NBasicProp <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.

Все это означает , что каждый из NBasicProp, UsualMinMaxLogicalProperties и UsualMinMaxDecProperties включен, что, в свою очередь, означает, что все, что определено в этих модулях, включено в текущий модуль. Разделив эту строку на три Include команды, мы можем выяснить, какая из них переопределяет eq_refl. Оказывается, NBasicProp, который находится в этом файле ( статическая ссылка ). Мы еще не совсем там: переопределения eq_refl здесь нет. Однако мы видим определение NBasicProp в терминах NMaxMinProp.

Это приводит нас к NMaxMin.v, который, в свою очередь, приводит нас к NSub.v, который ведет нас к NMulOrder.v, который ведет нас к NAddOrder.v, который ведет нас к NOrder.v, который ведет нас к NAdd .v, что приводит нас к NBase.v, ...

Я перейду к погоне здесь. В конечном итоге мы получаем Structures / Equality.v ( статическая ссылка ) с модулем BackportEq, который в итоге дает нам наше переопределение eq_refl. 

Module BackportEq (E:Eq)(F:IsEq E) <: IsEqOrig E.
 Definition eq_refl := @Equivalence_Reflexive _ _ F.eq_equiv.
 Definition eq_sym := @Equivalence_Symmetric _ _ F.eq_equiv.
 Definition eq_trans := @Equivalence_Transitive _ _ F.eq_equiv.
End BackportEq.

Как это определено, eq_refl (без каких-либо аргументов) имеет тип Reflexive eq, где Reflexive - класс 

Class Reflexive (R : relation A) :=
  reflexivity : forall x : A, R x x.

(находится в Classes / RelationClasses.v)

Это означает, что нам всегда нужно будет указывать дополнительный аргумент, чтобы получить что-то типа x = x. Здесь не определены неявные аргументы.

Почему импорт таких модулей, как PeanoNat.Nat, вообще плохая идея?

Если погоня за диким гусем, описанная выше, была недостаточно убедительной, позвольте мне сказать, что такие модули, как этот, которые расширяют и импортируют другие модули и типы модулей, часто не предназначены для импорта. Они часто имеют короткие имена (например, N, Z или Nat), поэтому любая теорема, которую вы хотите использовать, легко доступна без необходимости вводить длинное имя. Они обычно имеют длинную цепочку импорта и, таким образом, содержат огромное количество товаров. Если вы импортируете их, теперь огромное количество элементов загрязняет ваше глобальное пространство имен. Как вы видели с eq_refl, это может вызвать неожиданное поведение с тем, что вы считаете знакомой константой.

  1. Большинство модулей, встречающихся в этом приключении, имеют разновидность «тип модуля / функтор». Достаточно сказать, что их трудно понять полностью, но краткое руководство можно найти здесь .

  2. Моя работа была завершена открытием файлов в CoqIDE и выполнением команды Locate eq_refl. (или еще лучше, ctrl + shift + L) после всего, что может импортироваться из другого места. Locate также может сказать вам, откуда была импортирована константа. Хотелось бы, чтобы был более простой способ увидеть путь импорта в типах модулей, но я так не думаю. Вы можете догадаться, что мы окажемся в Coq.Classes.RelationClasses в зависимости от типа перезаписанного eq_refl, но это не так точно.

...