Library S_poly_nuevo2_tes
Require Export normal_tes.
Definition S_pol :=
[p,q:pol] Cases p q of
vpol x => vpol
| x vpol => vpol
| p q =>
(suma_app
(mult_m p
((divQ unQ (hcoef p)),
(div_term (lcm (hterm p) (hterm q)) (hterm p))))
(pol_opp (mult_m q
((divQ unQ (hcoef q)),
(div_term (lcm (hterm p) (hterm q))
(hterm q))))))
end.
Lemma full_term_S_pol: (f,g:pol)(full_term_pol f)->(full_term_pol g)->
(full_term_pol (S_pol f g)).
Induction f.
Intros.
Unfold S_pol.
Trivial.
Induction m.
Induction g.
Intros.
Unfold S_pol; Trivial.
Induction m0.
Intros.
Unfold S_pol.
Apply full_term_suma_app; Auto.
Apply full_term_opp; Auto.
Save.
Lemma S_pol_n_vpol: (p,q:pol)(~(equpol p vpol))->(~(equpol q vpol))->
(S_pol p q) = (suma_app
(mult_m p
((divQ unQ (hcoef p)),
(div_term (lcm (hterm p) (hterm q)) (hterm p))))
(pol_opp (mult_m q
((divQ unQ (hcoef q)),
(div_term (lcm (hterm p) (hterm q))
(hterm q)))))).
Induction p; Intros.
Elim H; Auto.
Induction q; Intros.
Elim H1; Auto.
Auto.
Save.
Hints Resolve S_pol_n_vpol.
Lemma S_pol_ext: (f,x,g,y:pol)(full_term_pol f)->
(full_term_pol x)->(full_term_pol g)->(full_term_pol y)->
~(equpol f vpol)->~(equpol g vpol)->(equpol f x)->(equpol g y)->
(equpol (S_pol f g) (S_pol x y)).
Intros.
Cut ~(equpol x vpol); Intros.
Cut ~(equpol y vpol); Intros.
Cut (S_pol f g)
=(suma_app
(mult_m f
((divQ unQ (hcoef f)),
(div_term (lcm (hterm f) (hterm g)) (hterm f))))
(pol_opp
(mult_m g
((divQ unQ (hcoef g)),
(div_term (lcm (hterm f) (hterm g)) (hterm g)))))); Intros.
Cut (S_pol x y)
=(suma_app
(mult_m x
((divQ unQ (hcoef x)),
(div_term (lcm (hterm x) (hterm y)) (hterm x))))
(pol_opp
(mult_m y
((divQ unQ (hcoef y)),
(div_term (lcm (hterm x) (hterm y)) (hterm y)))))); Intros.
Rewrite H9.
Rewrite H10.
Clear H9.
Clear H10.
Apply equpol_ss.
Apply mult_pm_comp_ss; Trivial; Simpl.
Right.
Split.
Cut (hterm f)=(hterm x); Intros.
Cut (hterm g)=(hterm y); Intros.
Rewrite H9.
Rewrite H10; Trivial.
Apply eq_hterm; Trivial.
Apply eq_hterm; Trivial.
Apply eg_numeraQ; Auto.
Apply opp_comp.
Apply mult_pm_comp_ss; Trivial; Simpl.
Right.
Split.
Cut (hterm f)=(hterm x); Intros.
Cut (hterm g)=(hterm y); Intros.
Rewrite H9.
Rewrite H10; Trivial.
Apply eq_hterm; Trivial.
Apply eq_hterm; Trivial.
Apply eg_numeraQ; Auto.
Apply S_pol_n_vpol; Auto.
Apply S_pol_n_vpol; Auto.
EAuto.
EAuto.
Save.
Lemma S_pol_ff: (f:pol)(equpol (S_pol f f) vpol).
Induction f.
Auto.
Intros.
(Unfold S_pol; Auto).
Save.
Hints Resolve S_pol_ff.
Lemma S_pol_sym: (f,g:pol)(equpol (S_pol f g) (pol_opp (S_pol g f))).
Induction f.
(Induction g; Auto).
Induction g.
Auto.
Intros.
Unfold S_pol.
Apply equpol_tran
with (suma_app
(pol_opp
(mult_m (cpol m0 p0)
((divQ unQ (hcoef (cpol m0 p0))),
(div_term (lcm (hterm (cpol m p)) (hterm (cpol m0 p0)))
(hterm (cpol m0 p0))))))
(mult_m (cpol m p)
((divQ unQ (hcoef (cpol m p))),
(div_term (lcm (hterm (cpol m p)) (hterm (cpol m0 p0)))
(hterm (cpol m p)))))).
Auto.
Apply equpol_tran
with (suma_app
(pol_opp
(mult_m (cpol m0 p0)
((divQ unQ (hcoef (cpol m0 p0))),
(div_term (lcm (hterm (cpol m0 p0)) (hterm (cpol m p)))
(hterm (cpol m0 p0))))))
(mult_m (cpol m p)
((divQ unQ (hcoef (cpol m p))),
(div_term (lcm (hterm (cpol m0 p0)) (hterm (cpol m p)))
(hterm (cpol m p)))))).
Apply equpol_ss.
Apply opp_comp.
Apply mult_pm_comp_2.
Simpl.
Right.
(Split; Auto).
Apply mult_pm_comp_2.
Simpl.
Right.
(Split; Auto).
Apply equpol_tran
with (suma_app
(mult_m (cpol m p)
((divQ unQ (hcoef (cpol m p))),
(div_term (lcm (hterm (cpol m0 p0)) (hterm (cpol m p)))
(hterm (cpol m p)))))
(pol_opp
(mult_m (cpol m0 p0)
((divQ unQ (hcoef (cpol m0 p0))),
(div_term (lcm (hterm (cpol m0 p0)) (hterm (cpol m p)))
(hterm (cpol m0 p0))))))); Auto.
Save.
Hints Resolve S_pol_sym.
Definition Groebner1_full:=
[F:(list pol_full)]
((full_fam (inc_list F))/\
(f:pol_full)(Ideal (inc f) (inc_list F))->(Red3 (inc_list F) (inc f) vpol)).
Hints Unfold Groebner1_full.
Definition Groebner2_full:=
[F:(list pol_full)]
((full_fam (inc_list F))/\
(f,g:pol_full)
(pol_In_ensemb (inc f) (inc_list F))->(pol_In_ensemb (inc g) (inc_list F))->
(Red3 (inc_list F) (S_pol (inc f) (inc g)) vpol)).
Hints Unfold Groebner2_full.
Lemma G1_impl_G2_full: (G:(list pol_full))(Groebner1_full G)->
(Groebner2_full G).
Intros G.
Unfold Groebner1_full; Intros.
Unfold Groebner2_full; Elim H; Intros.
Split; Trivial.
Clear H.
Induction f; Simpl.
Induction g; Simpl; Intros.
Cut (Ideal (S_pol x x0) (inc_list G)); Intros.
Elim (can_fun (S_pol x x0)); Intros.
Elim p1; Intros.
Clear p1.
Apply Red3_ext2 with x1; Intros; Auto.
Elim ex_fpol_eq with x1; Intros; Auto.
Apply Red3_ext2 with (inc x2); Auto.
Apply H1; Auto.
Apply pol_eq_id_eg with (S_pol x x0); Auto.
Apply equpol_tran with x1; Auto.
Apply full_term_S_pol; Auto.
Apply full_term_S_pol; Auto.
Replace (S_pol x x0) with (suma_app (mult_m x
((divQ unQ (hcoef x)),(div_term (lcm (hterm x) (hterm x0)) (hterm x))))
(pol_opp (mult_m x0 ((divQ unQ (hcoef x0)),
(div_term (lcm (hterm x) (hterm x0)) (hterm x0)))))).
Apply suma_p_id.
Apply pol_F_idmult; Auto.
Simpl.
Apply term_div_full; Auto.
Apply opp_p_id.
Apply pol_F_idmult; Trivial.
Apply elem_full with (inc_list G); Auto.
Simpl.
Apply term_div_full; Auto.
Cut ~(equpol x vpol); Intros.
Cut ~(equpol x0 vpol); Intros.
Symmetry; Auto.
Apply elem_n_vpol with (inc_list G); Trivial.
Apply elem_n_vpol with (inc_list G); Trivial.
Save.
Hints Resolve G1_impl_G2_full.
Definition Groebner3_full:= [F:(list pol_full)]
((full_fam (inc_list F))/\
(h,h1,h2:pol_full)
(normal (inc_list F) (inc h1))->(normal (inc_list F) (inc h2))->
(Red3 (inc_list F) (inc h) (inc h1))->
(Red3 (inc_list F) (inc h) (inc h2))->(equpol (inc h1) (inc h2))).
Hints Unfold Groebner3_full.
Definition confluente :=
[F:(list pol)][f:pol](g:pol)(h:pol)(Red3 F f g)->(Red3 F f h)->(common_succ F g h).
Hints Unfold confluente.
Inductive common_succ_full [F:(list pol_full);g,h:pol_full]: Prop:=
common_succ_red_full: (p:pol_full)(Red3 (inc_list F) (inc g) (inc p))->(Red3 (inc_list F) (inc h) (inc p))->(common_succ_full F g h).
Hints Resolve common_succ_red_full.
Lemma comp_common_succ_full: (p,q,r,s:pol_full)(F:(list pol_full))
(equpol (inc p) (inc q))->(equpol (inc r) (inc s))->
(common_succ_full F p r)->(common_succ_full F q s).
Intros p q r s F e1 e2.
Induction 1; Intros.
Split with p0.
Apply Red3_ext2 with f:=(inc p); Auto.
Apply Red3_ext2 with f:=(inc r); Auto.
Save.
Lemma trans_common_red_full:(f,g,h:pol_full)(F:(list pol_full))
(Red1 (inc_list F) (inc h) (inc f))->(common_succ_full F g f)->
(common_succ_full F g h).
Intros.
Inversion H0.
Apply common_succ_red_full with p; Trivial.
Apply Red3_tran with (inc f); Trivial.
Apply Red3_ste; Trivial.
Save.
Hints Resolve trans_common_red_full.
Lemma conmt_common_succ_full: (p,q:pol_full)(F:(list pol_full))
(common_succ_full F p q)->(common_succ_full F q p).
Induction 1.
Intros.
Exists p0; Assumption.
Save.
Hints Resolve conmt_common_succ_full.
Definition confluente_full :=
[F:(list pol_full)][f:pol_full](g:pol_full)(h:pol_full)
(Red3 (inc_list F) (inc f) (inc g))->
(Red3 (inc_list F) (inc f) (inc h))->
(common_succ_full F g h).
Hints Unfold confluente_full.
Definition Groebner3_CR_full:= [F:(list pol_full)]
((full_fam (inc_list F))/\(h:pol_full)(confluente_full F h)).
Hints Unfold Groebner3_CR_full.
Lemma G3_CR_impl_G3_full: (G:(list pol_full))(Groebner3_CR_full G)->
(Groebner3_full G).
Unfold Groebner3_CR_full Groebner3_full.
Intros G; Destruct 1; Intros fG cr; Split.
Assumption.
Intros h h1 h2 nh1 nh2 r01 r02.
Elim (cr h h1 h2); Trivial.
Intros x r1 r2.
Apply equpol_tran with (inc x).
Apply normal_eq with (inc_list G); Auto.
Apply equpol_sym; Apply normal_eq with (inc_list G); Auto.
Save.
Lemma cr_full: (G:(list pol_full))(h1,h2:pol_full)
(Groebner3_CR_full G)->(Red_equiv (inc_list G) (inc h1) (inc h2))->
(Ex2 [g:pol_full](Red3 (inc_list G) (inc h1) (inc g))
[g:pol_full](Red3 (inc_list G) (inc h2) (inc g))).
Intros G h1 h2.
Destruct 1.
Intros fG G3G Reh1h2.
Elim Reh1h2.
Intros.
Elim (can_fun g); Intros; Trivial.
Elim p; Intros; Clear p.
Split with (exist pol [p:pol](full_pol p) x H4); Simpl; Auto.
Apply Red3_trans with g; Auto.
Intros.
Elim (can_fun h); Intros; Trivial.
Elim p; Intros; Clear p.
Split with (exist pol [p:pol](full_pol p) x H4); Simpl; Auto.
Apply Red3_ext1 with h; Auto.
Intros g h.
Intros f1G fg fh Regh.
Destruct 1.
Intros g0 Hg0.
Intros.
Split with g0; Auto.
Intros g f h fGG fg ff fh Regf.
Destruct 1.
Intros g0 Hg0 H1g0 Regff.
Destruct 1.
Intros g1 h1g1 h2g1.
Elim (can_fun f); Intros; Trivial.
Elim p; Intros; Clear p.
Elim (G3G (exist pol [p:pol](full_pol p) x H2) g0 g1); Auto.
Intros g2 h1g2 h2g2.
Split with g2; Auto.
Apply Red3_tran with (inc g0); Auto.
Apply Red3_tran with (inc g1); Auto.
Simpl.
Apply Red3_ext2 with f; Auto.
Simpl.
Apply Red3_ext2 with f; Auto.
Save.
Lemma G3_CR_impl_G1_full: (G:(list pol_full))(Groebner3_CR_full G)->
(Groebner1_full G).
Intros G G3CR.
Split; Intros.
Unfold Groebner3_CR_full in G3CR.
Elim G3CR; Auto.
Cut (equiv_Id (inc_list G) (inc f) vpol); Intros.
Elim ex_fpol_eq with vpol; Auto; Intros.
Cut (Red_equiv (inc_list G) (inc f) vpol); Intros.
Elim cr_full with G f x; Intros; Auto.
Apply Red3_ext1 with (inc x0); Auto.
Apply equpol_tran with (inc x); Auto.
Apply equpol_sym.
Apply normal_eq with (inc_list G); Auto.
Apply normal_ext with vpol; Auto.
Inversion H1.
Apply Red_equiv_eq; Auto.
Apply equpol_tran with vpol; Auto.
Apply Red_equiv_step; Auto.
Apply Red1_ext1 with vpol; Auto.
Apply Red_equiv_sym; Auto.
Apply Red_equiv_ext with vpol; Auto.
Apply Red_equiv_sym; Auto.
Apply Red_equiv_ext with vpol; Auto.
Apply congr_conv.
Apply equiv_Id_equiv_Id2; Trivial.
Inversion G3CR; Auto.
Save.
Index
This page has been generated by coqdoc