(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


Set Implicit Arguments.
Unset Strict Implicit.
Require Export Parts2.
(** Title "Restrictions, inverse images." *)
Section Restrictions1.
Variable E F : Setoid.
Variable f : MAP E F.

Definition restrict : forall A : part_set E, MAP A F.
(* Goal: forall A : Carrier (part_set E), Carrier (MAP (@set_of_subtype_image E (@part E A)) F) *)
intros A; try assumption.
(* Goal: Carrier (MAP (@set_of_subtype_image E (@part E A)) F) *)
apply (Build_Map (Ap:=fun x : A => f (A x))).
(* Goal: @pred_compatible E (fun x : Carrier E => @in_part F (@Ap E F f x) A) *)
red in |- *.
(* Goal: forall (x y : Carrier (@set_of_subtype_image E (@part E A))) (_ : @Equal (@set_of_subtype_image E (@part E A)) x y), @Equal F (@Ap E F f (@subtype_image_inj E (@part E A) x)) (@Ap E F f (@subtype_image_inj E (@part E A) y)) *)
intros x y; try assumption.
(* Goal: forall _ : @Equal (@set_of_subtype_image E (@part E A)) x y, @Equal F (@Ap E F f (@subtype_image_inj E (@part E A) x)) (@Ap E F f (@subtype_image_inj E (@part E A) y)) *)
elim y.
(* Goal: forall (subtype_elt : Carrier E) (subtype_prf : @Pred_fun E A subtype_elt) (_ : @Equal (@set_of_subtype_image E (@part E A)) x (@Build_subtype E A subtype_elt subtype_prf)), @Equal F (@Ap E F f (@subtype_image_inj E (@part E A) x)) (@Ap E F f (@subtype_image_inj E (@part E A) (@Build_subtype E A subtype_elt subtype_prf))) *)
elim x.
(* Goal: forall _ : @in_part F x (@image E F f A), @in_part F x (@image E F f (invimage f (@image E F f A))) *)
simpl in |- *; auto with algebra.
Defined.

Lemma restrict_prop :
 forall (A : part_set E) (x : E) (p : in_part x A),
 Equal (restrict A (Build_subtype (subtype_elt:=x) p)) (f x).
(* Goal: forall _ : @in_part F x (@image E F f A), @in_part F x (@image E F f (invimage f (@image E F f A))) *)
simpl in |- *; auto with algebra.
Qed.

Lemma restrict_prop_in_part :
 forall (A : part_set E) (x : A), Equal (restrict A x) (f (A x)).
(* Goal: forall _ : @in_part F x (@image E F f A), @in_part F x (@image E F f (invimage f (@image E F f A))) *)
simpl in |- *; auto with algebra.
Qed.
End Restrictions1.
Hint Resolve restrict_prop: algebra.
Section Inverse_image1.
Variable E F : Setoid.
Section Inverse_image1_1.
Variable f : MAP E F.

Definition invimage : part_set F -> part_set E.
(* Goal: forall _ : Carrier (part_set F), Carrier (part_set E) *)
intros A.
(* Goal: Carrier (part_set E) *)
apply (Build_Predicate (Pred_fun:=fun x : E => in_part (f x) A)).
(* Goal: @pred_compatible E (fun x : Carrier E => @in_part F (@Ap E F f x) A) *)
red in |- *.
(* Goal: forall (x y : Carrier E) (_ : @in_part F (@Ap E F f x) A) (_ : @Equal E y x), @in_part F (@Ap E F f y) A *)
intros x y H' H'0; try assumption.
(* Goal: @in_part F (@Ap E F f y) A *)
apply in_part_comp_l with (Ap f x); auto with algebra.
Defined.
End Inverse_image1_1.
Variable f : MAP E F.

Lemma invimage_in :
 forall (A : part_set F) (x : E), in_part x (invimage f A) -> in_part (f x) A.
(* Goal: forall _ : @in_part F x (@image E F f A), @in_part F x (@image E F f (invimage f (@image E F f A))) *)
simpl in |- *; auto with algebra.
Qed.

Lemma in_invimage :
 forall (A : part_set F) (x : E), in_part (f x) A -> in_part x (invimage f A).
(* Goal: forall _ : @in_part F x (@image E F f A), @in_part F x (@image E F f (invimage f (@image E F f A))) *)
simpl in |- *; auto with algebra.
Qed.
Hint Resolve in_invimage: algebra.

Lemma invimage_included :
 forall A B : part_set F,
 included A B -> included (invimage f A) (invimage f B).
(* Goal: forall A : Carrier (part_set E), @included E A (invimage f (@image E F f A)) *)
unfold included in |- *.
(* Goal: forall _ : @in_part F x (@image E F f A), @in_part F x (@image E F f (invimage f (@image E F f A))) *)
simpl in |- *; auto with algebra.
Qed.
Hint Resolve invimage_included: algebra.

Lemma invimage_comp :
 forall A B : part_set F, Equal A B -> Equal (invimage f A) (invimage f B).
(* Goal: forall (A B : Carrier (part_set F)) (_ : @Equal (part_set F) A B), @Equal (part_set E) (invimage f A) (invimage f B) *)
intros A B H'; try assumption.
(* Goal: @Equal (part_set E) (invimage f A) (invimage f B) *)
apply included_antisym; auto with algebra.
Qed.
Hint Resolve invimage_comp: algebra.

Lemma invimage_image :
 forall A : part_set F, included (image f (invimage f A)) A.
(* Goal: forall A : Carrier (part_set E), @included E A (invimage f (@image E F f A)) *)
unfold included in |- *.
(* Goal: forall _ : @in_part F x (@image E F f A), @in_part F x (@image E F f (invimage f (@image E F f A))) *)
simpl in |- *; auto with algebra.
(* Goal: forall (A : Predicate F) (x : Carrier F) (_ : @ex (Carrier E) (fun x0 : Carrier E => and (@in_part F (@Ap E F f x0) A) (@Equal F x (@Ap E F f x0)))), @in_part F x A *)
intros A x H'; try assumption.
(* Goal: @in_part F x A *)
elim H'; intros x0 E0; elim E0; intros H'0 H'1; try exact H'1; clear E0 H'.
(* Goal: @in_part F (@Ap E F f x) A *)
(* Goal: @in_part E x (invimage f (@image E F f (invimage f A))) *)
apply in_part_comp_l with (Ap f x0); auto with algebra.
Qed.

Lemma image_invimage :
 forall A : part_set E, included A (invimage f (image f A)).
(* Goal: forall A : Carrier (part_set E), @included E A (invimage f (@image E F f A)) *)
unfold included in |- *.
(* Goal: forall _ : @in_part F x (@image E F f A), @in_part F x (@image E F f (invimage f (@image E F f A))) *)
simpl in |- *; auto with algebra.
(* Goal: forall (A : Predicate E) (x : Carrier E) (_ : @in_part E x A), @ex (Carrier E) (fun x0 : Carrier E => and (@in_part E x0 A) (@Equal F (@Ap E F f x) (@Ap E F f x0))) *)
intros A x H'; exists x; split; [ try assumption | idtac ]; auto with algebra.
Qed.
Hint Resolve invimage_image image_invimage: algebra.

Lemma invimage_image_invimage :
 forall A : part_set F,
 Equal (invimage f (image f (invimage f A))) (invimage f A).
(* Goal: forall A : Carrier (part_set E), @Equal (part_set F) (@image E F f (invimage f (@image E F f A))) (@image E F f A) *)
simpl in |- *.
(* Goal: forall A : Predicate E, @eq_part F (@image E F f (invimage f (@image E F f A))) (@image E F f A) *)
unfold eq_part in |- *.
(* Goal: forall (A : Predicate F) (x : Carrier E), and (forall _ : @in_part E x (invimage f (@image E F f (invimage f A))), @in_part E x (invimage f A)) (forall _ : @in_part E x (invimage f A), @in_part E x (invimage f (@image E F f (invimage f A)))) *)
intros A x; split; [ idtac | intros H'; try assumption ].
(* Goal: forall A : Carrier (part_set E), @Equal (part_set F) (@image E F f (invimage f (@image E F f A))) (@image E F f A) *)
simpl in |- *.
(* Goal: forall _ : @ex (Carrier E) (fun x0 : Carrier E => and (@in_part E x0 A) (@Equal F x (@Ap E F f x0))), @ex (Carrier E) (fun x0 : Carrier E => and (@ex (Carrier E) (fun x : Carrier E => and (@in_part E x A) (@Equal F (@Ap E F f x0) (@Ap E F f x)))) (@Equal F x (@Ap E F f x0))) *)
intros H'; try assumption.
(* Goal: @ex (Carrier E) (fun x0 : Carrier E => and (@ex (Carrier E) (fun x : Carrier E => and (@in_part E x A) (@Equal F (@Ap E F f x0) (@Ap E F f x)))) (@Equal F x (@Ap E F f x0))) *)
elim H'; intros x0 E0; elim E0; intros H'0 H'1; try exact H'0; clear E0 H'.
(* Goal: @in_part F (@Ap E F f x) A *)
(* Goal: @in_part E x (invimage f (@image E F f (invimage f A))) *)
apply in_part_comp_l with (Ap f x0); auto with algebra.
(* Goal: @in_part E x (invimage f (@image E F f (invimage f A))) *)
auto with algebra.
Qed.

Lemma image_invimage_image :
 forall A : part_set E, Equal (image f (invimage f (image f A))) (image f A).
(* Goal: forall A : Carrier (part_set E), @Equal (part_set F) (@image E F f (invimage f (@image E F f A))) (@image E F f A) *)
simpl in |- *.
(* Goal: forall A : Predicate E, @eq_part F (@image E F f (invimage f (@image E F f A))) (@image E F f A) *)
unfold eq_part in |- *.
(* Goal: forall (A : Predicate E) (x : Carrier F), and (forall _ : @in_part F x (@image E F f (invimage f (@image E F f A))), @in_part F x (@image E F f A)) (forall _ : @in_part F x (@image E F f A), @in_part F x (@image E F f (invimage f (@image E F f A)))) *)
intros A x; split; [ try assumption | idtac ].
(* Goal: forall _ : @in_part F x (@image E F f A), @in_part F x (@image E F f (invimage f (@image E F f A))) *)
simpl in |- *; auto with algebra.
(* Goal: forall _ : @ex (Carrier E) (fun x0 : Carrier E => and (@in_part E x0 A) (@Equal F x (@Ap E F f x0))), @ex (Carrier E) (fun x0 : Carrier E => and (@ex (Carrier E) (fun x : Carrier E => and (@in_part E x A) (@Equal F (@Ap E F f x0) (@Ap E F f x)))) (@Equal F x (@Ap E F f x0))) *)
intros H'; try assumption.
elim H'; intros x0 E0; elim E0; intros H'0 H'1; elim H'0; intros x1 E1;
 elim E1; intros H'2 H'3; try exact H'2; clear E1 H'0 E0 H'.
(* Goal: @in_part E x (invimage f (@image E F f (invimage f A))) *)
exists x1; split; [ try assumption | idtac ]; auto with algebra.
(* Goal: @in_part E x (invimage f (@image E F f (invimage f A))) *)
apply Trans with (Ap f x0); auto with algebra.
(* Goal: forall _ : @in_part F x (@image E F f A), @in_part F x (@image E F f (invimage f (@image E F f A))) *)
simpl in |- *; auto with algebra.
(* Goal: forall _ : @ex (Carrier E) (fun x0 : Carrier E => and (@in_part E x0 A) (@Equal F x (@Ap E F f x0))), @ex (Carrier E) (fun x0 : Carrier E => and (@ex (Carrier E) (fun x : Carrier E => and (@in_part E x A) (@Equal F (@Ap E F f x0) (@Ap E F f x)))) (@Equal F x (@Ap E F f x0))) *)
intros H'; try assumption.
(* Goal: @ex (Carrier E) (fun x0 : Carrier E => and (@ex (Carrier E) (fun x : Carrier E => and (@in_part E x A) (@Equal F (@Ap E F f x0) (@Ap E F f x)))) (@Equal F x (@Ap E F f x0))) *)
elim H'; intros x0 E0; elim E0; intros H'0 H'1; try exact H'0; clear E0 H'.
exists x0; split; [ exists x0; split; [ try assumption | idtac ] | idtac ];
(* Goal: @in_part E x (invimage f (@image E F f (invimage f A))) *)
 auto with algebra.
Qed.
End Inverse_image1.
Hint Resolve invimage_image_invimage image_invimage_image: algebra.
Hint Resolve in_invimage: algebra.
Hint Resolve invimage_included: algebra.
Hint Resolve invimage_comp: algebra.
