Library coeficiente_tes
Require Export Lcm_tes.
Require Export Div_poly_tes.
Fixpoint coef [p:pol]: term -> Q:=
[t:term] Cases p of
vpol => OQ
| (cpol (c,u) p1) => Cases (eq_tm_dec t u) of
(left x) => (plusQ c (coef p1 t))
| (right y) => (coef p1 t)
end
end.
Lemma coef_suma_pol: (p,q:pol)(t:term)(eqQ
(coef (suma_app p q) t) (plusQ (coef p t) (coef q t))).
Induction p.
Intros.
Simpl.
Apply eqQ_sym.
Apply eqQ_trans with (plusQ (coef q t) OQ); Auto.
Induction m; Intros.
Simpl.
Elim (eq_tm_dec t b); Intros; Auto.
Apply eqQ_trans with (plusQ a (plusQ (coef p0 t) (coef q t)));Auto.
Save.
Hints Resolve coef_suma_pol.
Lemma term_equpol2: (p:pol)(t1,t2:term)(t1=t2)->
(eqQ (coef p t1) (coef p t2)).
Intros; Rewrite -> H; Auto.
Save.
Hints Resolve term_equpol2.
Lemma term_equpol: (p,p':pol)(t:term)(equpol p p')->
(eqQ (coef p t) (coef p' t)).
Intros p p' t H; Elim H.
Auto.
Auto.
Intros.
Apply eqQ_trans with (coef q t); Auto.
Induction m; Intros.
Simpl.
Elim (eq_tm_dec t b); Intros.
Apply eqQ_trans with
(plusQ (coef p0 t) (coef (cpol (a,b) q) t));Auto.
Rewrite -> a0.
Simpl.
Elim (eq_tm_dec b b); Intros.
Apply eqQ_trans with
(plusQ (plusQ (coef p0 b) a) (coef q b));Auto.
Apply eqQ_trans with
(plusQ (plusQ a (coef p0 b)) (coef q b));Auto.
Apply eqQ_trans with
(plusQ a (plusQ (coef p0 b) (coef q b)));Auto.
Elim b0; Auto.
Apply eqQ_trans with (plusQ (coef p0 t) (coef q t));Auto.
Apply eqQ_trans with
(plusQ (coef p0 t) (coef (cpol (a,b) q) t)).
Apply plusQ_comp_l.
Simpl.
Elim (eq_tm_dec t b); Intros.
Elim b0; Auto.
Auto.
Auto.
Intros.
Apply eqQ_trans with (plusQ (coef p0 t) (coef q t));Auto.
Apply eqQ_trans with (plusQ (coef p'0 t) (coef q' t));Auto.
Intros.
Simpl.
Elim (eq_tm_dec t t0); Intros; Auto.
Induction m.
Unfold z_monom; Intros.
Simpl.
Elim (eq_tm_dec t b); Intros; Trivial.
Apply eqQ_trans with (plusQ OQ (coef p0 t)); Auto.
Apply eqQ_trans with (plusQ (coef p0 t) OQ); Auto.
Save.
Hints Resolve term_equpol.
Lemma coef_pol_opp: (p:pol)(t:term)(eqQ (coef p t)
(multQ_neg (coef (pol_opp p) t))).
Induction p.
Auto.
Induction m; Intros.
Simpl.
Elim (eq_tm_dec t b); Intros; Trivial.
Apply eqQ_trans with (plusQ (multQ_neg (multQ_neg a))
(multQ_neg (coef (pol_opp p0) t))); Auto.
Save.
Hints Resolve coef_pol_opp.
Lemma coef_pol_opp2: (p:pol)(t:term)(eqQ
(multQ_neg (coef p t)) (coef (pol_opp p) t)).
Intros.
(Apply eqQ_trans with (multQ_neg (multQ_neg (coef (pol_opp p) t)));
Auto).
Save.
Hints Resolve coef_pol_opp2.
Lemma coef_n_term: (a:Q)(t,t0:term)(p:pol)(~t=t0)->
(eqQ (coef (cpol (a,t0) p) t) (coef p t)).
Intros.
Simpl.
Elim (eq_tm_dec t t0); Auto; Intros.
Elim H; Trivial.
Save.
Hints Resolve coef_n_term.
Lemma coef_term_mult:(p:pol)(t,t0:term)(c:Q)(full n t0)->
(full_term_pol p)->
(eqQ (coef (mult_m p (c,t)) (term_mult t0 t))
(multQ (coef p t0) c)).
Induction p.
Auto.
Induction m; Intros.
Inversion H1.
Elim (decQ c); Intros.
Apply eqQ_trans with OQ; Auto.
Cut (equpol (mult_m (cpol (a,b) p0) (c,t))
(cpol (mult_mon (c,t) (a,b)) (mult_m p0 (c,t)))); Auto; Intros.
Apply eqQ_trans with (coef
(cpol (mult_mon (c,t) (a,b)) (mult_m p0 (c,t)))
(term_mult t0 t)); Auto.
Cut (z_monom (c,t)); Auto; Intros.
Cut (equpol (cpol (mult_mon (c,t) (a,b)) (mult_m p0 (c,t)))
(mult_m p0 (c,t))); Intros.
Apply eqQ_trans with (coef (mult_m p0 (c,t)) (term_mult t0 t)); Auto.
Cut (equpol (mult_m p0 (c,t)) vpol); Intros.
Apply eqQ_trans with (coef vpol (term_mult t0 t)); Auto.
Auto.
Auto.
Cut (equpol (mult_m (cpol (a,b) p0) (c,t))
(cpol (mult_mon (c,t) (a,b)) (mult_m p0 (c,t)))); Auto; Intros.
Apply eqQ_trans with (coef
(cpol (mult_mon (c,t) (a,b)) (mult_m p0 (c,t)))
(term_mult t0 t)); Auto.
Cut (equmon (mult_mon (c,t) (a,b)) ((multQ c a),(term_mult t b)));
Auto; Intros.
Apply eqQ_trans with (coef
(cpol ((multQ c a),(term_mult t b))
(mult_m p0 (c,t))) (term_mult t0 t));
Auto.
Elim (eq_tm_dec b t0); Intros.
Rewrite -> a1.
Simpl.
Elim (eq_tm_dec (term_mult t0 t) (term_mult t t0)); Intros.
Elim (eq_tm_dec t0 t0); Intros.
Apply eqQ_trans with (plusQ (multQ a c) (multQ (coef p0 t0) c)).
Apply plusQ_comp; Trivial.
Apply H; Trivial.
Apply eqQ_sym.
Apply eqQ_trans with (multQ c (plusQ a (coef p0 t0))); Auto.
Apply eqQ_trans with (plusQ (multQ c a) (multQ c (coef p0 t0))); Auto.
Elim b1; Trivial.
Elim b1; Trivial.
Simpl.
Elim (eq_tm_dec (term_mult t0 t) (term_mult t b)); Intros.
Cut ~(term_mult t b)=(term_mult t t0); Intros.
Elim H9.
Symmetry.
Transitivity (term_mult t0 t); Auto.
Apply term_mult_n_eq with n:=n; Auto.
Elim (eq_tm_dec t0 b); Intros.
Elim b1; Auto.
Apply H; Auto.
Save.
Hints Resolve coef_term_mult.
Definition term_in_pol: pol->term->Prop:=
[p:pol][t:term](~(eqQ (coef p t) OQ)).
Definition no_term_in_pol: pol->term->Prop:=
[p:pol][t:term](eqQ (coef p t) OQ).
Lemma coef_z_in_pol: (y:Q)(eqQ y OQ)->
(t:term)(p:pol)({(term_in_pol p t)}+{(no_term_in_pol p t)})->
(y0:term)({(term_in_pol (cpol (y,y0) p) t)}+{(no_term_in_pol (cpol (y,y0) p) t)}).
Intros.
Elim H0; Intros.
Left.
Red.
Red in a.
Simpl.
Elim (eq_tm_dec t y0); Auto.
Elim (eq_tm_dec t y0); Intros.
Right.
Red.
Simpl.
Elim (eq_tm_dec t y0); Intros; Auto.
Right.
Red.
Simpl.
Elim (eq_tm_dec t y0); Auto.
Save.
Hints Resolve coef_z_in_pol.
Lemma dec_term_in_pol: (f:pol)(t:term)
{(term_in_pol f t)}+{(no_term_in_pol f t)}.
Induction f.
Right.
Red; Auto.
Induction m; Intros.
Elim (decQ a); Intros; Auto.
Elim (eq_tm_dec t b); Intros.
Elim (decQ_t (coef p t) (multQ_neg a)); Intros.
Right.
Red.
Simpl.
Elim (eq_tm_dec t b); Intros.
Apply eqQ_trans with (plusQ a (multQ_neg a)); Auto.
Elim b1; Auto.
Left.
Red.
Simpl.
Elim (eq_tm_dec t b); Intros.
Red; Intros.
Absurd (eqQ (coef p t) (multQ_neg a)); Trivial.
Apply suma_op_inv.
Apply eqQ_trans with (plusQ a (coef p t)); Auto.
Elim b2; Trivial.
Elim H with t:=t; Intros.
Left.
Red.
Red in a0.
Simpl.
Elim (eq_tm_dec t b); Intros; Auto.
Right.
Red.
Red in b2.
Simpl.
Elim (eq_tm_dec t b); Intros.
Elim b1; Auto.
Trivial.
Save.
Hints Resolve dec_term_in_pol.
Lemma comp_no_term_in_pol: (p,q:pol)(t:term)(equpol p q)->
(no_term_in_pol p t)->(no_term_in_pol q t).
Intros.
Red.
Red in H0.
(Apply eqQ_trans with (coef p t); Auto).
Save.
Hints Resolve comp_no_term_in_pol.
Lemma comp_term_in_pol: (p,q:pol)(t:term)(equpol p q)->
(term_in_pol p t)->(term_in_pol q t).
Intros.
Unfold term_in_pol.
Red in H0.
(Apply comp_nOQ with c:=(coef p t); Auto).
Save.
Hints Resolve comp_term_in_pol.
Lemma term_in_pol_opp: (p:pol)(t:term)
(term_in_pol (pol_opp p) t)->(term_in_pol p t).
Unfold term_in_pol; Intros.
Apply comp_nOQ with (multQ_neg (coef (pol_opp p) t)); Auto.
Save.
Hints Resolve term_in_pol_opp.
Lemma no_term_in_pol_opp: (p:pol)(t:term)
(no_term_in_pol (pol_opp p) t)->(no_term_in_pol p t).
Induction p; Auto.
Induction m; Intros.
Unfold no_term_in_pol.
Red in H0.
(Apply eqQ_trans with (multQ_neg (coef (pol_opp (cpol (a,b) p0)) t));
Auto).
Save.
Hints Resolve no_term_in_pol_opp.
Lemma term_in_pol_nvpol: (f:pol)(t:term)(term_in_pol f t)->
~(equpol f vpol).
Intros.
(Red; Intros).
(Cut (term_in_pol vpol t); Intros).
(Elim H1; Auto).
Apply comp_term_in_pol with f; Auto.
Save.
Hints Resolve term_in_pol_nvpol.
Lemma no_equpol_Ttm: (p:pol)(full_term_pol p)->
(k:Q)(~(eqQ k OQ))->(t:term)(full n t)->
(no_term_in_pol p t)->(~(equpol
(suma_app (cpol (k,t) vpol) p) vpol)).
Intros.
Apply term_in_pol_nvpol with t.
Red in H2.
Red.
Apply comp_nOQ with (plusQ (coef (cpol (k,t) vpol) t) (coef p t)); Auto.
Apply comp_nOQ with (plusQ k OQ).
Apply plusQ_comp; Auto.
Unfold coef.
Elim (eq_tm_dec t t); Intros; Auto.
Elim b; Auto.
Apply comp_nOQ with k; Auto.
Save.
Hints Resolve no_equpol_Ttm.
Lemma n_zmonom_n_vpol: (m:monom)(full_mon n m)->(~(z_monom m))->
~(equpol (cpol m vpol) vpol).
Induction m; Intros.
Unfold z_monom in H0.
Apply eq_nvpol with (suma_app (cpol (a,b) vpol) vpol); Auto.
Apply no_equpol_Ttm; Auto.
Red; Auto.
Save.
Hints Resolve n_zmonom_n_vpol.
Lemma eq_term_in_pol_monom: (k:Q)(t,t':term)(full n t)->
(full n t')->(term_in_pol (cpol (k,t') vpol) t)->
t=t'.
Intros.
Elim (eq_tm_dec t t'); Trivial.
Intros.
Red in H1.
Unfold coef in H1.
Elim H1.
(Elim (eq_tm_dec t t'); Trivial).
Intros.
Elim b; Auto.
Save.
Hints Resolve eq_term_in_pol_monom.
Lemma no_term_in_cpol: (y:Q)(y0,t:term)(p:pol)
(no_term_in_pol (cpol (y,y0) p) t)->
~(t=y0)->(no_term_in_pol p t).
Intros.
Red.
Red in H.
(Apply eqQ_trans with (coef (cpol (y,y0) p) t); Auto).
Save.
Lemma split_term_in_pol_cons: (y:Q)(y0,t:term)(p:pol)
(term_in_pol (cpol (y,y0) p) t)->
(t=y0)\/(term_in_pol p t).
Intros.
Elim (eq_tm_dec t y0); Intros.
Left ; Trivial.
Right.
Red.
Unfold not; Intros.
Elim H.
Simpl.
Elim (eq_tm_dec t y0); Trivial; Intros.
Elim b; Auto.
Save.
Hints Resolve split_term_in_pol_cons.
Lemma term_in_sum: (f,g:pol)(t:term)(term_in_pol (suma_app f g) t)->
(term_in_pol f t)\/(term_in_pol g t).
Intros.
Red in H.
Unfold term_in_pol.
Cut (eqQ (coef (suma_app f g) t) (plusQ (coef f t) (coef g t))); Intros; Auto.
Elim (decQ (coef f t)); Intros; Auto.
Right.
Apply comp_nOQ with (coef (suma_app f g) t); Auto.
Apply eqQ_trans with (plusQ (coef f t) (coef g t)); Auto.
Apply eqQ_trans with (plusQ OQ (coef g t)); Auto.
Apply eqQ_trans with (plusQ (coef g t) OQ); Auto.
Save.
Lemma Ttm_no_term_in_pol: (t:term)(f:pol)(full n t)->
((t':term)(term_in_pol f t')->(Ttm t t'))->
(no_term_in_pol f t).
Intros.
(Elim (dec_term_in_pol f t); Trivial; Intros).
(Cut (Ttm t t)->~t=t; Intros).
(Elim H1; Auto).
(Apply Ttm_strict with n; Trivial).
Save.
Hints Resolve Ttm_no_term_in_pol.
Lemma term_in_pol_monom: (k:Q)(t:term)(~(eqQ k OQ))->
(term_in_pol (cpol (k,t) vpol) t).
Intros.
Unfold term_in_pol.
Simpl.
Elim (eq_tm_dec t t).
Intros.
(Apply comp_nOQ with c:=k; Auto).
Intros.
(Elim b; Auto).
Save.
Hints Resolve term_in_pol_monom.
Lemma Ttm_no_term_in_pol2: (t:term)(f:pol)(full n t)->
((t':term)(term_in_pol f t')->(Ttm t' t))->(no_term_in_pol f t).
Intros.
Elim (dec_term_in_pol f t); Trivial; Intros.
Cut (Ttm t t); Intros; Auto.
Cut ~t=t; Intros.
Elim H2; Auto.
Apply Ttm_strict with n; Trivial.
Save.
Hints Resolve Ttm_no_term_in_pol2.
Lemma full_coef: (f:pol)(t0:term)(full_term_pol f)->
(term_in_pol f t0)->(full n t0).
Unfold term_in_pol.
Induction 1; Intros.
Elim H0; Auto.
Elim (eq_tm_dec t0 t); Intros.
Rewrite a0; Trivial.
Apply H2.
Cut (eqQ (coef (cpol (a,t) p) t0) (coef p t0)); Intros.
Apply comp_nOQ with c:=(coef (cpol (a,t) p) t0); Auto.
Apply coef_n_term; Trivial.
Save.
Hints Resolve full_coef.
Lemma dec_sum_term_in_pol: (f,g:pol)(t:term)(term_in_pol f t)->
(no_term_in_pol g t)->(term_in_pol (suma_app f g) t).
Intros.
Red.
(Apply comp_nOQ with (plusQ (coef g t) (coef f t)); Auto).
Red in H.
Red in H0.
Apply eqQ_sym.
(Apply eqQ_trans with (plusQ (coef f t) (coef g t)); Auto).
Save.
Lemma coef_Ttm_split_pol: (f,f1,f2:pol)(t:term)(full n t)->
(full_term_pol f)->(full_term_pol f1)->(full_term_pol f2)->
(equpol f (suma_app f1 (suma_app (cpol ((coef f t),t) vpol) f2)))->
(t0:term)(full n t0)->(Ttm t0 t)->((t':term)(term_in_pol f1 t')->(Ttm t t'))->
(eqQ (coef f2 t0) (coef f t0)).
Intros.
Cut (equpol f (suma_app (suma_app f1 (cpol ((coef f t),t) vpol)) f2)); Intros.
Apply eqQ_trans
with (coef (suma_app (suma_app f1 (cpol ((coef f t),t) vpol)) f2) t0).
Apply eqQ_trans with
(plusQ (coef (suma_app f1 (cpol ((coef f t),t) vpol)) t0) (coef f2 t0)); Auto.
Apply eqQ_trans with (plusQ OQ (coef f2 t0)).
Apply eqQ_trans with (plusQ (coef f2 t0) OQ); Auto.
Apply plusQ_comp; Trivial.
Apply eqQ_sym.
Apply eqQ_trans with (plusQ (coef f1 t0) (coef (cpol ((coef f t),t) vpol) t0)).
Auto.
Apply plusQ_zero.
Change (no_term_in_pol f1 t0).
Apply Ttm_no_term_in_pol; Trivial; Intros.
Apply Ttm_trans with t n; Auto.
Apply full_coef with f1; Trivial.
Cut ~t=t0; Intros.
Apply eqQ_trans with (coef vpol t0); Auto.
Red; Intros.
Cut t0=t; Auto.
Change ~t0=t.
Apply Ttm_strict with n; Trivial.
Auto.
Apply equpol_tran with (suma_app f1 (suma_app (cpol ((coef f t),t) vpol) f2)); Auto.
Save.
Hints Resolve coef_Ttm_split_pol.
Lemma split_term_in_pol: (f1,f2:pol)(full_term_pol f1)->(full_term_pol f2)->
(k:Q)(t,t0:term)(full n t)->(full n t0)->
(term_in_pol (suma_app f1 (suma_app (cpol (k,t) vpol) f2)) t0)->
(Ttm t0 t)->((t':term)(term_in_pol f1 t')->(Ttm t t'))->(term_in_pol f2 t0).
Intros.
Cut (term_in_pol (suma_app (suma_app f1 (cpol (k,t) vpol)) f2) t0); Intros.
Cut (no_term_in_pol (suma_app f1 (cpol (k,t) vpol)) t0); Intros.
Red in H6 H7.
Red.
Apply comp_nOQ with (coef (suma_app (suma_app f1 (cpol (k,t) vpol)) f2) t0); Trivial.
Apply eqQ_trans with
(plusQ (coef (suma_app f1 (cpol (k,t) vpol)) t0) (coef f2 t0)); Auto.
Apply eqQ_trans with (plusQ OQ (coef f2 t0)); Auto.
Apply eqQ_trans with (plusQ (coef f2 t0) OQ); Auto.
Red.
Apply eqQ_trans with (plusQ (coef f1 t0) (coef (cpol (k,t) vpol) t0)); Trivial.
Apply plusQ_zero.
Change (no_term_in_pol f1 t0).
Apply Ttm_no_term_in_pol; Intros; Trivial.
Apply Ttm_trans with t n; Auto.
Apply full_coef with f1; Trivial.
Cut ~t=t0; Intros.
Apply eqQ_trans with (coef vpol t0); Auto.
Red; Intros.
Cut t0=t; Auto.
Change ~t0=t.
Apply Ttm_strict with n; Trivial.
Apply comp_term_in_pol with (suma_app f1 (suma_app (cpol (k,t) vpol) f2)); Auto.
Save.
Hints Resolve split_term_in_pol.
Lemma gen_split_pol: (f:pol)(full_term_pol f)->(t:term)(full n t)->
(EX f1 | (full_term_pol f1) /\ ((t':term)(term_in_pol f1 t')->(Ttm t t'))
& (EX f2 | (full_term_pol f2) /\ ((t':term)(term_in_pol f2 t')->(Ttm t' t))
& (equpol f (suma_app f1 (suma_app (cpol ((coef f t),t) vpol) f2))))).
Induction f.
Intros.
Split with vpol.
Split; Trivial.
Intros t' e; Elim e; Auto.
Split with vpol.
Split; Trivial.
Intros t' e; Elim e; Auto.
Simpl; Apply equpol_sym.
Apply equpol_elim; Auto.
Induction m; Intros.
Inversion H0.
Elim H with t; Trivial; Intros.
Elim H7; Intros.
Elim H8; Intros.
Elim H11; Intros.
Clear H11 H8 H7 H.
Elim (Ttm_total b t n); Trivial; Intros.
Elim a1; Intros; Clear a1.
Split with x.
Split; Trivial.
Split with (cpol (a,b) x0).
Split; Auto; Intros.
Cut t'=b\/(term_in_pol x0 t'); Intros.
Elim H7; Intros; Clear H7.
Rewrite H8; Trivial.
Apply H14; Trivial.
Apply split_term_in_pol_cons with a; Trivial.
Apply equpol_tran with (cpol (a,b)
(suma_app x (suma_app (cpol ((coef p t),t) vpol) x0))); Auto.
Apply equpol_tran with (suma_app x
(cpol (a,b) (suma_app (cpol ((coef p t),t) vpol) x0))).
Auto.
Apply equpol_ss; Trivial.
Apply equpol_tran with (cpol ((coef (cpol (a,b) p) t),t)
(cpol (a,b) (suma_app vpol x0))); Auto.
Apply equpol_tran with (suma_app (cpol ((coef p t),t) vpol) (cpol (a,b) x0)); Auto.
Apply equpol_tran with (cpol ((coef p t),t) (cpol (a,b) (suma_app vpol x0))).
Auto.
Apply eq_mon_cpol.
Simpl.
Right.
Split; Trivial.
Elim (eq_tm_dec t b); Auto; Intros.
Cut ~b=t; Intros.
Elim H; Auto.
Apply Ttm_strict with n; Trivial.
Split with (cpol (a,b) x).
Split; Auto; Intros.
Cut t'=b\/(term_in_pol x t'); Intros.
Elim H7; Intros; Clear H7.
Rewrite H8; Trivial.
Apply H10; Trivial.
Apply split_term_in_pol_cons with a; Trivial.
Split with x0.
Split; Trivial.
Apply equpol_tran with (cpol (a,b)
(suma_app x (suma_app (cpol ((coef p t),t) vpol) x0))); Auto.
Simpl.
Apply equpol_cpol2; Trivial.
Apply equpol_ss; Trivial.
Apply eq_mon_cpol.
Simpl.
Right.
Split; Trivial.
Elim (eq_tm_dec t b); Auto; Intros.
Cut ~t=b; Intros.
Elim H; Auto.
Apply Ttm_strict with n; Trivial.
Split with x.
Split; Auto.
Split with x0.
Split; Auto.
Apply equpol_tran with (cpol (a,b)
(suma_app x (suma_app (cpol ((coef p t),t) vpol) x0))); Auto.
Rewrite b0.
Apply equpol_tran with
(suma_app x (cpol (a,t) (suma_app (cpol ((coef p t),t) vpol) x0))).
Auto.
Apply equpol_ss; Trivial.
Apply equpol_tran with (suma_app (cpol ((coef p t),t) vpol) (cpol (a,t) x0)).
Auto.
Simpl.
Elim (eq_tm_dec t t); Intros.
Apply equpol_tran with (cpol ((plusQ (coef p t) a),t) x0); Auto.
Elim b1; Auto.
Save.
Hints Resolve gen_split_pol.
Lemma split_pol: (f:pol)(full_term_pol f)->(t:term)(term_in_pol f t)->
(EX f1 | (full_term_pol f1)/\((t':term)(term_in_pol f1 t')->(Ttm t t'))
& (EX f2 | (full_term_pol f2)/\((t':term)(term_in_pol f2 t')->(Ttm t' t))
& (equpol f (suma_app f1 (suma_app (cpol ((coef f t),t) vpol) f2))))).
Intros.
Cut (full n t); Intros.
Apply gen_split_pol; Trivial.
Apply full_coef with f; Trivial.
Save.
Hints Resolve split_pol.
Index
This page has been generated by coqdoc