Library reduccion2_tes
Require Export ideal_tes.
Require Export orden_pol.
Inductive red [f,g,h:pol]: Prop:=
red1_simpl: (t:term)(term_in_pol g t)->(full_term_pol g)->
(full_term_pol f)->
(full_term_pol h)->(~(equpol f vpol))->(term_div (hterm f) t)->
(equpol h (suma_app g (pol_opp (mult_m f ((divQ (coef g t) (hcoef f)),
(div_term t (hterm f)))))))->(red f g h).
Hints Resolve red1_simpl.
Inductive red_exp [f,g,h:pol;t:term]: Prop:=
red1_exp_simpl: (term_in_pol g t)->(full_term_pol g)->
(full_term_pol f)->
(full_term_pol h)->(~(equpol f vpol))->
(u:term)(full n u)->(t=(term_mult u (hterm f)))->
(c:Q)(eqQ c (divQ (coef g t) (hcoef f)))->
(equpol h (suma_app g (pol_opp (mult_m f (c,u)))))->
(red_exp f g h t).
Hints Resolve red1_exp_simpl.
Lemma elim_red_exp: (f,g,h:pol)(t:term)(red_exp f g h t)->(no_term_in_pol h t).
Intros.
Inversion H.
Red.
Apply eqQ_trans with (coef (suma_app g (pol_opp (mult_m f (c,u)))) t); Auto.
Apply eqQ_trans with (plusQ (coef g t) (coef (pol_opp (mult_m f (c,u))) t)); Auto.
Apply suma_op.
Apply eqQ_trans with (coef (mult_m f (c,u)) t); Auto.
Apply eqQ_trans with (multQ c (hcoef f)).
Apply eqQ_sym.
Apply eqQ_trans with (multQ (divQ (hcoef f) (hcoef f)) (coef g t)).
Apply eqQ_trans with (multQ (divQ (coef g t) (hcoef f)) (hcoef f)); Auto.
Apply eqQ_trans with (divQ (multQ (coef g t) (hcoef f)) (hcoef f)); Auto.
Apply eqQ_trans with (divQ (multQ (hcoef f) (coef g t)) (hcoef f)); Auto.
Apply eqQ_trans with (divQ (multQ (hcoef f) (coef g t)) (hcoef f)); Auto.
Rewrite H6.
Replace (term_mult u (hterm f)) with (hterm (mult_m f (c,u))).
Apply eqQ_trans with (hcoef (mult_m f (c,u))); Auto.
Apply eqQ_trans with (multQ (hcoef f) c); Auto.
Apply eqQ_trans with (multQ (hcoef f) (mon_coef (c,u))); Auto.
Apply eqQ_sym.
Apply hcoef_mult; Auto.
Transitivity (term_mult (hterm f) (mon_term (c,u))); Auto.
Apply hterm_mult_m; Auto.
Unfold z_monom.
Apply comp_nOQ with (divQ (coef g t) (hcoef f)); Auto.
Apply no_divQ_zero; Auto.
Save.
Lemma red_comp: (f,g,fi:pol)(t:term)(red_exp fi f g t)->
(EX x | (full_term_pol x)/\
((t':term)(term_in_pol x t')->(Ttm t t'))/\
(red fi (suma_app f (pol_opp x)) (suma_app g (pol_opp x)))).
Intros.
Inversion H.
Elim split_pol with f t; Trivial; Intros.
Elim H9; Intros; Clear H9.
Elim H10; Intros; Clear H10.
Elim H9; Intros; Clear H9.
Split with x.
Split; Trivial.
Split; Auto.
Cut (no_term_in_pol x t); Intros.
Apply red1_simpl with t; Trivial.
Apply dec_sum_term_in_pol; Trivial.
Apply no_term_in_pol_opp.
Apply comp_no_term_in_pol with x; Auto.
Auto.
Auto.
Rewrite H6; Auto.
Apply equpol_tran with
(suma_app (suma_app f (pol_opp (mult_m fi (c,u)))) (pol_opp x)).
Apply equpol_ss; Auto.
Apply equpol_tran with
(suma_app (suma_app f (pol_opp x)) (pol_opp (mult_m fi (c,u)))).
Apply equpol_tran with
(suma_app f (suma_app (pol_opp (mult_m fi (c,u))) (pol_opp x))); Trivial.
Apply equpol_tran with
(suma_app f (suma_app (pol_opp x) (pol_opp (mult_m fi (c,u))))); Auto.
Apply equpol_ss; Trivial.
Apply opp_comp.
Apply mult_pm_comp_2.
Simpl.
Right.
Split.
Rewrite H6.
Symmetry.
Transitivity (div_term (term_mult (hterm fi) u) (hterm fi)); Auto.
Apply div_mult_mon_inv with n; Auto.
Apply eqQ_trans with (divQ (coef f t) (hcoef fi)); Trivial.
Apply eg_denomQ.
Auto.
Apply eqQ_trans with (plusQ (coef f t) (coef (pol_opp x) t)); Auto.
Apply eqQ_trans with (plusQ (coef f t) OQ).
Auto.
Apply plusQ_comp; Trivial.
Cut (no_term_in_pol (pol_opp x) t); Intros.
Red in H15; Apply eqQ_sym; Trivial.
Apply no_term_in_pol_opp.
Apply comp_no_term_in_pol with x; Auto.
Apply Ttm_no_term_in_pol; Trivial.
Apply full_coef with f; Trivial.
Save.
Lemma red_impl_red_exp: (f,g,h:pol)(red f g h)->
(Ex [t:term](red_exp f g h t)).
Intros.
Inversion H.
Split with t.
Apply red1_exp_simpl
with u:=(div_term t (hterm f)) c:=(divQ (coef g t) (hcoef f));
Trivial.
(Apply term_div_full; Auto).
(Apply full_coef with g; Auto).
Transitivity (term_mult (hterm f) (div_term t (hterm f))); Auto.
Apply divis_im_divt with n; Auto.
(Apply full_coef with g; Auto).
Save.
Lemma red_exp_impl_red: (f,g,h:pol)(t:term)(red_exp f g h t)->
(red f g h).
Intros f g h t redexp; Inversion redexp.
Apply red1_simpl with t; Trivial.
(Rewrite H5; Auto).
Apply equpol_tran with (suma_app g (pol_opp (mult_m f (c,u)))).
Auto.
Apply equpol_ss; Trivial.
Apply opp_comp.
Apply mult_pm_comp_2.
Simpl.
Right .
(Split; Auto).
Rewrite H5.
Symmetry.
(Transitivity (div_term (term_mult (hterm f) u) (hterm f)); Auto).
Apply div_mult_mon_inv with n; Auto.
Save.
Inductive hred [f,g,h:pol]: Prop:=
hred1_simpl:
(full_term_pol g)->
(full_term_pol h)->
(full_term_pol f)->
(~(equpol g vpol))->
(~(equpol f vpol))->
(term_div (hterm f) (hterm g))->
(equpol h
(suma_app
g
(pol_opp
(mult_m f
((divQ (hcoef g) (hcoef f)),
(div_term (hterm g) (hterm f)))))))->
(hred f g h).
Lemma red_hred: (f,g,f1:pol)(hred f1 f g)->(red f1 f g).
Induction 1; Intros.
(Split with (hterm f); Trivial).
(Apply occ_n_vpol; Trivial).
(Apply equpol_tran
with (suma_app f
(pol_opp
(mult_m f1
((divQ (hcoef f) (hcoef f1)),
(div_term (hterm f) (hterm f1)))))); Trivial).
(Apply equpol_ss; Trivial).
Apply opp_comp.
Apply mult_pm_comp_2.
Simpl.
Right .
(Split; Auto).
Save.
Hints Resolve red_hred.
Lemma red_n_vpol1: (f,g,h:pol)(red h f g)->
(~(equpol f vpol)).
(Intros f g h r; Inversion r).
(Apply term_in_pol_nvpol with t; Assumption).
Save.
Lemma red_f_f: (f:pol)(full_term_pol f)->(~(equpol f vpol))->(red f f vpol).
Induction f.
Intros.
Elim H0; Auto.
Induction m; Intros.
Split with (hterm (cpol (a,b) p)); Trivial.
Apply occ_n_vpol; Trivial.
Apply equpol_tran with (suma_app (cpol (a,b) p) (pol_opp (cpol (a,b) p))).
Auto.
Apply monot_suma_l.
Apply opp_comp.
Apply equpol_tran with (mult_m (cpol (a,b) p) (unQ,(n_term_O n))).
Auto.
Apply mult_pm_comp_2.
Red.
Right; Split.
Unfold hterm; Symmetry.
Apply term_div_eq.
Change (full n (hterm (cpol (a,b) p))) ; Auto.
Apply eqQ_trans with (divQ (hcoef (cpol (a,b) p)) (hcoef (cpol (a,b) p))); Auto.
Save.
Hints Resolve red_f_f.
Lemma red_0_un_step: (f,p:pol)(t,u:term)(full_term_pol f)->(full_term_pol p)->
(full n t)->(full n u)->(~(equpol p vpol))->t=(term_mult u (hterm p))->
(equpol f (suma_app f (pol_opp (mult_m p ((divQ (coef f t) (hcoef p)),u)))))\/
(red p f (suma_app f (pol_opp (mult_m p((divQ (coef f t) (hcoef p)),u))))).
Intros f p t u.
Elim (dec_term_in_pol f t); Intros.
Right.
Split with t; Trivial.
Apply full_term_suma_app; Auto.
Rewrite H4; Auto.
Apply equpol_ss; Trivial.
Apply opp_comp.
Apply mult_pm_comp_2.
Simpl.
Right.
Split; Auto.
Rewrite H4.
Symmetry.
Replace (term_mult u (hterm p)) with (term_mult (hterm p) u); Auto.
Apply div_mult_mon_inv with n; Auto.
Left.
Apply equpol_tran with (suma_app f vpol).
Auto.
Apply equpol_ss; Trivial.
Apply equpol_tran with (pol_opp vpol); Trivial.
Apply opp_comp.
Apply equpol_sym.
Apply mult_m_z_monom; Auto.
Save.
Hints Resolve red_0_un_step.
Lemma red_ext1: (f,g,g',h:pol)(equpol g g')->(full_term_pol g')->
(red h f g)->(red h f g').
Intros f g g' h eg fg'.
Induction 1; Intros.
Apply red1_simpl with t:=t; Trivial.
Apply equpol_tran with g; Auto.
Save.
Hints Resolve red_ext1.
Lemma red_ext2: (f,g,f',h:pol)(equpol f f')->(full_term_pol f')->
(red h f g)->(red h f' g).
Intros f g g' h ef ff'.
Induction 1; Intros.
Apply red1_simpl with t:=t; Trivial.
Red.
Red in H0.
Red; Intros.
Red in H0.
Apply H0.
Apply eqQ_trans with (coef g' t); Auto.
Apply equpol_tran with (suma_app f (pol_opp
(mult_m h ((divQ (coef g' t) (hcoef h)),(div_term t (hterm h)))))).
Apply equpol_tran with (suma_app f (pol_opp
(mult_m h ((divQ (coef f t) (hcoef h)),(div_term t (hterm h)))))); Trivial.
Apply equpol_ss; Trivial.
Apply opp_comp.
Apply mult_pm_comp_2.
Red.
Right.
Split; Auto.
Auto.
Save.
Hints Resolve red_ext2.
Lemma red_ext3: (f,g:pol)(h,h':pol)(equpol h h')->(full_term_pol h')->
(red h f g)->(red h' f g).
Intros f g h h' eh fh'.
Induction 1; Intros.
Apply red1_simpl with t:=t; Trivial.
Apply eq_nvpol with p:=h; Auto.
Apply eq_term_div with p:=h; Auto.
Apply equpol_tran with (suma_app f (pol_opp
(mult_m h ((divQ (coef f t) (hcoef h)),(div_term t (hterm h)))))); Trivial.
Apply equpol_ss; Trivial.
Apply opp_comp.
Apply mult_pm_comp_ss; Trivial.
Red.
Right.
Split; Auto.
Replace (hterm h) with (hterm h'); Auto.
Save.
Hints Resolve red_ext3.
Inductive for_all_list_pol [P:pol->Prop]: (list pol)->Prop :=
For_all_nil: (for_all_list_pol P (nil ?))
| For_all_cs: (F:(list pol))(p:pol)(P p)
->(for_all_list_pol P F)->(for_all_list_pol P (cons p F)).
Hints Resolve For_all_nil For_all_cs.
Definition full_fam := (for_all_list_pol [p:pol](full_term_pol p)/\
~(equpol p vpol)).
Hints Unfold full_fam.
Lemma cons_full_fam: (q:pol)(F:(list pol))
(full_fam (cons q F))->(full_fam F).
(Induction F; Auto).
Intros.
(Inversion H0; Auto).
Save.
Hints Resolve cons_full_fam.
Lemma nvpol_full_fam: (q:pol)(F:(list pol))
(full_fam (cons q F))->(~(equpol q vpol)).
Induction q.
Intros.
(Inversion H; Auto).
(Elim H2; Auto).
Intros.
(Inversion H0; Auto).
(Elim H3; Auto).
Save.
Hints Resolve nvpol_full_fam.
Lemma full_term_full_fam: (q:pol)(F:(list pol))
(full_fam (cons q F))->(full_term_pol q).
(Induction q; Auto).
Intros.
Inversion H0.
Elim H3; Auto.
Save.
Hints Resolve full_term_full_fam.
Lemma full_fam_dec : (F:(list pol)){(full_fam F)}+{~(full_fam F)}.
Induction F.
Left.
Auto.
Intros.
Elim H; Intros; Clear H.
Elim (full_pol_tm_dec a); Intros.
Elim (vpol_dec_full_term a); Auto; Intros.
Right.
Red; Intros.
Cut ~(equpol a vpol); Intros; Auto.
Apply nvpol_full_fam with l; Auto.
Right.
Red; Intros.
Cut (full_term_pol a); Auto; Intros.
Apply full_term_full_fam with l; Auto.
Right.
Red; Intros.
Apply b.
Apply cons_full_fam with a; Auto.
Save.
Lemma elem_full: (p:pol)(F:(list pol))(pol_In_ensemb p F)->
(full_fam F)->(full_term_pol p).
Induction 1.
Intros.
Inversion_clear H3.
Generalize H4.
Induction 1.
Intros.
Assumption.
Intros.
Inversion H2.
Auto.
Save.
Hints Resolve elem_full.
Lemma elem_n_vpol: (p:pol)(F:(list pol))(pol_In_ensemb p F)->
(full_fam F)->(~(equpol p vpol)).
Induction 1; Intros.
Inversion_clear H3.
Generalize H4.
Induction 1; Intros; EAuto.
Inversion H2; Auto.
Save.
Hints Resolve elem_n_vpol.
Lemma full_pol_In_hterm: (G:(list pol))(full_fam G)->
(f:pol)(pol_In_ensemb f G)->(full n (hterm f)).
Intros.
(Cut (full_term_pol f); Intros).
Auto.
(Apply elem_full with G; Auto).
Save.
Hints Resolve full_pol_In_hterm.
Inductive Red1 [F:(list pol);g,h:pol]: Prop:=
Red1_simp: (full_fam F)->(f:pol)(pol_In_ensemb f F)->
(red f g h)->(Red1 F g h).
Hints Resolve Red1_simp.
Inductive Red3 [F:(list pol)]: pol->pol->Prop:=
Red3_eq: (g,h:pol)(full_fam F)->(full_term_pol g)->
(full_term_pol h)->(equpol g h)->(Red3 F g h)
|Red3_step: (g,h:pol)(full_fam F)->(full_term_pol g)->
(full_term_pol h)->(Red1 F g h)->
(Red3 F g h)
|Red3_trans: (g,f,h:pol)(full_fam F)->(full_term_pol f)->
(full_term_pol g)->(full_term_pol h)->
(Red3 F g f)->(Red3 F f h)->(Red3 F g h).
Hints Resolve Red3_eq Red3_step Red3_trans.
Lemma Red3_ste : (f,g:pol)(F:(list pol))(Red1 F f g)->
(Red3 F f g).
Intros f g F r; Apply Red3_step; Inversion r; Auto.
(Inversion H1; Auto).
(Inversion H1; Auto).
Save.
Hints Resolve Red3_ste.
Lemma Red3_full_l :
(f,g:pol)(F:(list pol))(Red3 F f g)->
(full_term_pol f).
Intros f g F r; Inversion r; Auto.
Save.
Lemma Red3_full_r :
(f,g:pol)(F:(list pol))(Red3 F f g)->
(full_term_pol g).
Intros f g F r; Inversion r; Auto.
Save.
Hints Resolve Red3_full_r Red3_full_l.
Lemma Red3_full_fam:
(f,g:pol)(F:(list pol))(Red3 F f g)->
(full_fam F).
Intros f g F r; Inversion r; Auto.
Save.
Hints Resolve Red3_full_fam.
Lemma Red3_tran : (f,g,h:pol)(F:(list pol))
(Red3 F f g)->(Red3 F g h)->
(Red3 F f h).
(Intros f g h F r1 r2; Apply Red3_trans with g; Auto).
(Inversion r1; Auto).
(Inversion r1; Auto).
(Inversion r1; Auto).
(Inversion r2; Auto).
Save.
Lemma Red1_ext1: (F:(list pol))(f,g,g':pol)(full_term_pol g')->(equpol g g')->
(Red1 F f g)->(Red1 F f g').
Intros F f g g' fg' e.
Induction 1; Intros.
Apply Red1_simp with f:=f0; Auto.
Apply red_ext1 with g; Trivial.
Save.
Hints Resolve Red1_ext1.
Lemma Red1_ext2: (F:(list pol))(f,g,f':pol)(full_term_pol f')->(equpol f f')->
(Red1 F f g)->(Red1 F f' g).
Intros F f g f' ff' e; Induction 1; Intros.
Apply Red1_simp with f:=f0; Auto.
Apply red_ext2 with f:=f; Auto.
Save.
Hints Resolve Red1_ext2.
Lemma Red3_ext1 : (F:(list pol))(f,g:pol)(Red3 F f g)->(g':pol)(equpol g g')->
(full_term_pol g')->(Red3 F f g').
Intros F f g; Induction 1.
Intros; Apply Red3_eq; (Apply equpol_tran with h; Auto) Orelse Auto.
Intros g1 h fF fg1 fh rgh g' ehg' fg'; Cut (Red1 F g1 g'); Auto.
Apply Red1_ext1 with h; Auto.
Intros.
Apply Red3_tran with f0; Auto.
Save.
Hints Resolve Red3_ext1.
Lemma Red3_ext2: (F:(list pol))(f,g:pol)(Red3 F f g)->(f':pol)(equpol f f')->
(full_term_pol f')->(Red3 F f' g).
Intros F f g; Induction 1.
Intros; Apply Red3_eq; (Apply equpol_tran with g0; Auto) Orelse Auto.
Intros; Apply Red3_step; (Apply Red1_ext2 with g0; Auto) Orelse Auto.
Intros.
Apply Red3_tran with f0; Auto.
Save.
Hints Resolve Red3_ext2.
Lemma red3_fFh2: (f,h,g:pol)(F:(list pol))
(Red3 F f h)->~(equpol g vpol)->(full_term_pol g)->(Red3 (cons g F) f h).
Induction 1.
Intros.
Auto.
Auto.
Intros.
Apply Red3_step; Auto.
Inversion H3.
Apply Red1_simp with f0; Auto.
Intros.
Auto.
Apply Red3_trans with f0; Auto.
Save.
Lemma red3_fFh: (f,h:pol)(F:(list pol))
(Red1 F f h)->~(equpol h vpol)->(Red3 (cons h F) f vpol).
Intros.
Inversion H.
Inversion H3.
Apply Red3_trans with h; Auto.
Apply Red3_step; Auto.
Apply Red1_simp with f0; Auto.
Apply Red3_step; Auto.
Apply Red1_simp with h; Auto.
Save.
Lemma red3_fFh_vpol: (f,h:pol)(F:(list pol))
(Red3 F f h)->~(equpol h vpol)->(Red3 (cons h F) f vpol).
Induction 1.
Intros.
Apply Red3_ext2 with h0; Auto.
Apply Red3_step; Auto.
Apply Red1_simp with h0; Auto.
Intros.
Apply red3_fFh; Auto.
Intros.
Apply Red3_tran with f0; Auto.
Apply red3_fFh2; Auto.
Save.
Lemma Red1_mult_m: (f,g:pol)(F:(list pol))(Red1 F f g)->(c:Q)(~(eqQ c OQ))->
(t:term)(full n t)->(Red1 F (mult_m f (c,t)) (mult_m g (c,t))).
Induction 1; Intros.
Apply Red1_simp with f:=f0; Auto.
Elim H2; Intros.
Split with (term_mult t t0); Trivial.
Red.
Red in H5.
Apply comp_nOQ with c:=(multQ (coef f t0) c); Auto.
Apply eqQ_sym.
Replace (term_mult t t0) with (term_mult t0 t); Auto.
Apply coef_term_mult; Auto.
Apply full_coef with f:=f; Auto.
Auto.
Auto.
Auto.
Apply equpol_tran with (mult_m (suma_app f (pol_opp
(mult_m f0 ((divQ (coef f t0) (hcoef f0)),(div_term t0 (hterm f0)))))) (c,t)).
Auto.
Apply equpol_tran with (suma_app (mult_m f (c,t)) (mult_m (pol_opp
(mult_m f0 ((divQ (coef f t0) (hcoef f0)),(div_term t0 (hterm f0))))) (c,t))).
Auto.
Apply equpol_ss; Trivial.
Apply equpol_tran with (pol_opp (mult_m
(mult_m f0 ((divQ (coef f t0) (hcoef f0)),(div_term t0 (hterm f0)))) (c,t))).
Auto.
Apply opp_comp.
Apply equpol_tran with (mult_m f0
(mult_mon ((divQ (coef f t0) (hcoef f0)),(div_term t0 (hterm f0))) (c,t))).
Auto.
Apply mult_pm_comp_2.
Simpl.
Right.
Split.
Transitivity (div_term (term_mult t0 t) (hterm f0)); Auto.
Apply mult_div_term1 with n:=n; Auto.
Apply full_coef with f:=f; Auto.
Apply eqQ_trans with (divQ (multQ (coef f t0) c) (hcoef f0)); Auto.
Apply eg_denomQ; Auto.
Apply eqQ_sym.
Apply eqQ_trans with (coef (mult_m f (c,t)) (term_mult t0 t)); Auto.
Apply coef_term_mult; Auto.
Apply full_coef with f:=f; Auto.
Save.
Hints Resolve Red1_mult_m.
Lemma Red3_mult_m: (f,g:pol)(F:(list pol))(Red3 F f g)->
(c:Q)(t:term)(full n t)->(Red3 F (mult_m f (c,t)) (mult_m g (c,t))).
Intros.
Elim (decQ c); Intros.
Apply Red3_eq.
Inversion H; Auto.
Inversion H; Auto.
Inversion H; Auto.
Apply equpol_tran with vpol; Auto.
Generalize f g F H c t H0 b.
Clear b H0 t c H F g f.
Induction 1; Intros.
Apply Red3_eq; Auto.
Apply Red3_step; Auto.
Apply Red3_tran with (mult_m f0 (c,t)); Auto.
Save.
Hints Resolve Red3_mult_m.
Lemma Red3_vpol_mult_m: (f:pol)(F:(list pol))(Red3 F f vpol)->
(c:Q)(t:term)(full n t)->(Red3 F (mult_m f (c,t)) vpol).
Intros.
Apply Red3_ext1 with (mult_m vpol (c,t)); Trivial.
Apply Red3_mult_m; Trivial.
Save.
Hints Resolve Red3_vpol_mult_m.
Lemma sufc_Red1: (f,g,fi:pol)(F:(list pol))(full_fam F)->(full_term_pol g)->
(full_term_pol f)->(pol_In_ensemb fi F)->(m:monom)(full_mon n m)->
~(z_monom m)->(equpol f (suma_app g (pol_opp (mult_m fi m))))->
(no_term_in_pol f (hterm (mult_m fi m)))->(Red1 F g f).
Induction m; Intros.
Red in H6.
Split with fi; Auto.
Cut (full_term_pol fi); Intros.
Cut ~(equpol fi vpol); Intros.
Apply red1_simpl with t:=(hterm (mult_m fi (a,b))); Trivial.
Red.
Cut ~(eqQ (coef (pol_opp (mult_m fi (a,b))) (hterm (mult_m fi (a,b)))) OQ); Intros.
Cut (eqQ (coef f (hterm (mult_m fi (a,b))))
(plusQ (coef g (hterm (mult_m fi (a,b))))
(coef (pol_opp (mult_m fi (a,b))) (hterm (mult_m fi (a,b)))))); Intros.
Cut (eqQ OQ
(plusQ (coef g (hterm (mult_m fi (a,b))))
(coef (pol_opp (mult_m fi (a,b))) (hterm (mult_m fi (a,b)))))); Intros.
Cut (eqQ (coef g (hterm (mult_m fi (a,b))))
(multQ_neg
(coef (pol_opp (mult_m fi (a,b))) (hterm (mult_m fi (a,b)))))); Intros; Auto.
Apply comp_nOQ with c:=(multQ_neg (coef (pol_opp (mult_m fi (a,b)))
(hterm (mult_m fi (a,b))))); Auto.
Apply eqQ_trans with (coef f (hterm (mult_m fi (a,b)))); Auto.
Apply eqQ_trans with (coef (suma_app g (pol_opp (mult_m fi (a,b))))
(hterm (mult_m fi (a,b)))); Auto.
Apply comp_nOQ with c:=(multQ_neg (coef (mult_m fi (a,b))
(hterm (mult_m fi (a,b))))); Auto.
Apply multQ_n_OQ.
Cut (term_in_pol (mult_m fi (a,b)) (hterm (mult_m fi (a,b)))); Intros ; Auto.
Replace (hterm (mult_m fi (a,b))) with (term_mult (hterm fi) (mon_term (a,b)));
Auto.
Symmetry.
Apply hterm_mult_m; Auto.
Apply equpol_tran with (suma_app g (pol_opp (mult_m fi (a,b)))); Trivial.
Apply equpol_ss; Trivial.
Apply opp_comp.
Apply mult_pm_comp_2.
Simpl.
Unfold z_monom in H3.
Right.
Split.
Replace (hterm (mult_m fi (a,b))) with (term_mult (hterm fi) (mon_term (a,b))).
Simpl.
Transitivity (term_mult (div_term (hterm fi) (hterm fi)) b).
Transitivity (term_mult b (div_term (hterm fi) (hterm fi))); Auto.
Replace (div_term (hterm fi) (hterm fi)) with (n_term_O n).
Symmetry.
Apply term_mult_full_nulo; Auto.
Symmetry.
Apply term_div_eq; Auto.
Apply mult_div_term1 with n:=n; Auto.
Simpl.
Symmetry.
Transitivity (term_mult (hterm fi) (mon_term (a,b))); Auto.
Apply hterm_mult_m; Auto.
Apply eqQ_trans with (divQ (coef (mult_m fi (a,b)) (hterm (mult_m fi (a,b))))
(hcoef fi)).
Apply eqQ_trans with (divQ (hcoef (mult_m fi (a,b))) (hcoef fi)).
Apply eqQ_trans with (divQ (multQ (hcoef fi) (mon_coef (a,b))) (hcoef fi)).
Auto.
Apply eg_denomQ; Auto.
Apply eqQ_sym.
Apply hcoef_mult; Trivial.
Apply eg_denomQ; Auto.
Apply eg_denomQ; Auto.
Cut (equpol (suma_app f (mult_m fi (a,b))) g); Intros.
Apply eqQ_trans with (plusQ (coef f (hterm (mult_m fi (a,b))))
(coef (mult_m fi (a,b)) (hterm (mult_m fi (a,b))))).
Apply eqQ_trans with (plusQ OQ
(coef (mult_m fi (a,b)) (hterm (mult_m fi (a,b))))); Auto.
Apply eqQ_trans with (plusQ (coef (mult_m fi (a,b)) (hterm (mult_m fi (a,b))))
OQ); Auto.
Apply eqQ_trans with (coef (suma_app f (mult_m fi (a,b)))
(hterm (mult_m fi (a,b)))); Auto.
Auto.
Apply elem_n_vpol with F; Auto.
Apply elem_full with F; Auto.
Save.
Hints Resolve sufc_Red1.
Lemma Red1_dif_id: (g,h:pol)(F:(list pol))(Red1 F g h)->
(Ideal (suma_app g (pol_opp h)) F).
Induction 1.
Induction 3; Intros.
Apply pol_eq_id_eg with
(mult_m f ((divQ (coef g t) (hcoef f)),(div_term t (hterm f)))); Auto.
Apply pol_F_idmult; Trivial.
Simpl.
Apply term_div_full; Auto.
Apply full_coef with g; Auto.
Save.
Hints Resolve Red1_dif_id.
Lemma Red3_dif_id: (g,h:pol)(F:(list pol))(Red3 F g h)->
(Ideal (suma_app g (pol_opp h)) F).
Induction 1; Intros.
Apply pol_eq_id_eg with vpol.
Auto.
Apply equpol_sym.
Apply equpol_tran with (suma_app g0 (pol_opp g0)); Auto.
Apply full_term_suma_app; Auto.
Auto.
Apply pol_eq_id_eg with
(suma_app (suma_app g0 (pol_opp f)) (suma_app f (pol_opp h0))); Auto.
Save.
Hints Resolve Red3_dif_id.
Lemma Red1_en_cons: (F:(list pol))(g,h:pol)(Red1 F g h)->(Ideal h (cons g F)).
Induction 1.
Induction 3; Intros.
Apply pol_eq_id_eg
with (suma_app g
(pol_opp
(mult_m f
((divQ (coef g t) (hcoef f)),(div_term t (hterm f))))));
Auto.
Apply suma_p_id; Auto.
Apply opp_p_id.
Apply ideal_mon.
Apply pol_F_idmult; Auto.
Red.
Apply term_div_full; Auto.
Apply full_coef with g; Auto.
Save.
Lemma Red3_en_cons: (F:(list pol))(g,h:pol)(Red3 F g h)->(Ideal h (cons g F)).
Induction 1; Intros.
Apply pol_eq_id_eg with g0; Auto.
Apply Red1_en_cons; Auto.
Apply id_trans with f; Auto.
Save.
Lemma Red1_en_cons_inv: (F:(list pol))(g,h:pol)(Red1 F g h)->(Ideal g (cons h F)).
Induction 1.
Induction 3; Intros.
Apply pol_eq_id_eg
with (suma_app h
(mult_m f ((divQ (coef g t) (hcoef f)),(div_term t (hterm f)))));
Auto.
Apply suma_p_id; Auto.
Apply ideal_mon.
Apply pol_F_idmult; Auto.
Red.
Apply term_div_full; Auto.
Apply full_coef with g; Auto.
Save.
Lemma Red3_en_cons_inv: (F:(list pol))(g,h:pol)(Red3 F g h)->(Ideal g (cons h F)).
Induction 1; Intros.
Apply pol_eq_id_eg with h0; Auto.
Apply Red1_en_cons_inv; Auto.
Apply id_trans with f; Auto.
Save.
Lemma Red1_vpol: (g:pol)(F:(list pol))(Red1 F g vpol)->(Ideal g F).
Intros.
Apply pol_eq_id_eg with (suma_app g (pol_opp vpol)); Auto.
Inversion H.
Inversion H2; Auto.
Save.
Hints Resolve Red1_vpol.
Lemma Red_vpol: (g:pol)(F:(list pol))(Red3 F g vpol)->(Ideal g F).
Intros.
Apply pol_eq_id_eg with (suma_app g (pol_opp vpol)); Auto.
Inversion H; Auto.
Save.
Hints Resolve Red_vpol.
Lemma Red1_en_id: (g,h:pol)(F:(list pol))(Red1 F g h)->(Ideal g F)->
(Ideal h F).
Induction 1.
Induction 3.
Intros.
Generalize (pol_F_idmult_opp f
((divQ (coef g t) (hcoef f)),(div_term t (hterm f))) F).
Intros.
Generalize (H11 H1).
Intros.
Apply pol_eq_id_eg
with f:=(suma_app g
(pol_opp
(mult_m f
((divQ (coef g t) (hcoef f)),(div_term t (hterm f))))));
Auto.
(Apply suma_p_id; Trivial).
Apply opp_p_id.
(Apply pol_F_idmult; Trivial).
Simpl.
Apply term_div_full; Auto.
Apply full_coef with g; Auto.
Save.
Hints Resolve Red1_en_id.
Lemma Red3_en_id: (g,h:pol)(F:(list pol))(Red3 F g h)->(Ideal g F)->
(Ideal h F).
Induction 1.
Intros.
(Apply pol_eq_id_eg with g0; Auto).
Intros.
(Apply Red1_en_id with g:=g0; Auto).
Auto.
Save.
Hints Resolve Red3_en_id.
Lemma Red1_en_id_inv: (g,h:pol)(F:(list pol))(Red1 F g h)->(Ideal h F)
->(Ideal g F).
Induction 1.
Induction 3.
Intros.
Generalize (ch_m_plus h g f
((divQ (coef g t) (hcoef f)),(div_term t (hterm f))) H9).
Intros.
Apply pol_eq_id_eg
with f:=(suma_app h
(mult_m f
((divQ (coef g t) (hcoef f)),(div_term t (hterm f)))));
Auto.
Apply suma_p_id; Trivial.
Apply pol_F_idmult; Trivial.
Simpl.
(Apply term_div_full; Auto).
(Apply full_coef with g; Auto).
Save.
Hints Resolve Red1_en_id_inv.
Lemma Red3_en_id_inv: (g,h:pol)(F:(list pol))(Red3 F g h)->
(Ideal h F)->(Ideal g F).
Induction 1.
Intros.
(Apply pol_eq_id_eg with h0; Auto).
Intros.
(Apply Red1_en_id_inv with h:=h0; Auto).
Auto.
Save.
Hints Resolve Red3_en_id_inv.
Index
This page has been generated by coqdoc