Library normal_tes
Require Export noetred_tes.
Definition normal: (list pol)->pol->Prop := [F:(list pol)][f:pol]
(g:pol)(~(Red1 F f g)).
Hints Unfold normal.
Lemma normal_ext: (p,q:pol)(F:(list pol))(normal F p)->
(full_term_pol p)->(equpol p q)->(normal F q).
Unfold normal.
Intros.
Unfold not in H.
Unfold not.
Intros.
Apply H with g.
Apply Red1_ext2 with q; Trivial.
(Apply equpol_sym; Trivial).
Save.
Hints Resolve normal_ext.
Lemma normal_eq_aux : (F:(list pol))
(f:pol)
(g:pol)(Red3 F f g)->(normal F f)->
((equpol f g)/\(normal F g)).
Induction 1.
(Split; Auto).
Apply normal_ext with p:=g0; Auto.
Intros.
Red in H4.
(Elim H4 with h; Auto).
Intros.
Split.
Apply equpol_tran with f0.
(Elim H5; Auto).
(Elim H7; Auto).
(Elim H5; Auto).
(Elim H7; Auto).
(Elim H5; Auto).
Save.
Lemma normal_eq : (F:(list pol))
(f:pol)
(g:pol)(Red3 F f g)->(normal F f)->
(equpol f g).
(Intros x1 x2 x3 x4 x5;
Elim (normal_eq_aux x1 x2 x3 x4 x5); Auto).
Save.
Hints Resolve normal_eq.
Lemma normal_Red_normal : (F:(list pol))
(f:pol)
(g:pol)(Red3 F f g)->(normal F f)->
(normal F g).
(Intros x1 x2 x3 x4 x5;
Elim (normal_eq_aux x1 x2 x3 x4 x5); Auto).
Save.
Lemma vpol_normal: (G:(list pol))(normal G vpol).
Unfold normal; Unfold not; Intros.
Inversion H.
Inversion H2.
Apply H3; Auto.
Save.
Hints Resolve vpol_normal.
Lemma Red3_vpol_normal: (F:(list pol))(f:pol)
(Red3 F vpol f)->(equpol vpol f).
Intros.
(Apply normal_eq with F; Trivial).
Save.
Hints Resolve Red3_vpol_normal.
Lemma prev_calcula_fn2: (g,f:pol)
(full_pol g)
->(full_term_pol f)->~(equpol f vpol)->
{h:pol | (red f g h)}+{(normal (cons f (nil pol)) g)}.
Induction g.
Intros; Right; Auto.
Induction m.
Clear m.
Intros.
Cut (full n b); Intros.
Cut (full_term_pol (cpol (a,b) p)); Intros.
Elim H with f; Intros; Trivial.
Elim a0; Intros.
Left.
Split with (cpol (a,b) x).
Inversion p0.
Apply red1_simpl with t; Auto.
Inversion H0.
Red.
Red; Intros.
Red in H5.
Elim H5.
Apply eqQ_trans with (coef (cpol (a,b) p) t); Auto.
Apply eqQ_sym.
Apply coef_n_term.
Red; Intros.
Rewrite <- H20 in H18.
Cut (no_term_in_pol p t); Auto.
Red.
Apply coef_low_pol; Auto.
Rewrite <- H20 in H16; Trivial.
Apply equpol_tran
with (cpol (a,b)
(suma_app p
(pol_opp
(mult_m f
((divQ (coef p t) (hcoef f)),(div_term t (hterm f)))))));
Auto.
Replace (cpol (a,b)
(suma_app p
(pol_opp
(mult_m f
((divQ (coef p t) (hcoef f)),(div_term t (hterm f)))))))
with (suma_app (cpol (a,b) p)
(pol_opp
(mult_m f
((divQ (coef p t) (hcoef f)),(div_term t (hterm f)))))).
Apply equpol_ss; Trivial.
Apply opp_comp.
Apply mult_pm_comp_2.
Red.
Right.
Split; Trivial.
Apply eg_denomQ.
Auto.
Apply eqQ_sym.
Apply coef_n_term.
Red; Intros.
Inversion H0.
Rewrite <- H12 in H19.
Cut (no_term_in_pol p t); Auto.
Red.
Apply coef_low_pol; Auto.
Rewrite <- H12 in H17; Trivial.
Auto.
Elim (dec_term_div (hterm f) b n); Intros; Auto.
Left.
Split
with (suma_app (cpol (a,b) p)
(pol_opp
(mult_m f ((divQ a (hcoef f)),(div_term b (hterm f)))))).
Apply red1_simpl with b; Trivial.
Red.
Red; Intros.
Cut (eqQ (coef (cpol (a,b) p) b) a); Intros.
Inversion H0.
Cut (eqQ a OQ); Intros.
Elim H10; Auto.
Apply eqQ_trans with (coef (cpol (a,b) p) b); Auto.
Apply coef_first; Trivial.
Apply full_term_suma_app; Auto.
Apply equpol_ss; Trivial.
Apply opp_comp.
Apply mult_pm_comp_2.
Red.
Right.
Split; Trivial.
Apply eg_denomQ.
Auto.
Apply eqQ_sym.
Apply coef_first; Trivial.
Right.
Red; Intros.
Red in b0.
Red; Intros.
Inversion H5.
Inversion H8.
Elim b0
with (suma_app p
(pol_opp
(mult_m f0
((divQ (coef p t) (hcoef f0)),(div_term t (hterm f0)))))).
Apply Red1_simp with f0; Auto.
Apply red1_simpl with t; Auto.
Cut (equpol f0 f); Intros.
Elim (eq_tm_dec t b); Intros.
Rewrite a0 in H14.
Elim b1; Auto.
Cut (hterm f0)=(hterm f); Intros.
Rewrite H17 in H14; Auto.
Auto.
Red.
Red; Intros.
Red in H9.
Elim H9.
Apply eqQ_trans with (coef p t); Auto.
Apply pol_In_ensemb_unic; Trivial.
Inversion H0; Auto.
Apply full_term_suma_app.
Inversion H0; Auto.
Apply full_term_opp.
Apply full_mult_m; Trivial.
Apply term_div_full.
Apply full_coef with f:=(cpol (a,b) p); Auto.
Auto.
Inversion H0; Auto.
Inversion H0; Auto.
Inversion H0; Auto.
Save.
Lemma prev_calcula_fn3bis: (F:(list pol_full))(f:pol_full)(full_fam (inc_list F))->
{g:pol_full|(Red1 (inc_list F) (inc f) (inc g))} + {(normal (inc_list F) (inc f))}.
Induction F.
Induction f; Intros.
Right.
Simpl.
Red; Intros.
Red; Intros.
Inversion H0; Auto.
Inversion H2.
Intros.
Elim H with f; Intros.
Left.
Elim a0; Intros.
Split with x.
Inversion p.
Apply Red1_simp with f0; Auto.
Unfold inc_list; Simpl.
Apply pol_In_tl; Auto.
Elim (prev_calcula_fn2 (inc f) (inc a)); Intros; Auto.
Elim a0; Intros.
Left.
Elim (can_fun x); Trivial; Intros.
Elim p0; Intros.
Clear p0.
Split with (exist pol [x:pol](full_pol x) x0 H1).
Apply Red1_simp with (inc a); Auto.
Unfold inc_list; Simpl.
Apply pol_In_hd; Auto.
Simpl.
Apply red_ext1 with x; Auto.
Inversion p; Auto.
Right.
Red; Intros.
Red; Intros.
Inversion H1.
Inversion H3.
Cut (red (inc a) (inc f) g); Intros.
Red in b0.
Elim b0 with g.
Apply Red1_simp with (inc a); Auto.
Inversion H10; Auto.
Apply red_ext3 with f0; Auto.
Red in b.
Elim b with g.
Apply Red1_simp with f0; Auto.
Inversion H0; Auto.
Inversion H0; Auto.
Elim H3; Auto.
Inversion H0; Auto.
Save.
Lemma calcula_fnbis: (F:(list pol_full))(f:pol_full)(full_fam (inc_list F))->
{g:pol_full|(normal (inc_list F) (inc g))/\(Red3 (inc_list F) (inc f) (inc g))}.
Intros.
Cut (noetheriano ? (inc_Red1 F)); Intros.
Red in H0.
Elim H0 with f; Intros.
Elim (prev_calcula_fn3bis F x); Intros; Trivial.
Elim a; Intros.
Elim (H2 x0); Intros.
Split with x1.
Elim p0.
Split; Trivial.
Apply Red3_trans with (inc x0); Auto.
Inversion p.
Inversion H4; Auto.
Split with x.
Split; Auto.
Apply buen_ord_red1; Auto.
Save.
Definition for_norm: (list pol_full)->pol_full->pol_full.
Intros F g.
Elim (full_fam_dec (inc_list F)); Intros fF.
Elim (calcula_fnbis F g); Intros.
Exact x.
Trivial.
Cut (full_pol vpol); Intros.
Exact (exist pol [x:pol](full_pol x) vpol H).
Trivial.
Defined.
Transparent for_norm.
Lemma norm_corr: (F:(list pol_full))(f:pol_full)(full_fam (inc_list F))->
(normal (inc_list F) (inc (for_norm F f))).
Intros F f fF.
Unfold for_norm.
Elim (full_fam_dec (inc_list F)); Simpl.
Clear fF.
Intros fF.
Elim (calcula_fnbis F f fF); Simpl.
Tauto.
Intros.
Elim b; Auto.
Save.
Lemma Red3_norm: (F:(list pol_full))(f:pol_full)(full_fam (inc_list F))->
(Red3 (inc_list F) (inc f) (inc (for_norm F f))).
Intros F f fF.
Unfold for_norm.
Elim (full_fam_dec (inc_list F)); Simpl.
Clear fF.
Intros fF.
Elim (calcula_fnbis F f fF); Simpl.
Tauto.
Intros.
Elim b; Auto.
Save.
Lemma full_term_norm: (F:(list pol_full))(f:pol_full)(full_fam (inc_list F))->
(full_term_pol (inc (for_norm F f))).
Intros.
Cut (Red3 (inc_list F) (inc f) (inc (for_norm F f))); Intros.
Inversion H0; Auto.
Apply Red3_norm; Auto.
Save.
Lemma fn_equpol_vpol: (F:(list pol_full))(f:pol_full)(full_fam (inc_list F))->
(equpol (inc f) vpol)->(equpol (inc (for_norm F f)) vpol).
Intros.
Cut (Red3 (inc_list F) (inc f) (inc (for_norm F f))); Intros.
Cut (Red3 (inc_list F) vpol (inc (for_norm F f))); Intros.
Apply equpol_sym; Trivial.
Apply Red3_vpol_normal with (inc_list F); Auto.
Apply Red3_ext2 with (inc f); Auto.
Apply Red3_norm; Auto.
Save.
Lemma equpol_fn: (F:(list pol_full))(f:pol_full)(full_fam (inc_list F))->
(normal (inc_list F) (inc f))->(equpol (inc (for_norm F f)) (inc f)).
Intros.
Cut (normal (inc_list F) (inc (for_norm F f))); Intros.
Cut (Red3 (inc_list F) (inc f) (inc (for_norm F f))); Intros.
Elim normal_eq_aux with (inc_list F) (inc f) (inc (for_norm F f)); Intros; Auto.
Apply Red3_norm; Auto.
Apply norm_corr; Auto.
Save.
Lemma pol_fn_id2: (F:(list pol_full))(g:pol_full)(full_fam (inc_list F))->
(equpol (inc (for_norm F g)) vpol)->(Ideal (inc g) (inc_list F)).
Intros.
Cut (Red3 (inc_list F) (inc g) (inc (for_norm F g))); Intros.
Cut (Red3 (inc_list F) (inc g) vpol); Intros.
Apply Red_vpol; Intros; Trivial.
Apply Red3_ext1 with (inc (for_norm F g)); Auto.
Apply Red3_norm; Auto.
Save.
Lemma fn_p_id: (F:(list pol_full))(g:pol_full)(full_fam (inc_list F))->
(Ideal (inc (for_norm F g)) (cons (inc g) (inc_list F))).
Intros.
Cut (Red3 (inc_list F) (inc g) (inc (for_norm F g))); Intros.
Apply Red3_en_cons; Trivial.
Apply Red3_norm; Auto.
Save.
Lemma pol_fn_id: (F:(list pol_full))(g:pol_full)(full_fam (inc_list F))->
(Ideal (inc g) (cons (inc (for_norm F g)) (inc_list F))).
Intros.
Cut (Red3 (inc_list F) (inc g) (inc (for_norm F g))); Intros.
Apply Red3_en_cons_inv; Auto.
Apply Red3_norm; Auto.
Save.
Lemma no_div_term_fn: (F:(list pol_full))(g,f:pol_full)(full_fam (inc_list F))->
(pol_In_ensemb (inc f) (inc_list F))->
(t:term)(term_in_pol (inc (for_norm F g)) t) -> ~(term_div (hterm (inc f)) t).
Intros.
Cut (normal (inc_list F) (inc (for_norm F g))); Intros.
Cut (Red3 (inc_list F) (inc g) (inc (for_norm F g))); Intros.
Cut (full_term_pol (inc (for_norm F g))); Intros.
Cut (full_term_pol (inc f)); Intros.
Cut ~(equpol (inc f) vpol); Intros.
Cut (full n t); Intros.
Red; Intros.
Cut (red (inc f) (inc (for_norm F g)) (suma_app (inc (for_norm F g))
(pol_opp (mult_m (inc f)
((divQ (coef (inc (for_norm F g)) t) (hcoef (inc f))),
(div_term t (hterm (inc f)))))))); Intros.
Red in H2.
Elim H2 with (suma_app (inc (for_norm F g)) (pol_opp (mult_m (inc f)
((divQ (coef (inc (for_norm F g)) t) (hcoef (inc f))),
(div_term t (hterm (inc f))))))).
Apply Red1_simp with (inc f); Auto.
Apply red1_simpl with t; Auto.
Apply full_term_suma_app; Auto.
Apply full_coef with (inc (for_norm F g)); Auto.
Apply elem_n_vpol with (inc_list F); Auto.
Apply elem_full with (inc_list F); Auto.
Inversion H3; Auto.
Apply Red3_norm; Auto.
Apply norm_corr; Auto.
Save.
Lemma for_norm_dec_vpol: (F:(list pol_full))(g:pol_full)(full_fam (inc_list F))->
{(equpol (inc (for_norm F g)) vpol)}+{~(equpol (inc (for_norm F g)) vpol)}.
Intros.
Elim (equpol_dec_full_term (inc (for_norm F g)) vpol); Auto.
Save.
Index
This page has been generated by coqdoc