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


(*****************************************************************************)
(*          Projet Formel - Calculus of Inductive Constructions V5.10        *)
(*****************************************************************************)
(*									     *)
(*	                       SubSetoid                  		     *)
(*									     *)
(*****************************************************************************)
(*									     *)
(*                     A. SAIBI	  May 95                  		     *)
(*									     *)
(*****************************************************************************)

(* (SubSetoid A P) setoid of elements of A with the property P *)

Require Export Map.

Set Implicit Arguments.
Unset Strict Implicit.

Section sub_setoid.

Variable U : Setoid.

Definition Reg_law (A : U -> Prop) := forall x y : U, x =_S y -> A x -> A y.

Structure > Setoid_pred : Type := 
  {Pred :> U -> Prop; Prf_reg :> Reg_law Pred}.

Variable A : Setoid_pred.

Structure SubType : Type :=  {Elt_sub : U; Prf_constr : A Elt_sub}.

Definition Equal_SubType (a b : SubType) := Elt_sub a =_S Elt_sub b.

Lemma Equal_SubType_equiv : Equivalence Equal_SubType.
Proof.
(* Goal: @Equivalence SubType Equal_SubType *)
apply Build_Equivalence.
(* Goal: @Reflexive SubType Equal_SubType *)
(* Goal: @Partial_equivalence SubType Equal_SubType *)
unfold Reflexive in |- *; intro x; exact (Refl (Elt_sub x)).
(* Goal: @Partial_equivalence SubType Equal_SubType *)
apply Build_Partial_equivalence.
(* Goal: @Transitive SubType Equal_SubType *)
(* Goal: @Symmetric SubType Equal_SubType *)
unfold Transitive in |- *; intros a b c H1 H2; unfold Equal_SubType in |- *.
(* Goal: @Equal U (Elt_sub a) (Elt_sub c) *)
(* Goal: @Symmetric SubType Equal_SubType *)
apply Trans with (Elt_sub b); auto.
(* Goal: @Symmetric SubType Equal_SubType *)
unfold Symmetric in |- *; intros a b H; unfold Equal_SubType in |- *.
(* Goal: @Equal U (Elt_sub b) (Elt_sub a) *)
apply Sym; auto.
Qed.

Canonical Structure SubSetoid : Setoid := Equal_SubType_equiv.

End sub_setoid.

Section restricted_map.

Variables (A B : Setoid) (f : Map A B) (P : Setoid_pred A).

Definition Restricted_fun (a : SubSetoid P) := f (Elt_sub a).

Lemma Restricted_map_law : Map_law Restricted_fun.
Proof.
(* Goal: @Map_law (@SubSetoid A P) B Restricted_fun *)
unfold Map_law in |- *; simpl in |- *.
(* Goal: forall (x y : @SubType A P) (_ : @Equal_SubType A P x y), @Equal B (Restricted_fun x) (Restricted_fun y) *)
unfold Equal_SubType in |- *; intros a1 a2 H.
(* Goal: @Equal B (Restricted_fun a1) (Restricted_fun a2) *)
unfold Restricted_fun in |- *; apply Pres1; trivial.
Qed.

Canonical Structure RestrictedMap := Build_Map Restricted_map_law.

End restricted_map.

