#coq #proof
Вопрос:
Есть ли способ передать переменную типа в качестве параметра модулю в Coq, чтобы мне не приходилось повторять переменную типа?
Вот что я имею в виду: я хочу доказать некоторые основные факты о теории множеств. Давайте начнем с одной части законов Деморгана. Используя Ensemble
стандартную библиотеку, я:
Require Import Ensembles.
Variable U : Type.
Lemma demorgan1: forall A B: Ensemble U,
Included U
(Intersection U (Complement U A) (Complement U B))
(Complement U (Union U A B)).
Это работает, но очень раздражает, когда все эти U
буквы повсюду.
Есть ли способ передать модуль в U
качестве параметра Ensembles
, чтобы все объекты, импортированные из него, автоматически U
передавались в качестве первого аргумента?
Ответ №1:
Ensembles
Библиотека сохранилась по историческим причинам, но в настоящее время она в значительной степени устарела. Как правило , проще работать непосредственно с предикатами U -> Prop
, что Ensemble U
в любом случае и происходит. Но, возвращаясь к вашему вопросу, вы можете добиться того, чего хотите, используя неявные аргументы:
Require Import Ensembles.
Variable U : Type.
Arguments Included {U} _ _.
Arguments Intersection {U} _ _.
Arguments Union {U} _ _.
Arguments Complement {U} _.
Lemma demorgan1: forall A B: Ensemble U,
Included
(Intersection (Complement A) (Complement B))
(Complement (Union A B)).
Неявные аргументы-это аргументы, указанные в фигурных скобках в Arguments
объявлении или в заголовке определения. Coq пытается автоматически определить, с помощью каких неявных аргументов следует создавать экземпляры, основываясь на типах других аргументов. В этом случае он знает, что первым аргументом этих функций должно быть U
то, что A
, B
, и т. Д. имеют тип Ensemble U
.
В целом, не стоит переопределять, какие аргументы подразумеваются в чужом определении: этот выбор является частью интерфейса библиотеки, и его хорошо использовать по замыслу авторов. Хорошо продуманная, современная библиотека, как правило, будет снабжена разумным выбором неявных аргументов. Но в случае устаревших библиотек , таких как Ensembles
, переопределение их, вероятно, имеет смысл.
Комментарии:
1. Спасибо за ответ! Есть ли где-нибудь, куда я мог бы пойти, чтобы посмотреть пример кода, использующего более современный стиль просто обработки предикатов
U -> Prop
как наборов?2. @setholopolus Вы можете посмотреть, например, в библиотеке stdpp: gitlab.mpi-sws.org/iris/stdpp/-/blob/master/theories/propset.v .