Library sset1
Fundamental set theory
Original file by Carlos Simpson (CNRS/UNSA)
Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Module Axioms.
Some definitions
Definition fterm:= Set -> Set.
Definition fterm2:= Set -> Set -> Set.
Definition property := Set -> Prop.
Definition relation := Set -> Set -> Prop.
Definition reflexive_r (R: relation) := forall x, R x x.
Definition symmetric_r (R: relation) := forall x y, R x y -> R y x.
Definition transitive_r (R: relation) := forall y x z, R x y -> R y z -> R x z.
Definition antisymmetric_r (R: relation) := forall x y, R x y -> R y x -> x = y.
Definition singl_val (p: property):=
forall x y, p x -> p y -> x = y.
Definition singl_val2 (p q: property):=
forall x y, p x -> q x -> p y -> q y -> x = y.
Definition singl_val_fp (p: property) (f: fterm) :=
forall x y, p x -> p y -> f x = f y.
Definition exactly_one (P Q: Prop) := (P \/ Q) /\ ~(P /\ Q).
This destructures a conjunction
Lemma proj31 A B C: [/\ A, B & C] -> A.
Proof. by destruct 1. Qed.
Lemma proj32 A B C: [/\ A, B & C] -> B.
Proof. by destruct 1. Qed.
Lemma proj33 A B C: [/\ A, B & C] -> C.
Proof. by destruct 1. Qed.
Lemma proj31_1 a b c d : [/\ a, b & c] /\ d -> a.
Proof. move => h; exact (proj31 (proj1 h)). Qed.
Lemma proj32_1 a b c d : [/\ a, b & c] /\ d -> b.
Proof. move => h; exact (proj32 (proj1 h)). Qed.
Lemma iff_sym (P Q: Prop): (P <-> Q) -> (Q <-> P).
Proof. exact: Logic.iff_sym. Qed.
Lemma iff_trans (P Q R: Prop): (P <-> Q) -> (Q <-> R) -> (P <-> R).
Proof. exact: Logic.iff_trans. Qed.
Lemma iff_neg (P Q: Prop): (P <-> Q) -> ( ~ P <-> ~ Q).
Proof. by move => h; split => np q; case: np; apply/h. Qed.
Realisation: if x is a set, Ro maps an object of type x to a set
Injectivity of Ro
Defines inc as "is element of" and sub as "is subset of"
Definition inc (x y : Set) := exists a : y, Ro a = x.
Definition sub (a b : Set) := forall x : Set, inc x a -> inc x b.
Definition ssub (a b : Set) := (sub a b) /\ (a <> b).
Extensionality for sets
nonempty: the set has an element.
Axiom of choice: let t be a nonempty type, p a predicate on t.
If p is true for some object it is for (chooseT p ne).
Section Choose.
Variable (t : Type).
Implicit Type (p : t -> Prop) (q:inhabited t).
Parameter chooseT : forall p q, t.
Axiom chooseT_pr : forall p q, ex p -> p (chooseT p q).
End Choose.
Image: if f:x -> Set is an abstraction, then IM f is a set,
it contains y if and only if y is (f z) for some z:x.
Parameter IM : forall (x : Set) (f : x -> Set), Set.
Axiom IM_P : forall (x : Set) (f : x -> Set) (y : Set),
inc y (IM f) <-> exists a : x, f a = y.
Excluded middle and consequences.
Axiom p_or_not_p: forall P:Prop, P \/ ~ P.
Ltac ex_middle u := match goal with
| |- ?p => case: (p_or_not_p p) ; [ done | move => u ]
end.
Lemma excluded_middle (p:Prop): ~ ~ p -> p.
Proof. move => nnp; ex_middle np; case: (nnp np). Qed.
Lemma equal_or_not (x y: Set) : x = y \/ x <> y.
Proof. apply: p_or_not_p. Qed.
Lemma inc_or_not (x y:Set): inc x y \/ ~ (inc x y).
Proof. apply: p_or_not_p. Qed.
Ltac dneg u := match goal with
H : ~ _ |- ~ _ => move => u; apply:H
end.
Ltac in_TP4:= solve [by constructor 1 | by constructor 2 |
by constructor 3 | by constructor 4].
End Axioms.
Export Axioms.
Tatics like aw use autorewite and trivial;
tactics like fprops use auto
Ltac aw := autorewrite with aw; trivial.
Ltac bw := autorewrite with bw; trivial.
Ltac fprops := auto with fprops.
Ltac set_extens v:= apply: extensionality=> v.
Ltac ue :=
match goal with
| H:?a = ?b |- _ => solve [ rewrite H ; fprops | rewrite - H ; fprops]
end.
End Tactics1.
Export Tactics1.
Ltac bw := autorewrite with bw; trivial.
Ltac fprops := auto with fprops.
Ltac set_extens v:= apply: extensionality=> v.
Ltac ue :=
match goal with
| H:?a = ?b |- _ => solve [ rewrite H ; fprops | rewrite - H ; fprops]
end.
End Tactics1.
Export Tactics1.
Module Constructions.
Lemma sub_trans: transitive_r sub.
Proof. by move => y x z sab sbc t xa; apply: sbc; apply: sab. Qed.
Lemma sub_refl: reflexive_r sub.
Proof. by move => x y. Qed.
Lemma ssub_trans1 b a c: ssub a b -> sub b c -> ssub a c.
Proof.
move => [sab nab] sbc; split; first by apply: (sub_trans sab).
move => nac; apply: nab; move: sab sbc; rewrite nac; apply: extensionality.
Qed.
Lemma ssub_trans2 b a c: sub a b -> ssub b c -> ssub a c.
Proof.
move => sab [sbc nbc]; split; first by apply: (sub_trans sab).
move => nac; case: nbc; move: sbc sab; rewrite nac; apply: extensionality.
Qed.
emptyset is a type without constructor; empty is classical.
Basic property of Ro.
Equivalence between nonempty and ~ empty.
Lemma in_set0 x: ~ inc x emptyset.
Proof. move=> [[]]. Qed.
Lemma set0_P x: empty x <-> x = emptyset.
Proof.
split; last by move => -> y; exact: in_set0.
by move => Iyx; set_extens t => Ht; [ case: (Iyx t) | case: (in_set0 Ht) ].
Qed.
Lemma emptyset_dichot x: x = emptyset \/ nonempty x.
Proof.
case: (p_or_not_p (nonempty x)) => // h; first by right.
by left; apply /set0_P => t tx; case: h; exists t.
Qed.
Lemma nonemptyP x: nonempty x <-> (x <> emptyset).
Proof.
split => xne; last by case: (emptyset_dichot x) => // ->.
move => xe; case: xne; rewrite xe => y;case; case.
Qed.
Lemma sub0_set x : sub emptyset x.
Proof. by move=> t /in_set0. Qed.
Hint Resolve sub0_set sub_refl : fprops.
Lemma sub_set0 x: sub x emptyset <-> (x = emptyset).
Proof.
split;move => h; [ by apply/set0_P => t tx; case: (h _ tx); case |ue].
Qed.
Axiom of choice applied to (inc x y), and the property (P a)
that says realisation of a is x: This gives a partial inverse of Ro.
Definition Bo (x y : Set) (hyp : inc x y) :=
chooseT (fun a : y => Ro a = x)
(match hyp with | ex_intro w _ => inhabits w end).
Lemma B_eq x y (hyp : inc x y): Ro (Bo hyp) = x.
Proof. rewrite /Bo /inc; apply: chooseT_pr hyp. Qed.
Lemma B_back (x:Set) (y:x) (hyp : inc (Ro y) x): Bo hyp = y.
Proof. by apply: R_inj; apply: B_eq. Qed.
Genereralised axiom of choice. choose p is satisfied by p
if somebody satisfies p
Definition choose (p: property) := chooseT p (inhabits emptyset).
Lemma choose_pr p: ex p -> p (choose p).
Proof. by apply: chooseT_pr. Qed.
Axiom of choice applied to inc. If x not empty, rep x is in x.
Definition rep (x : Set) := choose (fun y : Set => inc y x).
Lemma rep_i x: nonempty x -> inc (rep x) x.
Proof. by move => [y yinx]; apply: (choose_pr (p:= inc ^~ x)); exists y. Qed.
Given a function f, Zorec remembers a and f a
CoInductive Zorec (x : Set) (f : x -> Prop) : Set :=
Zorec_c :forall (a: x), f a -> Zorec f.
Definition Zo (x:Set) (p:property) :=
IM (fun (z : Zorec (fun (a : x) => p (Ro a))) => let (a, _) := z in Ro a).
Lemma Zo_i x (p:property) y: inc y x -> p y -> inc y (Zo x p).
Proof.
rewrite /Zo; move => [a Roa]; rewrite -{1} Roa => py.
by apply/ IM_P; exists (Zorec_c (f:= (fun a : x => p (Ro a))) py).
Qed.
Lemma Zo_hi x (p: property) y: inc y (Zo x p) -> p y.
Proof. by case /IM_P => v <-; case:v. Qed.
Lemma Zo_S x (p: property): sub (Zo x p) x.
Proof. move=> y /IM_P [v <-];case:v => z _; apply: R_inc. Qed.
Lemma Zo_P x (p: property) y: inc y (Zo x p) <-> (inc y x /\ p y).
Proof.
split; last by move=> [u v]; apply: Zo_i.
move=> H; split; [ apply: (Zo_S H) | apply: (Zo_hi H) ].
Qed.
Lemma Zo_exten1 (X : Set) (p q: property):
(forall x, inc x X-> (p x <-> q x)) -> Zo X p = Zo X q.
Proof.
by move => h; set_extens t => /Zo_P [pa pb]; apply :Zo_i => //; apply /h.
Qed.
Lemma Zo_exten2 (X Y: Set) (p q: property):
(forall x, (inc x X /\ p x <-> inc x Y /\ q x)) -> Zo X p = Zo Y q.
Proof.
by move => h; set_extens t => /Zo_P pa; apply/Zo_P /h.
Qed.
End Constructions.
Export Constructions.
Module Little.
Definition doubleton (x y : Set) :=
IM (fun z => if z then x else y).
Lemma set2_1 x y: inc x (doubleton x y).
Proof. by apply /IM_P; exists true. Qed.
Lemma set2_2 x y : inc y (doubleton x y).
Proof. by apply /IM_P; exists false. Qed.
Lemma set2_hi z x y: inc z (doubleton x y) -> z = x \/ z = y.
Proof. by move=> izd; case /IM_P: izd; case; [left | right]. Qed.
Hint Resolve set2_1 set2_2: fprops.
Lemma set2_P z x y : inc z (doubleton x y) <-> (z = x \/ z = y).
Proof. split; [apply: set2_hi | by case => ->; fprops]. Qed.
Lemma doubleton_inj x y z w:
doubleton x y = doubleton z w -> (x = z /\ y = w) \/ (x = w /\ y = z).
Proof.
move=> eql.
have x_zw: inc x (doubleton z w) by rewrite -eql; fprops.
have y_zw: inc y (doubleton z w) by rewrite -eql; fprops.
case: (set2_hi x_zw) => xs.
left; split; first by [].
have w_xy: inc w (doubleton x y) by rewrite eql; fprops.
case: (set2_hi w_xy); last by [].
by case: (set2_hi y_zw) ; move: xs => -> ->.
case: (set2_hi y_zw); first by right.
have z_xy: inc z (doubleton x y) by rewrite eql; fprops.
by case: (set2_hi z_xy); move => -> ->; left.
Qed.
Lemma set2_ne x y: nonempty (doubleton x y).
Proof. by exists x; fprops. Qed.
Lemma sub_set2 x y z: inc x z -> inc y z -> sub (doubleton x y) z.
Proof. by move=> xz yz t /set2_P [] ->. Qed.
Lemma set2_C : commutative doubleton.
Proof.
move => a b; apply: extensionality; apply: sub_set2; apply/set2_P; fprops.
Qed.
Lemma set2_pr a b X:
inc a X -> inc b X ->
(forall z : Set, inc z X -> z = a \/ z = b)
-> X = doubleton a b.
Proof.
move => ax bx h; set_extens t; last by case /set2_P => ->.
by move => ta; apply /set2_P; apply: h.
Qed.
Definition doubleton (x y : Set) :=
IM (fun z => if z then x else y).
Lemma set2_1 x y: inc x (doubleton x y).
Proof. by apply /IM_P; exists true. Qed.
Lemma set2_2 x y : inc y (doubleton x y).
Proof. by apply /IM_P; exists false. Qed.
Lemma set2_hi z x y: inc z (doubleton x y) -> z = x \/ z = y.
Proof. by move=> izd; case /IM_P: izd; case; [left | right]. Qed.
Hint Resolve set2_1 set2_2: fprops.
Lemma set2_P z x y : inc z (doubleton x y) <-> (z = x \/ z = y).
Proof. split; [apply: set2_hi | by case => ->; fprops]. Qed.
Lemma doubleton_inj x y z w:
doubleton x y = doubleton z w -> (x = z /\ y = w) \/ (x = w /\ y = z).
Proof.
move=> eql.
have x_zw: inc x (doubleton z w) by rewrite -eql; fprops.
have y_zw: inc y (doubleton z w) by rewrite -eql; fprops.
case: (set2_hi x_zw) => xs.
left; split; first by [].
have w_xy: inc w (doubleton x y) by rewrite eql; fprops.
case: (set2_hi w_xy); last by [].
by case: (set2_hi y_zw) ; move: xs => -> ->.
case: (set2_hi y_zw); first by right.
have z_xy: inc z (doubleton x y) by rewrite eql; fprops.
by case: (set2_hi z_xy); move => -> ->; left.
Qed.
Lemma set2_ne x y: nonempty (doubleton x y).
Proof. by exists x; fprops. Qed.
Lemma sub_set2 x y z: inc x z -> inc y z -> sub (doubleton x y) z.
Proof. by move=> xz yz t /set2_P [] ->. Qed.
Lemma set2_C : commutative doubleton.
Proof.
move => a b; apply: extensionality; apply: sub_set2; apply/set2_P; fprops.
Qed.
Lemma set2_pr a b X:
inc a X -> inc b X ->
(forall z : Set, inc z X -> z = a \/ z = b)
-> X = doubleton a b.
Proof.
move => ax bx h; set_extens t; last by case /set2_P => ->.
by move => ta; apply /set2_P; apply: h.
Qed.
singleton x is a set with one element
Definition singleton x := doubleton x x.
Lemma set1_eq x y: inc y (singleton x) -> y = x.
Proof. by case/set2_P. Qed.
Lemma set1_1 x: inc x (singleton x).
Proof. by apply/set2_P;left. Qed.
Hint Resolve set1_1: fprops.
Lemma set1_P y x: inc y (singleton x) <-> (y = x).
Proof. by split; [ apply:set1_eq| move => ->; fprops ]. Qed.
Lemma set1_inj: injective singleton.
Proof. by move => x y eq; apply: set1_eq; rewrite -eq; fprops. Qed.
Lemma set1_ne x: nonempty (singleton x).
Proof. by apply: set2_ne. Qed.
Lemma set1_sub x X: inc x X -> sub (singleton x) X.
Proof. by move=> ixy; apply: sub_set2. Qed.
Hint Resolve set1_ne: fprops.
Definition C0 := emptyset.
Definition C1 := singleton C0.
Definition C2 := doubleton C0 C1.
Lemma C1_p1 x: inc x C1 <-> x = C0.
Proof. exact: set1_P. Qed.
Lemma TP_ne1: C1 <> C0.
Proof. by apply /nonemptyP; exists C0; apply: set1_1. Qed.
Lemma TP_ne: C0 <> C1.
Proof. apply: nesym; apply: TP_ne1. Qed.
Lemma C2_P x: inc x C2 <-> (x = C0 \/ x = C1).
Proof. by apply: set2_P. Qed.
Lemma inc_C0_2: inc C0 C2.
Proof. by apply: set2_1. Qed.
Lemma inc_C1_2: inc C1 C2.
Proof. by apply: set2_2. Qed.
Hint Resolve TP_ne TP_ne1: fprops.
Hint Resolve inc_C0_2 inc_C1_2: fprops.
Definition alls (X: Set)(P: property) := forall a, inc a X -> P a.
A set is small if it has zero or one elements singletonp x says x has the form singleton y
Definition small_set x := singl_val (inc ^~x).
Definition singletonp x := exists u, x = singleton u.
Definition doubletonp x:= exists a b, a <> b /\ x = doubleton a b.
Lemma small0: small_set emptyset.
Proof. by move=> u v /= /in_set0. Qed.
Lemma small1 x: small_set (singleton x).
Proof. by move=> u v /set1_P -> /set1_P ->. Qed.
Lemma set1_pr x X: inc x X -> (forall z, inc z X -> z = x) ->
X = singleton x.
Proof.
move=> xX zy; set_extens t; first by move => ty;apply/set1_P;apply: zy.
by move /set1_P ->.
Qed.
Lemma set1_pr1 x X: nonempty X -> (forall z, inc z X -> z = x) ->
X = singleton x.
Proof.
by move=> [y yx] p; apply: set1_pr => //; rewrite - (p _ yx).
Qed.
Lemma singletonP x: singletonp x <-> (nonempty x /\ small_set x).
Proof.
split; first by move=> [z ->]; split;[fprops | apply: small1].
by move=> [[y yx] h]; exists y; apply: (set1_pr yx); move => z zx; apply: h.
Qed.
Lemma small_set_pr x: small_set x -> x = emptyset \/ singletonp x.
Proof.
move=> sx; case: (emptyset_dichot x); first by left.
by move=> ne; right; apply/singletonP.
Qed.
Lemma subset1P A x : sub A (singleton x) <-> (A = emptyset \/ A = singleton x).
Proof.
split; last by case => ->; fprops.
move => asx; case: (emptyset_dichot A); first by left.
by move => nea; right; apply: set1_pr1 => // z /asx /set1_P.
Qed.
Lemma sub1setP A x : sub (singleton x) A <-> inc x A.
Proof. by split; [ apply; fprops | move => xA t /set1_P ->]. Qed.
End Little.
Export Little.
Definition singletonp x := exists u, x = singleton u.
Definition doubletonp x:= exists a b, a <> b /\ x = doubleton a b.
Lemma small0: small_set emptyset.
Proof. by move=> u v /= /in_set0. Qed.
Lemma small1 x: small_set (singleton x).
Proof. by move=> u v /set1_P -> /set1_P ->. Qed.
Lemma set1_pr x X: inc x X -> (forall z, inc z X -> z = x) ->
X = singleton x.
Proof.
move=> xX zy; set_extens t; first by move => ty;apply/set1_P;apply: zy.
by move /set1_P ->.
Qed.
Lemma set1_pr1 x X: nonempty X -> (forall z, inc z X -> z = x) ->
X = singleton x.
Proof.
by move=> [y yx] p; apply: set1_pr => //; rewrite - (p _ yx).
Qed.
Lemma singletonP x: singletonp x <-> (nonempty x /\ small_set x).
Proof.
split; first by move=> [z ->]; split;[fprops | apply: small1].
by move=> [[y yx] h]; exists y; apply: (set1_pr yx); move => z zx; apply: h.
Qed.
Lemma small_set_pr x: small_set x -> x = emptyset \/ singletonp x.
Proof.
move=> sx; case: (emptyset_dichot x); first by left.
by move=> ne; right; apply/singletonP.
Qed.
Lemma subset1P A x : sub A (singleton x) <-> (A = emptyset \/ A = singleton x).
Proof.
split; last by case => ->; fprops.
move => asx; case: (emptyset_dichot A); first by left.
by move => nea; right; apply: set1_pr1 => // z /asx /set1_P.
Qed.
Lemma sub1setP A x : sub (singleton x) A <-> inc x A.
Proof. by split; [ apply; fprops | move => xA t /set1_P ->]. Qed.
End Little.
Export Little.
Image of a set by a function
Definition fun_image (x : Set) (f : fterm) := IM (fun a : x => f (Ro a)).
Lemma funI_i x f a: inc a x -> inc (f a) (fun_image x f).
Proof. by move => ax; apply/IM_P; exists (Bo ax); rewrite (B_eq ax). Qed.
Lemma funI_P f x y:
inc y (fun_image x f) <-> exists2 z, inc z x & y = f z.
Proof.
split; last by move=> [a ax ->]; apply:funI_i.
case/IM_P => a <-; exists (Ro a) => //; apply: R_inc.
Qed.
End Image.
Export Image.
Set of all elements in a not in b
Definition complement (A B : Set) := Zo A (fun x : Set => ~ inc x B).
Notation "a -s b" := (complement a b) (at level 50).
Lemma setC_P A B x: inc x (A -s B) <-> (inc x A /\ ~ inc x B).
Proof. by exact: Zo_P. Qed.
Lemma setC_i x A B: inc x A -> ~ inc x B -> inc x (A -s B).
Proof. by move => xa xb; apply /setC_P. Qed.
Hint Resolve setC_i: fprops.
Lemma nin_setC x A B: inc x A -> ~ inc x (A -s B) -> inc x B.
Proof. move=> xa nx_cab; ex_middle h; case: nx_cab; fprops. Qed.
Lemma empty_setC A B: A -s B = emptyset -> sub A B.
Proof.
move=> eql t ta; apply:(nin_setC ta); rewrite eql; apply: in_set0.
Qed.
Lemma setC_T A B: sub A B -> A -s B = emptyset.
Proof.
by move => sab; apply /set0_P => x /setC_P [xa] []; apply: sab.
Qed.
Lemma sub_setC A B: sub (A -s B) A.
Proof. by move => t;case /setC_P. Qed.
Lemma setC_ne A B: ssub A B -> nonempty (B -s A).
Proof.
move=> [s neq]; apply /nonemptyP;dneg ceq; move: (empty_setC ceq).
by apply: extensionality.
Qed.
Lemma setC_K A B: sub A B -> B -s (B -s A) = A.
Proof.
move=> sax; set_extens t.
by move /setC_P => [tx /setC_P notp];ex_middle h; case: notp.
move =>ta; apply/setC_P; split; [apply: (sax _ ta) | by apply/setC_P; case ].
Qed.
Lemma setC_v A: A -s A = emptyset.
Proof. by apply /set0_P => y /setC_P []. Qed.
Lemma setC_0 A: A -s emptyset = A.
Proof.
apply: extensionality; first by apply:sub_setC.
move => y yx; apply/setC_P; split => //;apply /in_set0.
Qed.
Lemma set_SC A B C : sub A B -> sub (A -s C) (B -s C).
Proof.
by move => sab x; case/setC_P =>xa xnc; apply /setC_P;split =>//; apply sab.
Qed.
Lemma set_CS A B C : sub A B -> sub (C -s B) (C -s A).
Proof.
move => sac t; case/setC_P => tc ntb; apply /setC_P.
by split => //;dneg ta; apply: sac.
Qed.
Lemma set_CSS A B C D : sub A C -> sub D B -> sub (A -s B)(C -s D).
Proof. move => sAC sDB; apply: (sub_trans (set_CS sDB) (set_SC sAC)). Qed.
Lemma set_CSm A B X:
sub A X -> sub B X -> (sub A B <-> sub (X -s B) (X -s A)).
Proof.
move=> ax bx; split; first by apply: set_CS.
by move => h; rewrite -(setC_K ax) -(setC_K bx); apply: set_CS.
Qed.
Lemma subsetC_P A B E : sub A E -> sub B E ->
( (sub A (E -s B)) <-> (sub B (E -s A))).
Proof.
move =>aE bE;split => i1 t ts;apply/setC_P; split.
- by apply bE.
- by move /i1 => /setC_P; case.
- by apply aE.
- by move /i1 => /setC_P; case.
Qed.
Lemma subCset_P A B E:sub A E -> sub B E ->
( (sub (E -s A) B) <-> (sub (E -s B) A)).
Proof.
move => ae be; rewrite -{2} (setC_K ae) -{1} (setC_K be).
apply: subsetC_P; apply: sub_setC.
Qed.
a -s1 b contains all elements of a but b
Notation "a -s1 b" := (a -s (singleton b)) (at level 50).
Lemma setC1_P x A b: inc x (A -s1 b) <-> (inc x A /\ x <> b).
Proof.
split; first by case /setC_P => xa /set1_P => xb.
by move => [xA xb]; apply /setC_P; split => //;apply /set1_P.
Qed.
Lemma setC1_1 x A: ~ (inc x (A -s1 x)).
Proof. by apply /setC_P=> [[_]] /set1_P []. Qed.
End Complement.
Export Complement.
Uaux: like Zo_rec, but f has a different type.
Section UnionDef.
Variable (I:Set)(f : I->Set).
CoInductive Uaux : Set := Uaux_c : forall a:I, f a -> Uaux.
Definition uniont :=
IM (fun a : Uaux => (let: Uaux_c u v := a in @Ro (f u) v)).
End UnionDef.
Lemma setUt_P (I:Set) (f:I->Set) x:
inc x (uniont f) <-> exists z, inc x (f z).
Proof.
split; first by move/IM_P=>[a] <-; case: a => b fb; exists b; apply: R_inc.
by move => [z xf]; apply /IM_P;exists (Uaux_c (Bo xf)); rewrite B_eq.
Qed.
Definition union X := uniont (@Ro X).
Lemma setU_P X x:
inc x (union X) <-> exists2 z, inc x z & inc z X.
Proof.
split; first by move/setUt_P => [z xr]; exists (Ro z); [ | apply: R_inc].
by move => [z wz zX]; apply/setUt_P; exists (Bo zX); rewrite (B_eq zX).
Qed.
Lemma setU_i x y a: inc x y -> inc y a -> inc x (union a).
Proof. by move => xy ya; apply/setU_P; exists y. Qed.
Lemma setU_hi x X: inc x (union X) -> exists2 y, inc x y & inc y X.
Proof. by case /setU_P => t pt; exists t. Qed.
Lemma setU_s1 x y: inc x y -> sub x (union y).
Proof. by move=> xy t tx ; apply: setU_i xy. Qed.
Lemma setU_s2 x z: (forall y, inc y z -> sub y x) -> sub (union z) x.
Proof. by move=> asub t /setU_P [a ta az]; apply: (asub _ az). Qed.
Lemma setU_0: union emptyset = emptyset.
Proof. by apply /set0_P => x /setU_P [y _ /in_set0]. Qed.
Union of two sets
Definition union2 (x y : Set) := union (doubleton x y).
Notation "a \cup b" := (union2 a b) (at level 50).
Lemma setU2_hi x y a: inc a (x \cup y) -> inc a x \/ inc a y.
Proof. by case /setU_P => t aat /set2_P [] <-; [left | right]. Qed.
Lemma setU2_1 x y a: inc a x -> inc a (x \cup y).
Proof. move => ax; apply (setU_i ax); fprops. Qed.
Lemma setU2_2 x y a: inc a y -> inc a (x \cup y).
Proof. move => ay;apply: (setU_i ay); fprops. Qed.
Hint Resolve setU2_1 setU2_2: fprops.
Lemma setU2_P a b x: inc x (a \cup b) <-> (inc x a \/ inc x b).
Proof. by split; [apply: setU2_hi | case ; fprops ]. Qed.
Lemma subsetU2l a b: sub a (a \cup b).
Proof. exact: setU2_1. Qed.
Lemma subsetU2r a b: sub b (a \cup b).
Proof. exact: setU2_2. Qed.
Lemma setU2_C: commutative union2.
Proof.
move => x y; set_extens t; case/setU2_P => ts; apply /setU2_P; fprops.
Qed.
Lemma setU2_id: idempotent union2.
Proof. move => x;set_extens t; [ by case /setU2_P | fprops]. Qed.
Lemma setU2_A: associative union2.
Proof.
move => a b c; rewrite setU2_C.
set_extens t; case /setU2_P; (try case /setU2_P); move => tx;
apply/setU2_P;fprops; left; apply/setU2_P;fprops.
Qed.
Lemma setU2_CA : left_commutative union2.
Proof. by move =>A B C; rewrite !setU2_A (setU2_C B). Qed.
Lemma setU2_AC : right_commutative union2.
Proof. by move => A B C;rewrite -!setU2_A (setU2_C B). Qed.
Lemma set2_UUl : left_distributive union2 union2.
Proof.
by move => A B C; rewrite setU2_A !(setU2_AC _ C) -(setU2_A _ C) setU2_id.
Qed.
Lemma set2_UUr : right_distributive union2 union2.
Proof. move => a b c; rewrite !(setU2_C a); exact: set2_UUl. Qed.
Lemma setU2_S1 A B C : sub A B -> sub (C \cup A) (C \cup B).
Proof. move=> sAB t; case /setU2_P => ts; apply/setU2_P; fprops. Qed.
Lemma setU2_S2 A B C : sub A B -> sub (A \cup C) (B \cup C).
Proof. by move=> sAB; rewrite -!(setU2_C C); exact: setU2_S1. Qed.
Lemma setU2_SS A B C D : sub A C -> sub B D -> sub (A \cup B) (C \cup D).
Proof.
move => s1 s2; apply: sub_trans (setU2_S1 (C:=C) s2); apply: (setU2_S2 s1).
Qed.
Lemma setU2_12S A B C: sub A C -> sub B C -> sub (A \cup B) C.
Proof. rewrite -{3}(setU2_id C); exact:setU2_SS. Qed.
Lemma subU2_setP A B C : (sub (B\cup C) A) <-> (sub B A /\ sub C A).
Proof.
split.
move => h;split; apply: (sub_trans _ h);[apply: subsetU2l |apply: subsetU2r].
by move => [h1 h2];apply: setU2_12S.
Qed.
Lemma sub_setU2 A B C : (sub A B) \/ (sub A C) -> sub A (B \cup C).
Proof.
case => h; apply: (sub_trans h);[apply: subsetU2l |apply: subsetU2r].
Qed.
Lemma setU2id_Pl A T: sub A T <-> A \cup T = T.
Proof.
split; last by move => <-;apply: subsetU2l.
move => sat; apply: extensionality; last by apply: subsetU2r.
by rewrite - {2}(setU2_id T); apply:setU2_S2.
Qed.
Lemma setU2id_Pr A T: sub A T <-> T \cup A = T.
Proof. rewrite setU2_C; exact: setU2id_Pl. Qed.
Lemma setU2_0 A : A \cup emptyset = A.
Proof. apply/setU2id_Pr; fprops. Qed.
Lemma set0_U2 A : emptyset \cup A = A.
Proof. rewrite setU2_C; exact: setU2_0. Qed.
Lemma setU_1 x: union (singleton x) = x.
Proof. apply: setU2_id. Qed.
Lemma setU2_11 x y: (singleton x) \cup (singleton y) = doubleton x y.
Proof. apply:set2_pr; fprops => z /setU2_P; case => /set1_P ->;fprops. Qed.
Lemma subCset_P2 A B C : (sub (A -s B) C) <-> (sub A (B \cup C)).
Proof.
split => h t.
move => ta; apply/setU2_P; case: (inc_or_not t B) => ax; [by left | right].
by apply:h; apply/setC_P; split.
by case /setC_P => ta tb; move: (h _ ta) => /setU2_P;case.
Qed.
Lemma setU2_eq0P A B : (A \cup B = emptyset) <-> (A = emptyset /\ B = emptyset).
Proof.
split; [move => sube | by move => [-> ->]; rewrite setU2_id ].
split; apply /set0_P => t ta; case: (in_set0 (x:= t));
rewrite - sube; apply /setU2_P;fprops.
Qed.
Lemma setU2Cr1 A B: A \cup (A -s B) = A.
Proof. apply /setU2id_Pr; apply: sub_setC. Qed.
Lemma setU2Cr2 A B: A \cup (B -s A) = A \cup B.
Proof.
set_extens t; case /setU2_P => t1; apply/setU2_P; fprops.
by right;case /setC_P:t1.
case: (inc_or_not t A)=> ta; fprops.
Qed.
Lemma setU2_Cr A T: sub A T -> A \cup (T -s A) = T.
Proof. by move => sat; rewrite setU2Cr2; apply /setU2id_Pl. Qed.
Union of x and a single element y
Notation "a +s1 b" := (a \cup (singleton b)) (at level 50).
Lemma setU1_hi x y z: inc z (x +s1 y) -> (inc z x \/ z = y).
Proof. case /setU2_P; fprops; move /set1_P;fprops. Qed.
Lemma setU1_P x y z: (inc z (x +s1 y) ) <-> (inc z x \/ z = y).
Proof.
split; first by case /setU2_P; [left | move /set1_P; right].
by case =>h; apply/setU2_P; [by left | right; apply/set1_P].
Qed.
Lemma setU1_1 a b: inc a (b +s1 a).
Proof. by apply/setU1_P; right. Qed.
Lemma sub_setU1 a b: sub b (b +s1 a).
Proof. by move=> t tb; apply/setU1_P; left. Qed.
Lemma setU1_r a b y: inc y b -> inc y (b +s1 a).
Proof. apply: sub_setU1. Qed.
Hint Resolve setU1_1 setU1_r sub_setU1: fprops.
Lemma setU1_eq x y: inc y x -> x +s1 y = x.
Proof.
move=> yx; apply: extensionality; last by fprops.
by move => t; case /setU1_P => // ->.
Qed.
Lemma setU1_sub x y z: sub x z -> inc y z -> sub (x +s1 y) z.
Proof. by move=> xz yz t; case/setU1_P ; [ apply: xz | move=> -> ]. Qed.
Lemma setCU_K x y: sub y x <-> (x -s y) \cup y = x.
Proof.
split; last by move => h t ty; rewrite -h; apply/setU2_P; right.
move => yx; set_extens t; first by case /setU2_P; [ by case/setC_P| apply: yx].
move => tx; apply/setU2_P; case: (inc_or_not t y) => ty;fprops.
Qed.
Lemma setU1_K a x: ~(inc a x) -> (x +s1 a) -s1 a = x.
Proof.
move => nax; set_extens t.
by case /setC1_P; case /setU1_P.
move => tw; apply/setC1_P; split; [fprops | dneg ta;ue ].
Qed.
Lemma setC1_K x y: inc y x -> (x -s1 y) +s1 y = x.
Proof. by move => h; apply/setCU_K => t /set1_P ->. Qed.
Lemma setU1_inj x A B: ~(inc x A) -> ~(inc x B) ->
A +s1 x = B +s1 x -> A = B.
Proof. by move => h1 h2 eq1; rewrite -(setU1_K h1) -(setU1_K h2) eq1. Qed.
Lemma setC1_inj x A B: inc x A -> inc x B -> A -s1 x = B -s1 x -> A = B.
Proof. by move => h1 h2 eq1; rewrite -(setC1_K h1) -(setC1_K h2) eq1. Qed.
Definition tripleton a b c := (doubleton a b) +s1 c.
Lemma set3_P a b c x:
inc x (tripleton a b c) <-> [\/ x = a , x = b | x = c].
Proof.
split; last by rewrite /tripleton;case => ->; fprops.
case /setU1_P; [case /set2_P | ]; in_TP4.
Qed.
Definition C3 := C2 +s1 C2.
Definition C4 := C3 +s1 C3.
Lemma C2_neC01: C2 <> C0 /\ C2 <> C1.
Proof.
split => h; first by move: inc_C0_2; rewrite h /C0; case; case.
move: inc_C1_2; rewrite h; move /set1_P; fprops.
Qed.
Lemma C3_P x: inc x C3 <-> [\/ x = C0, x = C1 | x = C2].
Proof.
split.
case /setU1_P; last (by constructor 3); by case /C2_P; in_TP4.
case => ->; apply /setU1_P; [left | left | right]; fprops.
Qed.
Lemma C3_neC012: [/\ C3 <> C0, C3 <> C1 & C3 <> C2].
Proof.
have pa: inc C0 C3 by apply/C3_P; constructor 1.
have pb: inc C1 C3 by apply/C3_P; constructor 2.
have pc: inc C2 C3 by apply/C3_P; constructor 3.
move:C2_neC01 => [pd pe].
split => h; first by move: pa ; rewrite h; case; case.
by move: pb ; rewrite h; move/set1_P; fprops.
move: pc; rewrite h; case/set2_P; fprops.
Qed.
Lemma C4_P x: inc x C4 <-> [\/ x = C0, x = C1, x = C2 | x = C3].
Proof.
split.
case /setU1_P; last (by constructor 4); by case /C3_P; in_TP4.
case => ->; apply/setU1_P; last (by right); left; apply /C3_P; in_TP4.
Qed.
Lemma funI_set0 f: fun_image emptyset f = emptyset.
Proof. by apply /set0_P => t /funI_P [z /in_set0]. Qed.
Lemma funI_setne f x: nonempty x -> nonempty (fun_image x f).
Proof. by move => [a ax]; exists (f a); apply:funI_i. Qed.
Lemma funI_setne1 f x: fun_image x f = emptyset -> x = emptyset.
Proof.
by move => dr;apply /set0_P => t /(funI_i f); rewrite dr; case; case.
Qed.
Lemma funI_set2 f a b: fun_image (doubleton a b) f = doubleton (f a) (f b).
Proof.
set_extens t; first by move/funI_P => [z] /set2_P;case => -> <-; fprops.
move /set2_P; case => ->; apply: funI_i; fprops.
Qed.
Lemma funI_set1 f x: fun_image (singleton x) f = singleton (f x).
Proof. apply:funI_set2. Qed.
Lemma funI_setU f X:
fun_image (union X) f = union (fun_image X (fun z => (fun_image z f))).
Proof.
set_extens t.
move /funI_P => [y yu -> ]; move/setU_P:yu=> [x yx xz].
apply/setU_P; exists (fun_image x f); by apply:funI_i.
move/setU_P => [x tx /funI_P [y yz dy]].
move:tx; rewrite dy; move/funI_P => [u ua ->]; apply: funI_i.
apply (setU_i ua yz).
Qed.
Lemma funI_setU2 f: {morph (fun_image ^~ f): x y / x \cup y}.
Proof. by move => x y;rewrite /union2 funI_setU funI_set2. Qed.
Lemma funI_setU1 g X a:
fun_image (X +s1 a) g = fun_image X g +s1 (g a).
Proof. by rewrite funI_setU2 funI_set1. Qed.
Lemma funI_S f a b: sub a b -> sub (fun_image a f) (fun_image b f).
Proof. by move => h t /funI_P [z za ->]; apply: funI_i; apply: h. Qed.
If a set E contains a unique x satisfying p, then select p E is this element
Definition select (p: property) (E: Set) := union (Zo E p).
Lemma select_uniq (p: property) E:
(singl_val2 (inc ^~ E) p) ->
forall x, inc x E -> p x -> x = (select p E).
Proof.
move => h x xE px; rewrite /select.
suff: (Zo E p) = singleton x by move => ->; rewrite setU_1.
by apply: set1_pr; [ apply: Zo_i | move => z; case/Zo_P => ze pz; apply: h].
Qed.
Lemma select_pr (p : property) E:
(exists2 x, inc x E & p x) ->
(singl_val2 (inc ^~ E) p) ->
(p (select p E) /\ inc (select p E) E).
Proof. by move => [z ze pz] pc; rewrite -(select_uniq pc ze pz). Qed.
Defines Yo P x y to be x if P is true and y otherwise
Definition Yo (P : Prop) (x y : Set) :=
select (fun z => (z = x /\ P) \/ (z = y /\ ~P)) (doubleton x y).
Lemma Y_true (P:Prop) (hyp :P) x y: Yo P x y = x.
Proof.
symmetry; apply: select_uniq.
- move => u v _ [] [-> pa] _ [] [-> pb] //.
- fprops.
- by left; split.
Qed.
Lemma Y_false (P:Prop) (hyp : ~P) x y: Yo P x y = y.
Proof.
symmetry; apply: select_uniq.
- move => u v _ [] [-> pa] _ [] [-> pb] //.
- fprops.
- by right ; split.
Qed.
Lemma Y_same (P: Prop) x : Yo P x x = x.
Proof.
case: (p_or_not_p P) => h; [apply: (Y_true h) | apply: (Y_false h) ].
Qed.
Ltac Ytac eq:=
match goal with
| |- context [Yo ?p _ _ ] =>
case: (p_or_not_p p) => eq;
[rewrite (Y_true eq) | rewrite (Y_false eq) ]
end.
Ltac Ytac0 := match goal with
| h: ?p |- context [Yo ?p _ _ ] => rewrite (Y_true h)
| h: (~ ?p) |- context [Yo ?p _ _ ] => rewrite (Y_false h)
| h: ?j <> ?i |- context [Yo (?i = ?j) _ _ ]
=> rewrite (Y_false (sym_not_equal h))
| |- context [Yo (?i = ?i) _ _ ] => rewrite (Y_true (refl_equal i))
| |- context [Yo (C0 = C1) _ _ ] => rewrite (Y_false TP_ne)
| |- context [Yo (C1 = C0) _ _ ] => rewrite (Y_false TP_ne1)
| |- context [Yo ?p ?x ?x ] => rewrite (Y_same p x)
end.
End Union.
Export Union.
Forall all p:X-> 2, we consider the inverse image of 0.
The set of all these quantities is the set of subsets of X
Definition powerset (x : Set) :=
IM (fun p : x -> C2 =>
Zo x (fun y : Set => forall hyp : inc y x, Ro (p (Bo hyp)) = C0)).
Lemma setP_i y x : sub y x -> inc y (powerset x).
Proof.
have fp: forall a:x, inc (Yo (inc (Ro a) y) C0 C1) C2.
by move => a; Ytac h; fprops.
move => sxy; apply/IM_P; exists (fun a => Bo (fp a)).
set_extens t.
move /Zo_P => [tz h]; move: (h tz); rewrite B_eq; Ytac w.
by move: w; rewrite B_eq.
by move: TP_ne1.
move => ty; apply /Zo_P; split; first by apply: sxy.
by move => hyp; rewrite B_eq B_eq; Ytac0.
Qed.
Lemma setP_hi x y: inc x (powerset y) -> sub x y.
Proof. by case /IM_P => t <-; apply: Zo_S. Qed.
Lemma setP_P x y : inc x (powerset y) <-> sub x y.
Proof. split ; [ apply: setP_hi | apply: setP_i]. Qed.
Lemma setP_Ti x: inc x (powerset x).
Proof. by apply/setP_P. Qed.
Lemma setP_0i x: inc emptyset (powerset x).
Proof. apply/setP_P; fprops. Qed.
Lemma setP_S a b: sub a b <-> sub (powerset a) (powerset b).
Proof.
split => sab.
move=> x /setP_P sxa; apply /setP_P; apply: (sub_trans sxa sab).
by apply /setP_P;apply: sab; apply /setP_P.
Qed.
Lemma setP_0: powerset emptyset = singleton emptyset.
Proof.
set_extens t; first by move /setP_P /sub_set0 ->; fprops.
move /set1_P ->; apply: setP_0i.
Qed.
Lemma setP_1 x: powerset (singleton x) = doubleton emptyset (singleton x).
Proof.
set_extens t.
by move /setP_P /subset1P => [] ->; apply/set2_P; [left | right].
case /set2_P => ->; fprops; apply /setP_P; fprops.
Qed.
Lemma setP_00 : powerset (powerset emptyset) = C2.
Proof. rewrite setP_0 setP_1 //. Qed.
End Powerset.
Export Powerset.
Intersection: set of all z in some element of x,
that are in all elements of x
Definition intersection (x : Set) :=
Zo (union x) (fun y : Set => forall z : Set, inc z x -> inc y z).
Lemma setI_0: intersection emptyset = emptyset.
Proof. apply /set0_P => t /Zo_S;rewrite setU_0; apply /in_set0. Qed.
Lemma setI_i x a:
nonempty x -> (forall y, inc y x -> inc a y) -> inc a (intersection x).
Proof.
move => [y yx] all_ayx; apply Zo_i=> //.
move: (all_ayx _ yx) (yx); apply: setU_i.
Qed.
Lemma setI_hi x a y: inc a (intersection x) -> inc y x -> inc a y.
Proof. move/Zo_hi; apply. Qed.
Lemma setI_s1 x y: inc y x -> sub (intersection x) y.
Proof. by move=> yx t ti; move: ti yx; apply: setI_hi. Qed.
Intersection of two sets
Definition intersection2 x y := intersection (doubleton x y).
Notation "a \cap b" := (intersection2 a b) (at level 50).
Lemma setI2_i x y a: inc a x -> inc a y -> inc a (x \cap y).
Proof.
move => ax ay.
by apply: setI_i; [ apply: set2_ne | move=> t; case /set2_P => -> ].
Qed.
Hint Resolve setI2_i : fprops.
Lemma setI2_1 x y a: inc a (x \cap y) -> inc a x.
Proof. move => ai; apply: (setI_hi ai); fprops. Qed.
Lemma setI2_2 x y a: inc a (x \cap y) -> inc a y.
Proof. move => ai; apply: (setI_hi ai); fprops. Qed.
Lemma setI2_P x y a: inc a (x \cap y) <-> (inc a x /\ inc a y).
Proof.
split => ai; last by move: ai=> [ax ay]; fprops.
by split; [apply: (setI2_1 ai) | apply:(setI2_2 ai)].
Qed.
Lemma subsetI2l a b: sub (a \cap b) a.
Proof. apply: setI2_1. Qed.
Lemma subsetI2r a b: sub (a \cap b) b.
Proof. apply: setI2_2. Qed.
Lemma setI2_id: idempotent intersection2.
Proof.
by move => x;set_extens t; [case/setI2_P | move=> tx; apply/setI2_P; split].
Qed.
Lemma setI_1 x: intersection (singleton x) = x.
Proof. apply: setI2_id. Qed.
Lemma setI2_C: commutative intersection2.
Proof. move => x y; set_extens t; move /setI2_P => [pa pb]; fprops. Qed.
Lemma setI2_A: associative intersection2.
Proof.
move => x y z; rewrite setI2_C.
set_extens t; case /setI2_P; case /setI2_P=> tx ty tz; apply/setI2_P;fprops.
Qed.
Lemma setI2_CA : left_commutative intersection2.
Proof. by move =>A B C; rewrite !setI2_A (setI2_C B). Qed.
Lemma setI2_AC : right_commutative intersection2.
Proof. by move => A B C;rewrite -!setI2_A (setI2_C B). Qed.
Lemma set2_IIl : left_distributive intersection2 intersection2.
Proof.
by move => A B C; rewrite setI2_A !(setI2_AC _ C) -(setI2_A _ C) setI2_id.
Qed.
Lemma set2_IIr : right_distributive intersection2 intersection2.
Proof. move => a b c; rewrite !(setI2_C a); exact: set2_IIl. Qed.
Lemma setI2_S1 A B C : sub A B -> sub (C \cap A) (C \cap B).
Proof. move=> sAB t; case /setI2_P => ta tc; fprops. Qed.
Lemma setI2_S2 A B C : sub A B -> sub (A \cap C) (B \cap C).
Proof. by move=> sAB; rewrite -!(setI2_C C); exact: setI2_S1. Qed.
Lemma setI2_SS A B C D : sub A C -> sub B D -> sub (A \cap B) (C \cap D).
Proof.
move => s1 s2; apply: sub_trans (setI2_S1 (C:=C) s2); apply: (setI2_S2 s1).
Qed.
Lemma setI2_12S A B C: sub C A -> sub C B -> sub C (A \cap B).
Proof. rewrite -{3}(setI2_id C); exact:setI2_SS. Qed.
Lemma subsetI2_P A B C : sub C (A\cap B) <-> (sub C A /\ sub C B).
Proof.
split; last by move => [h1 h2]; apply : setI2_12S.
move => h;split; apply: (sub_trans h); [apply: subsetI2l |apply: subsetI2r].
Qed.
Lemma subI2_set A B C : (sub A C) \/ (sub B C) -> sub (A \cap B) C.
Proof.
case => h; apply: (sub_trans _ h);[apply: subsetI2l |apply: subsetI2r].
Qed.
Lemma setI2id_Pl A T: sub A T <-> A \cap T = A.
Proof.
split; last by move => <-;apply: subsetI2r.
move => sat; apply: extensionality; first by apply: subsetI2l.
by rewrite - {1}(setI2_id A); apply:setI2_S1.
Qed.
Lemma setI2id_Pr A T: sub A T <-> T \cap A = A.
Proof. rewrite setI2_C; apply: setI2id_Pl. Qed.
Lemma setPI : morphism_2 powerset intersection2 intersection2.
Proof.
move => A B; set_extens t.
move/setP_P /subsetI2_P => [ta tb];apply/setI2_P.
by split; apply/setP_P.
by move /setI2_P=> [ta tb]; apply/setP_P; apply: setI2_12S;apply/setP_P.
Qed.
Lemma set_UI2l: left_distributive union2 intersection2.
Proof.
move => A B C; set_extens t.
case /setU2_P.
by case /setI2_P => ta tb;apply/setI2_P; split; apply/setU2_P; left.
by move => tc;apply/setI2_P; split; apply/setU2_P; right.
case/setI2_P;case /setU2_P=> tac; case /setU2_P => tbc;apply/setU2_P; fprops.
Qed.
Lemma set_UI2r: right_distributive union2 intersection2.
Proof. move => a b c; rewrite !(setU2_C a); apply: set_UI2l. Qed.
Lemma set_IU2l: left_distributive intersection2 union2.
Proof.
move => A B C; set_extens t.
case /setI2_P; case /setU2_P=> tab tc; apply/setU2_P; fprops.
case/setU2_P; case/setI2_P => tab tc; apply/setI2_i => //; apply/setU2_P;fprops.
Qed.
Lemma set_IU2r: right_distributive intersection2 union2.
Proof. move => a b c; rewrite !(setI2_C a); apply: set_IU2l. Qed.
Lemma set_U2K A B: (A \cup B) \cap A = A.
Proof.
apply: extensionality; first by apply:subsetI2r.
apply/subsetI2_P;split; [ apply:subsetU2l | fprops].
Qed.
Lemma set_K2U A B: A \cap (B \cup A) = A.
Proof. rewrite setU2_C setI2_C; exact: set_U2K. Qed.
Lemma set_I2K A B: (A \cap B) \cup A = A.
Proof.
apply: extensionality; last by apply:subsetU2r.
apply/subU2_setP;split; [ apply:subsetI2l | fprops].
Qed.
Lemma set_K2I A B: A \cup (B \cap A) = A.
Proof. rewrite setU2_C setI2_C; exact: set_I2K. Qed.
Lemma setU2_ni x A B: ~inc x (A\cup B) -> (~ inc x A /\ ~ inc x B).
Proof. by move => h; split;dneg xab; apply/setU2_P; [left | right]. Qed.
Lemma setI2_ni x A B: ~inc x (A\cap B) -> (~ inc x A \/ ~ inc x B).
Proof.
move => h; case: (inc_or_not x A); fprops => xa; right => xB; case: h; fprops.
Qed.
Lemma setC_ni x A B: ~inc x (A -s B) -> (~ inc x A \/ inc x B).
Proof.
move => h; case: (inc_or_not x B) => nxb; [by right | left].
move => xa; case: h; fprops.
Qed.
Lemma set_CU2 A B X: X -s (A\cup B) = (X -s A) \cap (X -s B).
Proof.
set_extens t.
case/setC_P => tX tu; apply/setI2_P; move: (setU2_ni tu) => [ta tb].
split; fprops.
case /setI2_P => /setC_P [tx ta] /setC_P [_] tb.
by apply/setC_P;split; [ | case/setU2_P].
Qed.
Lemma set_CI2 A B X: X -s (A\cap B) = (X -s A) \cup (X -s B).
Proof.
set_extens t.
case/setC_P => tX tu; apply/setU2_P; case: (setI2_ni tu) => ti; fprops.
by case /setU2_P => /setC_P [ta tab]; apply/setC_P;split => //; case/setI2_P.
Qed.
Lemma setCI2_pr1 A B E: sub A E -> A -s B = A \cap (E -s B).
Proof.
move => ae; set_extens t.
case /setC_P => ta tb; apply/setI2_P; split; first by exact.
by apply/setC_P; split; [ apply: ae |].
case /setI2_P => ta /setC_P [_] tb; fprops.
Qed.
Lemma set_CC A B E: sub B E -> (E -s (A -s B)) = (E -s A) \cup B.
Proof.
move => be; set_extens t.
case/setC_P => te td; apply/setU2_P.
case: (setC_ni td)=> ta; [left | right]; fprops.
move => h; apply /setC_P;case /setU2_P :h.
by case /setC_P => te ta;split => //;case/setC_P.
by move => tB;split; [ apply: be |case/setC_P ].
Qed.
Lemma setI2_Cr A B : (A \cap B) \cup (A -s B) = A.
Proof. by rewrite set_UI2l setU2Cr1 setU2Cr2 set_K2U. Qed.
Lemma setCU2_l A B C : (A \cup B) -s C = (A -s C) \cup (B -s C).
Proof.
set_extens t.
case/setC_P => /setU2_P [] tab tc; apply/setU2_P; fprops.
case/setU2_P => /setC_P [tab tc];apply/setC_P; split; fprops.
Qed.
Lemma setCU2_r A B C : A -s (B \cup C) = (A -s B) \cap (A -s C).
Proof.
set_extens t.
case/setC_P => ta /setU2_ni [tb tc]; apply/setI2_P; fprops.
case/setI2_P => /setC_P [ta tb] /setC_P [_] tc.
by apply/setC_P;split; [ | case /setU2_P].
Qed.
Lemma setCI2_l A B C : (A \cap B) -s C = (A -s C) \cap (B -s C).
Proof.
set_extens t.
by case/setC_P;case/setI2_P => ta tb tc; apply/setI2_P;split; apply/setC_P.
case/setI2_P => /setC_P [ta tc] /setC_P [tb _]; apply/setC_P; fprops.
Qed.
Lemma setCI2_r A B C : A -s (B \cap C) = (A -s B) \cup (A -s C).
Proof.
set_extens t.
case/setC_P => ta tbc; apply/setU2_P; case(setI2_ni tbc)=> tb; fprops.
by case/setU2_P; case/setC_P => ta tc; apply/setC_P; split => //; case /setI2_P.
Qed.
Lemma setCC_l A B C : (A -s B) -s C = A -s (B \cup C).
Proof.
set_extens t; case /setC_P.
by case /setC_P => ta tb tc; apply/setC_P; split; [ | case/setU2_P ].
move => ta /setU2_ni [tb tc]; apply/setC_P;fprops.
Qed.
Lemma setCC_r A B C : A -s (B -s C) = (A -s B) \cup (A \cap C).
Proof.
set_extens t.
case /setC_P => ta tbc; apply/setU2_P;case: (setC_ni tbc) => tbc'; fprops.
by case /setU2_P; [case /setC_P => ta tb | case /setI2_P => ta tc];
apply/setC_P;split => // ;case /setC_P.
Qed.
Two sets are disjoint if the intersection is empty
Definition disjoint (x y: Set) := x \cap y = emptyset.
Definition disjointVeq (x y: Set) := x = y \/ disjoint x y.
Ltac empty_tac1 u :=
case: (in_set0 (x:= u));
match goal with
H: ?x = emptyset |- _ => rewrite - H
| H: emptyset = ?x |- _ => rewrite H
| H: disjoint _ _ |- _ => rewrite - H; apply /setI2_P; split end;
fprops.
Lemma setI2_0 A : disjoint A emptyset.
Proof. apply/setI2id_Pr;fprops. Qed.
Lemma set0_I2 A : disjoint emptyset A.
Proof. rewrite /disjoint setI2_C; exact: setI2_0. Qed.
Lemma disjoint_pr a b:
(forall u, inc u a -> inc u b -> False) -> disjoint a b.
Proof. move=> p; apply /set0_P => u; case/setI2_P; apply: p. Qed.
Lemma set_IC1r A B: A \cap (A -s B) = A -s B.
Proof. apply/ setI2id_Pr; apply: sub_setC. Qed.
Lemma set_I2Cr A B: disjoint B (A -s B).
Proof. by apply: disjoint_pr; move=> u uy; case /setC_P. Qed.
Ltac empty_tac2 u :=
match goal with H: disjoint ?x ?y |- _ =>
case: (in_set0 (x:= u)); rewrite - H; apply: setI2_i =>//
end.
Ltac mdi_tac v:= match goal with
| |- ?a = ?b \/ _
=> case: (equal_or_not a b); first (by left); move=> v;
right; apply: disjoint_pr
| |- disjointVeq ?a ?b
=> case: (equal_or_not a b); first (by left); move=> v;
right; apply: disjoint_pr
end.
Lemma subsets_disjoint_P A B E: sub A E ->
(sub A B <-> disjoint A (E -s B)).
Proof.
move => ae;split.
by move => ab; apply: disjoint_pr => u ua; case /setC_P; move: (ab _ ua).
move => dae t ta; ex_middle tb; empty_tac2 t; apply/setC_P; split; fprops.
Qed.
Lemma disjoint_subsets_P A E: sub A E -> forall B,
(disjoint A B <-> sub A (E -s B)).
Proof.
move => sae; split.
move => dab t ta; apply/setC_P; split; first by apply: sae.
move => tb;empty_tac2 t.
by move => sd; apply: disjoint_pr => u ua; move: (sd _ ua); case /setC_P.
Qed.
Lemma setCId_Pl A B: A -s B = A <-> disjoint A B.
Proof.
split => xx.
apply/(disjoint_subsets_P (@sub_refl A)); rewrite xx; fprops.
apply:extensionality; first by apply:sub_setC.
move => t tA; apply/ setC_P;split => // tB; empty_tac2 t.
Qed.
Lemma subCset_P3 A B C : sub A (B -s C) <-> ((sub A B) /\ (disjoint A C)).
Proof.
split => h.
by split; [move => t ta | apply: disjoint_pr => t ta]; case /setC_P: (h _ ta).
move: h => [sa dac] t ta; apply/setC_P; split; first by apply: sa.
move => tC; empty_tac2 t.
Qed.
Lemma nondisjoint a b c: inc a b -> inc a c -> ~ disjoint b c.
Proof. by move=> ab ac dg; empty_tac1 a. Qed.
Lemma disjointVeq_pr x y z: disjointVeq x y -> inc z x -> inc z y -> x = y.
Proof. by move => H zx zy ;case: H => //; move: (nondisjoint zx zy). Qed.
Lemma disjoint_S: symmetric_r disjoint.
Proof. by move => x y;rewrite /disjoint setI2_C. Qed.
Lemma subsetC1_P A B x: (sub A (B -s1 x)) <-> (sub A B /\ ~inc x A).
Proof.
split; first by case/subCset_P3=> [pa pb]; split => // xa; empty_tac2 x; fprops.
move => [pa pb] t ta; apply/setC1_P; split; fprops; dneg tx; ue.
Qed.
Lemma setC1_proper A x : inc x A -> ssub (A -s1 x) A.
Proof.
move => xa; split; first by apply: sub_setC.
move => eq1; move: xa; rewrite -eq1; exact: setC1_1.
Qed.
Lemma setC1_eq a X: ~(inc a X) -> X -s1 a = X.
Proof.
move=> h.
set_extens t; first by move => /setC1_P [].
by move => tx; apply /setC1_P; split => // ta; case: h; rewrite - ta.
Qed.
Lemma properI2_r A B : ~(sub B A) -> ssub (A \cap B) B.
Proof. by move => nba; split;[ apply:subsetI2r | move /setI2id_Pr]. Qed.
Lemma properI2_l A B : ~(sub A B) -> ssub (A \cap B) A.
Proof. rewrite setI2_C; apply: properI2_r. Qed.
Lemma properU2_r A B : ~(sub A B) -> ssub B (A \cup B).
Proof.
move => nba; split; [ apply:subsetU2r | dneg hh ;by apply /setU2id_Pl].
Qed.
Lemma properU2_l A B : ~(sub B A) -> ssub A (A \cup B).
Proof. rewrite setU2_C; apply: properU2_r. Qed.
Lemma properI2_set A B C : (ssub B A) \/ (ssub C A) -> (ssub (B \cap C) A).
Proof. by case; apply: ssub_trans2 => t; case/setI2_P. Qed.
Lemma properI2 A B C : (ssub A (B \cap C)) -> (ssub A B /\ ssub A C).
Proof.
by move=> ta; split; apply: (ssub_trans1 ta) => t; case/setI2_P.
Qed.
Lemma properU2 A B C : (ssub (B \cup C) A) -> (ssub B A /\ ssub C A).
Proof. move=> ta; split; apply: ssub_trans2 ta => t tb; fprops. Qed.
Lemma properD A B C : ssub A (B -s C) -> (ssub A B /\ disjoint A C).
Proof.
move => [pa pb]; move/subCset_P3: pa => [pc pd]; split => //; split => //.
by dneg ab; rewrite -ab; symmetry; apply/setCId_Pl.
Qed.
End Intersection.
Export Intersection.
The object (J x y) is a set from which x and y can be recovered.
Bourbaki (English edition) uses an axiom; he uses a doubleton in the French
version; we use here another doubleton and an axiom.
Definition kpair x y := doubleton (singleton x) (doubleton x y).
Definition kpr1 x := union (intersection x).
Definition kpr2 x :=
union (Zo (union x) (fun z => (doubleton (kpr1 x) z) = (union x))).
Module Type PairSig.
Parameter first_proj second_proj : Set -> Set.
Parameter pair_ctor : Set -> Set -> Set.
Axiom kpr1E: first_proj = kpr1.
Axiom kpr2E: second_proj = kpr2.
Axiom kprE: pair_ctor = kpair.
End PairSig.
Module Pair : PairSig.
Definition pair_ctor := kpair.
Definition first_proj := kpr1.
Definition second_proj := kpr2.
Lemma kprE: pair_ctor = kpair. Proof. by []. Qed.
Lemma kpr1E: first_proj = kpr1. Proof. by []. Qed.
Lemma kpr2E: second_proj = kpr2. Proof. by []. Qed.
End Pair.
Notation J := Pair.pair_ctor.
Notation P := Pair.first_proj.
Notation Q := Pair.second_proj.
Lemma pr1_pair x y: P (J x y) = x.
Proof.
rewrite Pair.kpr1E /kpr1 Pair.kprE.
suff: (intersection (kpair x y)) = singleton x by move => -> ; apply: setU_1.
have sx_k: (inc (singleton x) (kpair x y)) by rewrite /kpair; fprops.
apply: set1_pr.
apply: setI_i; first by exists (singleton x).
move => z; case/set2_P => ->; fprops.
move=> z zi; apply/set1_P; apply: (setI_hi zi sx_k).
Qed.
Lemma pr2_pair x y: Q (J x y) = y.
Proof.
rewrite Pair.kpr2E /kpr2 - Pair.kpr1E pr1_pair.
have ->: (union (J x y) = doubleton x y).
rewrite Pair.kprE /kpair; set_extens t =>ts; last first.
by apply: (setU_i ts); fprops.
case /setU2_P: ts => // /set1_P ->; fprops.
rewrite -{3}(setU_1 y); congr (union _); apply: set1_pr.
apply: Zo_i; fprops.
move => z /Zo_P => [] [] /set2_P; case => // -> sd.
by move: (set2_2 x y); rewrite - sd ; move/set1_P.
Qed.
Hint Rewrite pr1_pair pr2_pair : aw.
Lemma pr1_def a b c d: J a b = J c d -> a = c.
Proof. by move=> eql; transitivity (P (J a b)); [| rewrite eql]; aw. Qed.
Lemma pr2_def a b c d: J a b = J c d -> b = d.
Proof. by move=> eql; transitivity (Q (J a b)); [ | rewrite eql ]; aw. Qed.
Definition pairp (x : Set) := (J (P x) (Q x) = x).
Lemma pair_is_pair x y : pairp (J x y).
Proof. rewrite /pairp; aw. Qed.
Hint Resolve pair_is_pair: fprops.
Lemma pair_exten a b:
pairp a -> pairp b -> P a = P b -> Q a = Q b -> a = b.
Proof. by move=> pa pb Pab Qab; rewrite -pa Pab Qab pb. Qed.
End Pair.
Export Pair.
Module Cartesian.
Definition product (A B : Set) :=
union (fun_image A (fun x => (fun_image B (J x)))).
Definition coarse A := product A A.
Notation "A \times B" := (product A B) (at level 40).
Lemma setX_P x A B:
inc x (A \times B) <-> [/\ pairp x, inc (P x) A & inc (Q x) B].
Proof.
split.
move/setU_P => [a xa /funI_P [t ty ft]].
move: xa; rewrite ft; move/funI_P => [u uz ->]; aw; split; fprops.
move => [ px Px Qx];apply/setU_P; exists (fun_image B (J (P x)));
apply/funI_P; [ exists (Q x); fprops; aw | by exists (P x) ].
Qed.
Lemma setX_pair x A B: inc x (A \times B) -> pairp x.
Proof. by case/setX_P. Qed.
Lemma setX_i x A B:
pairp x -> inc (P x) A -> inc (Q x) B -> inc x (A \times B).
Proof. by move => pa pb pc; apply/setX_P. Qed.
Lemma setXp_i x y A B:
inc x A -> inc y B -> inc (J x y) (A \times B).
Proof. move => pa pb; apply setX_i; aw; fprops. Qed.
Lemma setXp_P x y A B:
inc (J x y) (A \times B) <-> (inc x A /\ inc y B).
Proof.
by split; [move/setX_P=> [_]; aw | move=> [xa ya]; apply: setXp_i].
Qed.
Hint Resolve setXp_i: fprops.
A product is empty if and only one factor is empty
Lemma setX_0l B: emptyset \times B = emptyset.
Proof. by apply /set0_P => x /setX_P [_ /in_set0]. Qed.
Lemma setX_0r A: A \times emptyset = emptyset.
Proof. by apply /set0_P => y /setX_P [_ _ /in_set0]. Qed.
Lemma setX_0 A B:
A \times B = emptyset -> (A = emptyset \/ B = emptyset).
Proof.
move=> pe; case: (emptyset_dichot A);first by left.
by case => t tx; right; apply /set0_P => u up; empty_tac1 (J t u).
Qed.
Hint Rewrite setX_0r setX_0l : bw.
The product A \times B is increasing in A and B,
strictly if the other argument is non empty.
Lemma setX_Sl x x' y: sub x x' -> sub (x \times y) (x' \times y).
Proof. move => xx' t; move/setX_P=> [pt pa pb]; apply/setX_P; split;fprops. Qed.
Lemma setX_Sr x y y': sub y y' -> sub (x \times y) (x \times y').
Proof. move => xx' t; move/setX_P=> [pt pa pb]; apply/setX_P;split;fprops. Qed.
Lemma setX_Slr x x' y y':
sub x x' -> sub y y' -> sub (x \times y) (x' \times y').
Proof.
move=> xx' yy'; apply: (@sub_trans (x \times y')); first by apply:setX_Sr.
by apply: setX_Sl.
Qed.
Lemma setX_Sll x y: sub x y -> sub (coarse x ) (coarse y).
Proof. by move => s; apply: setX_Slr. Qed.
Lemma setX_lS x x' y: nonempty y ->
sub (x \times y) (x' \times y) -> sub x x'.
Proof.
by move=> [ t ty ] s z zx; move: (s _ (setXp_i zx ty)); case/setXp_P.
Qed.
Lemma setX_rS x y y': nonempty x ->
sub (x \times y) (x \times y') -> sub y y'.
Proof.
by move=> [ t tx ] s z zy; move: (s _ (setXp_i tx zy)); case/setXp_P.
Qed.
Definition indexed (x i: Set) := x \times singleton i.
Definition indexedr (i x: Set) := singleton i \times x.
Notation "a *s1 b" := (indexed a b) (at level 50).
Lemma indexed_pi x i y: inc y x -> inc (J y i) (x *s1 i).
Proof. move => pa; apply: setXp_i => //; fprops. Qed.
Lemma indexed_P x i y:
inc y (x *s1 i) <-> [/\ pairp y, inc (P y) x & Q y = i].
Proof.
split; first by move /setX_P => [pa pb /set1_P].
move =>[pa pb <-]; apply: setX_i; fprops.
Qed.
Lemma indexedrP a b c:
inc a (indexedr b c) <-> [/\ pairp a , P a = b & inc (Q a) c].
Proof.
split; first by move/setX_P => [pa /set1_P pb pc].
move =>[pa pb pc]; apply/setX_P;split => //; rewrite pb;fprops.
Qed.
End Cartesian.
Export Cartesian.
Definition prop_inc1 (X : Set) (P: property)
& (phantom Prop (forall x0 : Set, P x0)) :=
forall x, inc x X -> P x.
Definition prop_inc11 X Y (P: relation)
& (phantom Prop (forall x y: Set, P x y)) :=
forall x y, inc x X -> inc y Y -> P x y.
Definition prop_inc2 X (P: relation)
& (phantom Prop (forall x y: Set, P x y)) :=
forall x y, inc x X -> inc y X -> P x y.
Notation "{ 'inc' d , P }" :=
(prop_inc1 d (inPhantom P))
(at level 0, format "{ 'inc' d , P }") : type_scope.
Notation "{ 'inc' d1 & d2 , P }" :=
(prop_inc11 d1 d2 (inPhantom P))
(at level 0, format "{ 'inc' d1 & d2 , P }") : type_scope.
Notation "{ 'inc' d & , P }" :=
(prop_inc2 d (inPhantom P))
(at level 0, format "{ 'inc' d & , P }") : type_scope.
Definition prop_when1 (X : property) (P: property)
& (phantom Prop (forall x : Set, P x)) :=
forall x, X x -> P x.
Definition prop_when11 (X Y: property) (P: relation)
& (phantom Prop (forall x y: Set, P x y)) :=
forall x y, X x -> Y y -> P x y.
Definition prop_when2 (X: property) (P: relation)
& (phantom Prop (forall x y: Set, P x y)) :=
forall x y, X x -> X y -> P x y.
Definition prop_when22 (X:relation) (P: relation)
& (phantom Prop (forall x y: Set, P x y)) :=
forall x y, X x y -> P x y.
Notation "{ 'when' d , P }" :=
(prop_when1 d (inPhantom P))
(at level 0, format "{ 'when' d , P }") : type_scope.
Notation "{ 'when' d1 & d2 , P }" :=
(prop_when11 d1 d2 (inPhantom P))
(at level 0, format "{ 'when' d1 & d2 , P }") : type_scope.
Notation "{ 'when' d & , P }" :=
(prop_when2 d (inPhantom P))
(at level 0, format "{ 'when' d & , P }") : type_scope.
Notation "{ 'when' : d , P }" :=
(prop_when22 d (inPhantom P))
(at level 0, format "{ 'when' : d , P }") : type_scope.
Definition commutes_at (f g: Set -> Set) x:= f (g x) = g (f x).
Definition commutes f g := forall x, commutes_at f g x.
Definition compatible_1 f (p q: property) :=
forall x, (p x) -> q (f x).
Definition compatible_2 f (p q:relation) :=
forall x y, (p x y) -> q (f x) (f y).
Definition compatible_3 f (p q:property) :=
forall x y, (p x) -> (p y) -> q (f x y).
Notation "{ 'compat' f : x / p >-> q }" :=
(compatible_1 f (fun x => p) (fun x => q))
(at level 0, f at level 99, x ident,
format "{ 'compat' f : x / p >-> q }") : type_scope.
Notation "{ 'compat' f : x / p }" :=
(compatible_1 f (fun x => p) (fun x => p))
(at level 0, f at level 99, x ident,
format "{ 'compat' f : x / p }") : type_scope.
Notation "{ 'compat' f : x y / p >-> q }" :=
(compatible_2 f (fun x y => p) (fun x y => q))
(at level 0, f at level 99, x ident, y ident,
format "{ 'compat' f : x y / p >-> q }") : type_scope.
Notation "{ 'compat' f : x y / p }" :=
(compatible_2 f (fun x y => p) (fun x y => p))
(at level 0, f at level 99, x ident, y ident,
format "{ 'compat' f : x y / p }") : type_scope.
Notation "{ 'compat' f : x & / p >-> q }" :=
(compatible_3 f (fun x => p) (fun x => q))
(at level 0, f at level 99, x ident,
format "{ 'compat' f : x & / p >-> q }") : type_scope.
Notation "{ 'compat' f : x & / p }" :=
(compatible_3 f (fun x => p) (fun x => p))
(at level 0, f at level 99, x ident,
format "{ 'compat' f : x & / p }") : type_scope.
Module Function.
A graph is a set of pair; the set of first projections is the domain, the set of second projections is the range
Definition sgraph r := alls r pairp.
Definition domain f := fun_image f P.
Definition range f := fun_image f Q.
A functional graph is one for which P is injective
Definition fgraph f := sgraph f /\ {inc f &, injective P}.
Definition related r x y := inc (J x y) r.
Lemma fgraph_sg f: fgraph f -> sgraph f.
Proof. by case. Qed.
Lemma fgraph_pr f x y y':
fgraph f -> inc (J x y) f -> inc (J x y') f -> y = y'.
Proof.
move=> [_ fg] ia ib.
move: (fg _ _ ia ib); aw => h; exact: (pr2_def (h (erefl x))).
Qed.
Hint Resolve fgraph_sg : fprops.
We give here some properties of the domain and range
Lemma domain_i1 f x: inc x f -> inc (P x) (domain f).
Proof. by apply: funI_i. Qed.
Lemma range_i2 f x: inc x f -> inc (Q x) (range f).
Proof. by apply: funI_i. Qed.
Hint Resolve domain_i1 range_i2: fprops.
Lemma domain_i f x y: inc (J x y) f -> inc x (domain f).
Proof. by move => pf; apply/funI_P; exists (J x y); aw. Qed.
Lemma range_i f x y: inc (J x y) f -> inc y (range f).
Proof. by move => pf; apply/funI_P; exists (J x y); aw. Qed.
Lemma domainP r: sgraph r -> forall x,
(inc x (domain r) <-> (exists y, inc (J x y) r)).
Proof.
move=> gr; split; last by move=> [y ]; apply domain_i.
by case/funI_P => y yr ->; exists (Q y); rewrite (gr _ yr).
Qed.
Lemma rangeP r : sgraph r -> forall y,
(inc y (range r) <-> (exists x, inc (J x y) r)).
Proof.
move=> gr y; split;last by move=> [x]; apply range_i.
by case/funI_P => x xr ->; exists (P x); rewrite (gr _ xr).
Qed.
Ltac ex_tac:=
match goal with
| H:inc (J ?x ?y) ?z |- exists x, inc (J x ?y) ?z
=> exists x ; assumption
| H:inc (J ?x ?y) ?z |- exists y, inc (J ?x y) ?z
=> exists y ; assumption
| H:inc (J ?x ?y) ?z |- ex2 _ (fun t => inc (J t ?y) ?z)
=> exists x ; trivial
| H:inc (J ?x ?y) ?z |- ex2 _ (fun t => inc (J ?x t) ?z)
=> exists y ; trivial
| H:inc (J ?x ?y) ?z |- ex2 (fun t => inc (J t ?y) ?z) _
=> exists x ; trivial
| H:inc (J ?x ?y) ?z |- ex2 (fun t => inc (J ?x t) ?z) _
=> exists y ; trivial
| H:inc ?x ?y |- ex2 (fun t=> inc t ?y) _
=> exists x ; fprops
| H:inc ?x ?y |- ex2 _ (fun t => inc t ?y)
=> exists x ; fprops
| H:inc ?x ?y |- exists x, inc x ?y /\ _
=> exists x; split => //
| H:inc ?x ?y |- exists x, [/\ inc x ?y, _ & _ ]
=> exists x; split => //
| |- ex2 (fun t => inc t (singleton ?y)) _
=> exists y ; fprops
| H : inc (J ?x ?y) ?g |- inc ?x (domain ?g)
=> exact: (domain_i H)
| H : inc (J ?x ?y) ?g |- inc ?y (range ?g)
=> exact: (range_i H)
| H : inc ?x ?y |- nonempty ?y
=> exists x;assumption
| |- exists y, inc (J (P ?x) y) _
=> exists (Q x) ; aw
| |- exists y, inc (J y (Q ?x)) _
=> exists (P x) ; aw
end.
Lemma sgraph_exten r r':
sgraph r -> sgraph r' ->
(forall u v, (related r u v <-> related r' u v)) -> r = r'.
Proof.
move=> gr gr'; rewrite /related => p.
by set_extens t => tr; [move: (gr _ tr)=> pt | move: (gr' _ tr)=> pt];
rewrite - pt; apply /p; rewrite pt.
Qed.
Lemma setI2_graph1 x y: sgraph x -> sgraph (x \cap y).
Proof. by move=> gx t /setI2_P [tx _]; apply: gx. Qed.
Lemma setI2_graph2 x y: sgraph y -> sgraph (x \cap y).
Proof. by move=> gx t /setI2_P [_ tx ]; apply: gx. Qed.
Lemma setU2_graph: {compat union2 : x & / sgraph x}.
Proof. by move=> x y gx gy t /setU2_P [] tx; [apply: gx | apply: gy]. Qed.
Lemma range_set0: range emptyset = emptyset.
Proof. apply: funI_set0. Qed.
Lemma domain_set0: domain emptyset = emptyset.
Proof. apply: funI_set0. Qed.
Lemma domain_set0_P r: (domain r = emptyset <-> r = emptyset).
Proof. split; [apply :funI_setne1 | by move ->; exact domain_set0 ]. Qed.
Lemma range_set0_P r: (range r = emptyset <-> r = emptyset).
Proof. split; [apply :funI_setne1 | by move ->; exact range_set0 ]. Qed.
Lemma domain_set0P x: nonempty (domain x) <-> nonempty x.
Proof.
split; last by move => h; apply:funI_setne.
by move/nonemptyP => h; apply /nonemptyP; dneg xx; apply/domain_set0_P.
Qed.
Lemma domain_set1 x y: domain (singleton (J x y)) = singleton x.
Proof. by rewrite /domain funI_set1; aw. Qed.
Lemma range_set1 x y: range (singleton (J x y)) = singleton y.
Proof. by rewrite /range funI_set1; aw. Qed.
Lemma range_setU2: {morph range: x y / x \cup y}.
Proof. apply:funI_setU2. Qed.
Lemma domain_setU2: {morph domain: x y / x \cup y}.
Proof. apply:funI_setU2. Qed.
Lemma domain_setU z: domain (union z) = union (fun_image z domain).
Proof. apply: funI_setU. Qed.
Lemma range_setU z: range (union z) = union (fun_image z range).
Proof. apply: funI_setU. Qed.
Lemma range_setU1 f x y: range (f +s1 (J x y)) = (range f) +s1 y.
Proof. by rewrite range_setU2 range_set1. Qed.
Lemma domain_setU1 f x y: domain (f +s1 (J x y)) = (domain f) +s1 x.
Proof. by rewrite domain_setU2 domain_set1. Qed.
Lemma sgraph_set0: sgraph emptyset.
Proof. by move=> t; case; case. Qed.
Hint Resolve sgraph_set0 : fprops.
Hint Rewrite range_set0 domain_set0 : bw.
Lemma fgraph_set0: fgraph emptyset.
Proof. by split; [fprops | move=> x y; case; case]. Qed.
Lemma fgraph_setU1 f x y:
fgraph f -> ~ inc x (domain f) -> fgraph (f +s1 (J x y)).
Proof.
rewrite /fgraph; move => [fg ff] nid; split.
move=> t; case/setU1_P; [ apply: fg | move=> ->; fprops].
move=> a b; case/setU1_P => ap; case/setU1_P => bp.
- by apply: ff.
- by rewrite bp; aw => xv; case: nid; rewrite -xv; fprops.
- by rewrite ap; aw => xv; case: nid; rewrite xv; fprops.
- by move => _; rewrite ap bp.
Qed.
Lemma fgraph_setU2 a b: fgraph a -> fgraph b ->
disjoint (domain a) (domain b) ->
fgraph (a \cup b).
Proof.
move=> [fg fgg] [sg gfg] ei; split.
move=> t; case/setU2_P; fprops.
move=> x y; case/setU2_P => xab; case /setU2_P=> yab;
first (by apply: fgg); last (by apply: gfg);
move=> sp;empty_tac2 (P y); apply/funI_P; ex_tac.
Qed.
Vg f x is the value of x by a graph f; if there is a z such that
J x z is in f, then V chooses one.
Definition action_prop (f g: Set -> Set -> Set) :=
forall a b x, f (g a b) x = (f a (f b x)).
Definition Vg (f x: Set) := select (fun y : Set => inc (J x y) f) (range f).
Definition same_Vg f g:= Vg f =1 Vg g .
Definition allf (g: Set) (p: property) :=
forall x, inc x (domain g) -> (p (Vg g x)).
Notation "f1 =1g f2" := (same_Vg f1 f2)
(at level 70, no associativity) : fun_scope.
The function V is well-defined for functional graphs.
Here are some properties
Section Vprops.
Variable f: Set.
Hypothesis fgf: fgraph f.
Lemma fdomain_pr1 x: inc x (domain f) -> inc (J x (Vg f x)) f.
Proof.
move: fgf => [p1 p2] /funI_P [z zf ->].
have q1: exists2 y, inc y (range f) & inc (J (P z) y) f.
exists (Q z); [ apply /funI_P; ex_tac | by rewrite (p1 _ zf)].
have q2: singl_val2 (inc ^~ (range f)) (fun u => inc (J (P z) u) f).
move => a b pa ar pb br.
have aux: (P (J (P z) a) = P (J (P z) b)) by aw.
by move: (pr2_def (p2 _ _ ar br aux)).
exact:(proj1 (select_pr q1 q2)).
Qed.
Lemma in_graph_V x: inc x f -> x = J (P x) (Vg f (P x)).
Proof.
move => xf; apply (proj2 fgf _ _ xf); aw.
by apply:fdomain_pr1=> //; apply: domain_i1.
Qed.
Lemma pr2_V x: inc x f -> Q x = Vg f (P x).
Proof. by move=> xf; rewrite (in_graph_V xf); aw. Qed.
Lemma range_gP y:
(inc y (range f) <-> (exists2 x, inc x (domain f) & y = Vg f x)).
Proof.
move: (fgf) => [sg _]; split.
case/(rangeP sg)=> x Px; exists x; first by ex_tac.
by move:(in_graph_V Px); aw; apply: pr2_def.
by move => [x xdf ->]; apply/(rangeP sg); exists x; apply: fdomain_pr1.
Qed.
Lemma inc_V_range x: inc x (domain f) -> inc (Vg f x) (range f).
Proof. move=> xd; apply/range_gP; ex_tac. Qed.
End Vprops.
Hint Resolve inc_V_range: fprops.
Two functional graphs are equal if they have the same domain and evaluation
Lemma fgraph_exten f g:
fgraph f -> fgraph g -> domain f = domain g ->
{inc (domain f), f =1g g} -> f = g.
Proof.
move=> ff fg sd hyp; set_extens t => tf.
move: (domain_i1 tf) => pa.
rewrite (in_graph_V ff tf) (hyp _ pa); apply: fdomain_pr1 => //; ue.
move: (domain_i1 tf); rewrite - sd => pa.
rewrite (in_graph_V fg tf) - (hyp _ pa); apply: fdomain_pr1 => //.
Qed.
Graph associated to a function restricted to some set as domain.
Definition Lg (x : Set) (p : fterm) :=
fun_image x (fun y => J y (p y)).
Lemma Lg_i x y p : inc x y -> inc (J x (p x)) (Lg y p).
Proof. move => xy; apply/funI_P; ex_tac. Qed.
Lemma Lg_fgraph p x: fgraph (Lg x p).
Proof.
split; first by move =>t; case/funI_P=> [z _ ->]; fprops.
move=> a b;case/funI_P=> [z1 _ j1] ; case /funI_P => [z2 _ j2].
by rewrite j1 j2 2! pr1_pair => ->.
Qed.
Lemma Lg_domain x p: domain (Lg x p) = x.
Proof.
set_extens t.
case/funI_P => [e zL ->]; case /funI_P: zL => z zx ->; aw.
by move => tw;apply/funI_P; exists (J t (p t)); aw => //;apply:Lg_i.
Qed.
Hint Rewrite Lg_domain : bw.
Hint Resolve Lg_fgraph: fprops.
Lemma LVg_E x p y: inc y x -> Vg (Lg x p) y = p y.
Proof.
by move=> yx; move: (pr2_V (Lg_fgraph p x) (Lg_i p yx)); aw.
Qed.
Hint Rewrite LVg_E : bw.
Lemma Lg_exten a f g: {inc a, f =1 g} -> Lg a f = Lg a g.
Proof.
move=> eqv; apply: fgraph_exten; fprops; bw.
by move => x xa /=; bw; apply: eqv.
Qed.
Lemma Lg_range p x: range (Lg x p) = fun_image x p.
Proof.
set_extens z.
by move/funI_P=> [a ia ->]; move/funI_P: ia => [b ib ->];aw; apply:funI_i.
move/funI_P => [b ba ->];apply/funI_P.
by exists (J b (p b));aw => //; apply: Lg_i.
Qed.
Lemma Lg_recovers f: fgraph f -> Lg (domain f) (Vg f) = f.
Proof.
move=> fg; apply: fgraph_exten; fprops; bw => x xf /=; bw.
Qed.
Lemma Lg_create a f: Lg a (fun x => Vg (Lg a f) x) = Lg a f.
Proof. apply: Lg_exten=>//; move=> x xa/=; bw. Qed.
Lemma Lg_range_P sf f a:
inc a (range (Lg sf f)) <-> exists2 b, inc b sf & a = f b.
Proof. rewrite Lg_range; apply/funI_P. Qed.
Graph of the identity function.
Definition identity_g (x : Set) := Lg x id.
Lemma identity_fgraph x: fgraph (identity_g x).
Proof. rewrite/identity_g; fprops. Qed.
Lemma identity_sgraph x: sgraph (identity_g x).
Proof. by case: (identity_fgraph x). Qed.
Lemma identity_d x: domain (identity_g x) = x.
Proof. rewrite/identity_g; bw. Qed.
Lemma identity_r x: range (identity_g x) = x.
Proof.
set_extens t; first by move/Lg_range_P => [y yi ->].
by move => tx; apply/Lg_range_P; exists t.
Qed.
Lemma identity_ev x a: inc x a -> Vg (identity_g a) x = x.
Proof. rewrite/identity_g => xa; bw. Qed.
Hint Resolve identity_sgraph : fprops.
Definition cst_graph x y:= Lg x (fun _ => y).
Lemma cst_graph_pr x y: cst_graph x y = x *s1 y.
Proof.
set_extens t.
by move/funI_P => [z zx ->]; apply: indexed_pi.
move /indexed_P => [pt Pt Qt];apply/funI_P; ex_tac; rewrite - Qt //.
Qed.
Lemma cst_graph_ev x y t : inc t x -> Vg (cst_graph x y) t = y.
Proof. move => tw; rewrite /cst_graph; bw. Qed.
Lemma cst_graph_d x y : domain (cst_graph x y) = x.
Proof. rewrite /cst_graph; bw. Qed.
Lemma cst_graph_fgraph a b: fgraph (cst_graph a b).
Proof. rewrite /cst_graph; fprops. Qed.
Hint Rewrite cst_graph_d cst_graph_ev : bw.
Hint Resolve cst_graph_fgraph: fprops.
Lemma setU1_V_out f x y:
fgraph f -> ~ (inc x (domain f)) -> Vg (f +s1 (J x y)) x = y.
Proof.
move=>ff /(fgraph_setU1 y ff) fg.
have h1: inc (J x y) (f +s1 (J x y)) by fprops.
by move: (pr2_V fg h1); aw.
Qed.
Lemma setU1_V_in f x y u:
fgraph f -> ~ (inc x (domain f)) -> inc u (domain f) ->
Vg (f +s1 (J x y)) u = Vg f u.
Proof.
move=> ff /(fgraph_setU1 y ff) fg /(fdomain_pr1 ff) aux.
have h1: inc (J u (Vg f u)) (f +s1 (J x y)) by fprops.
by move: (pr2_V fg h1); aw.
Qed.
Case of a subgraph
Lemma sub_fgraph f g: fgraph g -> sub f g -> fgraph f.
Proof.
move=> [fg ffg] s; split.
by move=> t tf; apply: (fg _ (s _ tf)).
by move=> x y xf yf; apply: ffg; apply: s.
Qed.
Lemma domain_S f g: sub f g -> sub (domain f) (domain g).
Proof. apply: funI_S. Qed.
Lemma range_S f g: sub f g -> sub (range f) (range g).
Proof. apply: funI_S. Qed.
Lemma sub_graph_ev f g:
fgraph g -> sub f g -> {inc (domain f), f =1g g}.
Proof.
move=> fg sfg x xdf.
set ipg:=(sfg _ (fdomain_pr1 (sub_fgraph fg sfg) xdf)).
by move: (in_graph_V fg ipg); aw; apply: pr2_def.
Qed.
restriction of a graph to a set
Definition restr f x := Lg x (Vg f).
Lemma restr_d f x: domain (restr f x) = x.
Proof. rewrite /restr; bw. Qed.
Lemma restr_fgraph f x: fgraph (restr f x).
Proof. by rewrite /restr; fprops. Qed.
Lemma restr_ev f x i: inc i x -> Vg (restr f x) i = Vg f i.
Proof. move=> ix; rewrite /restr; bw. Qed.
Hint Rewrite restr_ev restr_d: bw.
Hint Resolve restr_fgraph : fprops.
Lemma double_restr f a b: sub a b -> (restr (restr f b) a) = (restr f a).
Proof.
by move => sb; apply: Lg_exten => t ta /=; bw; apply: sb.
Qed.
Lemma restr_Lg a b f: sub b a -> restr (Lg a f) b = Lg b f.
Proof.
move => sba; apply:fgraph_exten; fprops; bw.
by move => t tb /=; bw; apply: sba.
Qed.
Lemma restr_to_domain f g: fgraph f -> sub g f -> restr f (domain g) = g.
Proof.
move => h1 h2; move: (sub_fgraph h1 h2) => fgg.
apply:fgraph_exten; bw; fprops.
move => t tx /=;bw; symmetry; apply: sub_graph_ev => //.
Qed.
Lemma restr_range1 f x: fgraph f -> sub x (domain f) ->
sub (range (restr f x)) (range f).
Proof.
move=> pa pb t/funI_P [u /funI_P [z zx -> ->]]; aw.
exact: (inc_V_range pa (pb _ zx)).
Qed.
Composition of two graphs. If the graphs are composable,
we can simplify the definition
Definition composablef (f g : Set) :=
[/\ fgraph f, fgraph g & sub (range g) (domain f)].
Definition composef f g := Lg (domain g) (fun y => Vg f (Vg g y)).
Notation "x \cf y" := (composef x y) (at level 50).
Notation "x \cfP y" := (composablef x y) (at level 50).
Lemma composef_ev x f g:
inc x (domain g) -> Vg (f \cf g) x = Vg f (Vg g x).
Proof. move => pa; rewrite /composef; bw. Qed.
Lemma composef_fgraph f g: fgraph (f \cf g).
Proof. rewrite /composef; fprops. Qed.
Lemma composef_domain f g: domain (f \cf g) = domain g.
Proof. by rewrite /composef; bw. Qed.
Lemma composef_range f g: f \cfP g ->
sub (range (f \cf g)) (range f).
Proof.
move => [pa pb pc] t; move /(range_gP (composef_fgraph f g)) => [x].
rewrite composef_domain => xdg; rewrite (composef_ev _ xdg) => ->.
apply /(range_gP pa); exists (Vg g x) => //.
apply: pc; apply /(range_gP pb).
ex_tac.
Qed.
Hint Rewrite composef_ev : bw.
Hint Resolve composef_fgraph: fprops.
End Function.
Export Function.