Какова стандартная конструкция декартова произведения для ансамбля?

Я использую тип 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?

Стоит ли изучать PHP в 2023-2024 годах?
Стоит ли изучать PHP в 2023-2024 годах?
Привет всем, сегодня я хочу высказать свои соображения по поводу вопроса, который я уже много раз получал в своем сообществе: "Стоит ли изучать PHP в...
Поведение ключевого слова "this" в стрелочной функции в сравнении с нормальной функцией
Поведение ключевого слова "this" в стрелочной функции в сравнении с нормальной функцией
В JavaScript одним из самых запутанных понятий является поведение ключевого слова "this" в стрелочной и обычной функциях.
Приемы CSS-макетирования - floats и Flexbox
Приемы CSS-макетирования - floats и Flexbox
Здравствуйте, друзья-студенты! Готовы совершенствовать свои навыки веб-дизайна? Сегодня в нашем путешествии мы рассмотрим приемы CSS-верстки - в...
Тестирование функциональных ngrx-эффектов в Angular 16 с помощью Jest
В системе управления состояниями ngrx, совместимой с Angular 16, появились функциональные эффекты. Это здорово и делает код определенно легче для...
Концепция локализации и ее применение в приложениях React ⚡️
Концепция локализации и ее применение в приложениях React ⚡️
Локализация - это процесс адаптации приложения к различным языкам и культурным требованиям. Это позволяет пользователям получить опыт, соответствующий...
Пользовательский скаляр GraphQL
Пользовательский скаляр GraphQL
Листовые узлы системы типов GraphQL называются скалярами. Достигнув скалярного типа, невозможно спуститься дальше по иерархии типов. Скалярный тип...
2
0
232
1
Перейти к ответу Данный вопрос помечен как решенный

Ответы 1

Ответ принят как подходящий

Тип 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 — она не дает вам ничего, кроме работы с предикатами.

Спасибо за ваш ответ, это работает отлично! Ваш последний комментарий о том, что «обычно гораздо проще просто работать с предикатами», интригует. У вас есть ссылка на пример этого стиля?

Matthew Piziak 18.05.2019 20:06

@MatthewPiziak Например, предикат Forall для списков (в Coq.Lists.List) имеет тип forall A, (A -> Prop) -> list A -> Prop вместо того, чтобы использовать ансамбль в качестве аргумента. Более того, я думаю, что не совсем ясно выразился в своем ответе: дело не совсем в том, что работа с предикатами - это Полегче, просто ансамбли - это ненужный уровень косвенности.

Arthur Azevedo De Amorim 21.05.2019 16:33

Другие вопросы по теме