(* 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                                                     *)



Require Export Relations.

Set Implicit Arguments.
Unset Strict Implicit.

(* evite le clash d'univers entre le setoide des foncteur et SET *)
  
(***  SETOID  ***)

Structure > Setoid' : Type := 
  {Carrier' :> Type;
   Equal' : Relation Carrier';
   Prf_equiv' :> Equivalence Equal'}.

Infix "=_S'" := Equal' (at level 70).

(*** rewrite rules ***)

Lemma Refl' : forall (S : Setoid') (x : S), x =_S' x.
Proof.
(* Goal: forall (S : Setoid') (x : Carrier' S), @Equal' S x x *)
intro S; exact (Prf_refl S).
Qed.

Lemma Sym' : forall (S : Setoid') (x y : S), x =_S' y -> y =_S' x.
Proof.
(* Goal: forall (S : Setoid') (x y : Carrier' S) (_ : @Equal' S x y), @Equal' S y x *)
intro S; exact (Prf_sym S).
Qed.

Lemma Trans' :
 forall (S : Setoid') (x y z : S), x =_S' y -> y =_S' z -> x =_S' z.
Proof.
(* Goal: forall (S : Setoid') (x y z : Carrier' S) (_ : @Equal' S x y) (_ : @Equal' S y z), @Equal' S x z *)
intro S; exact (Prf_trans S).
Qed.

(* *)

(***  MAP  ***)

Section maps'.

Variable A B : Setoid'.

Definition Map_law' (f : A -> B) := forall x y : A, x =_S' y -> f x =_S' f y.

Structure > Map' : Type :=  {Ap' :> A -> B; Pres' :> Map_law' Ap'}.

(*** rewrite rule ***)

Lemma Pres1' : forall (m : Map') (x y : A), x =_S' y -> m x =_S' m y.
Proof.
(* Goal: forall (m : Map') (x y : Carrier' A) (_ : @Equal' A x y), @Equal' B (Ap' m x) (Ap' m y) *)
exact Pres'.
Qed.

(* *)

Definition Ext' (f g : Map') := forall x : A, f x =_S' g x.

Lemma Ext_equiv' : Equivalence Ext'.
Proof.
(* Goal: @Equivalence Map' Ext' *)
intros; apply Build_Equivalence.
(* Goal: @Reflexive Map' Ext' *)
(* Goal: @Partial_equivalence Map' Ext' *)
unfold Reflexive in |- *; unfold Ext' in |- *; intros f x.
(* Goal: @Equal' B (Ap' f x) (Ap' f x) *)
(* Goal: @Partial_equivalence Map' Ext' *)
apply Refl'.
(* Goal: @Partial_equivalence Map' Ext' *)
apply Build_Partial_equivalence.
(* Goal: @Transitive Map' Ext' *)
(* Goal: @Symmetric Map' Ext' *)
unfold Transitive in |- *; unfold Ext' in |- *; intros f g h e1 e2 x.
(* Goal: @Equal' B (Ap' f x) (Ap' h x) *)
(* Goal: @Symmetric Map' Ext' *)
(* *) apply Trans' with (g x).
(* Goal: @Equal' B (Ap' f x) (Ap' g x) *)
(* Goal: @Equal' B (Ap' g x) (Ap' h x) *)
(* Goal: @Symmetric Map' Ext' *)
apply (e1 x).
(* Goal: @Equal' B (Ap' g x) (Ap' h x) *)
(* Goal: @Symmetric Map' Ext' *)
apply (e2 x).
(* Goal: @Symmetric Map' Ext' *)
unfold Symmetric in |- *; unfold Ext' in |- *; intros f g e x.
(* Goal: @Equal' B (Ap' g x) (Ap' f x) *)
apply Sym'; trivial.
Qed.

Canonical Structure Map_setoid' : Setoid' := Ext_equiv'.

End maps'.

(*** MAP2 ***)

Section fun2_to_map2'.

Variable A B C : Setoid'.

Definition Map2' := Map' A (Map_setoid' B C).

Variable f : A -> B -> C.

Definition Map2_congl_law' :=
  forall (b1 b2 : B) (a : A), b1 =_S' b2 -> f a b1 =_S' f a b2.

Definition Map2_congr_law' :=
  forall (a1 a2 : A) (b : B), a1 =_S' a2 -> f a1 b =_S' f a2 b.

Definition Map2_cong_law' :=
  forall (a1 a2 : A) (b1 b2 : B),
  a1 =_S' a2 -> b1 =_S' b2 -> f a1 b1 =_S' f a2 b2.

Hypothesis pgcl : Map2_congl_law'.
Hypothesis pgcr : Map2_congr_law'.

Lemma Map2_map_law1' : forall a : A, Map_law' (f a).
Proof.
(* Goal: forall a : Carrier' A, @Map_law' B C (f a) *)
intro a; unfold Map_law' in |- *.
(* Goal: forall (x y : Carrier' B) (_ : @Equal' B x y), @Equal' C (f a x) (f a y) *)
intros b1 b2 H; apply (pgcl a H).
Qed.

Canonical Structure Map2_map1' (a : A) := Build_Map' (Map2_map_law1' a).

Lemma Map2_map_law2' : Map_law' Map2_map1'.
Proof.
(* Goal: @Map_law' A (Map_setoid' B C) Map2_map1' *)
unfold Map_law', Map2_map1' in |- *.
(* Goal: forall (x y : Carrier' A) (_ : @Equal' A x y), @Equal' (Map_setoid' B C) (@Build_Map' B C (f x) (@Map2_map_law1' x)) (@Build_Map' B C (f y) (@Map2_map_law1' y)) *)
intros a1 a2 H; simpl in |- *; unfold Ext' in |- *; intro b; simpl in |- *.
(* Goal: @Equal' C (f a1 b) (f a2 b) *)
apply pgcr; trivial.
Qed.

Definition Build_Map2' : Map2' := Build_Map' Map2_map_law2'.

End fun2_to_map2'.


Section prop_map2'.

Variables (A B C : Setoid') (f : Map2' A B C).

Definition Ap2' (a : A) (b : B) := f a b.

Lemma Prf_map2_congl' : Map2_congl_law' Ap2'.
Proof.
(* Goal: @Map2_congl_law' A B C Ap2' *)
unfold Map2_congl_law' in |- *; intros b1 b2 a H.
(* Goal: @Equal' C (Ap2' a b1) (Ap2' a b2) *)
unfold Ap2' in |- *; apply (Pres1' (f a)); trivial.
Qed.

Lemma Prf_map2_congr' : Map2_congr_law' Ap2'.
Proof.
(* Goal: @Map2_congr_law' A B C Ap2' *)
unfold Map2_congr_law' in |- *; intros a1 a2 b H.
(* Goal: @Equal' C (Ap2' a1 b) (Ap2' a2 b) *)
apply (Pres1' f H b).
Qed.

Lemma Prf_map2_cong' : Map2_cong_law' Ap2'.
Proof.
(* Goal: @Map2_cong_law' A B C Ap2' *)
unfold Map2_cong_law' in |- *; intros a1 a2 b1 b2 H1 H2.
(* Goal: @Equal' C (Ap2' a1 b1) (Ap2' a2 b2) *)
(* *) apply Trans' with (Ap2' a2 b1).
(* Goal: @Equal' C (Ap2' a1 b1) (Ap2' a2 b1) *)
(* Goal: @Equal' C (Ap2' a2 b1) (Ap2' a2 b2) *)
apply (Prf_map2_congr' b1 H1).
(* Goal: @Equal' C (Ap2' a2 b1) (Ap2' a2 b2) *)
apply (Prf_map2_congl' a2 H2).
Qed.

End prop_map2'.

Coercion Ap2' : Map2' >-> Funclass.

Identity Coercion Map2'_Map' : Map2' >-> Map'.


