(* 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 Sets.
(** Title "Cartesian product of two sets." *)
Section Def.
Variable E F : Setoid.
Comments "The type of elements of a cartesian product:".

Record cart_type : Type :=  {cart_l : E; cart_r : F}.
Comments "Equality of couples:".

Definition cart_eq (x y : cart_type) :=
  Equal (cart_l x) (cart_l y) /\ Equal (cart_r x) (cart_r y).

Lemma cart_eq_equiv : equivalence cart_eq.
(* Goal: @Map_eq E (cart F G) (map_couple map_proj1 map_proj2) f *)
red in |- *.
(* Goal: and (@reflexive cart_type cart_eq) (@partial_equivalence cart_type cart_eq) *)
split; [ try assumption | idtac ].
(* Goal: @Map_eq E (cart F G) (map_couple map_proj1 map_proj2) f *)
red in |- *.
(* Goal: @Map_eq E (cart F G) (map_couple map_proj1 map_proj2) f *)
intros x; red in |- *.
(* Goal: forall _ : @Equal (cart E F) x y, @Equal G (f (@proj1 E F x) (@proj2 E F x)) (f (@proj1 E F y) (@proj2 E F y)) *)
elim x.
(* Goal: forall (cart_l : Carrier E) (cart_r : Carrier F), cart_eq (Build_cart_type cart_l cart_r) (Build_cart_type cart_l cart_r) *)
(* Goal: @partial_equivalence cart_type cart_eq *)
unfold cart_eq in |- *; simpl in |- *; auto with algebra.
(* Goal: @Map_eq E (cart F G) (map_couple map_proj1 map_proj2) f *)
red in |- *.
(* Goal: and (@transitive cart_type cart_eq) (@symmetric cart_type cart_eq) *)
split; [ idtac | try assumption ].
(* Goal: @Map_eq E (cart F G) (map_couple map_proj1 map_proj2) f *)
red in |- *.
(* Goal: forall (x y : cart_type) (_ : @app_rel cart_type cart_eq x y), @app_rel cart_type cart_eq y x *)
unfold app_rel, cart_eq in |- *.
(* Goal: and (@reflexive cart_type cart_eq) (@partial_equivalence cart_type cart_eq) *)
intros x y z H' H'0; split; [ try assumption | idtac ].
(* Goal: @Equal E (cart_l x) (cart_l z) *)
(* Goal: @Equal F (cart_r x) (cart_r z) *)
(* Goal: @symmetric cart_type cart_eq *)
apply Trans with (cart_l y); intuition.
(* Goal: @Equal F (cart_r x) (cart_r z) *)
(* Goal: @symmetric cart_type cart_eq *)
apply Trans with (cart_r y); intuition.
(* Goal: @Map_eq E (cart F G) (map_couple map_proj1 map_proj2) f *)
red in |- *.
(* Goal: forall (x y : cart_type) (_ : @app_rel cart_type cart_eq x y), @app_rel cart_type cart_eq y x *)
unfold app_rel, cart_eq in |- *.
(* Goal: forall (x y : cart_type) (_ : and (@Equal E (cart_l x) (cart_l y)) (@Equal F (cart_r x) (cart_r y))), and (@Equal E (cart_l y) (cart_l x)) (@Equal F (cart_r y) (cart_r x)) *)
intuition.
Qed.

Definition cart : Setoid := Build_Setoid cart_eq_equiv.
Comments "We will denote the cartesian product of" E "and" F "with"
  (cart E F).
End Def.
Section Projections.
Variable E F : Setoid.

Definition proj1 (x : cart E F) : E := cart_l x.

Definition proj2 (x : cart E F) : F := cart_r x.
Comments "We note" (proj1 x) "and" (proj2 x) "the components of a couple" x
  "in " (cart E F).

Lemma proj1_comp :
 forall x y : cart E F, Equal x y -> Equal (proj1 x) (proj1 y).
(* Goal: @Map_eq E (cart F G) (map_couple map_proj1 map_proj2) f *)
red in |- *.
(* Goal: @Equal (MAP E (cart F G)) (map_couple map_proj1 map_proj2) f *)
simpl in |- *.
(* Goal: forall (x y : cart_type) (_ : and (@Equal E (cart_l x) (cart_l y)) (@Equal F (cart_r x) (cart_r y))), and (@Equal E (cart_l y) (cart_l x)) (@Equal F (cart_r y) (cart_r x)) *)
unfold app_rel, cart_eq in |- *; intuition.
Qed.

Lemma proj2_comp :
 forall x y : cart E F, Equal x y -> Equal (proj2 x) (proj2 y).
(* Goal: @Map_eq E (cart F G) (map_couple map_proj1 map_proj2) f *)
red in |- *.
(* Goal: @Equal (MAP E (cart F G)) (map_couple map_proj1 map_proj2) f *)
simpl in |- *.
(* Goal: forall (x y : cart_type) (_ : and (@Equal E (cart_l x) (cart_l y)) (@Equal F (cart_r x) (cart_r y))), and (@Equal E (cart_l y) (cart_l x)) (@Equal F (cart_r y) (cart_r x)) *)
unfold app_rel, cart_eq in |- *; intuition.
Qed.
Hint Resolve proj1_comp proj2_comp: algebra.

Definition proj1_map : MAP (cart E F) E := Build_Map proj1_comp.

Definition proj2_map : MAP (cart E F) F := Build_Map proj2_comp.

Definition couple (x : E) (y : F) : cart E F := Build_cart_type x y.

Lemma couple_comp :
 forall (x x' : E) (y y' : F),
 Equal x x' -> Equal y y' -> Equal (couple x y) (couple x' y').
(* Goal: @Equal (MAP E (cart F G)) (map_couple map_proj1 map_proj2) f *)
simpl in |- *.
(* Goal: forall (x y : cart_type) (_ : and (@Equal E (cart_l x) (cart_l y)) (@Equal F (cart_r x) (cart_r y))), and (@Equal E (cart_l y) (cart_l x)) (@Equal F (cart_r y) (cart_r x)) *)
unfold app_rel, cart_eq in |- *; intuition.
Qed.
Hint Resolve couple_comp: algebra.

Lemma coupl_proj : forall x : cart E F, Equal (couple (proj1 x) (proj2 x)) x.
(* Goal: @Equal (MAP E (cart F G)) (map_couple map_proj1 map_proj2) f *)
simpl in |- *.
(* Goal: forall (x y : cart_type) (_ : and (@Equal E (cart_l x) (cart_l y)) (@Equal F (cart_r x) (cart_r y))), and (@Equal E (cart_l y) (cart_l x)) (@Equal F (cart_r y) (cart_r x)) *)
unfold app_rel, cart_eq in |- *; intuition.
Qed.
Hint Resolve coupl_proj: algebra.
End Projections.
Section Maps.
Variable E F G : Setoid.

Definition curry (f : MAP (cart E F) G) (x : E) (y : F) := f (couple x y).

Definition fun2_compatible (f : E -> F -> G) :=
  forall (x x' : E) (y y' : F),
  Equal x x' -> Equal y y' -> Equal (f x y) (f x' y').

Definition uncurry :
  forall f : E -> F -> G, fun2_compatible f -> MAP (cart E F) G.
(* Goal: forall (f : forall (_ : Carrier E) (_ : Carrier F), Carrier G) (_ : fun2_compatible f), Carrier (MAP (cart E F) G) *)
intros f H'; try assumption.
(* Goal: Carrier (MAP (cart E F) G) *)
apply (Build_Map (Ap:=fun x : cart E F => f (proj1 x) (proj2 x))).
(* Goal: @Map_eq E (cart F G) (map_couple map_proj1 map_proj2) f *)
red in |- *.
(* Goal: forall (x y : Carrier (cart E F)) (_ : @Equal (cart E F) x y), @Equal G (f (@proj1 E F x) (@proj2 E F x)) (f (@proj1 E F y) (@proj2 E F y)) *)
intros x y; try assumption.
(* Goal: forall _ : @Equal (cart E F) x y, @Equal G (f (@proj1 E F x) (@proj2 E F x)) (f (@proj1 E F y) (@proj2 E F y)) *)
elim x.
(* Goal: forall (cart_l : Carrier E) (cart_r : Carrier F) (_ : @Equal (cart E F) (@Build_cart_type E F cart_l cart_r) y), @Equal G (f (@proj1 E F (@Build_cart_type E F cart_l cart_r)) (@proj2 E F (@Build_cart_type E F cart_l cart_r))) (f (@proj1 E F y) (@proj2 E F y)) *)
elim y.
(* Goal: @Equal (MAP E (cart F G)) (map_couple map_proj1 map_proj2) f *)
simpl in |- *.
(* Goal: forall (x y : cart_type) (_ : and (@Equal E (cart_l x) (cart_l y)) (@Equal F (cart_r x) (cart_r y))), and (@Equal E (cart_l y) (cart_l x)) (@Equal F (cart_r y) (cart_r x)) *)
unfold app_rel, cart_eq in |- *; intuition.
Defined.
Variable f : MAP E (cart F G).

Definition map_proj1 : MAP E F := comp_map_map (proj1_map F G) f.

Definition map_proj2 : MAP E G := comp_map_map (proj2_map F G) f.

Definition map_couple : MAP E F -> MAP E G -> MAP E (cart F G).
(* Goal: forall (_ : Carrier (MAP E F)) (_ : Carrier (MAP E G)), Carrier (MAP E (cart F G)) *)
intros g h.
(* Goal: Carrier (MAP E (cart F G)) *)
apply (Build_Map (Ap:=fun x : E => couple (g x) (h x))).
(* Goal: @Map_eq E (cart F G) (map_couple map_proj1 map_proj2) f *)
red in |- *.
(* Goal: forall (x y : Carrier E) (_ : @Equal E x y), @Equal (cart F G) (@couple F G (@Ap E F g x) (@Ap E G h x)) (@couple F G (@Ap E F g y) (@Ap E G h y)) *)
intros x y H'; try assumption.
(* Goal: @Equal (cart F G) (@couple F G (@Ap E F g x) (@Ap E G h x)) (@couple F G (@Ap E F g y) (@Ap E G h y)) *)
apply couple_comp; auto with algebra.
Defined.

Lemma map_couple_proj_prop : Equal (map_couple map_proj1 map_proj2) f.
(* Goal: @Equal (MAP E (cart F G)) (map_couple map_proj1 map_proj2) f *)
simpl in |- *.
(* Goal: @Map_eq E (cart F G) (map_couple map_proj1 map_proj2) f *)
red in |- *.
(* Goal: @Equal (MAP E (cart F G)) (map_couple map_proj1 map_proj2) f *)
unfold map_proj1, map_proj2 in |- *; simpl in |- *.
(* Goal: forall (x y : cart_type) (_ : and (@Equal E (cart_l x) (cart_l y)) (@Equal F (cart_r x) (cart_r y))), and (@Equal E (cart_l y) (cart_l x)) (@Equal F (cart_r y) (cart_r x)) *)
unfold app_rel, cart_eq in |- *; intuition.
Qed.
End Maps.
Hint Resolve proj1_comp proj2_comp couple_comp coupl_proj
  map_couple_proj_prop: algebra.