Library set1
Fundamental set theory
Original file by Carlos Simpson (CNRS/UNSA)Copyright INRIA (2009) Apics Team (Jose Grimm).
Set Implicit Arguments.
Require Export Arith.
Module Axioms.
Realisation: if
x is a set, Ro maps an object of type x to a set
Parameter Ro : forall x : Set, x -> Set.
Injectivity of
Ro
Axiom R_inj : forall (x : Set) (a b : x), Ro a = Ro b -> a = b.
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.
Extensionality for sets
Axiom extensionality : forall a b : Set, sub a b -> sub b a -> a = b.
Extensionality for products
Axiom prod_extensionality :
forall (x : Type) (y : x -> Type) (u v : forall a : x, y a),
(forall a : x, u a = v a) -> u = v.
Lemma arrow_extensionality :
forall (x y : Type) (u v : x -> y), (forall a : x, u a = v a) -> u = v.
Proof. intros x y.
change (forall u v : forall a : x, (fun _ : x => y) a,
(forall a : x, u a = v a) -> u = v).
intros. apply prod_extensionality; assumption.
Qed.
nonempty: type is populated, or set has an element.
Inductive nonemptyT (t : Type) : Prop :=
nonemptyT_intro : t -> nonemptyT t.
Inductive nonempty (x : Set) : Prop :=
nonempty_intro : forall y : Set, inc y x -> nonempty x.
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).
Parameter chooseT : forall (t : Type) (p : t -> Prop)(q:nonemptyT t), t.
Axiom chooseT_pr :
forall (t : Type) (p : t -> Prop) (q : nonemptyT t),
ex p -> p (chooseT p q).
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, (x -> Set) -> Set.
Axiom IM_exists :
forall (x : Set) (f : x -> Set) (y : Set),
inc y (IM f) -> exists a : x, f a = y.
Axiom IM_inc :
forall (x : Set) (f : x -> Set) (y : Set),
(exists a : x, f a = y) -> inc y (IM f).
Excluded middle and consequences.
Axiom excluded_middle : forall P : Prop, ~ ~ P -> P.
Axiom iff_eq : forall P Q : Prop, (P -> Q) -> (Q -> P) -> P = Q.
Lemma p_or_not_p : forall P : Prop, P \/ ~ P.
Proof. intros. apply excluded_middle. intro. intuition.
Qed.
Lemma equal_or_not: forall x y:Set, x= y \/ x<> y.
Proof. intros. apply p_or_not_p.
Qed.
Lemma inc_or_not: forall x y:Set, inc x y \/ ~ (inc x y).
Proof. intros. apply p_or_not_p.
Qed.
End Axioms.
Export Axioms.
Module Tactics1.
Shorthands, for instance
EEE = Set -> Set -> Set.
Notation EE := (Set -> Set).
Notation EEE := (Set -> EE).
Notation EP := (Set -> Prop).
Notation EEP := (Set -> EP).
Infix "&":= and (right associativity, at level 100).
Lemma seq_deconj : forall P Q : Prop, P -> (P -> Q) -> (P & Q).
intros P Q p H. split ; [idtac | apply H]; assumption. Qed.
Lemma uneq : forall (f:EE) x y,
x = y -> f x = f y.
Proof. intros f x y H. rewrite H. trivial. Qed.
Lemma uneq2 : forall (f:EEE) x y x' y',
x = y -> x' = y' -> f x x' = f y y'.
Proof. intros f x y x' y' H H'. rewrite H. rewrite H'. trivial. Qed.
Ltac ir := intros.
Ltac rw u := rewrite u.
Ltac rwi u h := rewrite u in h.
Ltac wr u := rewrite <- u.
Ltac wri u h := rewrite <- u in h.
Ltac ap h := apply h.
Ltac am := assumption.
Ltac tv := trivial.
Ltac eau := eauto.
Ltac sy := symmetry.
Ltac uf u := unfold u.
Ltac ufi u h := unfold u in h.
Ltac nin h := induction h.
Ltac int := intuition.
Ltac app u := ap u; tv.
Ltac apw u v := apply u with v ; tv.
Ltac rww u := rw u; tv.
Ltac rwii u h:= rwi u h; tv.
Ltac wrii u h:= wri u h; tv.
Ltac wrr u := wr u; tv.
Ltac dneg := match goal with
H : ~ _ |- ~ _ => red; ir; elim H
end.
Ltac ex_middle := match goal with
| |- inc ?a ?b => nin (inc_or_not a b) ; tv
| |- ?a = ?b => nin (equal_or_not a b) ; tv
end.
Tatics like
aw use autorewite on the goal and try to solve; tactics
like awi just rewrite in an assumption, tatics like fprop use auto
Ltac aw := autorewrite with aw; tv.
Ltac awi u:= autorewrite with aw in u.
Ltac awii u:= autorewrite with aw in u; tv.
Ltac bw := autorewrite with bw; tv.
Ltac bwi u:= autorewrite with bw in u.
Ltac srw:= autorewrite with sw; tv.
Ltac srwi u:= autorewrite with sw in u.
Ltac fprops := auto with fprops.
Ltac gprops := auto with gprops.
Ltac au := first [ solve [am] | auto ].
Ltac set_extens:= app extensionality; unfold sub; intros.
Ltac EasyDeconj :=
match goal with
| |- (_ & _) => ap conj; [ EasyDeconj | EasyDeconj ]
| |- _ => idtac
end.
Ltac EasyExpand :=
match goal with
| id1:(?X1 /\ ?X2) |- _ => nin id1; EasyExpand
| |- _ => EasyDeconj
end.
Ltac ee := EasyExpand.
Ltac Remind u :=
set (recalx := u);
match goal with
| recalx:?X1 |- _ => assert X1; [ exact recalx | clear recalx ]
end.
Ltac cp := Remind.
Ltac Use_eq :=
match goal with
| H:?a = ?b |- ?f ?a = ?f ?b => rww H
| H:?a = ?b |- ?f ?a _ = ?f ?b _ => rww H
| H:?a = ?b |- ?f _ ?a = ?f _ ?b => rww H
| H:?a = ?b |- ?f ?a _ _ = ?f ?b _ _ => rww H
| H:?a = ?b |- ?f _ ?a _ = ?f _ ?b _ => rww H
| H:?a = ?b |- ?f _ _ ?a = ?f _ _ ?b => rww H
| H:?a = ?b |- _ => solve [ rww H ; fprops | wrr H ; fprops]
| Ha : ?a = ?c, Hb : ?b = ?c |- ?a = ?b => wr Ha ; wr Hb; tv
| H:?b = _ |- _ ?b => rww H
| H:?b = _ |- _ _ ?b => rww H
| H:?b = _ |- _ ?b _ => rww H
| H:?b = _ |- _ _ ?b _ => rww H
| H:?b = _ |- _ ?b _ _ => rww H
| H:?b = _ |- _ _ _ ?b => rww H
end.
Ltac ue := Use_eq.
Ltac eee := ee ; tv; try ue; fprops.
End Tactics1.
Export Tactics1.
Module Constructions.
exists_unique p says there a unique x such that (p x)
Definition exists_unique t (p : t->Prop) :=
(ex p) & (forall x y : t, p x -> p y -> x = y).
Defines
strict_sub as strict subset
Definition strict_sub (a b : Set) := (a <> b) & (sub a b).
Lemma sub_trans : forall a b c, sub a b -> sub b c -> sub a c.
Proof. uf sub; auto. Qed.
Lemma sub_refl : forall x, sub x x.
Proof. unfold sub; auto. Qed.
Lemma strict_sub_trans1 :
forall a b c, strict_sub a b -> sub b c -> strict_sub a c.
Proof. uf strict_sub. ir. nin H.
split. dneg. wri H2 H0. app extensionality. apw sub_trans b.
Qed.
Lemma strict_sub_trans2 :
forall a b c, sub a b -> strict_sub b c -> strict_sub a c.
Proof. unfold strict_sub. ir. nin H0. split. dneg.
rwi H2 H. app extensionality. apw sub_trans b.
Qed.
emptyset is a type without constructor; empty is classical.
Definition empty (x : Set) := forall y : Set, ~ inc y x.
Inductive emptyset : Set :=.
Basic property of
Ro.
Lemma R_inc : forall (x : Set) (a : x), inc (Ro a) x.
Proof. ir. exists a; tv.
Qed.
Equivalence between
nonempty and ~ empty.
Lemma inc_nonempty : forall x y, inc x y -> nonemptyT y.
Proof. uf inc; ir; nin H; app nonemptyT_intro.
Qed.
Lemma nonemptyT_not_empty : forall x:Set, nonemptyT x -> ~ empty x.
Proof. uf not. ir. nin H. ap (H0 (Ro H)(R_inc H)).
Qed.
Lemma nonemptyT_not_empty0 : forall x:Set, nonemptyT x = nonempty x.
Proof. ir. ap iff_eq; ir; nin H. exists (Ro H). exists H. tv.
ap (inc_nonempty H).
Qed.
Lemma emptyset_pr: forall x, ~ inc x emptyset.
Proof. ir. red. ir. nin H. elim x0.
Qed.
Lemma is_emptyset: forall x, (forall y, ~ (inc y x)) -> x = emptyset.
Proof. ir. set_extens. elim (H x0). am. elim (emptyset_pr H0).
Qed.
Ltac empty_tac :=
match goal with
| |- _ = emptyset => ap is_emptyset; red;ir; idtac
| H:inc _ emptyset |- _ => elim (emptyset_pr H)
| _ => idtac
end.
Ltac empty_tac1 u := elim (emptyset_pr (x:= u));
match goal with H: ?x = emptyset |- _ => wr H
| H: emptyset = ?x |- _ => rw H end ; fprops.
Lemma emptyset_sub_any:
forall x, sub emptyset x.
Proof. ir. red. ir. empty_tac.
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
and more properties of the emptyset.
Definition Bo (x y : Set) (hyp : inc x y) :=
chooseT (fun a : y => Ro a = x) (inc_nonempty hyp).
Lemma B_eq : forall x y (hyp : inc x y), Ro (Bo hyp) = x.
Proof. uf inc; uf Bo. ir. app chooseT_pr.
Qed.
Lemma B_back : forall (x:Set) (y:x) (hyp : inc (Ro y) x), Bo hyp = y.
Proof. ir. ap R_inj. ap B_eq.
Qed.
Lemma not_empty_nonemptyT : forall x , ~ empty x -> nonemptyT x.
Proof. ir. nin (p_or_not_p (nonemptyT x)). am. elim H.
red. ir. dneg. ap (nonemptyT_intro (Bo H1)).
Qed.
Lemma emptyset_dichot : forall x, (x = emptyset \/ nonempty x).
Proof. ir. nin (p_or_not_p (nonempty x)). au. left. empty_tac.
elim H. exists y. am.
Qed.
Let
T be a type, P a proposition, a a function that maps a proof
of P into T and b a function that maps a proof of ~P into T.
Let q x the property that a p =x and b q = x. We show that there
exists x with this property
Lemma by_cases_nonempty :
forall (T : Type) (P : Prop) (a : P -> T) (b : ~ P -> T), nonemptyT T.
Proof. ir. nin (p_or_not_p P); ap nonemptyT_intro; [ app a | app b].
Qed.
We can apply the axiom of choice. We have 4 lemmas: fundamental
property, uniqueness, case where P is true, case where P is false.
Definition by_cases (T : Type) (P : Prop) (a : P -> T) (b : ~ P -> T) :=
chooseT (fun x : T => (forall p : P, a p = x)
& (forall q : ~ P, b q = x))
(by_cases_nonempty a b).
Lemma by_cases_if :
forall (T : Type) (P : Prop) (a : P -> T) (b : ~ P -> T) (p : P),
(forall p1 p2: P, a p1 = a p2) ->
by_cases a b = a p.
Proof. ir.
assert ((forall p , a p = (by_cases a b))
& (forall q, b q = (by_cases a b))).
uf by_cases. app chooseT_pr. exists (a p). split. ir. app H.
ir. contradiction. nin H0. sy. app H0.
Qed.
Lemma by_cases_if_not :
forall (T : Type) (P : Prop) (a : P -> T) (b : ~ P -> T) (q : ~ P),
(forall p1 p2: ~P, b p1 = b p2) ->
by_cases a b = b q.
Proof. ir. assert ((forall p : P, a p = (by_cases a b))
& (forall q : ~ P, b q = (by_cases a b))). uf by_cases.
app chooseT_pr. exists (b q). split. ir. contradiction.
ir. app H. nin H0. sy. app H1.
Qed.
Genereralised axiom of choice.
choose p is satisfied by p
if somebody satisfies p, is the emptyset otherwise
Definition choose (p:EP) :=
chooseT (fun x => (ex p -> p x) & ~ ex p -> x = emptyset)
(nonemptyT_intro emptyset).
Lemma choose_pr : forall p, ex p -> p (choose p).
Proof. ir. unfold choose. assert (H0:=H).
set (q:= fun x => ex p -> p x & ~ ex p -> x = emptyset).
assert (q (chooseT q (nonemptyT_intro emptyset))). app chooseT_pr.
nin H. exists x. uf q. split;ir. am. contradiction. nin H1. app H1.
Qed.
Lemma choose_not : forall p, ~(ex p) -> choose p = emptyset.
Proof. ir. unfold choose. cp H.
set (q:= fun x => ex p -> p x & ~ ex p -> x = emptyset).
assert (q (chooseT q (nonemptyT_intro emptyset))). app chooseT_pr.
exists emptyset. uf q. split;ir. contradiction. tv. nin H1. app H2.
Qed.
Lemma arrow_EP_exten: forall (p q: EP),
(forall x, p x <-> q x) -> p = q.
Proof. ir. app arrow_extensionality. ir. nin (H a). app iff_eq.
Qed.
Lemma choose_equiv: forall (p q: EP),
(forall x, p x <-> q x) -> choose p = choose q.
Proof. ir. rww (arrow_EP_exten _ _ H).
Qed.
Definition choosenat p :=
chooseT (fun u => (ex p -> p u) & ~ ex p -> u = 0) (nonemptyT_intro 0).
Lemma choosenat_pr : forall p, (ex p) -> p (choosenat p).
Proof. ir. unfold choosenat.
set(q:= fun u : nat => ex p -> p u & ~ ex p -> u = 0).
assert (q (chooseT q (nonemptyT_intro 0))). app chooseT_pr.
cp H. nin H. exists x. uf q. split. auto. ir. contradiction. red in H0.
ee. app H0.
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 nonempty_rep : forall x, nonempty x -> inc (rep x) x.
Proof. ir. unfold rep. nin H. ap choose_pr. exists y. am.
Qed.
The negation of
forall x, ~ (p x) is the existence of x with (p x).
Lemma exists_proof : forall p : EP, ~ (forall x : Set, ~ p x) -> ex p.
Proof. ir. nin (p_or_not_p (ex p)). am. elim H. ir. dneg. exists x. am.
Qed.
Lemma not_exists_pr : forall p : EP, (~ ex p) = (forall x : Set, ~ p x).
Proof. ir. ap iff_eq; ir; intro H1. elim H. exists x; am.
nin H1. apw H x.
Qed.
Defines
Y P x y to x if P is true and y otherwise
Definition Yo : Prop -> EEE :=
fun P x y => by_cases (fun _ : P => x) (fun _ : ~ P => y).
Lemma Y_if : forall (P : Prop) (hyp : P) x y z, x = z -> Yo P x y = z.
Proof. ir. unfold Yo. wr H. set (a := fun _:P => x).
change (by_cases a (fun _ : ~ P => y) = a hyp). app by_cases_if.
Qed.
Lemma Y_if_not :
forall (P : Prop) (hyp : ~ P) x y z, y = z -> Yo P x z = y.
Proof. ir. unfold Yo. set (b := fun _: ~ P => z). rw H.
change (by_cases (fun _ : P => x) b = b hyp). app by_cases_if_not.
Qed.
Lemma Y_if_rw : forall (P:Prop) (hyp :P) x y, Yo P x y = x.
Proof. intros. app Y_if. Qed.
Lemma Y_if_not_rw : forall (P:Prop) (hyp : ~P) x y, Yo P x y = y.
Proof. intros. app Y_if_not. Qed.
Definition Yt (A:Type): Prop -> (A->A->A):=
fun P x y => by_cases (fun _ : P => x) (fun _ : ~ P => y).
Lemma Yt_if_rw : forall (A:Type)(P : Prop) (hyp : P) (x:A) y,
Yt P x y = x.
Proof. ir. unfold Yt. set (a := fun _:P => x).
change (by_cases a (fun _ : ~ P => y) = a hyp). app by_cases_if.
Qed.
Lemma Yt_if_not_rw : forall (A:Type) (P : Prop) (hyp : ~ P) x (y:A),
Yt P x y = y.
Proof. ir. unfold Yt. set (b := fun _: ~ P => y).
change (by_cases (fun _ : P => x) b = b hyp). app by_cases_if_not.
Qed.
Given a function f,
Zorec remembers a and f(a)
Inductive Zorec (x : Set) (f : x -> Prop) : Set :=
Zorec_c :forall (a: x), f a -> Zorec f.
Zo x p is the image of some function g; this means that inc y (Zo x p)
if and only if y = (g t) for some t; t is a record, say it remembers
a of type x, and p (Ro a) holds; g(t) is Ro a. Thus inc y x and
p y. The converse is true.
Definition Zo (x:Set) (p:EP) :=
IM (fun (z : Zorec (fun (a : x) => p (Ro a))) => let (a, _) := z in Ro a).
Lemma Z_inc : forall x (p: EP) y, inc y x -> p y -> inc y (Zo x p).
Proof. ir. unfold Zo. ap IM_inc. nin H. wri H H0.
exists (Zorec_c (fun a : x => p (Ro a)) x0 H0). tv.
Qed.
Lemma Z_sub : forall x p, sub (Zo x p) x.
Proof. ir. red. ir. nin (IM_exists H). wr H0. nin x1. apply R_inc.
Qed.
Lemma Z_all : forall x p y, inc y (Zo x p) -> (inc y x & p y).
Proof. ir. nin (IM_exists H). wr H0. nin x0. split. ap R_inc. am.
Qed.
Ltac Ztac :=
match goal with
| id1:(inc _ (Zo _ _)) |- inc _ (Zo _ _ )
=> nin (Z_all id1) ; ap Z_inc; auto
| id1:(inc _ (Zo _ _)) |- _ => nin (Z_all id1)
| |- (inc _ (Zo _ _)) => ap Z_inc; auto
| _ => idtac
end.
Definition Yy : forall P : Prop, (P -> Set) -> EE :=
fun P f x => by_cases f (fun _ : ~ P => x).
Lemma Yy_if :
forall (P : Prop) (hyp : P) (f : P -> Set) x z,
(forall p1 p2: P, f p1 = f p2) ->
f hyp = z -> Yy f x = z.
Proof. ir. unfold Yy. wr H0. app by_cases_if.
Qed.
Lemma Yy_if_not :
forall (P : Prop) (hyp : ~ P) (f : P -> Set) (x z : Set), x = z -> Yy f x = z.
Proof. ir. unfold Yy. set (b := fun _: ~ P => x). wr H.
change (by_cases f b = b hyp). app by_cases_if_not.
Qed.
Defines
Xo f y, where f is defined for objects of type x as: (f z)
if inc y x, and z expresses this, the emptyset otherwise.
Definition Xo (x : Set) (f : x -> Set) (y : Set) :=
Yy (fun hyp : inc y x => f (Bo hyp)) emptyset.
Lemma X_eq :
forall (x : Set) (f : x -> Set) (y z : Set),
(exists a : x, (Ro a = y) & (f a = z)) -> Xo f y = z.
Proof. ir. induction H. unfold Xo. nin H. symmetry in H.
assert (inc y x). rw H. apply R_inc.
apply Yy_if with H1. ir.
assert (Bo p1 = x0). apply R_inj. rww B_eq. rw H2.
assert (Bo p2 = x0). apply R_inj. rww B_eq. sy;ue.
assert (Bo H1 = x0). apply R_inj. rww B_eq. rww H2.
Qed.
Lemma X_rewrite : forall (x : Set) (f : x -> Set) (a : x), Xo f (Ro a) = f a.
Proof. ir. apply X_eq. exists a. auto. Qed.
Set of all elements of
x satisfying p
Definition cut (x : Set) (p : x -> Prop) :=
Zo x (fun y : Set => forall hyp : inc y x, p (Bo hyp)).
Lemma cut_sub : forall (x : Set) (p : x -> Prop), sub (cut p) x.
Proof. ir. unfold cut. apply Z_sub. Qed.
Definition cut_to (x : Set) (p : x -> Prop) (y : cut p) :=
Bo (cut_sub (p:=p) (R_inc y)).
Lemma cut_to_R_eq :
forall (x : Set) (p : x -> Prop) (y : cut p), Ro (cut_to y) = Ro y.
Proof. ir. unfold cut_to. rww B_eq. Qed.
Lemma cut_pr : forall (x : Set) (p : x -> Prop) (y : cut p), p (cut_to y).
Proof. ir. unfold cut_to. ufi cut y.
set (R_inc y). Ztac. ap H0.
Qed.
Lemma cut_inc :
forall (x : Set) (p : x -> Prop) (y : x), p y -> inc (Ro y) (cut p).
Proof. ir. unfold cut. Ztac. ap R_inc.
ir. assert (Bo hyp = y). ap R_inj. ap B_eq. ue.
Qed.
End Constructions.
Export Constructions.
Module Little.
singleton: image of a set with one point
Inductive one_point : Set :=
one_point_intro.
Definition singleton (x : Set) := IM (fun p : one_point => x).
Lemma singleton_inc : forall x, inc x (singleton x).
Proof. ir. uf singleton. ap IM_inc. exists one_point_intro. tv. Qed.
Hint Resolve sub_refl singleton_inc: fprops.
Lemma singleton_eq : forall x y, inc y (singleton x) -> y = x.
Proof. ir. sy. nin (IM_exists H). am. Qed.
Lemma singleton_rw: forall x y, inc y (singleton x) = (y = x).
Proof. ir. ap iff_eq. ir. ap (singleton_eq H). ir. rw H. fprops. Qed.
Hint Rewrite singleton_rw: aw.
Lemma singleton_inj : forall x y, singleton x = singleton y -> x = y.
Proof. ir. assert (inc x (singleton y)). wr H. fprops. app singleton_eq. Qed.
Lemma nonempty_singleton: forall x, nonempty (singleton x).
Proof. ir. exists x. fprops.
Qed.
Lemma sub_singleton: forall x y,
inc x y -> sub (singleton x) y.
Proof. ir. red. ir. rww (singleton_eq H0).
Qed.
doubleton: image of a set with two points
Inductive two_points : Set :=
| two_points_a | two_points_b.
Definition TPa := Ro two_points_a.
Definition TPb := Ro two_points_b.
Lemma two_points_pr: forall x,
inc x two_points = (x= TPa \/ x = TPb).
Proof. ir. uf TPa; uf TPb. ap iff_eq.
ir. nin H; wr H. elim x0; auto.
ir. nin H; rw H;app R_inc.
Qed.
Lemma two_points_distinct: TPa <> TPb.
Proof. red. ir. set (R_inj H). discriminate e.
Qed.
Lemma two_points_distinctb: TPb <> TPa.
Proof. red. ir. set (R_inj H). discriminate e.
Qed.
Lemma inc_TPa_two_points: inc TPa two_points.
Proof. uf TPa. app R_inc. Qed.
Lemma inc_TPb_two_points: inc TPb two_points.
Proof. uf TPb. app R_inc. Qed.
Definition doubleton (x y : Set) :=
IM (fun t => two_points_rect (fun _ : two_points => Set) x y t).
Lemma doubleton_first : forall x y, inc x (doubleton x y).
Proof. ir. uf doubleton. ap IM_inc. exists two_points_a. tv. Qed.
Lemma doubleton_second : forall x y : Set, inc y (doubleton x y).
Proof. ir. uf doubleton. ap IM_inc. exists two_points_b. tv. Qed.
Lemma doubleton_or :
forall x y z : Set, inc z (doubleton x y) -> z = x \/ z = y.
Proof. ir. nin (IM_exists H). nin x0; intuition.
Qed.
Hint Resolve doubleton_first doubleton_second inc_TPa_two_points inc_TPb_two_points: fprops.
Ltac db_tac :=
match goal with
| H: inc _ (doubleton _ _ ) |- _ => nin (doubleton_or H); ue
| H: inc _ (singleton _ ) |- _ => rwi singleton_rw H; ue
end.
Lemma doubleton_rw : forall x y z : Set,
inc z (doubleton x y) = (z = x \/ z = y).
Proof. ir. ap iff_eq. app doubleton_or. ir. nin H; rw H; fprops.
Qed.
Lemma two_points_pr2: doubleton TPa TPb = two_points.
Proof. set_extens. rw two_points_pr. app doubleton_or.
rwi two_points_pr H. nin H; rw H; fprops.
Qed.
Lemma doubleton_inj : forall x y z w,
doubleton x y = doubleton z w -> (x = z & y = w) \/ (x = w & y = z).
Proof. ir.
assert (inc x (doubleton z w)). wr H; fprops.
assert (inc y (doubleton z w)). wr H; fprops.
assert (inc w (doubleton x y)). rw H; fprops.
assert (inc z (doubleton x y)). rw H; fprops.
nin (doubleton_or H0). left. split. am.
nin (doubleton_or H2). nin (doubleton_or H1). rw H5; rw H4; am. am. auto.
right. split. am. nin (doubleton_or H1). am. sy.
wri H4 H5. nin (doubleton_or H3). rww H5. am.
Qed.
Lemma doubleton_singleton : forall x, doubleton x x = singleton x.
Proof. ir. set_extens; db_tac.
Qed.
Lemma nonempty_doubleton: forall x y, nonempty (doubleton x y).
Proof. ir. exists x. fprops. Qed.
Lemma sub_doubleton: forall x y z,
inc x z -> inc y z -> sub (doubleton x y) z.
Proof. ir. red. ir. db_tac.
Qed.
Lemma doubleton_symm: forall a b,
doubleton a b = doubleton b a.
Proof. ir. set_extens; db_tac.
Qed.
End Little.
Export Little.
Module Complement.
Set of all elements in a not in b
Definition complement (a b : Set) := Zo a (fun x : Set => ~ inc x b).
Lemma inc_complement :
forall a b x, inc x (complement a b) = (inc x a & ~ inc x b).
Proof. ir. uf complement. ap iff_eq; ir. Ztac. au. ee. Ztac.
Qed.
Hint Rewrite inc_complement: sw.
Lemma use_complement :
forall a b x, inc x a -> ~ inc x (complement a b) -> inc x b.
Proof. ir. ex_middle. elim H0. srw. auto.
Qed.
Lemma sub_complement: forall a b, sub (complement a b) a.
Proof. ir. uf sub; ir. srwi H; eee. Qed.
Lemma empty_complement: forall a b,
complement a b = emptyset -> sub a b.
Proof. ir. red. ir. app (@use_complement a b x). rw H. app emptyset_pr.
Qed.
Lemma strict_sub_nonempty_complement : forall x y,
strict_sub x y -> nonempty (complement y x).
Proof. ir. nin H. nin (emptyset_dichot (complement y x)).
elim H. app extensionality. app empty_complement. am.
Qed.
Lemma double_complement: forall a x,
sub a x -> complement x (complement x a) = a.
Proof. ir. set_extens. srwi H0. ee. ex_middle. elim H1.
auto. srw. ee. app H. red. ir. ee. app H2.
Qed.
Hint Rewrite double_complement: sw.
Lemma complement_itself : forall x,
complement x x = emptyset.
Proof. ir. empty_tac. srwi H. intuition.
Qed.
Lemma complement_emptyset : forall x,
complement x emptyset = x.
Proof. ir. set_extens. srwi H. intuition. srw. split. am. ap emptyset_pr.
Qed.
Lemma not_inc_complement_singleton: forall a b,
~ (inc b (complement a (singleton b))).
Proof. ir. red. ir. srwi H. nin H. elim H0. fprops.
Qed.
Lemma complement_monotone : forall a b x,
sub a x -> sub b x -> (sub a b = sub (complement x b) (complement x a)).
Proof. ir. ap iff_eq. ir. red. ir. srw. srwi H2.
ee. am. dneg. app H1.
ir. red. ir. nin (inc_or_not x0 (complement x b)).
cp (H1 _ H3). srwi H4. ee. intuition.
cp (H _ H2). app (use_complement H4 H3).
Qed.
End Complement.
Export Complement.
Module Image.
Image of a set by a function
Definition fun_image (x : Set) (f : EE) := IM (fun a : x => f (Ro a)).
Lemma inc_fun_image : forall x f a, inc a x -> inc (f a) (fun_image x f).
Proof. ir. uf fun_image. ap IM_inc. exists (Bo H). rww (B_eq H). Qed.
Lemma fun_image_rw : forall f x y,
inc y (fun_image x f) = exists z, (inc z x & f z = y).
Proof. ir. ap iff_eq; intros.
nin (IM_exists H). exists (Ro x0). split. app R_inc. tv.
induction H. induction H. wr H0. app inc_fun_image.
Qed.
Hint Rewrite fun_image_rw : aw.
End Image.
Export Image.
Module Powerset.
This is the set of all cuts, but in fact is the set of all subsets
Definition powerset (x : Set) :=
IM (fun p : x -> two_points =>
Zo x (fun y : Set => forall hyp : inc y x, p (Bo hyp) = two_points_a)).
Lemma powerset_inc : forall x y, sub x y -> inc x (powerset y).
Proof. ir. uf powerset. ap IM_inc.
exists (fun b:y =>by_cases (fun _:inc (Ro b) x => two_points_a)
(fun _:~inc (Ro b) x => two_points_b)).
set_extens. Ztac. set (H2 H1). ex_middle.
rwi by_cases_if_not e. discriminate e. rww B_eq. ir. tv.
Ztac. ir. rww by_cases_if. rww B_eq.
Qed.
Lemma powerset_sub : forall x y, inc x (powerset y) -> sub x y.
Proof. ir. ufi powerset H. nin (IM_exists H). wr H0. app Z_sub.
Qed.
Lemma powerset_inc_rw : forall x y, inc x (powerset y) = sub x y.
Proof. ir. apply iff_eq; ir. app powerset_sub. app powerset_inc. Qed.
Hint Rewrite powerset_inc_rw : aw.
Lemma inc_x_powerset_x: forall x, inc x (powerset x).
Proof. ir. aw. red; tv. Qed.
End Powerset.
Export Powerset.
Module Union.
Integral: records
p and e. Pose q = Ro p. By definition, inc q x.
Record Union_integral (x : Set) : Set :=
{Union_param : x; Union_elt : Ro Union_param}.
Union:
y is in the union if y= Ro e for some e, this is inc y q,
q defined above
Definition union (x : Set) :=
IM (fun i : Union_integral x => Ro (Union_elt i)).
Lemma union_inc : forall x y a, inc x y -> inc y a -> inc x (union a).
Proof. ir. set (w:= Bo H0). assert (Ro w = y). uf w; ap B_eq.
assert (inc x (Ro w)). rww H1. uf union. ap IM_inc.
exists (Build_Union_integral (Bo H2)). simpl. apply B_eq. Qed.
Lemma union_exists : forall x a,
inc x (union a) -> exists y, inc x y & inc y a.
Proof. ir. ufi union H. nin (IM_exists H).
exists (Ro (Union_param x0)). wr H0. split. ap R_inc. ap R_inc. Qed.
Lemma union_sub: forall x y, inc x y -> sub x (union y).
Proof. ir. red. ir. apply union_inc with x. am. am.
Qed.
Union of two sets
Definition union2 (x y : Set) := union (doubleton x y).
Lemma union2_or : forall x y a, inc a (union2 x y) -> inc a x \/ inc a y.
Proof. ir. ufi union2 H. nin (union_exists H). nin H0.
nin (doubleton_or H1) ; [ left | right ] ; wrr H2.
Qed.
Lemma union2_first : forall x y a, inc a x -> inc a (union2 x y).
Proof. ir. uf union2. apw union_inc x. fprops. Qed.
Lemma union2_second : forall x y a, inc a y -> inc a (union2 x y).
Proof. ir. uf union2. apw union_inc y. fprops. Qed.
Lemma inc_union2_rw : forall a b x,
inc x (union2 a b) = (inc x a \/ inc x b).
Proof. ir. apply iff_eq; ir. app union2_or.
induction H; [app union2_first | app union2_second].
Qed.
Lemma union2sub_first: forall a b, sub a (union2 a b).
Proof. red. ir. app union2_first. Qed.
Lemma union2sub_second: forall a b, sub b (union2 a b).
Proof. red. ir. app union2_second. Qed.
Union of
x and a single element
Definition tack_on x y := union2 x (singleton y).
Lemma tack_on_or : forall x y z, inc z (tack_on x y) ->
(inc z x \/ z = y).
Proof. ir. ufi tack_on H. set (H1:= union2_or H).
induction H1; [ left | right; awi H0]; assumption.
Qed.
Lemma tack_on_inc: forall x y z,
(inc z (tack_on x y) ) = (inc z x \/ z = y).
Proof. ir. ap iff_eq. ap tack_on_or. ir.
uf tack_on. induction H. app union2_first.
ap union2_second. wr H. fprops. Qed.
Hint Rewrite tack_on_inc : aw.
Lemma inc_tack_on_x: forall a b, inc a (tack_on b a).
Proof. ir. aw. au. Qed.
Lemma inc_tack_on_sub: forall a b, sub b (tack_on b a).
Proof. ir. red. ir. aw. au. Qed.
Lemma inc_tack_on_y: forall a b y, inc y b -> inc y (tack_on b a).
Proof. ir. aw. au. Qed.
Hint Resolve inc_tack_on_x inc_tack_on_y inc_tack_on_sub: fprops.
Lemma tack_on_when_inc: forall x y, inc y x -> tack_on x y = x.
Proof. ir. set_extens. awi H0. nin H0. am. ue. fprops.
Qed.
Lemma tack_on_sub: forall x y z, sub x z -> inc y z -> sub (tack_on x y) z.
Proof. ir. red. ir. awi H1. nin H1. app H. ue.
Qed.
Lemma tack_on_complement: forall x y, inc y x ->
x = tack_on (complement x (singleton y)) y.
Proof. ir. set_extens. nin (equal_or_not x0 y). rw H1. fprops. aw. left. srw.
split. am. dneg. awi H2. am.
awi H0. nin H0. srwi H0. nin H0. am. ue.
Qed.
Lemma sub_union : forall x z,
(forall y, inc y z -> sub y x) -> sub (union z) x.
Proof. ir. red; ir. nin (union_exists H0). ee. app (H _ H2).
Qed.
Lemma union2idem: forall x, union2 x x = x.
Proof. ir. set_extens. nin (union2_or H). am. am. app union2_first.
Qed.
Lemma union2comm: forall x y, union2 x y = union2 y x.
Proof. ir. set_extens ;
(nin (union2_or H); [app union2_second | app union2_first]).
Qed.
Lemma union2_sub: forall x y,
sub x y = (union2 x y = y).
Proof. ir. app iff_eq. ir. set_extens. nin (union2_or H0). app H. am.
app union2_second. ir. red. ir. wr H. app union2_first.
Qed.
End Union.
Export Union.
Module Intersection.
Intersection: set of all
z in rep x, that are in all elements of x;
rep x is some element of x,
its value is irrelevant, it exists if x nonempty
Definition intersection (x : Set) :=
Zo (union x) (fun y : Set => forall z : Set, inc z x -> inc y z).
Lemma intersection_inc : forall x a,
nonempty x -> (forall y, inc y x -> inc a y) -> inc a (intersection x).
Proof. ir. uf intersection. app Z_inc. nin H. apw union_inc y. app H0.
Qed.
Lemma intersection_forall :
forall x a y, inc a (intersection x) -> inc y x -> inc a y.
Proof. ir. ufi intersection H. Ztac. app H2. Qed.
Lemma intersection_sub : forall x y, inc y x -> sub (intersection x) y.
Proof. ir. uf sub. ir. apw intersection_forall x.
Qed.
Intersection of two sets
Definition intersection2 x y := intersection (doubleton x y).
Lemma intersection2_inc :
forall x y a, inc a x -> inc a y -> inc a (intersection2 x y).
Proof. ir. uf intersection2. ap intersection_inc. app nonempty_doubleton.
ir. set (H4:=doubleton_or H1). destruct H4 as [H5 | H6]; [rww H5|rww H6].
Qed.
Lemma intersection2_first :
forall x y a, inc a (intersection2 x y) -> inc a x.
Proof. ir. ufi intersection2 H.
apw intersection_forall (doubleton x y). fprops.
Qed.
Lemma intersection2_second :
forall x y a, inc a (intersection2 x y) -> inc a y.
Proof. ir. ufi intersection2 H.
apw intersection_forall (doubleton x y). fprops.
Qed.
Lemma intersection2_both: forall x y a,
inc a (intersection2 x y) -> (inc a x & inc a y).
Proof. ir. split. app (intersection2_first H). app (intersection2_second H).
Qed.
Lemma intersection2sub_first: forall a b, sub (intersection2 a b) a.
Proof. red. ir. app (intersection2_first H). Qed.
Lemma intersection2sub_second: forall a b, sub (intersection2 a b) b.
Proof. red. ir. app (intersection2_second H). Qed.
Lemma intersection2idem: forall x, intersection2 x x = x.
Proof. ir. set_extens. app (intersection2_first H). app intersection2_inc.
Qed.
Lemma intersection2comm: forall x y, intersection2 x y = intersection2 y x.
Proof. ir. set_extens ;
(app intersection2_inc; [app (intersection2_second H) |
app (intersection2_first H)]).
Qed.
Lemma intersection2_sub: forall x y,
sub x y = (intersection2 x y = x).
Proof. ir. app iff_eq. ir. set_extens. app (intersection2_first H0).
app intersection2_inc. ir. app H. red. ir. wri H H0.
app (intersection2_second H0).
Qed.
End Intersection.
Export Intersection.
Module Pair.
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.
Definition kpair x y := doubleton (singleton x) (doubleton x y).
Definition kpr1 x := union (intersection x).
Definition kpr2 x := let a := complement (union x) (intersection x) in
Yo (a = emptyset) (kpr1 x) (union a).
Lemma kpr0_pair:forall x y, intersection (kpair x y) = singleton x.
Proof. ir. uf kpr1. assert (inc (singleton x) (kpair x y)). uf kpair.
fprops. set_extens. ap (intersection_forall H0 H).
app intersection_inc. exists (singleton x). am. ir. ufi kpair H1.
nin (doubleton_or H1). ue. awi H0. rw H0. ue.
Qed.
Lemma kpr1_pair: forall x y, kpr1 (kpair x y) = x.
Proof. ir. uf kpr1. rw kpr0_pair. wr doubleton_singleton. ap (union2idem x).
Qed.
Lemma kpr2_pair: forall x y, kpr2 (kpair x y) = y.
Proof. ir. uf kpr2. rw kpr0_pair.
assert (union (kpair x y) = doubleton x y). uf kpair. set_extens.
nin (union_exists H). nin H0. nin (doubleton_or H1). rwi H2 H0. awi H0. ue.
rwi H2 H0. am. apw union_inc (doubleton x y). fprops. rw H.
nin (equal_or_not x y). wr H0. rw doubleton_singleton. rw Y_if_rw.
app kpr1_pair. rww complement_itself.
assert (complement (doubleton x y) (singleton x) = singleton y). set_extens.
srwi H1. nin H1. nin (doubleton_or H1). awi H2. contradiction. ue.
srw. awi H1. rw H1. split. fprops. aw. int. rw H1.
rw Y_if_not_rw. wr doubleton_singleton. ap (union2idem y). red. ir.
empty_tac1 (y).
Qed.
Lemma kpr1_def : forall a b c d, kpair a b = kpair c d -> a = c.
Proof. ir. transitivity (kpr1 (kpair a b)). rww kpr1_pair. rw H. rww kpr1_pair. Qed.
Lemma kpr2_def : forall a b c d, kpair a b = kpair c d -> b = d.
Proof. ir. transitivity (kpr2 (kpair a b)). rww kpr2_pair. rw H. rww kpr2_pair. Qed.
Definition is_kpair (u : Set) := exists x, exists y, u = kpair x y.
Lemma kpair_recov : forall u, is_kpair u -> kpair (kpr1 u) (kpr2 u) = u.
Proof. uf is_kpair. ir. nin H. nin H. rw H. rww kpr1_pair. rww kpr2_pair.
Qed.
Lemma pair_is_kpair : forall x y : Set, is_kpair (kpair x y).
Proof. uf is_kpair. ir. exists x. exists y. tv. Qed.
Parameter pair_constructor : Set -> Set -> Set.
Notation J := pair_constructor.
Axiom axiom_of_pair : forall x y x' y' : Set,
(J x y = J x' y') -> (x = x' & y = y').
Definition is_pair (u : Set) := exists x, exists y, u = J x y.
Definition pair_first (x y:Set):= singleton x.
Definition pair_second (x y:Set):= doubleton emptyset (singleton y).
Definition bpair_x (x y : Set) :=
doubleton (pair_first x y) (pair_second x y).
Lemma pair_distincta:forall x y z w,
pair_first x y <> pair_second z w.
Proof. ir. uf pair_first ; uf pair_second. red. ir.
assert (inc emptyset (singleton x)). rw H. fprops. awi H0.
assert (inc (singleton w) (singleton x)). rw H. fprops. awi H1.
empty_tac1 w. wr H1. fprops.
Qed.
Lemma pair_distinct:forall x y,
pair_second x y <> pair_first x y.
Proof. ir. red. ir. symmetry in H. app (pair_distincta H).
Qed.
Lemma pr1_injective_x : forall x y z w : Set,
bpair_x x y = bpair_x z w -> x = z.
Proof. ir. assert (pair_first x y = pair_first z w).
assert (inc (pair_first x y) (bpair_x z w)). wr H. uf bpair_x. fprops.
ufi bpair_x H0. db_tac. elim (pair_distincta H1).
ufi pair_first H0. app singleton_inj.
Qed.
Lemma pr2_injective_x : forall x y z w,
bpair_x x y = bpair_x z w -> y = w.
Proof. ir. assert (pair_second x y = pair_second z w).
assert (inc (pair_second x y) (bpair_x z w)). wr H. uf bpair_x. fprops.
ufi bpair_x H0. db_tac.
symmetry in H1. elim (pair_distincta H1). ufi pair_second H0.
assert (inc (singleton y) (doubleton emptyset (singleton w))). wrr H0.
fprops. nin (doubleton_or H1).
assert (inc y emptyset). wr H2. fprops. nin H3. elim x0. app singleton_inj.
Qed.
Lemma pr1_def : forall x y z w : Set,
J x y = J z w -> x = z.
Proof. ir. nin (axiom_of_pair H). am.
Qed.
Lemma pr2_def : forall x y z w,
J x y = J z w -> y = w.
Proof. ir. nin (axiom_of_pair H). am.
Qed.
First and second projections,
pr1 and pr2, denoted P and Q
Definition P (u : Set) :=
choose (fun x : Set => exists y : Set, u = J x y).
Definition Q (u : Set) :=
choose (fun y : Set => exists x : Set, u = J x y).
Lemma pair_recov : forall u, is_pair u -> J (P u) (Q u) = u.
Proof. uf is_pair. ir.
assert (exists y : Set, exists x : Set, u = J x y). nin H; nin H.
exists x0. exists x. am. nin (choose_pr H). nin (choose_pr H0).
assert (u = J (P u) x). am. assert (u = J x0 (Q u)). am.
assert (J (P u) x = J x0 (Q u)). wrr H3. rw (pr1_def H5). sy; am.
Qed.
Lemma pair_is_pair : forall x y : Set, is_pair (J x y).
Proof. uf is_pair. ir. exists x. exists y. tv. Qed.
Hint Resolve pair_is_pair: fprops.
Hint Rewrite pair_recov : aw.
Lemma is_pair_rw : forall x, is_pair x = (x = J (P x) (Q x)).
Proof. ir. ap iff_eq;ir. sy. aw. rw H. fprops.
Qed.
Lemma pr1_pair : forall x y, P (J x y) = x.
Proof. ir. cp (pair_is_pair x y). rwi is_pair_rw H. sy. ap (pr1_def H).
Qed.
Lemma pr2_pair : forall x y, Q (J x y) = y.
Proof. ir. cp (pair_is_pair x y). rwi is_pair_rw H. sy. ap (pr2_def H).
Qed.
Hint Rewrite pr1_pair pr2_pair : aw.
Lemma pair_extensionality : forall a b,
is_pair a -> is_pair b -> P a = P b -> Q a = Q b -> a = b.
Proof. ir. transitivity (J (P a) (Q a)). sy. aw. rw H1. rw H2. aw.
Qed.
V x f 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, otherwise it is the empty set.
Definition V (x f : Set) := choose (fun y : Set => inc (J x y) f).
Lemma V_inc : forall x z f,
(exists y, inc (J x y) f) -> z = V x f -> inc (J x z) f.
Proof. ir. rw H0. ap (choose_pr H). Qed.
Lemma V_or : forall x f,
(inc (J x (V x f)) f) \/
((forall z, ~(inc (J x z) f)) & (V x f = emptyset)).
Proof. ir. nin (p_or_not_p (ex (fun y=> inc (J x y) f))).
left. app V_inc. right. split. ir. dneg. exists z. am.
unfold V. app choose_not.
Qed.
End Pair.
Export Pair.
Ltac inter2tac :=
match goal with
| H:inc ?X1 (intersection2 ?X2 _ ) |- inc ?X1 ?X2
=> ap (intersection2_first H)
| H:inc ?X1 (intersection2 _ ?X2 ) |- inc ?X1 ?X2
=> ap (intersection2_second H)
| H:inc ?X1 ?X2 |- inc ?X1 (union2 ?X2 _)
=> app union2_first
| H:inc ?X1 ?X2 |- inc ?X1 (union2 _ ?X2)
=> app union2_second
| |- inc _ (intersection2 _ _ )
=> app intersection2_inc
| H:J _ _ = J _ _ |- _
=> solve [ rww (pr1_def H);fprops | rww (pr2_def H) ; fprops]
| H1: is_pair ?x, H2: is_pair ?y |- ?x = ?y => app pair_extensionality
end.
This is the set of all pairs
J x y with x in A, y in B
Module Cartesian.
Definition product (A B : Set) :=
union (fun_image A (fun x => (fun_image B (fun y => J x y)))).
Lemma product_inc_rw : forall x y z,
inc x (product y z) = (is_pair x & inc (P x) y & inc (Q x) z).
Proof. ir. uf product. app iff_eq. ir. nin (union_exists H). nin H0.
awi H1. nin H1. nin H1. wri H2 H0. awi H0. nin H0. nin H0.
wr H3. ee. fprops. aw. aw.
ir. ee. apply union_inc with (fun_image z (fun y : Set => J (P x) y)).
aw. exists (Q x). split. am. aw. aw. exists (P x). eee.
Qed.
Hint Rewrite product_inc_rw : aw.
Lemma product_pr :forall a b u,
inc u (product a b) -> (is_pair u & inc (P u) a & inc (Q u) b).
Proof. ir. wrr product_inc_rw.
Qed.
Lemma product_inc : forall a b u,
is_pair u -> inc (P u) a -> inc (Q u) b -> inc u (product a b).
Proof. ir. aw. au.
Qed.
Lemma product_pair_pr :
forall a b x y : Set, inc (J x y) (product a b) -> (inc x a & inc y b).
Proof. ir. awi H. intuition.
Qed.
Lemma product_pair_inc :
forall a b x y, inc x a -> inc y b -> inc (J x y) (product a b).
Proof. ir. aw. eee.
Qed.
Lemma pair_in_product: forall a b c, inc a (product b c) -> is_pair a.
Proof. ir. awi H. nin H. am.
Qed.
Hint Resolve product_pair_inc: fprops.
A product is empty if and only one factor is empty
Lemma empty_product1: forall y,
product emptyset y = emptyset.
Proof. ir. empty_tac. awi H. ee. app (emptyset_pr H0).
Qed.
Lemma empty_product2: forall x,
product x emptyset = emptyset.
Proof. ir. empty_tac. awi H. ee. app (emptyset_pr H1).
Qed.
Lemma empty_product_pr: forall x y,
product x y = emptyset -> (x = emptyset \/ y= emptyset).
Proof. ir. nin (emptyset_dichot x). left. am. right. nin H0.
empty_tac. assert (inc (J y0 y1) (product x y)). fprops.
rwi H H2. elim (emptyset_pr H2).
Qed.
Hint Rewrite empty_product2 empty_product1 : sw.
The product A*B is increasing in A and B, strictly if the other argument
is non empty.
Lemma product_monotone_left: forall x x' y,
sub x x' -> sub (product x y) (product x' y).
Proof. ir. red. ir. awi H0. ee. aw. ee. am. app H. am.
Qed.
Lemma product_monotone_right: forall x y y',
sub y y' -> sub (product x y) (product x y').
Proof. ir. red. ir. awi H0. ee. aw. eee.
Qed.
Lemma product_monotone: forall x x' y y',
sub x x' -> sub y y' -> sub (product x y) (product x' y').
Proof. ir. apply sub_trans with (product x' y). app product_monotone_left.
app product_monotone_right.
Qed.
Lemma product_monotone_left2: forall x x' y, nonempty y ->
sub (product x y) (product x' y) -> sub x x'.
Proof. ir. red. ir. nin H. assert (inc (J x0 y0) (product x' y)). app H0.
fprops. awi H2. ee. am.
Qed.
Lemma product_monotone_right2: forall x y y', nonempty x ->
sub (product x y) (product x y') -> sub y y'.
Proof. ir. red. ir. nin H. assert (inc (J y0 x0) (product x y')). app H0.
fprops. awi H2. ee. am.
Qed.
End Cartesian.
Export Cartesian.
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 is_graph r := forall y, inc y r -> is_pair y.
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 :=
is_graph f & (forall x y, inc x f -> inc y f -> P x = P y -> x = y).
Lemma fgraph_is_graph : forall f, fgraph f -> is_graph f.
Proof. ir. nin H. am. Qed.
Lemma fgraph_pr: forall f x y y',
fgraph f -> inc (J x y) f -> inc (J x y') f -> y = y'.
Proof. ir. nin H. assert (P (J x y) = P (J x y')). aw.
cp (H2 _ _ H0 H1 H3). inter2tac.
Qed.
Hint Resolve fgraph_is_graph : fprops.
We give here some properties of the domain and range
Lemma inc_pr1_domain : forall f x,
inc x f -> inc (P x) (domain f).
Proof. ir. uf domain. app inc_fun_image.
Qed.
Lemma inc_pr2_range : forall f x,
inc x f -> inc (Q x) (range f).
Proof. ir. uf range. app inc_fun_image.
Qed.
Lemma domain_rw: forall r x,
is_graph r ->
inc x (domain r) = (exists y, inc (J x y) r).
Proof. ir. uf domain. aw. app iff_eq. ir.
nin H0. ee. exists (Q x0). wr H1. aw. app H.
ir. nin H0. exists (J x x0). ee. am. aw.
Qed.
Lemma range_rw: forall r y,
is_graph r -> inc y (range r) = (exists x, inc (J x y) r).
Proof. ir. uf range. aw. app iff_eq. ir.
nin H0. ee. exists (P x). wr H1. aw. app H.
ir. nin H0. exists (J x y). ee. am. aw.
Qed.
Ltac ex_tac:=
match goal with
| H:inc (J ?x ?y) ?z |- exists x, inc (J x ?y) ?z
=> exists x ; am
| H:inc (J ?x ?y) ?z |- exists y, inc (J ?x y) ?z
=> exists y ; am
| H:inc (J ?x ?y) ?z |- exists x, _ & inc (J x ?y) ?z
=> exists x ; split; tv
| H:inc (J ?x ?y) ?z |- exists y, _ & inc (J ?x y) ?z
=> exists y ; split; tv
| H:inc (J ?x ?y) ?z |- exists x, inc (J x ?y) ?z & _
=> exists x ; split; tv
| H:inc (J ?x ?y) ?z |- exists y, inc (J ?x y) ?z & _
=> exists y ; split; tv
| H:inc ?x ?y |- exists x, inc x ?y & _
=> exists x ; split; tv
| |- exists x, inc x (singleton ?y) & _
=> exists y ; split; fprops
| H : inc (J ?x ?y) ?g |- inc ?x (domain ?g)
=> rww domain_rw; exists y ;am
| H : inc (J ?x ?y) ?g |- inc ?y (range ?g)
=> rww range_rw; exists x;am
| H : inc ?x ?y |- nonempty ?y
=> exists x;am
| |- exists y, inc (J (P ?x) y) _
=> exists (Q x) ; aw
| |- exists y, inc (J y (Q ?x)) _
=> exists (P x) ; aw
end.
Hint Rewrite range_rw domain_rw : aw.
The function
V is well-defined for function graphs.
Here are some properties
Lemma fdomain_pr1 : forall f x,
fgraph f -> inc x (domain f) -> inc (J x (V x f)) f.
Proof. ir. awi H0. ap (choose_pr H0). fprops.
Qed.
Lemma in_graph_V : forall f x,
fgraph f -> inc x f -> x = J (P x) (V (P x) f).
Proof. ir. ee. set H. nin f0. app H2. app fdomain_pr1.
app inc_pr1_domain. aw.
Qed.
Lemma pr2_V : forall f x,
fgraph f -> inc x f -> Q x = V (P x) f.
Proof. ir. rw (in_graph_V H H0). aw.
Qed.
Lemma frange_inc_rw : forall f y,
fgraph f -> inc y (range f) = (exists x, inc x (domain f) & y = V x f).
Proof. ir. set (fgraph_is_graph H). aw. ap iff_eq; ir; nin H0; exists x.
split. ex_tac. set (in_graph_V H H0). awi e. inter2tac.
nin H0. set (fdomain_pr1 H H0). ue.
Qed.
Hint Rewrite frange_inc_rw : sw.
Lemma inc_V_range: forall f x,
fgraph f -> inc x (domain f) -> inc (V x f) (range f).
Proof. ir. srw. exists x. eee.
Qed.
Case of a subgraph
Lemma sub_graph_fgraph : forall f g, fgraph g -> sub f g -> fgraph f.
Proof. ir. split. red. ir. nin H. app H. app H0.
ir. nin H. app H4; app H0.
Qed.
Lemma sub_graph_domain : forall f g, sub f g -> sub (domain f) (domain g).
Proof. ir. uf domain. red. ir. awi H0. aw.
nin H0. nin H0. exists x0. split. ap H. am. am.
Qed.
Lemma sub_graph_range : forall f g, sub f g -> sub (range f) (range g).
Proof. ir. uf range. red. ir. awi H0. aw.
nin H0. nin H0. set (H _ H0). ex_tac.
Qed.
Lemma sub_graph_ev: forall f g x,
fgraph g -> sub f g -> inc x (domain f) -> V x f = V x g.
Proof. ir. set (sub_graph_fgraph H H0).
set (sub_graph_domain H0). set (s _ H1).
set (fdomain_pr1 f0 H1). set (H0 _ i0). set (in_graph_V H i1).
awi e. inter2tac.
Qed.
Lemma fgraph_sub : forall f g,
fgraph f -> fgraph g -> sub (domain f) (domain g) ->
(forall x, inc x (domain f) -> V x f = V x g) -> sub f g.
Proof. ir. red. ir. rw (in_graph_V H H3). set (inc_pr1_domain H3).
rww H2. app fdomain_pr1. app H1.
Qed.
Two functional graphs are equal if they have the same domain and evaluation
Lemma fgraph_exten: forall f g,
fgraph f -> fgraph g -> domain f = domain g ->
(forall x, inc x (domain f) -> V x f = V x g) -> f = g.
Proof. ir. app extensionality; app fgraph_sub. ue. ue.
wr H1. ir. sy. app H2.
Qed.
Lemma range_union2: forall a b, range (union2 a b) = union2 (range a) (range b).
Proof. ir. uf range. set_extens. awi H. nin H. nin H. nin (union2_or H).
app union2_first. aw. ex_tac. app union2_second. aw. ex_tac.
aw. nin (union2_or H); awi H0; nin H0; nin H0; exists x0; split.
app union2_first. am. app union2_second. am.
Qed.
Lemma domain_union2: forall a b,
domain (union2 a b) = union2 (domain a) (domain b).
Proof. ir. uf domain. set_extens. awi H. nin H. nin H. nin (union2_or H).
app union2_first. aw. ex_tac. app union2_second. aw. ex_tac.
aw. nin (union2_or H); awi H0; nin H0; nin H0; exists x0; split.
app union2_first. am. app union2_second. am.
Qed.
Lemma fgraph_union2: forall a b, fgraph a -> fgraph b ->
intersection2 (domain a) (domain b) = emptyset ->
fgraph (union2 a b).
Proof. ir. red. nin H; nin H0. split. red. ir. nin (union2_or H4). app H.
app H0. ir. nin (union2_or H4). nin (union2_or H5). app H2.
assert (inc (P x) (domain a)). uf domain. aw. ex_tac.
assert (inc (P y) (domain b)). uf domain. aw. ex_tac. rwi H6 H9.
empty_tac1 (P y). app intersection2_inc.
nin (union2_or H5).
assert (inc (P x) (domain b)). uf domain. aw. ex_tac.
assert (inc (P y) (domain a)). uf domain. aw. ex_tac. rwi H6 H9.
empty_tac1 (P y). app intersection2_inc. app H3.
Qed.
Inverse image of a set by a graph
Definition inverse_image (a f : Set) :=
Zo (domain f) (fun x => inc (V x f) a).
Lemma inverse_image_sub :
forall a f, sub (inverse_image a f) (domain f).
Proof. uf inverse_image. ir. apply Z_sub.
Qed.
Lemma inverse_image_inc : forall a f x,
inc x (domain f) -> inc (V x f) a -> inc x (inverse_image a f).
Proof. ir. uf inverse_image. Ztac. Qed.
Lemma inverse_image_pr :
forall a f x, inc x (inverse_image a f) -> inc (V x f) a.
Proof. ir. ufi inverse_image H. Ztac. am.
Qed.
Graph associated to a function restricted to some set as domain.
Definition graph_constructor (x : Set) (p : EE) :=
fun_image x (fun y => J y (p y)).
Notation L := graph_constructor.
Lemma L_fgraph : forall p x, fgraph (L x p).
Proof. ir. uf fgraph. uf L. split; ir. red. ir. awi H. nin H. nin H. wr H0.
fprops. awi H. awi H0. nin H. nin H0. ee. wri H3 H1; wri H2 H1. awi H1.
wr H2; wr H3; wrr H1.
Qed.
Lemma L_domain : forall x p, domain (L x p) = x.
Proof. ir. uf domain. set_extens. awi H. nin H; ee.
ufi L H; awi H; nin H; ee. wr H0; wr H1; aw.
aw. exists (J x0 (p x0)). uf L. aw. split. ex_tac. tv.
Qed.
Hint Rewrite L_domain : bw.
Hint Resolve L_fgraph: gprops.
Lemma L_V_rewrite : forall x p y, inc y x -> V y (L x p) = p y.
Proof. ir. set (f := L x p).
assert (inc (J y (p y)) f). uf f. uf L. aw. ex_tac.
assert (inc (J y (V y f)) f). app V_inc. ex_tac.
assert (fgraph f). uf f. gprops. app (fgraph_pr H2 H1 H0).
Qed.
Hint Rewrite L_V_rewrite : bw.
Lemma L_range : forall p x,
range (L x p) = fun_image x p.
Proof. ir. uf range. uf L. set_extens; awi H; nin H; ee.
awi H; nin H; ee. aw. ex_tac. wr H0. wr H1. aw.
aw. exists (J x1 x0). split. aw. ex_tac. ue. aw.
Qed.
Lemma L_recovers : forall f,
fgraph f -> L (domain f) (fun x => V x f) = f.
Proof. ir. app fgraph_exten. gprops. bw. bw. ir. bw.
Qed.
Two fgraphs are equal if their domain and function are the same.
Lemma L_exten1 : forall a b f g,
a = b -> (forall x, inc x a -> f x = g x) ->
L a f = L b g.
Proof. ir. app fgraph_exten. gprops. gprops. bw. bw. ir. bw. app H0. ue.
Qed.
Lemma L_create : forall a f,
L a (fun x => V x (L a f)) = L a f.
Proof. ir. app L_exten1. ir. bw.
Qed.
Lemma L_range_rw: forall sf f a,
inc a (range (L sf f)) = exists b, inc b sf & f b = a.
Proof. ir. rw L_range. app iff_eq. ir. awi H. am. ir. aw.
Qed.
Hint Rewrite L_range_rw : bw.
Lemma L_V_out : forall x f y,
~inc y x -> V y (L x f) = emptyset.
Proof. ir. nin (V_or y (L x f)).
set (inc_pr1_domain H0). rwi pr1_pair i. bwi i. contradiction. intuition.
Qed.
Composition of two graphs. If the graphs are composable, we can simplify the definition
Definition fcomposable (f g : Set) :=
fgraph f & fgraph g & sub (range g) (domain f).
Definition fcompose (f g : Set) :=
L (inverse_image (domain f) g) (fun y => V (V y g) f).
Definition gcompose g f := L (domain f) (fun y => V (V y f) g).
Lemma fcompose_fgraph : forall f g, fgraph (fcompose f g).
Proof. ir. uf fcompose. gprops. Qed.
Lemma fcompose_domain :
forall f g, domain (fcompose f g) = inverse_image (domain f) g.
Proof. ir. uf fcompose. bw. Qed.
Lemma fcompose_range: forall f g, fgraph f ->
sub (range (fcompose f g)) (range f).
Proof. ir. red. ir. uf range. aw. ufi fcompose H0. bwi H0.
nin H0. nin H0. awi H0. set (inverse_image_pr H0). awi i. nin i.
ex_tac. rw (pr2_V H H2). aw. fprops.
Qed.
Lemma fcomposable_domain :
forall f g, fcomposable f g -> domain (fcompose f g) = domain g.
Proof. ir. uf fcompose. bw. ap extensionality.
ap inverse_image_sub. uf sub; ir. app inverse_image_inc.
red in H. ee. app H2. app inc_V_range.
Qed.
Lemma fcompose_ev : forall x f g,
inc x (domain (fcompose f g)) -> V x (fcompose f g) = V (V x g) f.
Proof. uf fcompose. ir. bwi H. bw.
Qed.
Lemma fcompose_ev1 : forall x f g, fcomposable f g ->
inc x (domain g) -> V x (fcompose f g) = V (V x g) f.
Proof. ir. app fcompose_ev. rw fcomposable_domain. am. am.
Qed.
Hint Rewrite fcompose_ev1 : bw.
Lemma alternate_compose: forall g f,
fcomposable g f -> gcompose g f = fcompose g f.
Proof. ir. uf gcompose. app fgraph_exten. gprops.
app fcompose_fgraph. bw. rww fcomposable_domain. bw. ir. bw.
Qed.
Graph of the identity function.
Definition identity_g (x : Set) := L x (fun y => y).
Lemma identity_fgraph : forall x, fgraph (identity_g x).
Proof. ir. uf identity_g. gprops.
Qed.
Lemma identity_domain : forall x, domain (identity_g x) = x.
Proof. ir. uf identity_g. bw.
Qed.
Lemma identity_ev : forall x a, inc x a -> V x (identity_g a) = x.
Proof. ir. uf identity_g. bw. Qed.
restriction of a graph to a set
Definition restr f x :=
Zo f (fun y=> inc (P y) x).
Lemma restr_inc_rw : forall f x y,
inc y (restr f x) = (inc y f & inc (P y) x).
Proof. ir. uf restr. ap iff_eq; ir; ee; Ztac; tv. Qed.
Hint Rewrite restr_inc_rw : aw.
Lemma restr_sub : forall f x, sub (restr f x) f.
Proof. ir. uf sub. ir. awi H. intuition.
Qed.
Lemma restr_fgraph : forall f x,
fgraph f -> fgraph (restr f x).
Proof. ir. eapply sub_graph_fgraph. eexact H. app restr_sub.
Qed.
Lemma restr_graph: forall x r,
is_graph r -> is_graph (restr r x).
Proof. ir. red. ir. awi H0. nin H0. app H.
Qed.
Hint Resolve restr_graph restr_fgraph : fprops.
Lemma restr_domain : forall f x, fgraph f ->
domain (restr f x) = intersection2 (domain f) x.
Proof. ir. uf domain. uf restr. set_extens. awi H0. nin H0; ee. Ztac.
wr H1. app intersection2_inc. aw. ex_tac.
nin (intersection2_both H0). aw. awi H1. nin H1. nin H1.
exists x1. split. Ztac. ue. am.
Qed.
Lemma restr_domain1 : forall f x,
fgraph f -> sub x (domain f) ->
domain (restr f x) = x.
Proof. ir. rww restr_domain. set_extens. inter2tac. app intersection2_inc.
app H0.
Qed.
Lemma fgraph_sub_eq : forall r s,
fgraph r -> fgraph s -> sub r s ->
sub (domain s) (domain r) -> r = s.
Proof. ir. app extensionality. uf sub. ir.
rewrite (in_graph_V H0 H3) in H3 |- *.
set (inc_pr1_domain H3). rwi pr1_pair i. set (H2 _ i).
assert (inc (J (P x) (V (P x) r)) r). app fdomain_pr1.
red in H0. ee. rww (H5 _ _ H3 (H1 _ H4)). aw.
Qed.
Lemma restr_to_domain : forall f g,
fgraph f -> fgraph g -> sub f g ->
restr g (domain f) = f.
Proof. ir. sy. app fgraph_sub_eq. fprops.
unfold sub. ir. uf restr; app Z_inc. app H1. app inc_pr1_domain.
rww restr_domain. uf sub;ir. inter2tac.
Qed.
Lemma restr_ev : forall f u x,
fgraph f -> sub u (domain f) -> inc x u ->
V x (restr f u) = V x f.
Proof. ir. assert (inc (J x (V x f)) f). app fdomain_pr1. app H0.
assert (inc (J x (V x f)) (restr f u)).
uf restr; Ztac. aw.
assert (fgraph (restr f u)). fprops. set (pr2_V H4 H3).
awi e. sy. am.
Qed.
Lemma restr_ev1 : forall f u x,
fgraph f -> inc x (domain f) -> inc x u ->
V x (restr f u) = V x f.
Proof. ir. assert (inc (J x (V x f)) f). app fdomain_pr1.
assert (inc (J x (V x f)) (restr f u)).
uf restr; Ztac. aw.
assert (fgraph (restr f u)). fprops. set (pr2_V H4 H3).
awi e. sy. am.
Qed.
Hint Rewrite restr_ev : bw.
Lemma restr_to_domain2 : forall x f,
fgraph f -> sub x (domain f) ->
L x (fun i => V i f) = restr f x.
Proof. ir. app fgraph_exten. gprops. fprops. bw. rww restr_domain1. bw.
ir. bw.
Qed.
Lemma double_restr: forall f a b, fgraph f ->
sub a b -> sub b (domain f) ->
(restr (restr f b) a) = (restr f a).
Proof. ir. uf restr. set_extens. Ztac. clear H2. Ztac. am.
Ztac. clear H2. Ztac.
Qed.
Other properties of graphs
Lemma fgraph_sub_V : forall f g x,
fgraph g -> inc x (domain f) -> sub f g -> V x f = V x g.
Proof. ir. set (sub_graph_fgraph H H1).
set (H1 _ (fdomain_pr1 f0 H0)). set (in_graph_V H i). awi e.
inter2tac.
Qed.
Restrictions
Definition is_restriction (f g :Set) :=
fgraph g & exists x, f = restr g x.
Lemma is_restriction_pr: forall f g,
is_restriction f g =
(fgraph f & fgraph g & sub f g).
Proof. ir. uf is_restriction. app iff_eq. ir. ee.
nin H0. rw H0. fprops. am. nin H0. rw H0. uf restr. app Z_sub.
ir. ee. am. set (sub_graph_domain H1). exists (domain f). app fgraph_exten.
fprops. rww restr_domain1. ir. bw. app sub_graph_ev.
Qed.
Union of graphs
Lemma domain_union : forall z, domain (union z) =
union (fun_image z domain).
Proof. ir. uf domain. set_extens. awi H. nin H. ee.
nin (union_exists H). ee. apw union_inc (domain x1).
uf domain. aw. ex_tac.
aw. ex_tac.
nin (union_exists H). nin H0. awi H1. nin H1; ee.
aw. wri H2 H0. awi H0. nin H0. nin H0. exists x2. ee. apw union_inc x1. am.
Qed.
Lemma tack_on_domain : forall f x y,
domain (tack_on f (J x y)) = tack_on (domain f) x.
Proof. ir. uf domain. set_extens. awi H. nin H; ee.
rwi tack_on_inc H. rw tack_on_inc; aw. nin H. left. exists x1. split; am.
right. wr H0; rw H. aw.
aw. rwi tack_on_inc H; nin H. awi H. nin H;ee.
exists x1. split. rw tack_on_inc. left; am. am.
exists (J x y). split. rw tack_on_inc; right; tv. aw. sy; am.
Qed.
Lemma range_union : forall z, range (union z) =
union (fun_image z range).
Proof. ir. set_extens.
ufi range H. awi H. nin H. nin H. induction (union_exists H). nin H1.
apw union_inc (range x1). uf range. aw.
exists x0; split; am. aw. exists x1. split. am. tv.
induction (union_exists H). ee. awi H1. nin H1. nin H1.
wri H2 H0. ufi range H0. awi H0. nin H0. ee. uf range. aw. exists x2. split.
apw union_inc x1. am.
Qed.
Lemma tack_on_range : forall f x y,
range (tack_on f (J x y)) = tack_on (range f) y.
Proof. uf range. ir. set_extens. awi H; nin H. ee.
rw tack_on_inc. rwi tack_on_inc H; nin H.
left; aw; exists x1; eee. right; wr H0; rw H;rw pr2_pair; tv.
awi H. nin H. nin H. nin H.
aw. exists x1. eee.
aw. exists (J x y). aw. symmetry in H. au.
Qed.
Lemma tack_on_fgraph : forall f x y,
fgraph f -> ~ inc x (domain f) ->
fgraph (tack_on f (J x y)).
Proof. ir. uf fgraph. ufi fgraph H. ee.
red. ir. rwi tack_on_inc H2. nin H2. app H. ue.
ir. awi H2. awi H3. nin H2; nin H3. app H1.
rwi H3 H4. awi H4. elim H0. wr H4. apply (inc_pr1_domain H2).
elim H0. rwi H2 H4. awi H4. rw H4. apply (inc_pr1_domain H3). ue.
Qed.
We create a function given a set
x and a map f : x->Set
Definition tcreate (x:Set) (f:x->Set) :=
L x (fun y => (Yy (fun (hyp : inc y x) => f (Bo hyp)) emptyset)).
Lemma tcreate_value_type : forall (x:Set) (f:x->Set) y,
V (Ro y) (tcreate f) = f y.
Proof. ir. assert (inc (Ro y) x). app R_inc. uf tcreate. bw.
apply Yy_if with H. ir. rw B_back. rww B_back. rww B_back.
Qed.
Lemma tcreate_value_inc : forall (x:Set) (f:x->Set) y (hyp : inc y x),
V y (tcreate f) = f (Bo hyp).
Proof. ir. assert (y = Ro (Bo hyp)). rw B_eq. tv.
transitivity (V (Ro (Bo hyp)) (tcreate f)). wr H; tv. ap tcreate_value_type.
Qed.
Lemma tcreate_domain : forall (x:Set) (f:x->Set), domain (tcreate f) = x.
Proof. ir. uf tcreate. bw.
Qed.
End Function.
Export Function.