Library sset1
Fundamental set theory
Original file by Carlos Simpson (CNRS/UNSA)Copyright INRIA (2009-2011) Apics Team (Jose Grimm).
Require Import ssreflect ssrbool eqtype ssrnat ssrfun.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
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.
Extensionality for sets
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.
move => P; apply excluded_middle => nor.
suff : ~ P by move=> q; apply nor; right.
by move=> p; apply nor; left.
Qed.
Lemma equal_or_not: forall x y:Set, x = y \/ x<> y.
Proof. move => x y; apply p_or_not_p. Qed.
Lemma inc_or_not: forall x y:Set, inc x y \/ ~ (inc x y).
Proof. move => x y; apply p_or_not_p. Qed.
End Axioms.
Export Axioms.
Module Tactics1.
Infix "&":= and (right associativity, at level 100).
Ltac dneg u := match goal with
H : ~ _ |- ~ _ => move => u; move :H; apply
end.
Ltac ex_middle u := match goal with
| |- inc ?a ?b => case (inc_or_not a b) ; [ done | move => u]
| |- ?a = ?b => case (equal_or_not a b) ; [ done | move => u ]
| |- ?p => case (p_or_not_p p) ; [ done | move => u ]
end.
Ltac EasyDeconj :=
match goal with
| |- (_ & _) => apply conj; [ EasyDeconj | EasyDeconj ]
| |- _ => try solve [intuition]
end.
Ltac EasyDeconj1 :=
match goal with
| |- (_ & _) => apply conj; [ EasyDeconj1 | EasyDeconj1 ]
| |- _ => try exact
end.
Ltac eee := EasyDeconj1.
Ltac ee := EasyDeconj.
Infix "&":= and (right associativity, at level 100).
Ltac dneg u := match goal with
H : ~ _ |- ~ _ => move => u; move :H; apply
end.
Ltac ex_middle u := match goal with
| |- inc ?a ?b => case (inc_or_not a b) ; [ done | move => u]
| |- ?a = ?b => case (equal_or_not a b) ; [ done | move => u ]
| |- ?p => case (p_or_not_p p) ; [ done | move => u ]
end.
Ltac EasyDeconj :=
match goal with
| |- (_ & _) => apply conj; [ EasyDeconj | EasyDeconj ]
| |- _ => try solve [intuition]
end.
Ltac EasyDeconj1 :=
match goal with
| |- (_ & _) => apply conj; [ EasyDeconj1 | EasyDeconj1 ]
| |- _ => try exact
end.
Ltac eee := EasyDeconj1.
Ltac ee := EasyDeconj.
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; trivial.
Ltac dw := autorewrite with dw; trivial.
Ltac awi u:= autorewrite with aw in u.
Ltac bw := autorewrite with bw; trivial.
Ltac srw:= autorewrite with sw; trivial.
Ltac fprops := auto with fprops.
Ltac gprops := auto with gprops.
Ltac set_extens v:= apply extensionality=> v.
End Tactics1.
Export Tactics1.
Ltac dw := autorewrite with dw; trivial.
Ltac awi u:= autorewrite with aw in u.
Ltac bw := autorewrite with bw; trivial.
Ltac srw:= autorewrite with sw; trivial.
Ltac fprops := auto with fprops.
Ltac gprops := auto with gprops.
Ltac set_extens v:= apply extensionality=> v.
End Tactics1.
Export Tactics1.
exists_unique p says there a unique x such that (p x)
Defines strict_sub as strict subset.
Definition strict_sub (a b : Set) := (sub a b) & (a <> b).
Lemma sub_trans : forall a b c, sub a b -> sub b c -> sub a c.
Proof. by move => a b c sab sbc x xa; apply sbc; apply sab. Qed.
Lemma sub_refl : forall x, sub x x.
Proof. by move =>x. Qed.
Lemma strict_sub_trans1 :
forall a b c, strict_sub a b -> sub b c -> strict_sub a c.
Proof.
move => a b c [sab nab] sbc.
split; first by apply: (sub_trans sab).
by dneg nac; move: sab sbc; rewrite nac; apply extensionality.
Qed.
Lemma strict_sub_trans2 :
forall a b c, sub a b -> strict_sub b c -> strict_sub a c.
Proof.
move => a b c sab [sbc nbc].
split; first by apply: (sub_trans sab).
by dneg nac; 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 inc_nonempty : forall x y, inc x y -> nonemptyT y.
Proof. by move=> _ y [ w _ ]; apply nonemptyT_intro. Qed.
Lemma nonemptyT_not_empty : forall x:Set, nonemptyT x -> ~ empty x.
Proof. by move=> x [ w ] Ex; apply: (Ex (Ro w)(R_inc w)). Qed.
Lemma nonemptyT_not_empty0 : forall x:Set, nonemptyT x = nonempty x.
Proof.
move => x; apply iff_eq; move => [w].
by exists (Ro w); exists w.
by apply: inc_nonempty.
Qed.
Lemma emptyset_pr: forall x, ~ inc x emptyset.
Proof. move=> _ [[]]. Qed.
Lemma is_emptyset: forall x, (forall y, ~ (inc y x)) -> x = emptyset.
Proof.
by move => x Iyx; set_extens t => Ht; [ case (Iyx t) | case (emptyset_pr Ht) ].
Qed.
Lemma not_nonempty_empty: nonempty emptyset -> False.
Proof. move=>[y]; case; case. Qed.
Lemma emptyset_dichot : forall x, (x = emptyset \/ nonempty x).
Proof.
move=> x; case: (p_or_not_p (nonempty x)) => [He | Hne]; first by auto.
by left; apply is_emptyset => y Hy; apply Hne; exists y.
Qed.
Lemma nonempty_or_empty: forall x, nonempty x = (x <> emptyset).
Proof.
move=> x; apply iff_eq.
move=> [y [yx _]] xe; move: yx; rewrite xe; case.
by move=> xne; case (emptyset_dichot x).
Qed.
Ltac empty_tac0 :=
match goal with
| H:inc _ emptyset |- _ => elim (emptyset_pr H)
end.
Ltac empty_tac v H:=
match goal with
| |- _ = emptyset => apply is_emptyset; move=> v H
end.
Ltac empty_tac3 v :=
match goal with
| |- _ = emptyset => apply is_emptyset; move=> v
end.
Ltac empty_tac1 u := elim (emptyset_pr (x:= u));
match goal with H: ?x = emptyset |- _ => rewrite <- H
| H: emptyset = ?x |- _ => rewrite H end ; fprops.
Ltac ue :=
match goal with
| H:?a = ?b |- _ => solve [ rewrite H ; fprops | rewrite - H ; fprops]
end.
Lemma emptyset_sub_any:
forall x, sub emptyset x.
Proof. by move=> x t Ht; empty_tac0. 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. by rewrite /Bo /inc; move=> x y hyp; apply chooseT_pr. Qed.
Lemma B_back : forall (x:Set) (y:x) (hyp : inc (Ro y) x), Bo hyp = y.
Proof. by move=> x y Hyp; apply R_inj; apply B_eq. 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.
move=> T P a b; case (p_or_not_p P) => [Ha | Hb ]; apply nonemptyT_intro; auto.
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.
move=> T P a b p eq_ap; symmetry.
set x:= _ a b.
have [Ha _ //] : (forall p, a p = x) & (forall q, b q = x).
rewrite /x /by_cases; apply chooseT_pr; by exists (a p); split.
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.
move=> T P a b q eq_bq; symmetry.
set x:= _ a b.
have [_ //] : (forall p : P, a p = x) & (forall q : ~ P, b q = x).
by rewrite /x /by_cases; apply chooseT_pr; exists (b q); split.
Qed.
Genereralised axiom of choice. choose p is satisfied by p
if somebody satisfies p, is the emptyset otherwise
Definition choose (p:Set -> Prop) :=
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.
rewrite /choose => p exp.
pose q x := ex p -> p x & ~ ex p -> x = emptyset.
have [q1 _ ]: (q (chooseT q (nonemptyT_intro emptyset))).
by apply chooseT_pr; elim exp; move=> x px; exists x; rewrite/q; split.
by apply q1.
Qed.
Lemma choose_not : forall p, ~(ex p) -> choose p = emptyset.
Proof.
rewrite /choose => p nexp.
pose q x := ex p -> p x & ~ ex p -> x = emptyset.
have [_ ] : (q (chooseT q (nonemptyT_intro emptyset))).
by apply chooseT_pr; exists emptyset; split.
by apply.
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. by rewrite /rep => x [y yinx ]; apply choose_pr; exists y. Qed.
The negation of forall x, ~ (p x) is the existence of x with (p x).
Lemma not_exists_pr : forall p : Set -> Prop, (~ ex p) = (forall x, ~ p x).
Proof.
move=> p; apply iff_eq => [nexp x px| allnp [x px]]; last by apply (allnp x).
by elim nexp; exists x.
Qed.
Lemma exists_proof : forall p : Set -> Prop, ~ (forall x : Set, ~ p x) -> ex p.
Proof.
move=> p; rewrite -not_exists_pr; apply excluded_middle.
Qed.
Lemma exists_proof2 : forall p : Set ->Set ->Prop, ~ (forall x y, ~ p x y)
-> (exists x, exists y, p x y).
Proof.
by move => p h; ex_middle h1; elim h => x y pxy; elim h1; exists x; exists y.
Qed.
Defines Y P x y to x if P is true and y otherwise
Definition Yo : Prop -> Set -> Set -> Set :=
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.
rewrite /Yo => P hP x y z xeqz.
by rewrite -xeqz -[x]/((fun _:P => x) hP); apply by_cases_if.
Qed.
Lemma Y_if_not :
forall (P : Prop) (hyp : ~ P) x y z, y = z -> Yo P x z = y.
Proof.
rewrite /Yo => P hnP x y z yeqz.
by rewrite -yeqz -[y]/((fun _:~P => y) hnP); apply by_cases_if_not.
Qed.
Lemma Y_if_rw : forall (P:Prop) (hyp :P) x y, Yo P x y = x.
Proof. by move=> p hP x y; apply Y_if. Qed.
Lemma Y_if_not_rw : forall (P:Prop) (hyp : ~P) x y, Yo P x y = y.
Proof. by move=> p hnP x y; apply Y_if_not. Qed.
Ltac Ytac eq:=
match goal with
| |- context [Yo (?i = ?j) _ _ ] =>
case (equal_or_not i j) => eq;
[rewrite (Y_if_rw eq) | rewrite (Y_if_not_rw eq) ]
end.
Ltac Ytac1 eq:=
match goal with
| |- context [Yo (inc ?i ?j) _ _ ] =>
case (inc_or_not i j) => eq;
[rewrite (Y_if_rw eq) | rewrite (Y_if_not_rw eq) ]
end.
Ltac Ytac0 := match goal with
| h: ?p |- context [Yo ?p _ _ ] => rewrite (Y_if_rw h)
| h: (~ ?p) |- context [Yo ?p _ _ ] => rewrite (Y_if_not_rw h)
| h: ?j <> ?i |- context [Yo (?i = ?j) _ _ ]
=> rewrite (Y_if_not_rw (sym_not_equal h))
| |- context [Yo (?i = ?i) _ _ ] => rewrite (Y_if_rw (refl_equal i))
end.
Given a function f, Zorec remembers a and f(a)
Lemma IM_rw: forall (x : Set) (f : x -> Set) (y : Set),
inc y (IM f) = exists a : x, f a = y.
Proof. by move=> x f y; apply iff_eq ; [ apply IM_exists | apply IM_inc]. Qed.
CoInductive 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:Set -> Prop) :=
IM (fun (z : Zorec (fun (a : x) => p (Ro a))) => let (a, _) := z in Ro a).
Lemma Z_inc : forall x (p: Set -> Prop) y, inc y x -> p y -> inc y (Zo x p).
Proof.
rewrite /Zo => x p y [a Roa]; rewrite -{1} Roa => py.
by apply IM_inc; exists (Zorec_c (f:= (fun a : x => p (Ro a))) py).
Qed.
Lemma Z_rw: forall x p y, inc y (Zo x p) = (inc y x & p y).
Proof.
move=> x y p; apply iff_eq; last by move=> [u v] ;apply Z_inc.
move=> H; case: (IM_exists H) => v Hv; rewrite -Hv.
by case v => a Poa; ee; apply R_inc.
Qed.
Lemma Z_sub : forall x p, sub (Zo x p) x.
Proof. by move=> x p y; rewrite Z_rw; intuition. Qed.
End Constructions.
Export Constructions.
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_rw: forall x,
inc x two_points = (x= TPa \/ x = TPb).
Proof.
rewrite /TPa /TPb /inc => x; apply iff_eq.
by case; case; auto.
case; [ by exists two_points_a | by exists two_points_b].
Qed.
Lemma two_points_distinct: TPa <> TPb.
Proof. move=> eq; pose e:=(R_inj eq); discriminate e. Qed.
Lemma two_points_distinctb: TPb <> TPa.
Proof. move=> eq; pose e:= (R_inj eq); discriminate e. Qed.
Lemma inc_TPa_two_points: inc TPa two_points.
Proof. rewrite /TPa; apply R_inc. Qed.
Lemma inc_TPb_two_points: inc TPb two_points.
Proof. by rewrite /TPb; apply R_inc. Qed.
Definition doubleton (x y : Set) :=
IM (two_points_rect x y).
Lemma doubleton_first : forall x y, inc x (doubleton x y).
Proof. by rewrite /doubleton => x y; apply IM_inc; exists two_points_a. Qed.
Lemma doubleton_second : forall x y : Set, inc y (doubleton x y).
Proof. by rewrite /doubleton => x y; apply IM_inc; exists two_points_b. Qed.
Lemma doubleton_or :
forall x y z : Set, inc z (doubleton x y) -> z = x \/ z = y.
Proof. by move=> x y z izd; case: (IM_exists izd) => a; case a; auto. Qed.
Hint Resolve doubleton_first doubleton_second inc_TPa_two_points inc_TPb_two_points: fprops.
Lemma doubleton_rw : forall x y z : Set,
inc z (doubleton x y) = (z = x \/ z = y).
Proof.
move=> x y z; apply iff_eq; [apply doubleton_or | by case => ->; fprops].
Qed.
Lemma two_points_pr2: doubleton TPa TPb = two_points.
Proof.
by set_extens x; rewrite two_points_rw doubleton_rw.
Qed.
Lemma doubleton_inj : forall x y z w,
doubleton x y = doubleton z w -> (x = z & y = w) \/ (x = w & y = z).
Proof.
move=> x y z w 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 (doubleton_or x_zw) => xs.
left; ee.
have w_xy: inc w (doubleton x y) by rewrite eql; fprops.
case (doubleton_or w_xy); last by [].
by case (doubleton_or y_zw) ; move: xs => -> ->.
case (doubleton_or y_zw); first by right.
have z_xy: inc z (doubleton x y) by rewrite eql; fprops.
by case (doubleton_or z_xy); intuition.
Qed.
Definition singleton x := doubleton x x.
Lemma doubleton_singleton : forall x, doubleton x x = singleton x.
Proof. by []. Qed.
Lemma singleton_rw: forall x y, inc y (singleton x) = (y = x).
Proof.
move=> x y; rewrite doubleton_rw; apply iff_eq; intuition.
Qed.
Hint Rewrite two_points_rw doubleton_rw singleton_rw: aw.
Lemma singleton_inc : forall x, inc x (singleton x).
Proof. move => x; aw. Qed.
Hint Resolve sub_refl singleton_inc: fprops.
Lemma singleton_eq : forall x y, inc y (singleton x) -> y = x.
Proof. by move => x y; aw. Qed.
Lemma singleton_inj : forall x y, singleton x = singleton y -> x = y.
Proof. by move => x y eq; apply singleton_eq; rewrite -eq; fprops. Qed.
Lemma nonempty_singleton: forall x, nonempty (singleton x).
Proof. by move => x; exists x; fprops. Qed.
Lemma sub_singleton: forall x y,
inc x y -> sub (singleton x) y.
Proof. by move=> x y ixy t itsx; rewrite (singleton_eq itsx). Qed.
Hint Resolve nonempty_singleton: fprops.
Lemma singleton_emptyset_not_empty: (singleton emptyset) <> emptyset.
Proof. rewrite - nonempty_or_empty; fprops. Qed.
Hint Resolve singleton_emptyset_not_empty two_points_distinctb: fprops.
Definition is_singleton x := exists u, x = singleton u.
Lemma is_singleton_rw: forall x,
is_singleton x = (nonempty x & (forall a b, inc a x -> inc b x -> a = b)).
Proof.
move=> x; apply iff_eq.
by move=> [z] ->; split; [fprops | move=> a b; aw=> -> ->].
move=> [[y yx] h]; exists y.
by set_extens u; aw; [ move => ax; apply: h | move=> -> ].
Qed.
Lemma is_singleton_pr: forall y x,
( (inc x y) & (forall z, inc z y -> z = x)) -> y = singleton x.
Proof. by move=> y x [xy zy]; set_extens t; aw; [ apply zy | move=> ->].
Qed.
Lemma singleton_pr1: forall a x, nonempty x ->
(forall z, inc z x -> z = a) -> x = singleton a.
Proof.
move=> a x [y yx] p.
move: (p _ yx) => aux; rewrite aux in yx.
apply is_singleton_pr; split=>//.
Qed.
Lemma nonempty_doubleton: forall x y, nonempty (doubleton x y).
Proof. by move=> x y; exists x; fprops. Qed.
Lemma sub_doubleton: forall x y z,
inc x z -> inc y z -> sub (doubleton x y) z.
Proof. by move=> x y z xz yz t; aw; case => ->. Qed.
Lemma doubleton_symm: forall a b,
doubleton a b = doubleton b a.
Proof. move=> a b; set_extens t; aw; intuition. Qed.
A set is small if it has zero or one elements
Definition small_set x :=
forall u v, inc u x -> inc v x -> u = v.
Lemma emptyset_small: small_set emptyset.
Proof. move=> u v ux; empty_tac0. Qed.
Lemma singleton_small: forall x, small_set (singleton x).
Proof. by move=> x u v ; aw; move => -> ->. Qed.
Lemma small_set_pr: forall x, small_set x ->
x = emptyset \/ is_singleton x.
Proof.
move=> x sx; case (emptyset_dichot x); first by auto.
move=> ne; right;rewrite is_singleton_rw //.
Qed.
End Little.
Export Little.
forall u v, inc u x -> inc v x -> u = v.
Lemma emptyset_small: small_set emptyset.
Proof. move=> u v ux; empty_tac0. Qed.
Lemma singleton_small: forall x, small_set (singleton x).
Proof. by move=> x u v ; aw; move => -> ->. Qed.
Lemma small_set_pr: forall x, small_set x ->
x = emptyset \/ is_singleton x.
Proof.
move=> x sx; case (emptyset_dichot x); first by auto.
move=> ne; right;rewrite is_singleton_rw //.
Qed.
End Little.
Export Little.
Set of all elements in a not in b
Definition complement (a b : Set) := Zo a (fun x : Set => ~ inc x b).
Lemma complement_rw :
forall a b x, inc x (complement a b) = (inc x a & ~ inc x b).
Proof. by rewrite /complement=> a b x; rewrite Z_rw. Qed.
Hint Rewrite complement_rw: sw.
Lemma use_complement :
forall a b x, inc x a -> ~ inc x (complement a b) -> inc x b.
Proof. by move=> a b x xa nx_cab; ex_middle h; case nx_cab; srw. Qed.
Lemma sub_complement: forall a b, sub (complement a b) a.
Proof. by move=> a b t; srw; case. Qed.
Lemma empty_complement: forall a b,
complement a b = emptyset -> sub a b.
Proof.
move=> a b eql t ta.
by apply (@use_complement a b t) => // ; rewrite eql; apply emptyset_pr.
Qed.
Lemma strict_sub_nonempty_complement : forall x y,
strict_sub x y -> nonempty (complement y x).
Proof.
move=> x y [s neq].
rewrite nonempty_or_empty; dneg ceq.
by apply extensionality=> //; apply empty_complement.
Qed.
Lemma double_complement: forall a x,
sub a x -> complement x (complement x a) = a.
Proof.
move=> a x sax.
set_extens t; srw.
by move=> [tx not_p]; ex_middle h; case not_p.
by move=> ta; apply conj; [apply (sax _ ta) | move => [tx nta ] ].
Qed.
Hint Rewrite double_complement: sw.
Lemma complement_itself : forall x,
complement x x = emptyset.
Proof. move=>x; apply is_emptyset=> y; srw; intuition. Qed.
Lemma complement_emptyset : forall x,
complement x emptyset = x.
Proof.
move=> x; set_extens t; srw; first by intuition.
by move=> tx; ee; apply emptyset_pr.
Qed.
Lemma not_inc_complement_singleton: forall a b,
~ (inc b (complement a (singleton b))).
Proof. by move=> a b; srw;aw ; move => [ _ nbb]; apply nbb. 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.
move=> a b x ax bx; apply iff_eq; rewrite /sub => ab t.
by srw; move=> [tx ntb]; ee; dneg ta; apply ab.
move => ta.
case (inc_or_not t (complement x b)); last by apply use_complement; apply ax.
move=> tcxb; move: (ab _ tcxb); srw; intuition.
Qed.
End Complement.
Export Complement.
Image of a set by a function
Definition fun_image (x : Set) (f : Set -> Set) := IM (fun a : x => f (Ro a)).
Lemma fun_image_rw : forall f x y,
inc y (fun_image x f) = exists z, (inc z x & f z = y).
Proof.
rewrite/fun_image => f x y; rewrite IM_rw; apply iff_eq; case=> a.
by exists (Ro a); ee ; apply R_inc.
by move=> [ax fay]; exists (Bo ax); rewrite (B_eq ax).
Qed.
Lemma inc_fun_image : forall x f a, inc a x -> inc (f a) (fun_image x f).
Proof. by move => x f a; rewrite fun_image_rw; exists a. Qed.
Hint Rewrite fun_image_rw : aw.
End Image.
Export Image.
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.
rewrite /powerset => x y sxy; apply 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 t; rewrite Z_rw.
move => [tx bc]; ex_middle w.
by set e:=(bc tx); move: e; rewrite B_eq by_cases_if_not=> e.
by move=> tx; split;[ apply sxy | move=> h; rewrite B_eq by_cases_if].
Qed.
Lemma powerset_sub : forall x y, inc x (powerset y) -> sub x y.
Proof.
rewrite/powerset=> x y ixpy.
by case (IM_exists ixpy)=> t eql; rewrite -eql; apply Z_sub.
Qed.
Lemma powerset_inc_rw : forall x y, inc x (powerset y) = sub x y.
Proof.
move=> x y; apply iff_eq ; [ apply powerset_sub | apply powerset_inc].
Qed.
Hint Rewrite powerset_inc_rw : aw.
Lemma inc_x_powerset_x: forall x, inc x (powerset x).
Proof. by move=> x; aw. Qed.
Lemma inc_e_powerset_x: forall x, inc emptyset (powerset x).
Proof. move=> x; aw; apply emptyset_sub_any. Qed.
Lemma powerset_monotone: forall a b,
sub a b -> sub (powerset a) (powerset b).
Proof. by move=> a b sab x; aw; move => sxa;apply: (sub_trans _ sab). Qed.
Lemma powerset_emptyset :
powerset emptyset = singleton emptyset.
Proof.
set_extens t; aw => eq.
apply extensionality=> //; apply emptyset_sub_any.
rewrite eq; apply emptyset_sub_any.
Qed.
End Powerset.
Export Powerset.
Integral: records p and e. Pose q = Ro p. By definition, inc q x.
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.
rewrite /union=> x y a xy ya.
have Bya: Ro (Bo ya) = y by apply B_eq.
have xBya: (inc x (Ro (Bo ya))) by rewrite Bya.
by apply IM_inc; exists (Build_Union_integral (Bo xBya)); simpl; apply B_eq.
Qed.
Lemma union_exists : forall x a,
inc x (union a) -> exists y, inc x y & inc y a.
Proof.
rewrite /union=> x a xu; case (IM_exists xu) => t pt.
by exists (Ro (Union_param t)); rewrite -pt; split; apply R_inc.
Qed.
Lemma union_rw: forall x a,
inc x (union a)= (exists y, inc x y & inc y a).
Proof.
move=> x y; apply iff_eq ; first by apply union_exists.
by case=> a [xa ay]; apply: (union_inc xa ay).
Qed.
Hint Rewrite union_rw : sw.
Lemma union_sub: forall x y, inc x y -> sub x (union y).
Proof. by move=>x y xy t tx ; apply union_inc with x. Qed.
Lemma sub_union : forall x z,
(forall y, inc y z -> sub y x) -> sub (union z) x.
Proof.
by move=> x z asub t; srw; move => [a [ta az]] ; apply (asub _ az).
Qed.
Lemma union_empty: union emptyset = emptyset.
Proof.
empty_tac x xi; case (union_exists xi)=> y [ _ ye].
by move: ye; apply emptyset_pr.
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.
rewrite/union2 => x y a; srw.
by case => t [ aat td ]; case (doubleton_or td)=> <-; auto.
Qed.
Lemma union2_first : forall x y a, inc a x -> inc a (union2 x y).
Proof. by rewrite /union2=> x y a ax; apply union_inc with x; fprops. Qed.
Lemma union2_second : forall x y a, inc a y -> inc a (union2 x y).
Proof. by rewrite /union2=> x y a ax; apply union_inc with y; fprops. Qed.
Lemma union2_rw : forall a b x,
inc x (union2 a b) = (inc x a \/ inc x b).
Proof.
move=> a b x; apply iff_eq; first by apply union2_or.
by case ; [apply union2_first | apply union2_second].
Qed.
Hint Rewrite union2_rw: aw.
Lemma union2sub_first: forall a b, sub a (union2 a b).
Proof. by move=> a b t tu; apply union2_first. Qed.
Lemma union2sub_second: forall a b, sub b (union2 a b).
Proof. by move=> a b t tu; apply union2_second. Qed.
Lemma union2sub: forall a b c, sub a c -> sub b c -> sub (union2 a b) c.
Proof. by move=> a b c ac bc x; aw; case; [apply ac | apply bc]. Qed.
Lemma union2idem: forall x, union2 x x = x.
Proof.
by move=> x; set_extens t=> tx; [case (union2_or tx) | apply union2_first].
Qed.
Lemma union2C: forall x y, union2 x y = union2 y x.
Proof. by move=> x y; set_extens t; aw; intuition. Qed.
Lemma union_singleton: forall x,
union (singleton x) = x.
Proof. move=>x; rewrite -doubleton_singleton; apply union2idem. Qed.
Lemma union_doubleton: forall x y,
union2 (singleton x)(singleton y) = doubleton x y.
Proof. by move=> x y ; set_extens t; aw. Qed.
Lemma union2A: forall x y z,
union2 x (union2 y z) = union2 (union2 x y) z.
Proof. move=> x y z; set_extens t; aw ;intuition. 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. rewrite/tack_on=> x y z; aw. Qed.
Lemma tack_on_rw: forall x y z,
(inc z (tack_on x y) ) = (inc z x \/ z = y).
Proof. move=> x y z; rewrite /tack_on; aw. Qed.
Hint Rewrite tack_on_rw : aw.
Lemma inc_tack_on_x: forall a b, inc a (tack_on b a).
Proof. by move=> a b; aw; auto. Qed.
Lemma inc_tack_on_sub: forall a b, sub b (tack_on b a).
Proof. by move=> a b t; aw; auto. Qed.
Lemma inc_tack_on_y: forall a b y, inc y b -> inc y (tack_on b a).
Proof. by move=> a b y; aw; auto. 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.
move=> x y yx.
apply extensionality; last by apply inc_tack_on_sub.
by move=> t; aw; case => // ->.
Qed.
Lemma tack_on_sub: forall x y z, sub x z -> inc y z -> sub (tack_on x y) z.
Proof. by move=> x y z xz yz t; aw; case ; [ apply xz | move=> -> ]. Qed.
Lemma tack_on_complement: forall x y, inc y x ->
x = tack_on (complement x (singleton y)) y.
Proof.
move=> x y yx; set_extens t; aw; srw; aw.
by case (equal_or_not t y); intuition.
by case; [intuition | move=> ->].
Qed.
End Union.
Export Union.
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 intersection_empty: intersection emptyset = emptyset.
Proof.
rewrite/intersection union_empty; empty_tac3 x.
rewrite Z_rw; move => [xe _]; empty_tac0.
Qed.
Lemma intersection_inc : forall x a,
nonempty x -> (forall y, inc y x -> inc a y) -> inc a (intersection x).
Proof.
rewrite /intersection => x a nx all_ayx; case nx=> y yx; apply Z_inc=> //.
move: (all_ayx _ yx) (yx); apply union_inc.
Qed.
Lemma intersection_forall :
forall x a y, inc a (intersection x) -> inc y x -> inc a y.
Proof.
rewrite /intersection => x a y; rewrite Z_rw; srw; move=> [_]; apply.
Qed.
Lemma intersection_sub : forall x y, inc y x -> sub (intersection x) y.
Proof. by move=> x y yx t ti; move: ti yx; apply intersection_forall.
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.
rewrite/intersection2 => x y a ax ay.
apply: intersection_inc; first by apply nonempty_doubleton.
by move=> t; aw; case=> ->.
Qed.
Lemma intersection2_first :
forall x y a, inc a (intersection2 x y) -> inc a x.
Proof.
rewrite/intersection2 => x y a ai.
by apply: intersection_forall; [ by apply ai | fprops].
Qed.
Lemma intersection2_second :
forall x y a, inc a (intersection2 x y) -> inc a y.
Proof.
rewrite/intersection2 => x y a ai.
by apply: intersection_forall; [ by apply ai |fprops ].
Qed.
Lemma intersection2_rw: forall x y a,
inc a (intersection2 x y) = (inc a x & inc a y).
Proof.
move=> x y a; apply iff_eq => ai.
by split; [ apply (intersection2_first ai) | apply (intersection2_second ai)].
by move: ai=> [ax ay]; apply intersection2_inc.
Qed.
Hint Rewrite intersection2_rw: aw.
Lemma intersection2sub_first: forall a b, sub (intersection2 a b) a.
Proof. by move=>a b t; apply intersection2_first. Qed.
Lemma intersection2sub_second: forall a b, sub (intersection2 a b) b.
Proof. by move=>a b t; apply intersection2_second. Qed.
Lemma intersection2sub: forall a b c, sub c a -> sub c b ->
sub c (intersection2 a b).
Proof. move=>a b c ca cb t tc; aw; ee. Qed.
Lemma intersection2idem: forall x, intersection2 x x = x.
Proof. move=> x; set_extens t; first by apply intersection2_first.
by move=> tx; apply intersection2_inc.
Qed.
Lemma intersection_singleton: forall x,
intersection (singleton x) = x.
Proof. move=>x; rewrite -doubleton_singleton; apply intersection2idem. Qed.
Lemma intersection2C: forall x y, intersection2 x y = intersection2 y x.
Proof. by move=>x y; set_extens t; aw; intuition. Qed.
Lemma intersection2A: forall x y z,
intersection2 x (intersection2 y z) = intersection2 (intersection2 x y) z.
Proof. move=> x y z; set_extens t; aw ;intuition. Qed.
Lemma intersection2_sub: forall x y,
sub x y = (intersection2 x y = x).
Proof.
move=> x y; apply iff_eq; last by move=> <-; apply intersection2sub_second.
move=> sxy; set_extens t; aw; first by intuition.
by move=> tx; ee; apply sxy.
Qed.
Two sets are disjopint if the intersection is empty
Definition disjoint x y := intersection2 x y = emptyset.
Lemma disjoint_pr: forall a b,
(forall u, inc u a -> inc u b -> False) -> disjoint a b.
Proof. move=> a b p; red; empty_tac3 u; aw; case; apply p. Qed.
Lemma disjoint_complement : forall x y,
disjoint y (complement x y).
Proof. by move=> x y; apply disjoint_pr; move=> u uy; srw; intuition. Qed.
Lemma disjoint_symmetric : forall x y,
disjoint x y -> disjoint y x.
Proof. by move=> x y; rewrite /disjoint intersection2C. Qed.
Ltac empty_tac2 u :=
match goal with H: disjoint ?x ?y |- _ =>
elim (emptyset_pr (x:= u)); rewrite <- H; apply intersection2_inc =>//
end.
End Intersection.
Export Intersection.
Lemma disjoint_pr: forall a b,
(forall u, inc u a -> inc u b -> False) -> disjoint a b.
Proof. move=> a b p; red; empty_tac3 u; aw; case; apply p. Qed.
Lemma disjoint_complement : forall x y,
disjoint y (complement x y).
Proof. by move=> x y; apply disjoint_pr; move=> u uy; srw; intuition. Qed.
Lemma disjoint_symmetric : forall x y,
disjoint x y -> disjoint y x.
Proof. by move=> x y; rewrite /disjoint intersection2C. Qed.
Ltac empty_tac2 u :=
match goal with H: disjoint ?x ?y |- _ =>
elim (emptyset_pr (x:= u)); rewrite <- H; apply intersection2_inc =>//
end.
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.
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 kpr0_pair: forall x y, intersection (J x y) = singleton x.
Proof.
move=> x y; rewrite Pair.kprE.
have sx_k: (inc (singleton x) (kpair x y)) by rewrite/ kpair; fprops.
apply is_singleton_pr; split.
apply intersection_inc; first by exists (singleton x).
by rewrite/kpair =>z; aw; case=> ->; fprops.
move=> z zi; suff: inc z (singleton x) by aw.
by move: zi sx_k; apply intersection_forall.
Qed.
Lemma pr1_pair: forall x y, P (J x y) = x.
Proof. by move=> x y; rewrite Pair.kpr1E /kpr1 kpr0_pair union_singleton. Qed.
Lemma pr2_pair: forall x y, Q (J x y) = y.
Proof.
move=> x y; rewrite Pair.kpr2E /kpr2.
have ->: (union (J x y) = doubleton x y).
rewrite Pair.kprE /kpair; set_extens t =>ts; last first.
by apply: (union_inc ts); fprops.
case (union_exists ts) => a; rewrite doubleton_rw; move => [ta aeq].
by move: aeq ta; case => -> //; aw => ->; fprops.
rewrite - Pair.kpr1E pr1_pair - {3}(union_singleton y); apply f_equal.
set_extens t; rewrite Z_rw /kpair; aw;last by move=> ->; auto.
move=> [h1 h2]; case h1 => // tx.
have : inc y (doubleton x t) by rewrite h2; fprops.
by aw; case; move => ->.
Qed.
Hint Rewrite pr1_pair pr2_pair : aw.
Lemma pr1_def : forall a b c d, J a b = J c d -> a = c.
Proof.
move=> a b c d eql.
by transitivity (P (J a b)); [| rewrite eql]; rewrite pr1_pair.
Qed.
Lemma pr2_def : forall a b c d, J a b = J c d -> b = d.
Proof.
move=> a b c d eql.
by transitivity (Q (J a b)); [ | rewrite eql ]; rewrite pr2_pair.
Qed.
Definition of a pair changed . It is any say x such that
(J (P x) (Q x) = x).
Definition is_pair (x : Set ) := (J (P x) (Q x) = x).
Lemma pair_is_pair : forall x y : Set, is_pair (J x y).
Proof. move=> x y; rewrite /is_pair; aw. Qed.
Hint Resolve pair_is_pair: fprops.
Lemma pair_exten : forall a b,
is_pair a -> is_pair b -> P a = P b -> Q a = Q b -> a = b.
Proof.
move=> a b pa pb Pab Qab.
by transitivity (J (P a) (Q a)) ; [| rewrite Pab Qab]; aw.
Qed.
End Pair.
Export Pair.
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 [eta J x]))).
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.
rewrite /product => x y z; apply iff_eq; rewrite union_rw.
case =>a [xa ai]; move: ai; aw ; case => b [biy fi]; move: fi xa.
move=> <-; aw; case=> t [tz Jx]; rewrite -Jx; aw; fprops.
move => [ px [ Px Qx]]; exists (fun_image z [eta J (P x)]).
aw; apply conj; [ exists (Q x); split; fprops; aw | by exists (P x) ].
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. by move=>a b u; aw. 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. by move=>a b u; aw. 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. by move=>a b u y; aw; 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. by move=>a b x y; aw; intuition. Qed.
Lemma product_pair_rw : forall a b x y : Set,
inc (J x y) (product a b) = (inc x a & inc y b).
Proof.
move=> a b x y; apply iff_eq; first by apply product_pair_pr.
by move=> [xa ya]; apply product_pair_inc.
Qed.
Lemma pair_in_product: forall a b c, inc a (product b c) -> is_pair a.
Proof. by move=>a b c; aw; intuition. 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.
move=> ir; apply is_emptyset => x; aw; move => [_ [ H _]]; empty_tac0.
Qed.
Lemma empty_product2: forall x,
product x emptyset = emptyset.
Proof. move=> ir; apply is_emptyset => x; aw; move => [_ [ _ H]]; empty_tac0.
Qed.
Lemma empty_product_pr: forall x y,
product x y = emptyset -> (x = emptyset \/ y= emptyset).
Proof.
move=> x y pe.
case (emptyset_dichot x); first by intuition.
by case => t tx; right; empty_tac u up; empty_tac1 (J t u).
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. by move=> x x' y xx' t; aw; intuition. Qed.
Lemma product_monotone_right: forall x y y',
sub y y' -> sub (product x y) (product x y').
Proof. by move=> x x' y xx' t; aw; intuition. Qed.
Lemma product_monotone: forall x x' y y',
sub x x' -> sub y y' -> sub (product x y) (product x' y').
Proof. by move=> x x' y y' xx' yy' t; aw; intuition. Qed.
Lemma product_monotone_left2: forall x x' y, nonempty y ->
sub (product x y) (product x' y) -> sub x x'.
Proof.
move=> x x' y [ t ty ] s z zx.
by move: (s _ (product_pair_inc zx ty)) ;aw; move=> [ _ [ H _ ]].
Qed.
Lemma product_monotone_right2: forall x y y', nonempty x ->
sub (product x y) (product x y') -> sub y y'.
Proof.
move=> x y y' [ t tx ] s z zy.
by move: (s _ (product_pair_inc tx zy)) ;aw; move=> [ _ [ _ H ]].
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.
Lemma domain0_rw: forall r x, inc x (domain r) = exists y, inc y r & P y =x.
Proof. by rewrite /domain=> r x;aw. Qed.
Lemma range0_rw: forall r x, inc x (range r) = exists y, inc y r & Q y =x.
Proof. by rewrite /range=> r x;aw. Qed.
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. by move=> f [r _ ]. Qed.
Lemma fgraph_pr: forall f x y y',
fgraph f -> inc (J x y) f -> inc (J x y') f -> y = y'.
Proof.
move=> f x y y' [g fg] ia ib.
have: J x y = J x y' by apply fg; auto; aw.
by apply pr2_def.
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. by rewrite /domain=> f x; apply inc_fun_image. Qed.
Lemma inc_pr2_range : forall f x,
inc x f -> inc (Q x) (range f).
Proof. by rewrite /range=> f x; apply 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.
move=> r x gr; rewrite domain0_rw; apply iff_eq; case=>y.
by move=> [yr eq]; exists (Q y); rewrite -eq; aw; rewrite (gr _ yr).
by exists (J x y); aw.
Qed.
Lemma range_rw: forall r y,
is_graph r -> inc y (range r) = (exists x, inc (J x y) r).
Proof.
move=> r x gr; rewrite range0_rw; apply iff_eq; case=>y.
by move=> [yr eq]; exists (P y); rewrite -eq; aw; rewrite (gr _ yr).
by exists (J y x); aw.
Qed.
Hint Rewrite range_rw domain_rw : dw.
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 |- exists x, _ & inc (J x ?y) ?z
=> exists x ; split; trivial
| H:inc (J ?x ?y) ?z |- exists y, _ & inc (J ?x y) ?z
=> exists y ; split; trivial
| H:inc (J ?x ?y) ?z |- exists x, inc (J x ?y) ?z & _
=> exists x ; split; trivial
| H:inc (J ?x ?y) ?z |- exists y, inc (J ?x y) ?z & _
=> exists y ; split; trivial
| H:inc ?x ?y |- exists x, inc x ?y & _
=> exists x ; split; fprops
| H:inc ?x ?y |- exists x, _ & inc x ?y
=> exists x ; split; fprops
| |- exists x, inc x (singleton ?y) & _
=> exists y ; split; fprops
| H1 : is_graph ?g, H : inc (J ?x ?y) ?g |- inc ?x (domain ?g)
=> rewrite (domain_rw _ H1) ; exists y; exact H
| H1 : is_graph ?g, H : inc (J ?x ?y) ?g |- inc ?y (range ?g)
=> rewrite (range_rw _ H1); exists x; exact 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.
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.
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. by move=> f x fg; dw; fprops; apply choose_pr. Qed.
Lemma in_graph_V : forall f x,
fgraph f -> inc x f -> x = J (P x) (V (P x) f).
Proof.
move=> f x fg xf ; move: (fg) => [ _ ffg].
by apply ffg; aw ; apply fdomain_pr1 => //; apply inc_pr1_domain.
Qed.
Lemma pr2_V : forall f x,
fgraph f -> inc x f -> Q x = V (P x) f.
Proof. by move=> f x fg xf; rewrite (in_graph_V fg xf); 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.
move=> f y fg; move: (fg) => [g _]; dw.
apply iff_eq; move => [x Px]; exists x.
split; first by ex_tac.
by move:(in_graph_V fg Px); aw; apply pr2_def.
by case Px => xd ->; apply fdomain_pr1.
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. by move=> f x fg; srw;exists x. Qed.
Case of a subgraph
Lemma sub_graph_fgraph : forall f g, fgraph g -> sub f g -> fgraph f.
Proof.
move=> f g [fg ffg] s; split.
by move=> t tf; apply (fg _ (s _ tf)).
by move=> x y xf yf; apply ffg; apply s.
Qed.
Lemma sub_graph_domain : forall f g, sub f g -> sub (domain f) (domain g).
Proof.
rewrite /domain=> f g s t; aw; move=> [z [zf Pz]];by exists z; ee.
Qed.
Lemma sub_graph_range : forall f g, sub f g -> sub (range f) (range g).
Proof.
rewrite /range=> f g s t; aw; move=> [z [zf Pz]]; by exists z; ee.
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.
move=> f g x fg sfg xdf.
set ff:=(sub_graph_fgraph fg sfg).
set ipg:=(sfg _ (fdomain_pr1 ff xdf)).
by move: (in_graph_V fg ipg); aw; apply pr2_def.
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.
move=> f g ff fg s sev t tf.
set ptdf:= inc_pr1_domain tf.
rewrite (in_graph_V ff tf) (sev _ ptdf).
by apply fdomain_pr1 => //; apply s.
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.
move=> f g ff fg d hyp.
apply extensionality; apply fgraph_sub=> //; rewrite - d;fprops.
by symmetry; apply hyp.
Qed.
Lemma range_union2: forall a b,
range (union2 a b) = union2 (range a) (range b).
Proof.
rewrite /range=> a b;set_extens x; aw.
by move=> [z [zu qz]]; move: zu; aw; case; [ left | right ]; ex_tac.
case; move=> [z [zs qz]]; exists z; aw; fprops.
Qed.
Lemma domain_union2: forall a b,
domain (union2 a b) = union2 (domain a) (domain b).
Proof.
rewrite /domain=> a b;set_extens x; aw.
by move=> [z [zu qz]]; move: zu; aw; case; [ left | right ]; ex_tac.
case; move=> [z [zs qz]]; exists z; aw; fprops.
Qed.
Lemma domain_singleton: forall x y, domain (singleton (J x y)) = singleton x.
Proof.
move => x y; rewrite /domain; set_extens t; aw.
by move=> [z]; aw; case => ->; aw.
by move=> ->; exists (J x y); aw.
Qed.
Lemma range_singleton: forall x y, range (singleton (J x y)) = singleton y.
Proof.
move => x y; rewrite /range; set_extens t; aw.
by move=> [z]; aw; case => ->; aw.
by move=> ->; exists (J x y); aw.
Qed.
Lemma fgraph_union2: forall a b, fgraph a -> fgraph b ->
disjoint (domain a) (domain b) ->
fgraph (union2 a b).
Proof.
move=> a b [fg fgg] [g gfg] ei; split.
by move=> t; aw; case; auto.
move=> x y; aw; case=> xs; case=>ys;
first (by apply fgg); last (by apply gfg);
move=> sp;empty_tac2 (P y); rewrite domain0_rw; ex_tac.
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. by move=> a f; apply Z_sub. Qed.
Lemma inverse_image_rw : forall a f x,
inc x (inverse_image a f)= ( inc x (domain f) & inc (V x f) a).
Proof. by move => a f x; rewrite Z_rw. 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. by move=> a f x; rewrite inverse_image_rw. Qed.
Lemma inverse_image_pr :
forall a f x, inc x (inverse_image a f) -> inc (V x f) a.
Proof. by move=> a f x; rewrite inverse_image_rw; intuition. Qed.
Graph associated to a function restricted to some set as domain.
Definition graph_constructor (x : Set) (p : Set -> Set) :=
fun_image x (fun y => J y (p y)).
Notation L := graph_constructor.
Lemma L_inc_rw: forall x p y,
inc y (L x p) = exists z, inc z x & J z (p z) = y.
Proof. by rewrite/L => x p y; aw. Qed.
Hint Rewrite L_inc_rw : aw.
Lemma L_fgraph : forall p x, fgraph (L x p).
Proof.
move => p x; split.
move =>t; aw; move=> [z [_ j]]; rewrite -j; fprops.
move=> a b; aw; move=> [z1 [_ j1]] [z2 [_ j2]].
by rewrite -j1 -j2 2! pr1_pair => ->.
Qed.
Lemma L_domain : forall x p, domain (L x p) = x.
Proof.
rewrite /domain=> x p; set_extens t; aw.
move=> [e [zL Pz]]; move: zL; aw;rewrite -Pz.
by move=> [z [zx eJ]]; rewrite -eJ; aw.
by exists (J t (p t)); aw; ee; ex_tac.
Qed.
Hint Rewrite L_domain : bw.
Hint Resolve L_fgraph: gprops.
Lemma L_V_rw : forall x p y, inc y x -> V y (L x p) = p y.
Proof.
move=> x p y yx.
have p1: inc (J y (p y)) (L x p) by aw; ex_tac.
symmetry;move: (pr2_V (L_fgraph p x) p1); aw.
Qed.
Hint Rewrite L_V_rw : bw.
Lemma L_range : forall p x,
range (L x p) = fun_image x p.
Proof.
rewrite /range => p t; set_extens z; aw; move=> [a [ia pa]].
by move: ia; aw; case => [b [ib pb]]; rewrite -pa -pb; ex_tac; aw.
by exists (J a z); aw; ee; ex_tac; rewrite -pa.
Qed.
Lemma L_recovers : forall f,
fgraph f -> L (domain f) (fun x => V x f) = f.
Proof.
move=> f fg; apply fgraph_exten; gprops; bw.
by move => x xf; 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.
move=>a b f g eqd eqv; apply fgraph_exten; gprops; bw.
by move => x xa; bw; [apply eqv | rewrite -eqd].
Qed.
Lemma L_create : forall a f,
L a (fun x => V x (L a f)) = L a f.
Proof. by move => a f; apply L_exten1=>//; move=> x xa; 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. by move=> sf f a; rewrite L_range; 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.
move=> x f y nyx; apply choose_not; dneg xx.
by move:xx => [u]; aw; move=> [z [zx sj]]; rewrite -(pr1_def sj).
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 f g := L (domain g) (fun y => V (V y g) f).
Lemma fcompose_fgraph : forall f g, fgraph (fcompose f g).
Proof. rewrite /fcompose=> f g; gprops. Qed.
Lemma fcompose_domain :
forall f g, domain (fcompose f g) = inverse_image (domain f) g.
Proof. rewrite /fcompose=> f g; bw. Qed.
Lemma fcompose_range: forall f g, fgraph f ->
sub (range (fcompose f g)) (range f).
Proof.
rewrite /range /fcompose => f g fg t; aw.
case=> z; aw; case; case=>a; case => ai <- <-; aw.
move : ai; rewrite inverse_image_rw; case => _ Vg.
by set (fdomain_pr1 fg Vg); ex_tac; aw.
Qed.
Lemma fcomposable_domain :
forall f g, fcomposable f g -> domain (fcompose f g) = domain g.
Proof.
rewrite /fcompose /fcomposable => f g [ff [fg s]]; bw.
apply extensionality; first by apply inverse_image_sub.
move =>t tg; rewrite inverse_image_rw.
by ee; apply s;apply inc_V_range.
Qed.
Lemma fcompose_ev : forall x f g, fcomposable f g ->
inc x (domain g) -> V x (fcompose f g) = V (V x g) f.
Proof.
rewrite /fcompose=> x f g [f1 [f2 f3]] xd; bw.
by rewrite inverse_image_rw; ee; apply f3; apply inc_V_range.
Qed.
Hint Rewrite fcompose_ev : bw.
Lemma alternate_compose: forall g f,
fcomposable g f -> gcompose g f = fcompose g f.
Proof.
rewrite /gcompose=> g f fc; apply fgraph_exten; gprops;bw.
by apply fcompose_fgraph.
by rewrite fcomposable_domain.
by move=> x xd;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. rewrite/identity_g => x; gprops. Qed.
Lemma identity_domain : forall x, domain (identity_g x) = x.
Proof. rewrite/identity_g => x; bw. Qed.
Lemma identity_range: forall x, range (identity_g x) = x.
Proof.
by rewrite/identity_g => x; set_extens t; bw; [move=> [b [bx]] <-| exists t].
Qed.
Lemma identity_ev : forall x a, inc x a -> V x (identity_g a) = x.
Proof. rewrite/identity_g => x a xa; 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. by move => f x y; rewrite Z_rw. Qed.
Hint Rewrite restr_inc_rw : aw.
Lemma restr_sub : forall f x, sub (restr f x) f.
Proof. by move=> f x ; apply Z_sub. Qed.
Lemma restr_fgraph : forall f x,
fgraph f -> fgraph (restr f x).
Proof. by move=> f x fg; apply (sub_graph_fgraph fg); apply Z_sub. Qed.
Lemma restr_graph: forall x r,
is_graph r -> is_graph (restr r x).
Proof. by move=> x t gr z zr; apply gr; apply (restr_sub zr). 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.
rewrite /domain /restr=> f x fg; set_extens t; aw.
move=> [z [iz pz]]; move: pz iz => <-; rewrite Z_rw.
by move=> [zf Px]; ee; ex_tac.
by move=> [[z [zf pz]] tx]; exists z ; ee; apply Z_inc=>//; rewrite pz.
Qed.
Lemma restr_domain1 : forall f x,
fgraph f -> sub x (domain f) ->
domain (restr f x) = x.
Proof.
by move=> f x g s; rewrite restr_domain // intersection2C -intersection2_sub.
Qed.
Lemma fgraph_sub_eq : forall r s,
fgraph r -> fgraph s -> sub r s ->
sub (domain s) (domain r) -> r = s.
Proof.
move=> r s fr [ _ fs] sg sd; apply extensionality => //.
move => t ts.
have ptds: inc (P t) (domain r) by apply sd; apply inc_pr1_domain.
have ->: ( t = J (P t) (V (P t) r)).
by apply fs; aw; apply sg ; apply fdomain_pr1.
apply fdomain_pr1=>//.
Qed.
Lemma restr_to_domain : forall f g,
fgraph f -> fgraph g -> sub f g ->
restr g (domain f) = f.
Proof.
move=> f g ff ffg sfg; symmetry; apply fgraph_sub_eq; fprops.
by rewrite /restr => t tf; apply Z_inc; [apply sfg | apply inc_pr1_domain].
by rewrite restr_domain => // t; apply intersection2_second.
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.
move=> f u x fg id iu.
have p1: inc (J x (V x f)) f by apply fdomain_pr1=>//; apply sd.
have p2: inc (J x (V x f)) (restr f u) by rewrite /restr; apply Z_inc; aw.
have p3: fgraph (restr f u) by fprops.
by symmetry; have p:= (pr2_V p3 p2); move: p; aw.
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. by move=> f u x ff sd xu; apply restr_ev1=> //; apply sd. 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.
move=> x f fg xd; apply fgraph_exten; fprops; gprops; bw.
by rewrite restr_domain1.
by move=> a ax; 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.
rewrite/restr=> f a v ff sa sb.
by set_extens t; rewrite 3! Z_rw; intuition.
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.
move=> f g x fgg xd sfg.
have fgf: fgraph f by apply (sub_graph_fgraph fgg).
have ipg: inc (J x (V x f)) g by apply sfg; apply fdomain_pr1.
by set w:= (in_graph_V fgg ipg); move: w; aw; apply pr2_def.
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.
rewrite /is_restriction => f g; apply iff_eq.
move => [fg [x res]]; rewrite res.
by ee; rewrite/restr; apply Z_sub.
move => [fgf [fgh s]]; split; first by exact.
set (sub_graph_domain s).
exists (domain f).
apply fgraph_exten; fprops; first by rewrite restr_domain1.
by move=> x ix; bw; apply sub_graph_ev.
Qed.
Union of graphs
Lemma domain_union : forall z, domain (union z) =
union (fun_image z domain).
Proof.
rewrite /domain=> z; set_extens t; aw.
move=> [a [au pa]]; rewrite -pa; case (union_exists au) => b [ab bz].
by apply union_inc with (domain b); rewrite /domain; aw; ex_tac.
rewrite union_rw; move=> [y [ty yf]]; move: yf; aw.
move=> [a [az fy]]; move: ty; rewrite -fy; aw.
by move=> [b [ba p]]; exists b; ee; apply: union_inc ba az.
Qed.
Lemma domain_tack_on : forall f x y,
domain (tack_on f (J x y)) = tack_on (domain f) x.
Proof.
by move=> f x y; rewrite /tack_on domain_union2 domain_singleton.
Qed.
Lemma range_union : forall z, range (union z) =
union (fun_image z range).
Proof.
rewrite /range=> z; set_extens t; aw.
move=> [a [au pa]]; rewrite -pa; case (union_exists au) => b [ab bz].
by apply union_inc with (range b); rewrite /range; aw; ex_tac.
rewrite union_rw; move=> [y [ty yf]]; move: yf; aw.
move=> [a [az fy]]; move: ty; rewrite -fy; aw.
by move=> [b [ba p]]; exists b; ee; apply: union_inc ba az.
Qed.
Lemma range_tack_on : forall f x y,
range (tack_on f (J x y)) = tack_on (range f) y.
Proof.
by move=> f x y; rewrite /tack_on range_union2 range_singleton.
Qed.
Lemma tack_on_fgraph : forall f x y,
fgraph f -> ~ inc x (domain f) ->
fgraph (tack_on f (J x y)).
Proof.
rewrite /fgraph=> f x y [fg ff] nid; split.
by move=> t; rewrite tack_on_rw; case; [ apply fg | move=> ->; fprops].
move=> a b; rewrite 2! tack_on_rw.
case=> ap.
case=> bp; first (by apply ff); move => eql; elim nid.
by rewrite bp in eql; awi eql; rewrite - eql; apply inc_pr1_domain.
rewrite {} ap; case=> bp; last by rewrite bp.
by aw; move=> eql; elim nid ; rewrite eql; apply inc_pr1_domain.
Qed.
End Function.
Export Function.