(**************************************************************************) (* ___ *) (* ||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: CFields.v,v 1.12 2004/04/23 10:00:52 lcf Exp $ *) (*#* printing [/] %\ensuremath{/}% #/# *) (*#* printing [//] %\ensuremath\ddagger% #‡# *) (*#* printing {/} %\ensuremath{/}% #/# *) (*#* printing {1/} %\ensuremath{\frac1\cdot}% #1/# *) (*#* printing [/]?[//] %\ensuremath{/?\ddagger}% #/?‡# *) include "algebra/CRings.ma". (* UNEXPORTED Transparent sym_eq. *) (* UNEXPORTED Transparent f_equal. *) (* UNEXPORTED Transparent cs_crr. *) (* UNEXPORTED Transparent csg_crr. *) (* UNEXPORTED Transparent cm_crr. *) (* UNEXPORTED Transparent cg_crr. *) (* UNEXPORTED Transparent cr_crr. *) (* UNEXPORTED Transparent csf_fun. *) (* UNEXPORTED Transparent csbf_fun. *) (* UNEXPORTED Transparent csr_rel. *) (* UNEXPORTED Transparent cs_eq. *) (* UNEXPORTED Transparent cs_neq. *) (* UNEXPORTED Transparent cs_ap. *) (* UNEXPORTED Transparent cm_unit. *) (* UNEXPORTED Transparent csg_op. *) (* UNEXPORTED Transparent cg_inv. *) (* UNEXPORTED Transparent cg_minus. *) (* UNEXPORTED Transparent cr_one. *) (* UNEXPORTED Transparent cr_mult. *) (* UNEXPORTED Transparent nexp_op. *) (* Begin_SpecReals *) (* FIELDS *) (*#* * Fields %\label{section:fields}% ** Definition of the notion Field *) inline procedural "cic:/CoRN/algebra/CFields/is_CField.con" as definition. inline procedural "cic:/CoRN/algebra/CFields/CField.ind". (* COERCION cic:/matita/CoRN-Procedural/algebra/CFields/cf_crr.con *) (* End_SpecReals *) inline procedural "cic:/CoRN/algebra/CFields/f_rcpcl'.con" as definition. inline procedural "cic:/CoRN/algebra/CFields/f_rcpcl.con" as definition. (* UNEXPORTED Implicit Arguments f_rcpcl [F]. *) (*#* [cf_div] is the division in a field. It is defined in terms of multiplication and the reciprocal. [x[/]y] is only defined if we have a proof of [y [#] Zero]. *) inline procedural "cic:/CoRN/algebra/CFields/cf_div.con" as definition. (* UNEXPORTED Implicit Arguments cf_div [F]. *) (* NOTATION Notation "x [/] y [//] Hy" := (cf_div x y Hy) (at level 80). *) (*#* %\begin{convention}\label{convention:div-form}% - Division in fields is a (type dependent) ternary function: [(cf_div x y Hy)] is denoted infix by [x [/] y [//] Hy]. - In lemmas, a hypothesis that [t [#] Zero] will be named [t_]. - We do not use [NonZeros], but write the condition [ [#] Zero] separately. - In each lemma, we use only variables for proof objects, and these variables are universally quantified. For example, the informal lemma $\frac{1}{x}\cdot\frac{1}{y} = \frac{1}{x\cdot y}$ #(1/x).(1/y) = 1/(x.y)# for all [x] and [y]is formalized as [[ forall (x y : F) x_ y_ xy_, (1[/]x[//]x_) [*] (1[/]y[//]y_) [=] 1[/] (x[*]y)[//]xy_ ]] and not as [[ forall (x y : F) x_ y_, (1[/]x[//]x_) [*] (1[/]y[//]y_) [=] 1[/] (x[*]y)[//](prod_nz x y x_ y_) ]] We have made this choice to make it easier to apply lemmas; this can be quite awkward if we would use the last formulation. - So every division occurring in the formulation of a lemma is of the form [e[/]e'[//]H] where [H] is a variable. Only exceptions: we may write [e[/] (Snring n)] and [e[/]TwoNZ], [e[/]ThreeNZ] and so on. (Constants like [TwoNZ] will be defined later on.) %\end{convention}% ** Field axioms %\begin{convention}% Let [F] be a field. %\end{convention}% *) (* UNEXPORTED Section Field_axioms *) (* UNEXPORTED cic:/CoRN/algebra/CFields/Field_axioms/F.var *) inline procedural "cic:/CoRN/algebra/CFields/CField_is_CField.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/rcpcl_is_inverse.con" as lemma. (* UNEXPORTED End Field_axioms *) (* UNEXPORTED Section Field_basics *) (*#* ** Field basics %\begin{convention}% Let [F] be a field. %\end{convention}% *) (* UNEXPORTED cic:/CoRN/algebra/CFields/Field_basics/F.var *) inline procedural "cic:/CoRN/algebra/CFields/rcpcl_is_inverse_unfolded.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/field_mult_inv.con" as lemma. (* UNEXPORTED Hint Resolve field_mult_inv: algebra. *) inline procedural "cic:/CoRN/algebra/CFields/field_mult_inv_op.con" as lemma. (* UNEXPORTED End Field_basics *) (* UNEXPORTED Hint Resolve field_mult_inv field_mult_inv_op: algebra. *) (* UNEXPORTED Section Field_multiplication *) (*#* ** Properties of multiplication %\begin{convention}% Let [F] be a field. %\end{convention}% *) (* UNEXPORTED cic:/CoRN/algebra/CFields/Field_multiplication/F.var *) inline procedural "cic:/CoRN/algebra/CFields/mult_resp_ap_zero.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/mult_lft_resp_ap.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/mult_rht_resp_ap.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/mult_resp_neq_zero.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/mult_resp_neq.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/mult_eq_zero.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/mult_cancel_lft.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/mult_cancel_rht.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/square_eq_aux.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/square_eq_weak.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/cond_square_eq.con" as lemma. (* UNEXPORTED End Field_multiplication *) (* UNEXPORTED Section x_square *) inline procedural "cic:/CoRN/algebra/CFields/x_xminone.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/square_id.con" as lemma. (* UNEXPORTED End x_square *) (* UNEXPORTED Hint Resolve mult_resp_ap_zero: algebra. *) (* UNEXPORTED Section Rcpcl_properties *) (*#* ** Properties of reciprocal %\begin{convention}% Let [F] be a field. %\end{convention}% *) (* UNEXPORTED cic:/CoRN/algebra/CFields/Rcpcl_properties/F.var *) inline procedural "cic:/CoRN/algebra/CFields/inv_one.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/f_rcpcl_wd.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/f_rcpcl_mult.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/f_rcpcl_resp_ap_zero.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/f_rcpcl_f_rcpcl.con" as lemma. (* UNEXPORTED End Rcpcl_properties *) (* UNEXPORTED Section MultipGroup *) (*#* ** The multiplicative group of nonzeros of a field. %\begin{convention}% Let [F] be a field %\end{convention}% *) (* UNEXPORTED cic:/CoRN/algebra/CFields/MultipGroup/F.var *) (*#* The multiplicative monoid of NonZeros. *) inline procedural "cic:/CoRN/algebra/CFields/NonZeroMonoid.con" as definition. inline procedural "cic:/CoRN/algebra/CFields/fmg_cs_inv.con" as definition. inline procedural "cic:/CoRN/algebra/CFields/plus_nonzeros_eq_mult_dom.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/cfield_to_mult_cgroup.con" as lemma. (* UNEXPORTED End MultipGroup *) (* UNEXPORTED Section Div_properties *) (*#* ** Properties of division %\begin{convention}% Let [F] be a field. %\end{convention}% %\begin{nameconvention}% In the names of lemmas, we denote [[/]] by [div], and [One[/]] by [recip]. %\end{nameconvention}% *) (* UNEXPORTED cic:/CoRN/algebra/CFields/Div_properties/F.var *) inline procedural "cic:/CoRN/algebra/CFields/div_prop.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/div_1.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/div_1'.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/div_1''.con" as lemma. (* UNEXPORTED Hint Resolve div_1: algebra. *) inline procedural "cic:/CoRN/algebra/CFields/x_div_x.con" as lemma. (* UNEXPORTED Hint Resolve x_div_x: algebra. *) inline procedural "cic:/CoRN/algebra/CFields/x_div_one.con" as lemma. (*#* The next lemma says $x\cdot\frac{y}{z} = \frac{x\cdot y}{z}$ #x.(y/z) = (x.y)/z#. *) inline procedural "cic:/CoRN/algebra/CFields/x_mult_y_div_z.con" as lemma. (* UNEXPORTED Hint Resolve x_mult_y_div_z: algebra. *) inline procedural "cic:/CoRN/algebra/CFields/div_wd.con" as lemma. (* UNEXPORTED Hint Resolve div_wd: algebra_c. *) (*#* The next lemma says $\frac{\frac{x}{y}}{z} = \frac{x}{y\cdot z}$ #[(x/y)/z = x/(y.z)]# *) inline procedural "cic:/CoRN/algebra/CFields/div_div.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/div_resp_ap_zero_rev.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/div_resp_ap_zero.con" as lemma. (*#* The next lemma says $\frac{x}{\frac{y}{z}} = \frac{x\cdot z}{y}$ #[x/(y/z) = (x.z)/y]# *) inline procedural "cic:/CoRN/algebra/CFields/div_div2.con" as lemma. (*#* The next lemma says $\frac{x\cdot p}{y\cdot q} = \frac{x}{y}\cdot \frac{p}{q}$ #[(x.p)/(y.q) = (x/y).(p/q)]# *) inline procedural "cic:/CoRN/algebra/CFields/mult_of_divs.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/div_dist.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/div_dist'.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/div_semi_sym.con" as lemma. (* UNEXPORTED Hint Resolve div_semi_sym: algebra. *) inline procedural "cic:/CoRN/algebra/CFields/eq_div.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/div_strext.con" as lemma. (* UNEXPORTED End Div_properties *) (* UNEXPORTED Hint Resolve div_1 div_1' div_1'' div_wd x_div_x x_div_one div_div div_div2 mult_of_divs x_mult_y_div_z mult_of_divs div_dist div_dist' div_semi_sym div_prop: algebra. *) (*#* ** Cancellation laws for apartness and multiplication %\begin{convention}% Let [F] be a field %\end{convention}% *) (* UNEXPORTED Section Mult_Cancel_Ap_Zero *) (* UNEXPORTED cic:/CoRN/algebra/CFields/Mult_Cancel_Ap_Zero/F.var *) inline procedural "cic:/CoRN/algebra/CFields/mult_cancel_ap_zero_lft.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/mult_cancel_ap_zero_rht.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/recip_ap_zero.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/recip_resp_ap.con" as lemma. (* UNEXPORTED End Mult_Cancel_Ap_Zero *) (* UNEXPORTED Section CField_Ops *) (*#* ** Functional Operations We now move on to lifting these operations to functions. As we are dealing with %\emph{partial}% #partial# functions, we don't have to worry explicitly about the function by which we are dividing being non-zero everywhere; this will simply be encoded in its domain. %\begin{convention}% Let [X] be a Field and [F,G:(PartFunct X)] have domains respectively [P] and [Q]. %\end{convention}% *) (* UNEXPORTED cic:/CoRN/algebra/CFields/CField_Ops/X.var *) (* UNEXPORTED cic:/CoRN/algebra/CFields/CField_Ops/F.var *) (* UNEXPORTED cic:/CoRN/algebra/CFields/CField_Ops/G.var *) (* begin hide *) inline procedural "cic:/CoRN/algebra/CFields/CField_Ops/P.con" "CField_Ops__" as definition. inline procedural "cic:/CoRN/algebra/CFields/CField_Ops/Q.con" "CField_Ops__" as definition. (* end hide *) (* UNEXPORTED Section Part_Function_Recip *) (*#* Some auxiliary notions are helpful in defining the domain. *) inline procedural "cic:/CoRN/algebra/CFields/CField_Ops/Part_Function_Recip/R.con" "CField_Ops__Part_Function_Recip__" as definition. inline procedural "cic:/CoRN/algebra/CFields/CField_Ops/Part_Function_Recip/Ext2R.con" "CField_Ops__Part_Function_Recip__" as definition. inline procedural "cic:/CoRN/algebra/CFields/part_function_recip_strext.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/part_function_recip_pred_wd.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/Frecip.con" as definition. (* UNEXPORTED End Part_Function_Recip *) (* UNEXPORTED Section Part_Function_Div *) (*#* For division things work out almost in the same way. *) inline procedural "cic:/CoRN/algebra/CFields/CField_Ops/Part_Function_Div/R.con" "CField_Ops__Part_Function_Div__" as definition. inline procedural "cic:/CoRN/algebra/CFields/CField_Ops/Part_Function_Div/Ext2R.con" "CField_Ops__Part_Function_Div__" as definition. inline procedural "cic:/CoRN/algebra/CFields/part_function_div_strext.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/part_function_div_pred_wd.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/Fdiv.con" as definition. (* UNEXPORTED End Part_Function_Div *) (*#* %\begin{convention}% Let [R:X->CProp]. %\end{convention}% *) (* UNEXPORTED cic:/CoRN/algebra/CFields/CField_Ops/R.var *) inline procedural "cic:/CoRN/algebra/CFields/included_FRecip.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/included_FRecip'.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/included_FDiv.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/included_FDiv'.con" as lemma. inline procedural "cic:/CoRN/algebra/CFields/included_FDiv''.con" as lemma. (* UNEXPORTED End CField_Ops *) (* UNEXPORTED Implicit Arguments Frecip [X]. *) (* NOTATION Notation "{1/} x" := (Frecip x) (at level 2, right associativity). *) (* UNEXPORTED Implicit Arguments Fdiv [X]. *) (* NOTATION Infix "{/}" := Fdiv (at level 41, no associativity). *) (* UNEXPORTED Hint Resolve included_FRecip included_FDiv : included. *) (* UNEXPORTED Hint Immediate included_FRecip' included_FDiv' included_FDiv'' : included. *)