Я пытаюсь смоделировать некоторые конкретные наборы (Ensembles) элементов, которые
сами являются ансамблями.
Все "внутренние" ансамбли являются декартовыми произведениями двух наборов, взятых
из некоторых других наборов наборов (W1 и W2), и я хочу показать, что если
(a, b) и (c, d) находятся в декартовом произведении, затем (a, d) и (c, b)
Также в продукте.
Я использую Coq's Ensembles, который выражает наборы как предикаты, но в
В моем случае также можно предположить, что множества равны, если они содержат
одни и те же элементы, и что термины либо в или не в наборах
(что не относится ко всем таким множествам в конструктивной логике ...)
У меня проблемы с завершением доказательства, так как, похоже, я теряю
информация, и был бы благодарен за любую помощь.
Сначала некоторые определения:
Require Import Ensembles.
Variables T1 T2:Type.
(* S1 and S2 are two "container" sets for the left and right elements,
but I'm not doing the cartesian product of S1 and S2 but of
some subsets of S1 and S2, (see W1 and W2 below)
*)
Variables (S1: Ensemble T1) (S2:Ensemble T2).
Notation "a ∈ A" := (In _ A a) (at level 50).
Notation "a === b" := (Same_set _ a b) (at level 50).
Hypothesis S1dec: forall x, x ∈ S1 \/ ~ x ∈ S1.
Hypothesis S2dec: forall y, y ∈ S2 \/ ~ y ∈ S2.
Variables (W1 : Ensemble (Ensemble T1)).
Variables (W2 : Ensemble (Ensemble T2)).
Hypothesis W1_closed: forall A B, A === B -> A ∈ W1 -> B ∈ W1.
Hypothesis W2_closed: forall A B, A === B -> A ∈ W2 -> B ∈ W2.
Hypothesis W1_in_S1: forall w, w ∈ W1 -> Included _ w S1.
Hypothesis W2_in_S2: forall w, w ∈ W2 -> Included _ w S2.
(* extract the elements on the left or right "side" of the product set *)
Definition projL (w:Ensemble (T1*T2)) := fun x => exists y, (x,y) ∈ w.
Definition projR (w:Ensemble (T1*T2)) := fun y => exists x, (x,y) ∈ w.
Декартовы произведения изготовлены из членов наборов W1 и W2.
(* The definition of the product set. The members are those
sets whose both left and right projection are in W1 and W2 *)
Definition prodW1W2 : Ensemble (Ensemble (T1*T2)) :=
fun (S:Ensemble (T1*T2)) =>
projL S ∈ W1 /\ projR S ∈ W2.
Может быть, полезно знать ...?
Lemma projL_closed: forall A B , A === B -> projL A === projL B.
Proof. firstorder. Qed.
Lemma projR_closed: forall A B , A === B -> projR A === projR B.
Proof. firstorder. Qed.
Вот теорема, которую я хотел бы доказать:
Theorem all_pairs_are_in_the_product:
forall WW, WW ∈ prodW1W2 ->
forall x y, (x, y) ∈ WW ->
forall z w, (z, w) ∈ WW ->
(x, w) ∈ WW.
Proof.
intros WW (H1 & H2 ) x y Hxy z w Hzw.
assert (WW === (fun x => let (a,b) := x in a ∈ projL WW /\ b ∈ projR WW)).
{
split; intros [a b] Hx.
- eexists; eauto; firstorder.
- destruct Hx; firstorder.
(* This is where I'm stuck *)
admit.
}
enough ((x, w) ∈ (fun x : T1 * T2 => let (a, b) := x in a ∈ projL WW /\ b ∈ projR WW))
as [Ha Hb] by firstorder.
firstorder.
Admitted.
Как типы и набор предназначены для совместного использования:
