Library Axiomas_n_full2_tes
Require Export Prop_basic2_tes.
Lemma comp_common_succ: (p,q,r,s:pol)(F:(list pol))
(full_term_pol q)->
(full_term_pol s)->(equpol p q)->(equpol r s)->
(common_succ F p r)->
(common_succ F q s).
Intros p q r s F fq fs e1 e2.
Induction 1; Intros.
Exists p0.
Apply Red3_ext2 with f:=p; Auto.
Apply Red3_ext2 with f:=r; Auto.
Save.
Hints Resolve comp_common_succ.
Lemma eq_Red_equiv_common: (f,g:pol)(F:(list pol))(h:pol)(Red1 F f h)->
(h':pol)(Red1 F g h')->(equpol h h')->(common_succ F f g).
Intros f g F.
Induction 1.
Intros f0 ff0 fg0 f0F.
Induction 1.
Intros f1 f1F rf1 e fh.
Split with h; Auto.
Apply Red3_ext1 with g:=h'; Auto.
Inversion f0F; Auto.
Save.
Hints Resolve eq_Red_equiv_common.
Lemma Red1_is_common: (f,g:pol)(F:(list pol))(Red1 F f g)->
(common_succ F f g).
Intros f g F.
Induction 1.
Intros fF f0 f0F rf0.
Split with g; Auto.
(Inversion rf0; Auto).
Save.
Hints Resolve Red1_is_common.
Lemma sufc_common1: (f,g,fi:pol)(F:(list pol))(full_fam F)->(full_term_pol f)->
(full_term_pol g)->(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))))->(common_succ F f g).
Induction m; Intros.
Cut (full_term_pol fi); Intros.
Cut ~(equpol fi vpol); Intros.
Elim (dec_term_in_pol f (hterm (mult_m fi (a,b)))); Intros.
Red in a0.
Elim (decQ (coef g (hterm (mult_m fi (a,b))))); Intros.
Cut (eqQ (coef f (hterm (mult_m fi (a,b))))
(multQ_neg (coef (mult_m fi (a,b)) (hterm (mult_m fi (a,b)))))); Intros.
Cut (equpol g (suma_app f (mult_m fi (a,b)))); Intros; Auto.
Clear H5.
Cut (Red1 F f g); Auto.
Apply sufc_Red1 with fi:=fi m:=(monom_op (a,b)); Trivial.
Unfold monom_op.
Unfold z_monom.
Simpl; Auto.
Apply equpol_tran with (suma_app f (mult_m fi (a,b))); Auto.
Red.
Apply eqQ_trans with (coef g (hterm (mult_m fi (a,b)))); Auto.
Replace (hterm (mult_m fi (monom_op (a,b)))) with (hterm (mult_m fi (a,b))).
Apply eqQ_trans with (plusQ (coef g (hterm (mult_m fi (a,b))))
(coef (pol_opp (mult_m fi (a,b))) (hterm (mult_m fi (a,b))))).
Apply eqQ_trans with (coef (suma_app g (pol_opp (mult_m fi (a,b))))
(hterm (mult_m fi (a,b)))); Auto.
Apply eqQ_trans with (plusQ OQ
(multQ_neg (coef (mult_m fi (a,b)) (hterm (mult_m fi (a,b)))))).
Auto.
Apply eqQ_trans with (plusQ
(multQ_neg (coef (mult_m fi (a,b)) (hterm (mult_m fi (a,b))))) OQ); Auto.
Auto.
Cut (Red1 F f (suma_app g (pol_opp (mult_m fi ((divQ
(coef g (hterm (mult_m fi (a,b)))) (hcoef fi)),(mon_term (a,b))))))); Intros.
Cut (Red1 F g (suma_app g (pol_opp (mult_m fi ((divQ
(coef g (hterm (mult_m fi (a,b)))) (hcoef fi)),(mon_term (a,b))))))); Intros.
Split with (suma_app g (pol_opp (mult_m fi ((divQ
(coef g (hterm (mult_m fi (a,b)))) (hcoef fi)),(mon_term (a,b)))))); Auto.
Apply Red1_simp with f:=fi; Auto.
Apply red1_simpl with t:=(hterm (mult_m fi (a,b))); Trivial.
Apply full_term_suma_app; Trivial.
Apply full_term_opp.
Apply full_mult_m; 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_ss; Trivial.
Apply opp_comp.
Apply mult_pm_comp_2; Auto.
Apply Red1_simp with f:=fi; Auto.
Apply red1_simpl with t:=(hterm (mult_m fi (a,b))); Trivial.
Auto.
Apply term_div_hterm; Trivial.
Apply equpol_tran with (suma_app (suma_app g (pol_opp (mult_m fi (a,b))))
(pol_opp (mult_m fi ((divQ (coef f (hterm (mult_m fi (a,b)))) (hcoef fi)),
(div_term (hterm (mult_m fi (a,b))) (hterm fi)))))).
Apply equpol_tran with (suma_app g (suma_app (pol_opp (mult_m fi (a,b)))
(pol_opp (mult_m fi ((divQ (coef f (hterm (mult_m fi (a,b)))) (hcoef fi)),
(div_term (hterm (mult_m fi (a,b))) (hterm fi))))))).
Apply equpol_ss; Trivial.
Apply equpol_tran with (pol_opp (suma_app
(mult_m fi ((divQ (coef f (hterm (mult_m fi (a,b)))) (hcoef fi)),
(div_term (hterm (mult_m fi (a,b))) (hterm fi))))
(pol_opp (pol_opp (mult_m fi (a,b)))))).
Apply opp_comp.
Apply equpol_tran with (suma_app
(mult_m fi ((divQ (coef f (hterm (mult_m fi (a,b)))) (hcoef fi)),
(div_term (hterm (mult_m fi (a,b))) (hterm fi))))
(mult_m fi (a,b))).
Simpl.
Replace (div_term (hterm (mult_m fi (a,b))) (hterm fi)) with b.
Apply equpol_tran with (mult_m fi
((plusQ (divQ (coef f (hterm (mult_m fi (a,b)))) (hcoef fi)) a),b)).
Apply mult_pm_comp_2.
Simpl.
Right.
Split; Trivial.
Apply eqQ_trans with (divQ
(plusQ (coef f (hterm (mult_m fi (a,b)))) (multQ a (hcoef fi))) (hcoef fi)).
Apply eg_denomQ; Auto.
Cut (equpol g (suma_app f (mult_m fi (a,b)))); Intros; Auto.
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
(coef (suma_app f (mult_m fi (a,b))) (hterm (mult_m fi (a,b)))); Auto.
Apply plusQ_comp; Auto.
Apply eqQ_trans with (hcoef (mult_m fi (a,b))); Auto.
Apply eqQ_trans with (multQ (hcoef fi) a); Auto.
Apply eqQ_trans with (multQ (hcoef fi) (mon_coef (a,b))); Auto.
Apply hcoef_mult; Auto.
Apply eqQ_sym.
Apply eqQ_trans with (plusQ a
(divQ (coef f (hterm (mult_m fi (a,b)))) (hcoef fi))); Auto.
Apply eqQ_trans with (divQ (plusQ
(multQ a (hcoef fi)) (coef f (hterm (mult_m fi (a,b))))) (hcoef fi)); Auto.
Auto.
Auto.
Auto.
Auto.
Auto.
Auto.
Cut (Red1 F g f); Intros; Auto.
Apply sufc_Red1 with fi:=fi m:=(a,b); Auto.
Apply elem_n_vpol with F; Trivial.
Apply elem_full with F; Trivial.
Save.
Hints Resolve sufc_common1.
Lemma sufc_common: (f,g,fi:pol)(F:(list pol))(full_fam F)->(full_term_pol f)->
(full_term_pol g)->(pol_In_ensemb fi F)->(m:monom)(full_mon n m)->
(equpol f (suma_app g (pol_opp (mult_m fi m))))->(common_succ F f g).
Induction m; Intros.
Elim (z_monom_dec (a,b)); Intros.
Cut (equpol f g); Intros.
Split with f; Auto.
Apply equpol_tran with (suma_app g (pol_opp (mult_m fi (a,b)))); Trivial.
Apply equpol_tran with (suma_app g vpol).
Apply equpol_ss; Trivial.
Apply equpol_tran with (pol_opp vpol); Auto.
Auto.
Apply sufc_common1 with fi:=fi m:=(a,b); Auto.
Save.
Hints Resolve sufc_common.
Lemma congr_conv : (F:(list pol))(f,g:pol)(suma_pol_mon F f g)-> (Red_equiv F f g).
Induction 1; Intros.
Auto.
Apply Red_equiv_trans with g1; Trivial.
Apply common_is_Red_equiv.
Apply sufc_common with fi:=fi m:=m; Trivial.
Apply equpol_sym.
Apply equpol_tran with
(suma_app g1 (suma_app (mult_m fi m) (pol_opp (mult_m fi m)))).
Apply equpol_tran with
(suma_app (suma_app g1 (mult_m fi m)) (pol_opp (mult_m fi m))).
Apply monot_suma; Assumption.
Auto.
Apply equpol_tran with (suma_app g1 vpol); Auto.
Save.
Hints Resolve congr_conv.
Index
This page has been generated by coqdoc