Library red_expl
Require Export Hmtc_axiom.
Lemma hred_suma: (f,g,fi:pol)(hred fi f g)->
(h:pol)(full_term_pol h)->(Ttm (hterm h) (hterm f))->
(red fi (suma_app f h) (suma_app g h)).
Induction 1.
Intros.
Cut (equpol (suma_app g h)
(suma_app (suma_app f h)
(pol_opp
(mult_m fi
((divQ (hcoef f) (hcoef fi)),
(div_term (hterm f) (hterm fi))))))).
Intros.
Cut (hterm (suma_app f h))=(hterm f).
Intros.
Cut (eqQ (hcoef (suma_app f h)) (hcoef f)); Intros.
Apply red1_simpl with t:=(hterm f); Trivial.
Apply aux_hterm_suma_Ttm; Auto.
Apply full_term_suma_app; Auto.
Apply full_term_suma_app; Auto.
Apply equpol_tran
with (suma_app (suma_app f h)
(pol_opp
(mult_m fi
((divQ (hcoef f) (hcoef fi)),
(div_term (hterm f) (hterm fi)))))); Trivial.
Apply equpol_ss; Trivial.
Apply opp_comp.
Apply mult_pm_comp_2.
Simpl.
Right .
Split; Trivial.
Apply eg_denomQ; Auto.
Apply eqQ_trans with (hcoef (suma_app f h)); Auto.
Rewrite <- H10; Auto.
(Apply hcoef_suma_Ttm; Auto).
(Apply hterm_suma_Ttm; Auto).
Apply equpol_tran with (suma_app h g).
Auto.
Apply equpol_tran
with (suma_app h
(suma_app f
(pol_opp
(mult_m fi
((divQ (hcoef f) (hcoef fi)),
(div_term (hterm f) (hterm fi))))))).
Auto.
Apply equpol_tran
with (suma_app f
(suma_app h
(pol_opp
(mult_m fi
((divQ (hcoef f) (hcoef fi)),
(div_term (hterm f) (hterm fi))))))).
Auto.
Auto.
Save.
Hints Resolve hred_suma.
Lemma hred_suma_bis: (f,g,fi:pol)(hred fi f g)->
(h:pol)(full_term_pol h)->
((t:term)(term_in_pol h t)->(Ttm t (hterm f)))->
(red fi (suma_app f h) (suma_app g h)).
Intros.
(Elim (vpol_dec_full_term h H0); Intros).
Apply red_ext1 with g.
(Apply equpol_tran with (suma_app g vpol); Auto).
(Inversion H; Auto).
Apply red_ext2 with f.
(Apply equpol_tran with (suma_app f vpol); Auto).
Inversion H; Auto.
Auto.
Cut (Ttm (hterm h) (hterm f)); Intros.
Auto.
(Apply H1; Auto).
Save.
Hints Resolve hred_suma_bis.
Lemma basic2: (f,g,fi:pol)(red fi f g)->
(h:pol)(full_term_pol h)->((t:term)(term_in_pol h t)->
(t':term)(term_in_pol f t')->(Ttm t' t))->
(red fi (suma_app f h) (suma_app g h)).
Intros f g fi r.
Cut ~(equpol f vpol).
Intros nfvpol.
Generalize r.
Clear r.
Induction 1.
Intros.
Cut (equpol (suma_app g h)
(suma_app (suma_app f h)
(pol_opp
(mult_m fi
((divQ (coef f t) (hcoef fi)),(div_term t (hterm fi))))))).
Intros.
(Apply red1_simpl with t; Trivial).
Apply term_in_Ttm_hterm; Auto.
Auto.
Auto.
Apply equpol_tran
with (suma_app (suma_app f h)
(pol_opp
(mult_m fi
((divQ (coef f t) (hcoef fi)),(div_term t (hterm fi)))))).
Auto.
Apply equpol_ss; Trivial.
Apply opp_comp.
Apply mult_pm_comp_2.
Simpl.
Right .
(Split; Trivial).
Apply eg_denomQ.
Auto.
(Apply coef_suma_Ttm; Auto).
Apply equpol_tran with (suma_app h g).
Auto.
Apply equpol_tran
with (suma_app (suma_app h f)
(pol_opp
(mult_m fi
((divQ (coef f t) (hcoef fi)),(div_term t (hterm fi)))))).
Apply equpol_tran
with (suma_app h
(suma_app f
(pol_opp
(mult_m fi
((divQ (coef f t) (hcoef fi)),(div_term t (hterm fi))))))).
Auto.
Auto.
Auto.
(Apply red_n_vpol1 with g fi; Assumption).
Save.
Hints Resolve basic2.
Lemma basic2_bis: (f,g,fi:pol)(red fi f g)->
(h:pol)(full_term_pol h)->
((t:term)(term_in_pol h t)->(Ttm (hterm f) t))->
(red fi (suma_app f h) (suma_app g h)).
Intros f g fi.
Induction 1.
Intros.
Cut (equpol (suma_app g h)
(suma_app (suma_app f h)
(pol_opp
(mult_m fi
((divQ (coef f t) (hcoef fi)),(div_term t (hterm fi))))))).
Intros.
(Apply red1_simpl with t; Trivial).
Apply term_in_Ttm_hterm; Auto.
Auto.
Auto.
Apply equpol_tran
with (suma_app (suma_app f h)
(pol_opp
(mult_m fi
((divQ (coef f t) (hcoef fi)),(div_term t (hterm fi)))))).
Auto.
Apply equpol_ss; Trivial.
Apply opp_comp.
Apply mult_pm_comp_2.
Simpl.
Right .
(Split; Trivial).
Apply eg_denomQ.
Auto.
(Apply coef_suma_Ttm; Auto).
Apply equpol_tran with (suma_app h g).
Auto.
Apply equpol_tran
with (suma_app (suma_app h f)
(pol_opp
(mult_m fi
((divQ (coef f t) (hcoef fi)),(div_term t (hterm fi)))))).
Apply equpol_tran
with (suma_app h
(suma_app f
(pol_opp
(mult_m fi
((divQ (coef f t) (hcoef fi)),(div_term t (hterm fi))))))).
Auto.
Auto.
Auto.
Save.
Hints Resolve basic2_bis.
Lemma basic3: (h,f,g:pol)(F:(list pol))
(Red1 F f g)->(full_term_pol h)->
(common_succ F (suma_app f h) (suma_app g h)).
Intros h f g F.
Induction 1.
Intros FF fi pfiF.
Induction 1.
Intros t tf ff ffi fg nfivpol tdtfi e fh.
(Cut (common_succ F (suma_app g h) (suma_app f h)); Auto).
Cut (equpol (suma_app g h)
(suma_app (suma_app f h)
(pol_opp
(mult_m fi
((divQ (coef f t) (hcoef fi)),(div_term t (hterm fi))))))).
Intros.
Apply sufc_common
with fi ((divQ (coef f t) (hcoef fi)),(div_term t (hterm fi))).
Assumption.
(Apply full_term_suma_app; Auto).
(Apply full_term_suma_app; Auto).
Assumption.
Simpl.
Apply term_div_full.
Apply full_coef with f; Auto.
Apply full_hterm_full_pol; Auto.
Assumption.
Apply equpol_tran with (suma_app h g).
Auto.
Apply equpol_tran
with (suma_app f
(suma_app h
(pol_opp
(mult_m fi
((divQ (coef f t) (hcoef fi)),(div_term t (hterm fi))))))).
Apply equpol_tran
with (suma_app h
(suma_app f
(pol_opp
(mult_m fi
((divQ (coef f t) (hcoef fi)),(div_term t (hterm fi))))))).
(Apply equpol_ss; Trivial).
Auto.
Auto.
Save.
Hints Resolve basic3.
Lemma pre_basic4_Red1: (h,h':pol)(F:(list pol))(Red1 F h h')->
(f:pol)(full_term_pol f)->(g:pol)(full_term_pol g)->
(equpol h (suma_app f (pol_opp g)))->
(EX f' | (Red3 F f f')
& (EX g' | (Red3 F g g')
& (equpol h' (suma_app f' (pol_opp g'))))).
Intros h h' F.
Induction 1.
Intros fF fi pfiF.
Induction 1.
Intros.
(Elim (dec_term_in_pol f t); Intros).
Elim (dec_term_in_pol g t); Intros.
Red in a.
Red in a0.
Elim (decQ_t (coef f t) (coef g t)); Intros.
(Cut (no_term_in_pol h t); Intros).
Red in H1.
Red in H11.
(Elim H1; Auto).
Red.
Apply eqQ_trans with (plusQ (coef f t) (coef (pol_opp g) t)).
Apply eqQ_trans with (coef (suma_app f (pol_opp g)) t); Auto.
Apply eqQ_trans with (plusQ (coef f t) (multQ_neg (coef g t))).
Auto.
Apply suma_op.
Apply eqQ_trans with (coef g t); Auto.
Split
with (suma_app f
(pol_opp
(mult_m fi
((divQ (coef f t) (hcoef fi)),(div_term t (hterm fi)))))).
Apply Red3_step; Auto.
(Apply full_term_suma_app; Auto).
Apply full_term_opp.
(Apply full_mult_m; Trivial).
(Apply term_div_full; Auto).
(Apply full_coef with h; Auto).
(Apply Red1_simp with fi; Auto).
(Apply red1_simpl with t; Auto).
Apply full_term_suma_app; Auto.
Apply full_term_opp.
Apply full_mult_m; Trivial.
Apply term_div_full; Auto.
Apply full_coef with h; Auto.
Split
with (suma_app g
(pol_opp
(mult_m fi
((divQ (coef g t) (hcoef fi)),(div_term t (hterm fi)))))).
(Apply Red3_step; Auto).
Apply full_term_suma_app; Auto.
Apply full_term_opp.
Apply full_mult_m; Trivial.
Apply term_div_full; Auto.
Apply full_coef with h; Auto.
Apply Red1_simp with fi; Auto.
Apply red1_simpl with t; Auto.
(Apply full_term_suma_app; Auto).
Apply full_term_opp.
(Apply full_mult_m; Trivial).
(Apply term_div_full; Auto).
(Apply full_coef with h; Auto).
Apply equpol_tran
with (suma_app h
(pol_opp
(mult_m fi
((divQ (coef h t) (hcoef fi)),(div_term t (hterm fi))))));
Trivial.
Apply equpol_tran
with (suma_app f
(suma_app
(pol_opp
(mult_m fi
((divQ (coef f t) (hcoef fi)),(div_term t (hterm fi)))))
(pol_opp
(suma_app g
(pol_opp
(mult_m fi
((divQ (coef g t) (hcoef fi)),
(div_term t (hterm fi))))))))).
Apply equpol_tran
with (suma_app f
(suma_app
(pol_opp
(mult_m fi
((divQ (coef f t) (hcoef fi)),(div_term t (hterm fi)))))
(suma_app (pol_opp g)
(pol_opp
(pol_opp
(mult_m fi
((divQ (coef g t) (hcoef fi)),
(div_term t (hterm fi))))))))).
Apply equpol_tran
with (suma_app f
(suma_app (pol_opp g)
(suma_app
(pol_opp
(mult_m fi
((divQ (coef f t) (hcoef fi)),(div_term t (hterm fi)))))
(pol_opp
(pol_opp
(mult_m fi
((divQ (coef g t) (hcoef fi)),
(div_term t (hterm fi))))))))).
Apply equpol_tran
with (suma_app (suma_app f (pol_opp g))
(suma_app
(pol_opp
(mult_m fi
((divQ (coef f t) (hcoef fi)),(div_term t (hterm fi)))))
(pol_opp
(pol_opp
(mult_m fi
((divQ (coef g t) (hcoef fi)),(div_term t (hterm fi)))))))).
Apply equpol_ss; Trivial.
Apply equpol_tran
with (pol_opp
(suma_app
(mult_m fi
((divQ (coef f t) (hcoef fi)),(div_term t (hterm fi))))
(pol_opp
(mult_m fi
((divQ (coef g t) (hcoef fi)),(div_term t (hterm fi))))))).
Apply opp_comp.
Apply equpol_tran
with (suma_app
(pol_opp
(mult_m fi
(monom_op
((divQ (coef f t) (hcoef fi)),(div_term t (hterm fi))))))
(pol_opp
(mult_m fi
((divQ (coef g t) (hcoef fi)),(div_term t (hterm fi)))))).
Apply equpol_tran
with (pol_opp
(suma_app
(mult_m fi
(monom_op
((divQ (coef f t) (hcoef fi)),(div_term t (hterm fi)))))
(mult_m fi
((divQ (coef g t) (hcoef fi)),(div_term t (hterm fi)))))).
Unfold monom_op.
Unfold mon_term.
Unfold mon_coef.
Apply equpol_tran
with (pol_opp
(mult_m fi
((plusQ (multQ_neg (divQ (coef f t) (hcoef fi)))
(divQ (coef g t) (hcoef fi))),(div_term t (hterm fi))))).
Apply equpol_tran
with (mult_m fi
(monom_op
((plusQ (multQ_neg (divQ (coef f t) (hcoef fi)))
(divQ (coef g t) (hcoef fi))),(div_term t (hterm fi))))).
Apply mult_pm_comp_2.
Simpl.
Right .
Split; Trivial.
Apply eqQ_trans
with (multQ_neg
(plusQ (divQ (multQ_neg (coef f t)) (hcoef fi))
(divQ (coef g t) (hcoef fi)))).
Apply eqQ_trans
with (multQ_neg
(divQ (plusQ (multQ_neg (coef f t)) (coef g t)) (hcoef fi))).
Apply eqQ_trans
with (divQ (multQ_neg (plusQ (multQ_neg (coef f t)) (coef g t)))
(hcoef fi)).
Apply eg_denomQ.
Auto.
Apply eqQ_trans with (plusQ (coef f t) (coef (pol_opp g) t)).
Apply eqQ_trans with (coef (suma_app f (pol_opp g)) t); Auto.
Apply eqQ_trans
with (plusQ (multQ_neg (multQ_neg (coef f t))) (multQ_neg (coef g t))).
Auto.
Auto.
Auto.
Apply eq_mulQ_neg.
Auto.
Apply eq_mulQ_neg.
Apply plusQ_comp; Trivial.
Auto.
Auto.
Auto.
Auto.
Auto.
Auto.
Auto.
Auto.
Apply equpol_ss; Trivial.
Auto.
Auto.
Split
with (suma_app f
(pol_opp
(mult_m fi
((divQ (coef f t) (hcoef fi)),(div_term t (hterm fi)))))).
(Apply Red3_step; Auto).
Apply full_term_suma_app; Auto.
Apply full_term_opp.
Apply full_mult_m; Trivial.
Apply term_div_full; Auto.
Apply full_coef with h; Auto.
Apply Red1_simp with fi; Auto.
Apply red1_simpl with t; Auto.
(Apply full_term_suma_app; Auto).
Apply full_term_opp.
(Apply full_mult_m; Trivial).
(Apply term_div_full; Auto).
(Apply full_coef with h; Auto).
Split with g.
Auto.
(Apply equpol_tran
with (suma_app h
(pol_opp
(mult_m fi
((divQ (coef h t) (hcoef fi)),(div_term t (hterm fi))))));
Trivial).
Apply equpol_tran
with (suma_app f
(suma_app
(pol_opp
(mult_m fi
((divQ (coef f t) (hcoef fi)),(div_term t (hterm fi)))))
(pol_opp g))).
Apply equpol_tran
with (suma_app f
(suma_app (pol_opp g)
(pol_opp
(mult_m fi
((divQ (coef f t) (hcoef fi)),(div_term t (hterm fi))))))).
Apply equpol_tran
with (suma_app (suma_app f (pol_opp g))
(pol_opp
(mult_m fi
((divQ (coef f t) (hcoef fi)),(div_term t (hterm fi)))))).
(Apply equpol_ss; Trivial).
Apply opp_comp.
Apply mult_pm_comp_2.
Simpl.
Right .
Split; Trivial.
Apply eg_denomQ.
Auto.
Apply eqQ_trans with (plusQ (coef f t) (coef (pol_opp g) t)).
Apply eqQ_trans with (coef (suma_app f (pol_opp g)) t); Auto.
Red in b.
Apply eqQ_trans with (plusQ (coef f t) (coef g t)).
Apply plusQ_comp_l.
Apply eqQ_sym.
Apply eqQ_trans with (multQ_neg (coef g t)); Auto.
Apply eqQ_trans with (plusQ (coef f t) OQ); Auto.
Auto.
Auto.
Auto.
Elim (dec_term_in_pol g t); Intros.
Split with f; Auto.
Split
with (suma_app g
(pol_opp
(mult_m fi
((divQ (coef g t) (hcoef fi)),(div_term t (hterm fi)))))).
Apply Red3_step; Auto.
(Apply full_term_suma_app; Auto).
Apply full_term_opp.
(Apply full_mult_m; Trivial).
(Apply term_div_full; Auto).
(Apply full_coef with h; Auto).
(Apply Red1_simp with fi; Auto).
(Apply red1_simpl with t; Auto).
Apply full_term_suma_app; Auto.
Apply full_term_opp.
Apply full_mult_m; Trivial.
Apply term_div_full; Auto.
Apply full_coef with h; Auto.
Apply equpol_tran
with (suma_app h
(pol_opp
(mult_m fi
((divQ (coef h t) (hcoef fi)),(div_term t (hterm fi))))));
Trivial.
Apply equpol_tran
with (suma_app f
(suma_app (pol_opp g)
(pol_opp
(pol_opp
(mult_m fi
((divQ (coef g t) (hcoef fi)),(div_term t (hterm fi)))))))).
Apply equpol_tran
with (suma_app (suma_app f (pol_opp g))
(pol_opp
(pol_opp
(mult_m fi
((divQ (coef g t) (hcoef fi)),(div_term t (hterm fi))))))).
Apply equpol_ss; Trivial.
Apply opp_comp.
Apply equpol_tran
with (pol_opp
(mult_m fi
(monom_op
((divQ (coef h t) (hcoef fi)),(div_term t (hterm fi)))))).
Auto.
Apply opp_comp.
Apply mult_pm_comp_2.
Simpl.
Right .
(Split; Trivial).
Apply eqQ_trans with (divQ (multQ_neg (coef h t)) (hcoef fi)).
Auto.
Apply eg_denomQ.
Auto.
Red in b.
Apply eqQ_trans
with (multQ_neg (plusQ (coef f t) (coef (pol_opp g) t))).
Apply eqQ_sym.
Apply eq_mulQ_neg.
(Apply eqQ_trans with (coef (suma_app f (pol_opp g)) t); Auto).
Apply eqQ_trans
with (plusQ (multQ_neg (coef f t)) (multQ_neg (coef (pol_opp g) t))).
Auto.
Apply eqQ_trans
with (plusQ (multQ_neg OQ) (multQ_neg (coef (pol_opp g) t))).
Auto.
Apply eqQ_trans with (plusQ OQ (multQ_neg (coef (pol_opp g) t))).
Auto.
Apply eqQ_trans with (multQ_neg (coef (pol_opp g) t)).
Apply eqQ_trans with (plusQ (multQ_neg (coef (pol_opp g) t)) OQ); Auto.
Auto.
Auto.
Auto.
Cut (no_term_in_pol h t); Intros.
Red in H1.
Red in H11.
Elim H1; Auto.
Apply comp_no_term_in_pol with (suma_app f (pol_opp g)); Auto.
Red.
Red in b.
Red in b0.
Apply eqQ_trans with (plusQ (coef f t) (coef (pol_opp g) t)).
Auto.
Apply eqQ_trans with (plusQ OQ (coef (pol_opp g) t)).
Auto.
Apply eqQ_trans with (coef (pol_opp g) t).
Apply eqQ_trans with (plusQ (coef (pol_opp g) t) OQ); Auto.
Apply eqQ_trans with (multQ_neg (coef g t)); Auto.
Save.
Hints Resolve pre_basic4_Red1.
Lemma pre_basic4_Red3:
(h,h':pol)
(F:(list pol))
(Red3 F h h')
->(f:pol)
(full_term_pol f)
->(g:pol)
(full_term_pol g)
->(equpol h (suma_app f (pol_opp g)))
->(EX f':pol | (Red3 F f f')
& (EX g':pol | (Red3 F g g')
& (equpol h' (suma_app f' (pol_opp g'))))).
Induction 1.
Intros.
Split with f; Auto.
Split with g0.
Auto.
(Apply equpol_tran with g; Auto).
Intros.
Apply pre_basic4_Red1 with g; Auto.
Intros.
Elim H5 with f0 g0; Trivial.
Intros.
Elim H12; Intros.
(Elim H7 with x x0; Trivial).
Intros.
Elim H16.
Intros.
Split with x1.
Auto.
(Apply Red3_tran with x; Auto).
(Split with x2; Trivial).
(Apply Red3_tran with x0; Auto).
(Inversion H11; Auto).
(Inversion H13; Auto).
Save.
Hints Resolve pre_basic4_Red3.
Lemma basic4: (f,g:pol)(F:(list pol))(full_term_pol f)->
(full_term_pol g)->(Red3 F (suma_app f (pol_opp g)) vpol)->
(common_succ F f g).
Intros.
Elim pre_basic4_Red3 with (suma_app f (pol_opp g)) vpol F f g; Trivial.
Intros.
Elim H3.
Intros.
(Split with x; Trivial).
(Apply Red3_ext1 with x0; Trivial).
Apply equpol_sym.
Apply equpol_tran with (suma_app x (suma_app x0 (pol_opp x0))).
Apply equpol_tran with (suma_app x vpol); Auto.
Apply equpol_tran with (suma_app x0 (suma_app x (pol_opp x0))).
Auto.
Apply equpol_tran with (suma_app x0 vpol); Auto.
(Inversion H2; Auto).
Save.
Hints Resolve basic4.
Index
This page has been generated by coqdoc