Я использую тип Ensemble
для наборов в Coq.Sets.Ensemble
. Эта библиотека определяет Union
и Intersection
, но я не могу найти никакой конструкции для декартова произведения.
Чтобы быть конкретным, я ищу конструктор, который принимает Ensemble U
и Ensemble V
и возвращает Ensemble (U * V)
, который содержит набор всех упорядоченных пар (u, v)
, где u ∈ U
и v ∈ V
.
Что-то явно названное Cartesian
было бы здорово. Или, может быть, есть способ внедрить ту же идею, используя обычные типы продуктов?
Я попытался построить лемму следующим образом:
Lemma cartesian_inclusion : forall A B C D : Ensemble U,
Included U A C /\ Included U B D -> Included (U * U) (A, B) (C, D).
Но я получаю следующую ошибку:
The term "(A, B)" has type "(Ensemble U * Ensemble U)%type" while it is expected to have type "Ensemble (U * U)".
Эта ошибка имеет смысл. (A, B)
дает вам продукт из наборов, тогда как я хочу набор продуктов. Как я могу выразить это в Coq?
Тип Ensemble U
определяется просто как U -> Prop
. Мы можем легко определить декартово произведение для ансамблей следующим образом:
Require Import Coq.Sets.Ensembles.
Definition Cartesian (U V : Type) (A : Ensemble U) (B : Ensemble V)
: Ensemble (U * V) :=
fun x => In _ A (fst x) /\ In _ B (snd x).
Вот доказательство сформулированной вами леммы:
Lemma cartesian_inclusion U V A B C D :
Included U A C /\ Included V B D ->
Included (U * V) (Cartesian _ _ A B) (Cartesian _ _ C D).
Proof.
intros [HU HV] [x y] [HA HB].
split.
- now apply HU.
- now apply HV.
Qed.
Кстати, библиотека ансамбля редко используется в современных разработках Coq — она не дает вам ничего, кроме работы с предикатами.
@MatthewPiziak Например, предикат Forall
для списков (в Coq.Lists.List
) имеет тип forall A, (A -> Prop) -> list A -> Prop
вместо того, чтобы использовать ансамбль в качестве аргумента. Более того, я думаю, что не совсем ясно выразился в своем ответе: дело не совсем в том, что работа с предикатами - это Полегче, просто ансамбли - это ненужный уровень косвенности.
Спасибо за ваш ответ, это работает отлично! Ваш последний комментарий о том, что «обычно гораздо проще просто работать с предикатами», интригует. У вас есть ссылка на пример этого стиля?