Library prueba_tes
Require Export pol_can.
Theorem add_effic: (p,q:pol)
{r:pol|(full_pol p)->(full_pol q)->
(full_pol r)
/\(equpol r (suma_app p q))
/\((t:term)(full n t)->
(low_pol t p)->(low_pol t q)->(low_pol t r))}.
Induction p.
Intro q; Split with q; Auto.
Intros m p' HRp; Elim m.
Intros cm tp; Induction q.
Split with (cpol (cm,tp) p'); Auto.
Intros mq q'; Elim mq; Intros cq tq.
Elim (Ttm_total_good tp tq n).
Destruct 1.
Intros i HRq.
Elim HRq; Intros.
Split with (cpol (cq,tq) x); Intros.
Elim p0; Intros; Clear p0; Trivial.
Elim H2; Intros; Clear H2.
Inversion H; Inversion H0; Split.
Auto.
Split; Intros.
Apply equpol_tran with (suma_app (cpol (cq,tq) q') (cpol (cm,tp) p')).
Simpl; Apply equpol_cpol.
Apply equpol_tran with (suma_app (cpol (cm,tp) p') q'); Auto.
Auto.
Apply low_pol_cpol with q'; Auto.
Inversion H0; Auto.
Clear a; Intros i H.
Elim (HRp (cpol (cq,tq) q')); Intros pq hpq.
Split with (cpol (cm,tp) pq); Intros fp fq.
Elim hpq; Intros; Auto.
Elim H1; Intros.
Clear H1.
Inversion fp; Inversion fq; Split.
Apply full_pol_cons; Auto.
Split; Intros.
Simpl; Apply equpol_cpol; Auto.
Apply low_pol_cpol with p'; Auto.
Inversion fp; Auto.
Intros e.
Elim (decQ_t cm (multQ_neg cq)); Intros eQ.
Elim (HRp q'); Intros pq hpq.
Split with pq; Intros fp fq.
Elim hpq; Intros.
Elim H1; Intros.
Clear H1.
Inversion fp; Inversion fq; Split; Trivial.
Split; Intros.
Apply equpol_tran with (suma_app p' q'); Trivial.
Replace tq with tp; Auto.
Apply H3; Auto.
Inversion H18.
Apply low_trans with tp; Auto.
Inversion H19.
Apply low_trans with tq; Auto.
Inversion fp; Auto.
Inversion fq; Auto.
Elim (HRp q'); Intros pq hpq H.
Split with (cpol ((plusQ cm cq),tp) pq).
Split.
Inversion H0.
Inversion H1.
Elim hpq; Intros; Auto.
Apply full_pol_cons; Auto.
Elim H17; Intros.
Apply H19; Auto.
Replace tp with tq; Auto.
Symmetry; Apply e; Auto.
Split; Intros.
Inversion H0.
Inversion H1.
Replace tq with tp.
Elim hpq; Intros; Auto.
Elim H17; Intros.
Clear H17.
Simpl.
Apply equpol_tran with (cpol (cm,tp) (suma_app (cpol (cq,tp) q') p')).
Simpl.
Apply equpol_tran with (cpol ((plusQ cm cq),tp) (suma_app q' p')).
Apply equpol_cpol.
Apply equpol_tran with (suma_app p' q'); Auto.
Apply equpol_sym; Apply equpol_smt.
Apply equpol_cpol; Auto.
Apply e; Auto.
Apply (low_pol_cpol t tp (plusQ cm cq) p' pq).
Inversion H3.
Apply low_cons; Trivial.
Save.
Hints Resolve add_effic.
Definition add_effic_fun : pol -> pol -> pol.
Intros p q.
Elim (add_effic p q).
Intros pq; Intros; Exact pq.
Defined.
Transparent add_effic_fun.
Lemma add_effic_full : (p,q:pol)(full_pol p)->(full_pol q)->
(full_pol (add_effic_fun p q)).
Intros.
Unfold add_effic_fun;Elim (add_effic p q); Simpl.
Tauto.
Save.
Lemma add_effic_cor_l : (p,q:pol)(full_pol p)->(full_pol q)->
(equpol (add_effic_fun p q)(suma_app p q)).
Intros.
Unfold add_effic_fun;Elim (add_effic p q); Simpl.
Tauto.
Save.
Hints Resolve add_effic_cor_l.
Lemma comp_sum_effic: (p,q:pol)(full_term_pol p)->(full_term_pol q)->
(equpol (add_effic_fun (fun_can p) (fun_can q)) (suma_app p q)).
Intros.
Cut (equpol p (fun_can p)); Intros.
Cut (equpol q (fun_can q)); Intros.
Apply equpol_tran with (suma_app (fun_can p) (fun_can q)).
Apply add_effic_cor_l.
Apply can_is_full; Trivial.
Apply can_is_full; Trivial.
Auto.
Apply can_corr; Trivial.
Apply can_corr; Trivial.
Save.
Lemma mult_m_full: (p:pol)(m:monom)
{r:pol | (full_mon n m)->(full_pol p)->(full_pol r)/\
(equpol r (mult_m p m))}.
Induction p.
Intros.
Split with vpol; Split; Auto.
Intros m p' hr m0.
Elim (z_monom_dec m0); Intros.
Split with vpol; Auto.
Generalize b; Elim m0; Intros; Clear b.
Elim (hr (a,b0)); Intros p'm0 y.
Elim m; Intros.
Elim (add_effic (cpol (mult_mon (a0,b) (a,b0)) vpol) p'm0); Intros r y5.
Split with r; Intros.
Inversion H0.
Elim y; Trivial; Clear y; Intros.
Elim y5; Trivial; Clear y5; Intros.
Elim H11; Clear H11; Intros.
Split; Trivial.
Apply equpol_tran
with (suma_app (cpol (mult_mon (a0,b) (a,b0)) vpol) p'm0); Trivial.
Simpl.
Apply equpol_cpol2; Auto.
Simpl.
Apply full_pol_cons; Auto.
Save.
Hints Resolve mult_m_full.
Definition mult_m_effic_fun : pol -> monom -> pol.
Intros p m.
Elim (mult_m_full p m).
Intros pm; Intros; Exact pm.
Defined.
Transparent mult_m_effic_fun.
Lemma mult_m_effic_full : (p:pol)(m:monom)(full_pol p)->(full_mon n m)->
(full_pol (mult_m_effic_fun p m)).
Intros.
Unfold mult_m_effic_fun; Elim (mult_m_full p m); Simpl.
Tauto.
Save.
Lemma mult_m_effic_cor_l : (p:pol)(m:monom)(full_pol p)->(full_mon n m)->
(equpol (mult_m_effic_fun p m)(mult_m p m)).
Intros.
Unfold mult_m_effic_fun; Elim (mult_m_full p m); Simpl.
Tauto.
Save.
Hints Resolve mult_m_effic_cor_l.
Lemma comp_mult_m_effic: (p:pol)(m:monom)(full_term_pol p)->(full_mon n m)->
(equpol (mult_m_effic_fun (fun_can p) m) (mult_m p m)).
Intros.
Cut (equpol p (fun_can p)); Intros.
Apply equpol_tran with (mult_m (fun_can p) m).
Apply mult_m_effic_cor_l; Trivial.
Apply can_is_full; Trivial.
Auto.
Apply can_corr; Trivial.
Save.
Lemma mult_p_can : (p,q:pol)
{r:pol|(full_pol p)->(full_pol q)->(full_pol r)/\(equpol r (mult_p p q))}.
Induction p.
Intros.
Split with vpol; Split; Auto.
Intros m p' hr q.
Elim (hr q); Intros qp' y.
Elim mult_m_full with p:=q m:=m.
Intros qm y0.
Elim (add_effic qm qp').
Intros r y1.
Split with r; Intros.
Elim y; Trivial; Clear y; Intros.
Elim y0; Trivial; Clear y0; Intros.
Elim y1; Trivial; Clear y1; Intros.
Split; Trivial.
Elim H6; Intros; Clear H6.
Simpl.
Apply equpol_tran with (suma_app qm qp'); Auto.
Inversion H; Trivial.
Inversion H; Trivial.
Save.
Hints Resolve mult_p_can.
Definition mult_p_effic_fun : pol -> pol -> pol.
Intros p q.
Elim (mult_p_can p q).
Intros pq; Intros; Exact pq.
Defined.
Transparent mult_p_effic_fun.
Lemma mult_p_effic_full : (p,q:pol)(full_pol p)->(full_pol q)->
(full_pol (mult_p_effic_fun p q)).
Intros.
Unfold mult_p_effic_fun; Elim (mult_p_can p q); Simpl.
Tauto.
Save.
Lemma mult_p_effic_cor_l : (p,q:pol)(full_pol p)->(full_pol q)->
(equpol (mult_p_effic_fun p q)(mult_p p q)).
Intros.
Unfold mult_p_effic_fun; Elim (mult_p_can p q); Simpl.
Tauto.
Save.
Hints Resolve mult_p_effic_cor_l.
Lemma comp_mult_p_effic: (p,q:pol)(full_term_pol p)->(full_term_pol q)->
(equpol (mult_p_effic_fun (fun_can p) (fun_can q)) (mult_p p q)).
Intros.
Cut (equpol p (fun_can p)); Intros.
Cut (equpol q (fun_can q)); Intros.
Apply equpol_tran with (mult_p (fun_can p) (fun_can q)).
Apply mult_p_effic_cor_l.
Apply can_is_full; Trivial.
Apply can_is_full; Trivial.
Apply equpol_tran with (mult_p (fun_can p) q); Auto.
Apply can_corr; Trivial.
Apply can_corr; Trivial.
Save.
Index
This page has been generated by coqdoc