Library ideal_tes
Require Export ecuaciones_tes.
Inductive Ideal: pol->(list pol)->Prop:=
ideal_vpol: (p:pol)(F:(list pol))(full_term_pol p)->
(equpol p vpol)->(Ideal p F)
| ideal_cpol: (p,p',q,q':pol)(F:(list pol))(full_term_pol p)->
(full_term_pol q')->
(Ideal p' F)->(equpol p (suma_app (mult_p q q') p'))->
(Ideal p (cons q F)).
Hints Resolve ideal_vpol ideal_cpol.
Inductive pol_In_ensemb [p:pol]: (list pol)->Prop:=
pol_In_hd: (p':pol)(F:(list pol))(full_term_pol p')->
(full_term_pol p)->(equpol p p')->(pol_In_ensemb p (cons p' F))
| pol_In_tl: (p':pol)(F:(list pol))(pol_In_ensemb p F)->
(pol_In_ensemb p (cons p' F)).
Hints Resolve pol_In_hd pol_In_tl.
Lemma pol_In_ensemb_unic: (f,f0:pol)(pol_In_ensemb f0 (cons f (nil pol)))->(equpol f0 f).
Intros.
Inversion H; Trivial.
Inversion H1; Trivial.
Save.
Lemma pol_In_ensemb_ext: (x:pol)(F:(list pol))(y:pol)(full_term_pol y)->
(equpol x y)->(pol_In_ensemb x F)->(pol_In_ensemb y F).
Intros x F y fy exy.
Induction 1; Intros.
Apply pol_In_hd; Auto.
Apply equpol_tran with x; Auto.
Apply pol_In_tl; Trivial.
Save.
Require Export Relations.
Lemma pol_eq_id_eg: (f,g:pol)(F:(list pol))(Ideal f F)->
(equpol f g)->(full_term_pol g)->(Ideal g F).
Intros f g F i d fg.
Inversion i.
(Apply ideal_vpol; Trivial).
(Apply equpol_tran with f; Auto).
(Apply ideal_cpol with p':=p' q':=q'; Trivial).
(Apply equpol_tran with f; Auto).
Save.
Hints Resolve pol_eq_id_eg.
Lemma ideal_mon : (F:(list pol))(p,g:pol)(Ideal p F)->(Ideal p (cons g F)).
Intros F p g i.
Inversion i.
Apply ideal_vpol; Auto.
(Apply ideal_cpol with p':=p q':=vpol; Trivial).
Replace (cons q F0) with F; Trivial.
Apply equpol_tran with (suma_app vpol p);Auto.
Save.
Hints Resolve ideal_mon.
Lemma mult_p_id: (f,g:pol)(F:(list pol))(Ideal f F)->(full_term_pol g)->
(Ideal (mult_p f g) F).
Induction 1.
Intros.
Apply ideal_vpol.
(Apply full_term_mult_p; Auto).
Apply equpol_tran with (mult_p vpol g); Auto.
Intros.
Apply ideal_cpol with p':=(mult_p p' g) q':=(mult_p q' g).
Apply full_term_mult_p; Auto.
Apply full_term_mult_p; Auto.
Auto.
Apply equpol_tran with (mult_p (suma_app (mult_p q q') p') g).
EAuto.
Apply equpol_tran
with (suma_app (mult_p (mult_p q q') g) (mult_p p' g)).
Auto.
EAuto.
Save.
Hints Resolve mult_p_id.
Lemma p_idp: (p:pol)(F:(list pol))(full_term_pol p)->(Ideal p (cons p F)).
Intros.
Apply ideal_cpol with p':=vpol q':=(cpol (unQ,(n_term_O n)) vpol).
Auto.
Auto.
Auto.
Apply equpol_tran with (mult_p p (cpol (unQ,(n_term_O n)) vpol)); Auto.
Save.
Hints Resolve p_idp.
Lemma pol_F_idF: (f:pol)(F:(list pol))(pol_In_ensemb f F)->
(full_term_pol f)->(Ideal f F).
Induction 1; Intros; Auto.
Apply pol_eq_id_eg with p'; Auto.
Save.
Hints Resolve pol_F_idF.
Lemma pol_F_idmult: (f:pol)(m:monom)(F:(list pol))(pol_In_ensemb f F)->
(full_term_pol f)->(full_mon n m)->(Ideal (mult_m f m) F).
Intros.
Apply pol_eq_id_eg with (mult_p f (cpol m vpol)); Auto.
Generalize m H0 H1; Induction m0; Intros.
Apply full_mult_m; Trivial.
Save.
Hints Resolve pol_F_idmult.
Lemma opp_p_id: (f:pol)(F:(list pol))(Ideal f F)->
(Ideal (pol_opp f) F).
Intros.
Apply pol_eq_id_eg
with (mult_p f (cpol ((multQ_neg unQ),(n_term_O n)) vpol)).
Auto.
Inversion H; Auto.
Inversion H; Auto.
Save.
Hints Resolve opp_p_id.
Lemma suma_p_id: (f:pol)(F:(list pol))(Ideal f F)->(g:pol)(Ideal g F)
->(Ideal (suma_app f g) F).
Induction 1.
Intros.
(Apply pol_eq_id_eg with f:=g; Auto).
(Apply equpol_tran with (suma_app vpol g); Auto).
Apply full_term_suma_app; Auto.
Inversion H2; Auto.
Intros.
Inversion H5.
Apply ideal_cpol with p':=p' q':=q'; Auto.
Apply equpol_tran with (suma_app p vpol); Auto.
Apply equpol_tran with p; Auto.
Apply ideal_cpol with p':=(suma_app p' p'0) q':=(suma_app q' q'0).
Apply full_term_suma_app; Auto.
Apply full_term_suma_app; Auto.
Elim (H3 p'0).
Auto.
Intros.
Apply ideal_cpol with p':=p'1 q':=q'1; Auto.
Assumption.
Apply equpol_tran
with (suma_app (suma_app (mult_p q q') (mult_p q q'0))
(suma_app p' p'0)).
Apply equpol_tran
with (suma_app (suma_app (mult_p q q') p')
(suma_app (mult_p q q'0) p'0)).
Auto.
Apply equpol_tran
with (suma_app (mult_p q q')
(suma_app p' (suma_app (mult_p q q'0) p'0))).
Auto.
Apply equpol_tran
with (suma_app (mult_p q q')
(suma_app (mult_p q q'0) (suma_app p' p'0))).
Auto.
Auto.
Auto.
Save.
Hints Resolve suma_p_id.
Lemma opp_p_id2: (f,g:pol)(F:(list pol))(Ideal f F)->
(equpol g (pol_opp f))->(full_term_pol g)->(Ideal g F).
Intros.
Apply pol_eq_id_eg with (pol_opp f); Auto.
Save.
Hints Resolve opp_p_id2.
Lemma oppm_idp: (p:pol)(m:monom)(F:(list pol))(full_term_pol p)->
(full_mon n m)->(Ideal (pol_opp (mult_m p m)) (cons p F)).
Intros.
Apply opp_p_id; Auto.
Save.
Hints Resolve oppm_idp.
Lemma pol_F_idmult_opp: (f:pol)(m:monom)(F:(list pol))
(pol_In_ensemb f F)->(full_term_pol f)->(full_mon n m)->
(Ideal (pol_opp (mult_m f m)) F).
Intros.
Apply opp_p_id; Auto.
Save.
Hints Resolve pol_F_idmult_opp.
Lemma id_trans: (F:(list pol))(f,g0,h0:pol)(Ideal h0 (cons f F))->
(Ideal f (cons g0 F))->(Ideal h0 (cons g0 F)).
Intros.
Inversion H; Auto.
Inversion H0.
Cut (equpol h0 p'); Intros.
Apply ideal_mon.
Apply pol_eq_id_eg with p'; Auto.
Apply equpol_tran with (suma_app (mult_p f q') p'); Auto.
Apply equpol_tran with (suma_app vpol p'); Auto.
Apply equpol_ss; Auto.
Apply equpol_tran with (mult_p vpol q'); Auto.
Apply ideal_cpol with (suma_app (mult_p p'0 q') p') (mult_p q'0 q');
Auto.
Apply equpol_tran with (suma_app (mult_p f q') p'); Auto.
Apply equpol_tran
with (suma_app (suma_app (mult_p g0 (mult_p q'0 q')) (mult_p p'0 q'))
p'); Auto.
Apply equpol_ss; Auto.
Apply equpol_tran with (mult_p (suma_app (mult_p g0 q'0) p'0) q'); Auto.
Apply equpol_tran
with (suma_app (mult_p (mult_p g0 q'0) q') (mult_p p'0 q')); Auto.
Save.
Definition Ideal_ens:= [F:(list pol)][p:pol](Ideal p F).
Hints Unfold Ideal_ens.
Definition eq_Ideal:= [I1,I2:(pol->Prop)]
((p:pol)(I1 p)->(I2 p)) /\ ((p:pol)(I2 p)->(I1 p)).
Hints Unfold eq_Ideal.
Lemma eq_Ideal_eq_p: (p:pol)(F:(list pol))(Ideal p F)->
(eq_Ideal (Ideal_ens F) (Ideal_ens (cons p F))).
Intros.
Unfold eq_Ideal.
Split.
Auto.
Unfold Ideal_ens.
Intros.
Inversion H0.
Auto.
(Apply pol_eq_id_eg with f:=(suma_app (mult_p p q') p'); Auto).
Save.
Hints Resolve eq_Ideal_eq_p.
Index
This page has been generated by coqdoc