Library Mult_poly_tes
Require Export Somme_poly_tes.
Fixpoint mult_m [p:pol] : monom -> pol :=
[m:monom]Cases p of
vpol => vpol
| (cpol m1 p1) => (cpol (mult_mon m m1) (mult_m p1 m))
end.
Fixpoint mult_p [p:pol] : pol -> pol :=
[q:pol]Cases p of
vpol => vpol
| (cpol m1 p1) => (suma_app (mult_m q m1) (mult_p p1 q))
end.
Theorem mult_m_vpol: (m:monom) (equpol (mult_m vpol m) vpol).
Auto.
Save.
Hints Resolve mult_m_vpol.
Theorem mult_vpol: (q:pol)(equpol (mult_p q vpol) vpol).
Induction q; Auto.
Save.
Hints Resolve mult_vpol.
Lemma mult_p_cpol: (m:monom)(p,p':pol)(equpol (mult_p p (cpol m p'))
(suma_app (mult_m p m) (mult_p p p'))).
Intros; Elim p; Auto; Intros.
Simpl.
Apply equpol_cpol2; Auto.
Apply equpol_tran with
(suma_app (suma_app (mult_m p0 m) (mult_m p' m0)) (mult_p p0 p'));
Auto.
Apply equpol_tran with
(suma_app (suma_app (mult_m p' m0) (mult_m p0 m)) (mult_p p0 p'));
Auto.
Apply equpol_tran with
(suma_app (mult_m p' m0) (suma_app (mult_m p0 m) (mult_p p0 p')));
Auto.
Save.
Hints Resolve mult_p_cpol.
Lemma mult_m_distr: (p,q:pol)(m:monom)(equpol (mult_m (suma_app p q) m)
(suma_app (mult_m p m) (mult_m q m))).
Intros; Elim p; Auto; Intros.
Simpl; Apply equpol_cpol; Trivial.
Save.
Hints Resolve mult_m_distr.
Lemma mult_m_asoc: (m,n:monom)(p:pol)(equpol (mult_m (mult_m p m) n)
(mult_m p (mult_mon m n))).
Induction p; Auto; Intros m0 p0 HR.
Simpl; Apply equpol_cpol2; Auto.
Save.
Hints Resolve mult_m_asoc.
Lemma mult_pm_comp_2: (m1,m2:monom)(p:pol)(equmon m1 m2)->
(equpol (mult_m p m1) (mult_m p m2)).
Induction p; Auto; Intros.
Simpl; Auto.
Save.
Hints Resolve mult_pm_comp_2.
Lemma mult_p_m_asoc: (m:monom)(p,q:pol)(equpol (mult_m (mult_p p q) m)
(mult_p (mult_m p m) q)).
Induction p; Auto; Intros.
Simpl.
Apply equpol_tran
with (suma_app (mult_m (mult_m q m0) m) (mult_m (mult_p p0 q) m)).
Auto.
Apply equpol_tran with
(suma_app (mult_m q (mult_mon m0 m)) (mult_m (mult_p p0 q) m)).
Auto.
Apply equpol_ss; Auto.
Save.
Hints Resolve mult_p_m_asoc.
Lemma mult_pm_comp: (m:monom)(p1,p2:pol)(equpol p1 p2)->
(equpol (mult_m p1 m) (mult_m p2 m)).
Intros m p1 p2 H; Elim H; Auto; Intros.
Apply equpol_tran with (mult_m q m); Auto.
Simpl.
Apply equpol_tran with
(suma_app (mult_m p m) (mult_m (cpol m0 q) m)); Auto.
Apply equpol_tran with
(cpol (mult_mon m m0) (suma_app (mult_m p m) (mult_m q m))); Auto.
Apply equpol_tran with
(suma_app (mult_m p m) (cpol (mult_mon m m0) (mult_m q m))); Auto.
Apply equpol_tran with (suma_app (mult_m p m) (mult_m q m)); Auto.
Apply equpol_tran with (suma_app (mult_m p' m) (mult_m q' m)); Auto.
Simpl; Elim m; Intros.
Simpl.
Apply equpol_tran
with (cpol ((plusQ (multQ a k) (multQ a k')),(term_mult b t))
(mult_m p (a,b))); Auto.
Simpl; Auto.
Save.
Hints Resolve mult_pm_comp.
Lemma mult_pm_comp_ss: (p1,p2:pol)(equpol p1 p2)->
(m1,m2:monom)(equmon m1 m2)->
(equpol (mult_m p1 m1) (mult_m p2 m2)).
Induction p1.
Induction p2; Auto; Intros.
Apply equpol_tran with (mult_m vpol m2); Auto.
Induction p2; Intros.
Apply equpol_tran with (mult_m vpol m1); Auto.
Apply equpol_tran with (mult_m (cpol m p) m2); Auto.
Save.
Hints Resolve mult_pm_comp_ss.
Lemma mult_p_comp: (p,p',r:pol)(equpol p p')->
(equpol (mult_p r p) (mult_p r p')).
Induction r; Auto.
Intros m p0 HR H; Simpl; Auto.
Save.
Hints Resolve mult_p_comp.
Lemma mult_p_conm: (p,p':pol)(equpol (mult_p p p') (mult_p p' p)).
Intros; Elim p.
Elim p'; Auto.
Intros; Simpl.
Apply equpol_tran with (suma_app (mult_m p' m) (mult_p p' p0));
Auto.
Save.
Hints Resolve mult_p_conm.
Lemma mult_p_comp_r: (p,p',r:pol)(equpol p p')->
(equpol (mult_p p r) (mult_p p' r)).
Intros.
(Apply equpol_tran with (mult_p r p); Auto).
(Apply equpol_tran with (mult_p r p'); Auto).
Save.
Hints Resolve mult_p_comp_r.
Lemma distr_mult_p: (f,g,h:pol)(equpol (mult_p (suma_app f g) h)
(suma_app (mult_p f h) (mult_p g h))).
Induction h.
Apply equpol_tran with vpol.
Auto.
Apply equpol_tran with (suma_app vpol vpol).
Auto.
Auto.
Intros m p HR.
Generalize (mult_p_cpol m (suma_app f g) p) .
Intros.
Apply equpol_tran
with (suma_app (mult_m (suma_app f g) m) (mult_p (suma_app f g) p)).
Auto.
Generalize (mult_m_distr f g m) .
Intros.
Apply equpol_tran
with (suma_app (suma_app (mult_m f m) (mult_m g m))
(mult_p (suma_app f g) p)).
Auto.
Clear H H0.
Generalize (mult_p_cpol m f p) .
Intros.
Apply equpol_tran
with (suma_app (suma_app (mult_m f m) (mult_p f p))
(mult_p g (cpol m p))).
Generalize (mult_p_cpol m g p) .
Intros.
Apply equpol_tran
with (suma_app (suma_app (mult_m f m) (mult_p f p))
(suma_app (mult_m g m) (mult_p g p))).
Clear H H0.
Apply equpol_tran
with (suma_app (suma_app (mult_m f m) (mult_m g m))
(suma_app (mult_p f p) (mult_p g p))).
Auto.
Apply equpol_tran
with (suma_app (mult_m f m)
(suma_app (mult_m g m) (suma_app (mult_p f p) (mult_p g p)))).
Auto.
Apply equpol_tran
with (suma_app (mult_m f m)
(suma_app (mult_p f p) (suma_app (mult_m g m) (mult_p g p)))).
Auto.
Auto.
Auto.
Auto.
Save.
Hints Resolve distr_mult_p.
Lemma distr_mult_p_r: (f,g,h:pol)(equpol (mult_p f (suma_app g h))
(suma_app (mult_p f g) (mult_p f h))).
Intros.
Apply equpol_tran with (mult_p (suma_app g h) f).
Auto.
Apply equpol_tran with (suma_app (mult_p g f) (mult_p h f)).
Auto.
Auto.
Save.
Hints Resolve distr_mult_p_r.
Lemma mult_p_assoc: (p,q,r:pol)(equpol (mult_p p (mult_p q r))
(mult_p (mult_p p q) r)).
Induction p; Auto; Intros.
Apply equpol_tran with (mult_p (mult_p q r) (cpol m p0)); Auto.
Apply equpol_tran with
(suma_app (mult_m (mult_p q r) m) (mult_p (mult_p q r) p0)); Auto.
Apply equpol_tran with
(suma_app (mult_m (mult_p q r) m) (mult_p p0 (mult_p q r))); Auto.
Apply equpol_tran with (mult_p (mult_p q (cpol m p0)) r); Auto.
Apply equpol_tran with
(mult_p (suma_app (mult_m q m) (mult_p q p0)) r); Auto.
Apply equpol_tran with
(mult_p (suma_app (mult_m q m) (mult_p p0 q)) r); Auto.
Apply equpol_tran with
(suma_app (mult_p (mult_m q m) r) (mult_p (mult_p p0 q) r)); Auto.
Save.
Hints Resolve mult_p_assoc.
Lemma neut_mult_m: (f:pol)(full_term_pol f)->
(equpol f (mult_m f (unQ,(n_term_O n)))).
Induction f; Auto.
Intro m; Elim m; Intros.
Simpl.
Inversion H0.
Generalize (H H5); Intros.
Apply equpol_tran
with (cpol ((multQ unQ a),(term_mult (n_term_O n) b)) p).
Generalize (term_mult_full_nulo b n H3); Intro.
Apply equpol_tran
with (cpol ((multQ unQ a),(term_mult b (n_term_O n))) p).
Rewrite H7.
Generalize (neut_multQ a); Intro.
Apply equpol_cpol2; Trivial.
Red; Right.
Split; Auto.
Apply eqQ_trans with (multQ a unQ); Auto.
Apply eq_mon_cpol.
Red; Right; Split; Auto.
Apply equpol_cpol2; Trivial.
Save.
Hints Resolve neut_mult_m.
Lemma neut_mult_p: (p:pol)(full_term_pol p)->(equpol
(mult_p p (cpol (unQ,(n_term_O n)) vpol)) p).
Induction p; Auto.
Intro m; Elim m; Intros.
Simpl.
Inversion H0.
Generalize (H H5); Intro.
EApply (equpol_tran
(cpol ((multQ a unQ),(term_mult b (n_term_O n)))
(mult_p p0 (cpol (unQ,(n_term_O n)) vpol)))
(cpol ((multQ a unQ),(term_mult b (n_term_O n))) p0)).
Auto.
Generalize (term_mult_full_nulo b n H3); Intro.
Rewrite H7.
Generalize (neut_multQ a); Intro; Auto.
Save.
Hints Resolve neut_mult_p.
Lemma regl_sig: (p,q:pol)(equpol (mult_p p (pol_opp q))
(pol_opp (mult_p p q))).
Intros.
Cut (equpol (suma_app (mult_p p (pol_opp q)) (mult_p p q)) vpol).
Auto.
Apply equpol_tran with (mult_p p (suma_app (pol_opp q) q)); Auto.
Apply equpol_tran with (mult_p p vpol); Auto.
Save.
Hints Resolve regl_sig.
Lemma mult_neg_unQ: (p:pol)(full_term_pol p)->(equpol
(mult_p p (cpol ((multQ_neg unQ),(n_term_O n)) vpol)) (pol_opp p)).
Intros.
Apply equpol_tran
with (pol_opp (mult_p p (cpol (unQ,(n_term_O n)) vpol))).
Apply equpol_tran
with (mult_p p (pol_opp (cpol (unQ,(n_term_O n)) vpol))); Auto.
Auto.
Save.
Hints Resolve mult_neg_unQ.
Lemma mult_p_m: (p:pol)(m:monom)(equpol (mult_m p m) (mult_p p (cpol m vpol))).
Intros.
Apply equpol_tran with (suma_app (mult_m p m) (mult_p p vpol)); Auto.
Apply equpol_tran with (suma_app (mult_m p m) vpol); Auto.
Save.
Hints Resolve mult_p_m.
Lemma mult_m_z_monom: (p:pol)(m:monom)(z_monom m)->
(equpol (mult_m p m) vpol).
(Induction p; Auto).
Intros.
Simpl.
(Apply equpol_tran with (mult_m p0 m0); Auto).
Save.
Hints Resolve mult_m_z_monom.
Lemma mul_opp_monom: (p:pol)(m:monom)(equpol (pol_opp (mult_m p m))
(mult_p p (pol_opp (cpol m vpol)))).
Intros.
Apply equpol_tran with (pol_opp (mult_p p (cpol m vpol))); Auto.
Save.
Hints Resolve mul_opp_monom.
Lemma mult_opp_monom2:(p:pol)(m:monom)(equpol (mult_m p m)
(pol_opp (mult_m p (monom_op m)))).
Intros.
Apply equpol_tran with (mult_p p (cpol m vpol)).
Auto.
Apply equpol_tran with (mult_p p (pol_opp (cpol (monom_op m) vpol)));Auto.
Apply mult_p_comp.
Simpl; Elim m; Auto.
Save.
Hints Resolve mult_opp_monom2.
Lemma distr_mult_m_monom: (p:pol)(c,c':Q)(t:term)(equpol
(suma_app (mult_m p (c,t)) (mult_m p (c',t)))
(mult_m p ((plusQ c c'),t))).
Intros.
Apply equpol_tran with (suma_app (mult_p p (cpol (c,t) vpol))
(mult_p p (cpol (c',t) vpol))); Auto.
Apply equpol_tran with (mult_p p (suma_app (cpol (c,t) vpol) (cpol (c',t) vpol)));
Auto.
Apply equpol_tran with (mult_p p (cpol ((plusQ c c'),t) vpol)); Auto.
Apply mult_p_comp.
Simpl; Auto.
Save.
Hints Resolve distr_mult_m_monom.
Lemma mult_m_monom_opp: (f:pol)(m:monom)(equpol
(mult_m f (monom_op m)) (pol_opp (mult_m f m))).
Intros.
Apply equpol_tran with (mult_p f (pol_opp (cpol m vpol))); Auto.
Apply equpol_tran with (mult_p f (cpol (monom_op m) vpol)); Auto.
Apply mult_p_comp.
Elim m; Auto.
Save.
Hints Resolve mult_m_monom_opp.
Lemma full_mult_m: (c:Q)(t:term)(p:pol)(full n t)->
(full_term_pol p)->(full_term_pol (mult_m p (c,t))).
(Induction p; Auto).
(Induction m; Intros).
Simpl.
Apply full_term_pol_cons.
(Apply term_mult_full; Trivial).
(Inversion H1; Auto).
(Apply H; Trivial).
(Inversion H1; Trivial).
Save.
Hints Resolve full_mult_m.
Lemma full_term_mult_p: (p:pol)(full_term_pol p)->
(q:pol)(full_term_pol q)->(full_term_pol (mult_p p q)).
Induction p; Auto.
Intros.
Simpl.
(Inversion H0; Auto).
Save.
Hints Resolve full_term_mult_p.
Index
This page has been generated by coqdoc