(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

(* This file was automatically generated: do not edit *********************)

include "CoRN.ma".

(* $Id: PartInterval.v,v 1.6 2004/04/23 10:01:00 lcf Exp $ *)

include "ftc/IntervalFunct.ma".

(* UNEXPORTED
Section Conversion
*)

(*#* *Correspondence

In this file we prove that there are mappings going in both ways
between the set of partial functions whose domain contains
[[a,b]] and the set of real-valued functions with domain on
that interval.  These mappings form an adjunction, and thus they have
all the good properties for preservation results.

**Mappings

We begin by defining the map from partial functions to setoid
functions as simply being the restriction of the partial function to
the interval [[a,b]].

%\begin{convention}% Let [F] be a partial function and [a,b:IR] such
that [I [=] [a,b]] is included in the domain of [F].
%\end{convention}%
*)

(* UNEXPORTED
cic:/CoRN/ftc/PartInterval/Conversion/F.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/PartInterval/Conversion/a.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/PartInterval/Conversion/b.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/PartInterval/Conversion/Hab.var
*)

(* begin hide *)

inline procedural "cic:/CoRN/ftc/PartInterval/Conversion/I.con" "Conversion__" as definition.

(* end hide *)

(* UNEXPORTED
cic:/CoRN/ftc/PartInterval/Conversion/Hf.var
*)

inline procedural "cic:/CoRN/ftc/PartInterval/IntPartIR_strext.con" as lemma.

inline procedural "cic:/CoRN/ftc/PartInterval/IntPartIR.con" as definition.

(* UNEXPORTED
End Conversion
*)

(* UNEXPORTED
Implicit Arguments IntPartIR [F a b Hab].
*)

(* UNEXPORTED
Section AntiConversion
*)

(*#*
To go the other way around, we simply take a setoid function [f] with
domain [[a,b]] and build the corresponding partial function.
*)

(* UNEXPORTED
cic:/CoRN/ftc/PartInterval/AntiConversion/a.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/PartInterval/AntiConversion/b.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/PartInterval/AntiConversion/Hab.var
*)

(* begin hide *)

inline procedural "cic:/CoRN/ftc/PartInterval/AntiConversion/I.con" "AntiConversion__" as definition.

(* end hide *)

(* UNEXPORTED
cic:/CoRN/ftc/PartInterval/AntiConversion/f.var
*)

inline procedural "cic:/CoRN/ftc/PartInterval/PartInt_strext.con" as lemma.

inline procedural "cic:/CoRN/ftc/PartInterval/PartInt.con" as definition.

(* UNEXPORTED
End AntiConversion
*)

(* UNEXPORTED
Implicit Arguments PartInt [a b Hab].
*)

(* UNEXPORTED
Section Inverses
*)

(*#*
In one direction these operators are inverses.
*)

inline procedural "cic:/CoRN/ftc/PartInterval/int_part_int.con" as lemma.

(* UNEXPORTED
End Inverses
*)

(* UNEXPORTED
Section Equivalences
*)

(*#* **Mappings Preserve Operations

We now prove that all the operations we have defined on both sets are
preserved by [PartInt].

%\begin{convention}% Let [F,G] be partial functions and [a,b:IR] and
denote by [I] the interval [[a,b]].  Let [f,g] be setoid functions of
type [I->IR] equal respectively to [F] and [G] in [I].
%\end{convention}%
*)

(* UNEXPORTED
cic:/CoRN/ftc/PartInterval/Equivalences/F.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/PartInterval/Equivalences/G.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/PartInterval/Equivalences/a.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/PartInterval/Equivalences/b.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/PartInterval/Equivalences/c.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/PartInterval/Equivalences/Hab.var
*)

(* begin hide *)

inline procedural "cic:/CoRN/ftc/PartInterval/Equivalences/I.con" "Equivalences__" as definition.

(* end hide *)

(* UNEXPORTED
cic:/CoRN/ftc/PartInterval/Equivalences/f.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/PartInterval/Equivalences/g.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/PartInterval/Equivalences/Ff.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/PartInterval/Equivalences/Gg.var
*)

inline procedural "cic:/CoRN/ftc/PartInterval/part_int_const.con" as lemma.

inline procedural "cic:/CoRN/ftc/PartInterval/part_int_id.con" as lemma.

inline procedural "cic:/CoRN/ftc/PartInterval/part_int_plus.con" as lemma.

inline procedural "cic:/CoRN/ftc/PartInterval/part_int_inv.con" as lemma.

inline procedural "cic:/CoRN/ftc/PartInterval/part_int_minus.con" as lemma.

inline procedural "cic:/CoRN/ftc/PartInterval/part_int_mult.con" as lemma.

inline procedural "cic:/CoRN/ftc/PartInterval/part_int_nth.con" as lemma.

(* begin show *)

(* UNEXPORTED
cic:/CoRN/ftc/PartInterval/Equivalences/HG.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/PartInterval/Equivalences/Hg.var
*)

(* end show *)

inline procedural "cic:/CoRN/ftc/PartInterval/part_int_recip.con" as lemma.

inline procedural "cic:/CoRN/ftc/PartInterval/part_int_div.con" as lemma.

(* UNEXPORTED
End Equivalences
*)