Какова стандартная декартова конструкция продукта для Ensemble? - PullRequest
Новая
       8

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

2 голосов
/ 18 мая 2019

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

1 Ответ

3 голосов
/ 18 мая 2019

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

...