Блог

Есть ли способ передать переменную типа в качестве параметра модулю в 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 передавались в качестве первого аргумента?

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 , переопределение их, вероятно, имеет смысл.