Library Hmtc
Require Export pol_can.
Definition hmonom: pol->monom :=
[p:pol]
Cases (fun_can p) of
vpol => (OQ,(n_term_O n))
| (cpol m q) => m
end.
Definition hterm := [p:pol](mon_term (hmonom p)).
Hints Unfold hterm.
Definition hcoef := [p:pol](mon_coef (hmonom p)).
Hints Unfold hcoef.
Lemma hmct_Leib: (f:pol) (hmonom f) = ((hcoef f),(hterm f)).
Intros; Unfold hcoef; Unfold hterm; Elim (hmonom f); Trivial.
Save.
Hints Resolve hmct_Leib.
Lemma coef_hterm: (f:pol)(full_term_pol f)->
(eqQ (hcoef f) (coef f (hterm f))).
Intros f ff.
Unfold hcoef.
Unfold hterm.
Unfold hmonom.
Unfold fun_can.
Elim (full_pol_tm_dec f).
Intros ff1.
Simpl.
Elim (can_fun f ff1).
Simpl.
Intros q hq.
Apply eqQ_trans
with (coef q
(mon_term
Cases q of
vpol => (OQ,(n_term_O n))
| (cpol m _) => m
end)).
(Elim hq; Intros fq eq; Generalize fq).
Elim q.
Simpl.
Trivial.
Simpl.
(Induction m; Intros c t q' hrq fq'; Simpl).
(Elim (eq_tm_dec t t); Intros ee).
(Apply eqQ_trans with (plusQ c OQ); Auto).
Cut (eqQ OQ (coef q' t)).
Auto.
(Inversion fq'; Auto).
(Elim ee; Auto).
(Elim hq; Auto).
(Intros fff; Elim (fff ff)).
Save.
Hints Resolve coef_hterm.
Lemma occ_n_vpol:(f:pol)(~(equpol f vpol))->
(full_term_pol f)->
(term_in_pol f (hterm f)).
Intros f nef ff.
Unfold term_in_pol.
Unfold hterm.
Unfold hmonom.
Unfold fun_can.
Elim (full_pol_tm_dec f).
Intros ff1; Simpl.
Elim (can_fun f ff1).
Intros q; Elim q; Simpl.
Destruct 1; Intros h1 h2; Elim (nef h2).
Induction m; Intros c t q' hr; Destruct 1; Intros fp ep.
Inversion fp.
Simpl.
Unfold not; Intros eft.
Apply H2.
Apply eqQ_trans with (coef f t); Try Assumption.
Apply eqQ_trans with (coef (cpol (c,t) q') t).
Simpl.
Simpl.
Elim (eq_tm_dec t t).
Intros eee.
Apply eqQ_trans with (plusQ c OQ).
Auto.
Cut (eqQ OQ (coef q' t)); Auto.
Intros xxx; Elim xxx; Auto.
Auto.
(Intros xxx; Elim (xxx ff)).
Save.
Hints Resolve occ_n_vpol.
Lemma full_hterm_full_pol: (f:pol)(full_term_pol f)->
(full n (hterm f)).
Induction f.
Unfold hterm.
Unfold hmonom.
Cut (full_pol (fun_can vpol)).
Elim (fun_can vpol).
Intros.
(Simpl; Auto).
Intros.
(Inversion H0; Auto).
(Apply can_is_full; Auto).
Induction m.
Intros y t p hr ff.
Unfold hterm.
Unfold hmonom.
Cut (full_pol (fun_can (cpol (y,t) p))).
Elim (fun_can (cpol (y,t) p)).
Intros.
(Simpl; Auto).
Intros.
(Inversion H0; Auto).
(Apply can_is_full; Auto).
Save.
Hints Resolve full_hterm_full_pol.
Lemma cond_ht_pol: (p:pol)(full_term_pol p)->
(~(equpol p vpol))->
(~(eqQ (hcoef p) OQ)).
(Intros p fp nef; Unfold not; Intros nezf).
Cut (eqQ (coef p (hterm p)) OQ).
Change (term_in_pol p (hterm p)).
Auto.
(Apply eqQ_trans with (hcoef p); Auto).
Save.
Hints Resolve cond_ht_pol.
Inductive equm : monom -> monom -> Prop :=
equmoni : (c,c':Q)(t:term)(full n t)->
(eqQ c c')->
(equm (c,t)(c',t)).
Hints Resolve equmoni.
Lemma equm_refl: (m:monom)(full_mon n m)->(equm m m).
Induction m; Intros; Simpl; Auto.
Save.
Hints Resolve equm_refl.
Lemma equm_sym : (m,n:monom)
(equm m n)->(equm n m).
Induction m; Induction n; Intros a0 b0 e; Inversion e; Auto.
Save.
Hints Resolve equm_sym.
Lemma equm_trans : (m,n,o:monom)
(equm m n)->(equm n o)->(equm m o).
(Induction m; Induction n; Induction o; Intros a1 b1 e1 e2; Inversion e1;
Inversion e2).
Apply equmoni; Trivial.
Apply eqQ_trans with a0; Trivial.
Save.
Hints Resolve equm_trans.
Definition fst_term :=
[p:pol]Cases p of
vpol => (OQ,(n_term_O n))
| (cpol m _) => m
end.
Lemma eq_homnom_fst : (p:pol)
(hmonom p)=(fst_term (fun_can p)).
Reflexivity.
Save.
Lemma fst_equm : (p,q:pol)(same_pol p q)->
(equm (fst_term p)(fst_term q)).
(Induction 1; Simpl; Auto).
Save.
Hints Resolve fst_equm.
Lemma equm_full_hmonom: (c:Q)(t:term)(q:pol)(full_pol (cpol (c,t) q))->
(equm (hmonom (cpol (c,t) q)) (c,t)).
Intros.
Replace hmonom with [x:pol](fst_term (fun_can x)); Auto.
Inversion H.
Apply equm_trans with (fst_term (cpol (c,t) q)); Auto.
Apply fst_equm; Auto.
Save.
Hints Resolve equm_full_hmonom.
Lemma full_hterm: (c:Q)(t:term)(q:pol)(full_pol (cpol (c,t) q))->
(hterm (cpol (c,t) q))=t.
Intros.
Inversion H.
Cut (equm (hmonom (cpol (c,t) q)) (c,t)); Auto; Intro e.
Replace hterm with [x:pol](mon_term (hmonom x)); Auto.
Inversion e; Auto.
Save.
Hints Resolve full_hterm.
Lemma full_hcoef: (c:Q)(t:term)(q:pol)(full_pol (cpol (c,t) q))->
(eqQ (hcoef (cpol (c,t) q)) c).
Intros.
Inversion H.
Cut (equm (hmonom (cpol (c,t) q)) (c,t)); Auto; Intro e.
Replace hcoef with [x:pol](mon_coef (hmonom x)); Auto.
Inversion e; Auto.
Save.
Hints Resolve full_hcoef.
Lemma equpol_can : (p,q:pol)(equpol p q)->
(full_term_pol p)->
(full_term_pol q)-> (equm (hmonom p)(hmonom q)).
Intros p q e fp fq.
Rewrite (eq_homnom_fst p).
Rewrite (eq_homnom_fst q).
(Apply fst_equm; Auto).
Save.
Hints Resolve equpol_can.
Lemma eq_hterm: (h,h':pol)(full_term_pol h)->(full_term_pol h')->
(equpol h h')->(hterm h)=(hterm h').
Intros.
Cut (equm (hmonom h) (hmonom h')).
Replace hterm with [x:pol](mon_term (hmonom x)).
Intros e; Inversion e.
Auto.
Auto.
Auto.
Save.
Hints Resolve eq_hterm.
Lemma eq_hcoef: (h,h':pol)(full_term_pol h)->
(full_term_pol h')->(equpol h h')->
(eqQ (hcoef h) (hcoef h')).
Intros.
(Apply eqQ_trans with (coef h (hterm h)); Auto).
(Apply eqQ_trans with (coef h' (hterm h')); Auto).
(Cut (hterm h)=(hterm h'); Intros).
(Rewrite H2; Auto).
Auto.
Save.
Hints Resolve eq_hcoef.
Lemma eq_term_div: (p,q:pol)(t:term)(full_term_pol p)->(full_term_pol q)->
(equpol p q)->
(term_div (hterm p) t)->(term_div (hterm q) t).
(Intros p q t fp fq d; Replace (hterm q) with (hterm p); Auto).
Save.
Hints Resolve eq_term_div.
Lemma term_monom_hterm: (k:Q)(t:term)(full n t)->(~(eqQ k OQ))->
(hterm (cpol (k,t) vpol))=t.
Intros.
Apply full_hterm; Auto.
Save.
Hints Resolve term_monom_hterm.
Lemma eq_coef_monom: (k:Q)(t:term)(full n t)->(eqQ k (hcoef (cpol (k,t) vpol))).
Intros.
Elim (decQ k); Intros; Auto.
Apply eqQ_trans with OQ; Auto.
Apply eqQ_trans with (coef (cpol (k,t) vpol) (hterm (cpol (k,t) vpol))); Auto.
Replace (hterm (cpol (k,t) vpol)) with (hterm vpol); Auto.
Simpl.
Elim (eq_tm_dec (hterm vpol) t); Auto.
Save.
Hints Resolve eq_coef_monom.
Lemma hcoef_vpol: (eqQ (hcoef vpol) OQ).
Apply eqQ_trans with (hcoef (cpol (OQ,(n_term_O n)) vpol)); Auto.
Save.
Lemma funcanvpol: (p:pol)((fun_can p) = vpol)->(hterm p)=(n_term_O n).
Intros; Unfold hterm; Unfold hmonom.
Rewrite H.
Simpl; Auto.
Save.
Lemma hterm_vpol: (hterm vpol) = (n_term_O n).
Cut (fun_can vpol)=vpol; Intros.
Apply funcanvpol; Trivial.
Unfold fun_can.
Elim (full_pol_tm_dec vpol); Simpl; Intros; Auto.
Elim (can_fun vpol a); Simpl; Intros.
Elim p; Intros.
Clear p.
Apply full_eq_vpol; Auto.
Save.
Lemma contr_hterm_vpol: (p:pol)(full_term_pol p)->~((hterm p)= (n_term_O n))->
~(equpol p vpol).
Intros.
Unfold not; Intros.
Cut (hterm p)=(n_term_O n); Intros.
Elim H0; Auto.
Cut (hterm p)=(hterm vpol); Intros.
Transitivity (hterm vpol); Auto.
Apply hterm_vpol.
Apply eq_hterm; Trivial.
Save.
Lemma gr_ht_nvpol: (f,h:pol)(full_term_pol f)->(full_term_pol h)->
(Ttm (hterm h) (hterm f))->(~(equpol f vpol)).
Intros.
Elim (eq_tm_dec (hterm f) (n_term_O n)); Intros.
Rewrite a in H1.
Elim (eq_tm_dec (hterm h) (n_term_O n)); Intros.
Rewrite a0 in H1.
Cut ~(Ttm (n_term_O n) (n_term_O n)); Intros.
Elim H2; Auto.
Apply Ttm_nonrefl.
Cut (Ttm (n_term_O n) (hterm h)); Intros.
Cut ~((Ttm (hterm h) (n_term_O n))/\(Ttm (n_term_O n) (hterm h))); Intros.
Unfold not in H3.
Elim H3; Auto.
Apply Ttm_antisym with n; Auto.
Elim (Ttm_total (n_term_O n) (hterm h) n); Intros; Auto.
Apply contr_hterm_vpol; Auto.
Save.
Lemma full_Ttm_pol_hterm: (f:pol)(full_pol f)->(t:term)(term_in_pol f t)->
~t=(hterm f)->(Ttm t (hterm f)).
Induction f.
Intros.
Elim H0; Auto.
Induction m; Intros.
Cut (hterm (cpol (a,b) p))=b; Intros; Auto.
Rewrite H3.
Rewrite H3 in H2.
Inversion H0.
Cut (term_in_pol p t); Intros.
Apply term_in_Ttm_pol with p; Trivial.
Cut t=b\/(term_in_pol p t); Intros.
Elim H11; Intros; Trivial.
Elim H2; Auto.
Apply split_term_in_pol_cons with a; Auto.
Save.
Lemma Ttm_pol_hterm: (f:pol)(full_term_pol f)->(t:term)(term_in_pol f t)->
(~(t=(hterm f)))->(Ttm t (hterm f)).
Intros.
Elim (can_fun f); Intros; Auto.
Elim p; Intros; Clear p.
Replace (hterm f) with (hterm x); Auto.
Apply full_Ttm_pol_hterm; Trivial.
Apply comp_term_in_pol with f; Auto.
Replace (hterm x) with (hterm f); Auto.
Save.
Hints Resolve Ttm_pol_hterm.
Lemma Ttm_hterm: (f:pol)(full_term_pol f)->(t:term)(full n t)->(Ttm (hterm f) t)->
(no_term_in_pol f t).
Intros.
Elim (dec_term_in_pol f t); Trivial; Intros.
Cut ~(equpol f vpol); Intros.
Cut (Ttm t (hterm f)); Intros.
Cut ~((Ttm (hterm f) t)/\(Ttm t (hterm f))); Intros.
Elim H4; Auto.
Apply Ttm_antisym with n; Auto.
Apply Ttm_pol_hterm; Trivial.
Red; Intro.
Cut (hterm f)=t.
Change ~(hterm f)=t.
Apply Ttm_strict with n; Auto.
Auto.
Apply term_in_pol_nvpol with t; Trivial.
Save.
Hints Resolve Ttm_hterm.
Lemma aux1_hterm_suma_Ttm: (f:pol)(full_term_pol f)->
(t:term)(term_in_pol f t)->
((t':term)(term_in_pol f t')->(~t=t')->(Ttm t' t))->
(t=(hterm f)).
Intros.
(Elim (eq_tm_dec t (hterm f)); Intros; Trivial).
(Cut (Ttm t (hterm f)); Intros).
(Cut (Ttm (hterm f) t); Intros).
(Cut ~((Ttm t (hterm f))/\(Ttm (hterm f) t)); Intros).
(Elim H4; Auto).
Apply Ttm_antisym with n.
(Apply full_coef with f; Auto).
Auto.
Apply H1.
(Apply occ_n_vpol; Auto).
(Apply term_in_pol_nvpol with t; Auto).
Trivial.
(Apply Ttm_pol_hterm; Auto).
Save.
Lemma hterm_pol_opp: (f:pol)(full_pol f)->((hterm f)=(hterm (pol_opp f))).
Induction f.
Intros; Auto.
Induction m; Intros.
Simpl.
Transitivity b; Auto.
Symmetry.
Inversion H0; Apply full_hterm; Auto.
Save.
Hints Resolve hterm_pol_opp.
Lemma hterm_pol_opp_term: (f:pol)(full_term_pol f)->((hterm f)=(hterm (pol_opp f))).
Intros.
Elim (can_fun f); Trivial; Intros.
Elim p; Intros; Clear p.
Replace (hterm f) with (hterm x); Auto.
Replace (hterm (pol_opp f)) with (hterm (pol_opp x)).
Apply hterm_pol_opp; Trivial.
Auto.
Save.
Hints Resolve hterm_pol_opp_term.
Lemma hcoef_pol_opp:(f:pol)(full_pol f)->(eqQ (hcoef f) (multQ_neg (hcoef (pol_opp f)))).
Induction f.
Intros.
Apply eqQ_trans with OQ.
Apply hcoef_vpol.
Apply eqQ_trans with (multQ_neg (hcoef vpol)).
Apply eqQ_trans with (multQ_neg OQ).
Auto.
Apply eq_mulQ_neg.
Apply hcoef_vpol.
Apply eq_mulQ_neg; Auto.
Induction m; Intros.
Apply eqQ_trans with a.
Apply full_hcoef; Trivial.
Apply eqQ_trans with
(multQ_neg (coef (pol_opp (cpol (a,b) p)) (hterm (pol_opp (cpol (a,b) p))))).
Apply eqQ_trans with (coef (cpol (a,b) p) (hterm (pol_opp (cpol (a,b) p)))); Auto.
Replace (hterm (pol_opp (cpol (a,b) p))) with (hterm (cpol (a,b) p)); Auto.
Replace (hterm (cpol (a,b) p)) with b.
Simpl.
Elim (eq_tm_dec b b); Intros.
Inversion H0.
Apply eqQ_trans with (plusQ a OQ); Auto.
Elim b0; Auto.
Symmetry; Apply full_hterm; Trivial.
Apply eq_mulQ_neg; Auto.
Save.
Hints Resolve hcoef_pol_opp.
Lemma hcoef_pol_opp_term: (f:pol)(full_term_pol f)->(eqQ (hcoef f) (multQ_neg (hcoef (pol_opp f)))).
Intros.
Apply eqQ_trans with (coef f (hterm f)); Auto.
Apply eqQ_trans with (multQ_neg (coef (pol_opp f) (hterm (pol_opp f)))).
Apply eqQ_trans with (coef f (hterm (pol_opp f))); Auto.
Apply eq_mulQ_neg; Auto.
Save.
Lemma eq_pol_opp_hcoef: (f,g:pol)(full_term_pol f)->(full_term_pol g)->
(eqQ (hcoef f) (hcoef g))->(eqQ (hcoef (pol_opp f)) (hcoef (pol_opp g))).
Intros.
Apply eqQ_trans with (multQ_neg (hcoef (pol_opp (pol_opp f)))).
Apply hcoef_pol_opp_term; Auto.
Apply eqQ_trans with (multQ_neg (hcoef (pol_opp (pol_opp g)))).
Apply eq_mulQ_neg.
Apply eqQ_trans with (hcoef g).
Auto.
Apply eqQ_trans with (hcoef f); Auto.
Apply eqQ_sym.
Apply hcoef_pol_opp_term; Auto.
Save.
Lemma eq_pol_opp_hterm: (f,g:pol)(full_term_pol f)->(full_term_pol g)->
(hterm f)=(hterm g)->(hterm (pol_opp f))=(hterm (pol_opp g)).
Intros.
Transitivity (hterm f).
Symmetry; Auto.
Transitivity (hterm g); Auto.
Save.
Lemma aux_hterm_suma_Ttm: (f,h:pol)(full_term_pol f)->(full_term_pol h)->
(Ttm (hterm h) (hterm f))->(term_in_pol (suma_app f h) (hterm f)).
Intros.
Red.
Cut ~(equpol f vpol); Intros.
Apply comp_nOQ with (plusQ (coef h (hterm f)) (coef f (hterm f))).
Apply eqQ_trans with (plusQ (coef f (hterm f)) (coef h (hterm f)));Auto.
Apply plusQ_zero_nzero.
Change (no_term_in_pol h (hterm f)) ; Auto.
Apply comp_nOQ with (hcoef f); Auto.
Apply gr_ht_nvpol with h; Auto.
Save.
Lemma hterm_suma_Ttm: (f,h:pol)(full_term_pol f)->(full_term_pol h)->(Ttm (hterm h) (hterm f))->
(hterm (suma_app f h))=(hterm f).
Intros.
Cut ~(equpol f vpol); Intros.
Cut (term_in_pol (suma_app f h) (hterm f)); Intros.
Symmetry.
Apply aux1_hterm_suma_Ttm; Auto; Intros.
Cut (term_in_pol f t')\/(term_in_pol h t'); Intros.
Elim H6; Intros; Clear H6; Auto.
Cut t'=(hterm h)\/(Ttm t' (hterm h)); Intros.
Elim H6; Intros; Clear H6.
Rewrite <- H8 in H1; Auto.
Apply Ttm_trans with (hterm h) n; Auto.
Apply full_coef with h; Auto.
Elim (eq_tm_dec t' (hterm h)); Intros; Auto.
Apply term_in_sum; Auto.
Apply aux_hterm_suma_Ttm; Auto.
Apply gr_ht_nvpol with h; Auto.
Save.
Lemma hcoef_suma_Ttm: (f,h:pol)(full_term_pol f)->(full_term_pol h)->
(Ttm (hterm h) (hterm f))->(eqQ (hcoef (suma_app f h)) (hcoef f)).
Intros.
Cut ~(equpol f vpol); Intros.
Apply eqQ_trans with (coef (suma_app f h) (hterm (suma_app f h))); Auto.
Apply eqQ_trans with (coef f (hterm f)); Auto.
Replace (hterm (suma_app f h)) with (hterm f).
Apply eqQ_trans with (plusQ (coef f (hterm f)) (coef h (hterm f))); Auto.
Apply eqQ_trans with (plusQ (coef f (hterm f)) OQ); Auto.
Apply plusQ_comp; Trivial.
Change (no_term_in_pol h (hterm f)); Auto.
Symmetry; Apply hterm_suma_Ttm; Auto.
Apply gr_ht_nvpol with h; Auto.
Save.
Lemma term_in_Ttm_hterm: (f,h:pol)(full_term_pol f)->
(full_term_pol h)->(t:term)(term_in_pol f t)->
((t1:term)(term_in_pol h t1)->(Ttm (hterm f) t1))->
(term_in_pol (suma_app f h) t).
Intros.
Cut ~(equpol f vpol); Intros.
Red in H1.
Red.
(Apply comp_nOQ with (plusQ (coef f t) (coef h t)); Auto).
(Apply comp_nOQ with (plusQ (coef h t) (coef f t)); Auto).
(Apply plusQ_zero_nzero; Trivial).
Elim (eq_tm_dec t (hterm f)); Intros.
Rewrite <- a in H2.
Change (no_term_in_pol h t).
Elim (dec_term_in_pol h t); Trivial.
Intros.
(Cut (Ttm t t); Intros).
(Cut ~t=t; Intros).
Elim H5; Auto.
(Apply Ttm_strict with n; Trivial).
Apply full_coef with h; Trivial.
Apply full_coef with h; Trivial.
Auto.
Cut (t1:term)(term_in_pol h t1)->(Ttm t t1); Intros.
Change (no_term_in_pol h t).
Elim (dec_term_in_pol h t); Trivial.
Intros.
(Cut (Ttm t t); Intros).
(Cut ~t=t; Intros).
Elim H6; Auto.
(Apply Ttm_strict with n; Trivial).
Apply full_coef with h; Trivial.
Apply full_coef with h; Trivial.
Auto.
Apply Ttm_trans with (hterm f) n.
Auto.
(Apply full_coef with f; Trivial).
Auto.
Apply full_coef with h; Trivial.
Auto.
Apply term_in_pol_nvpol with t; Trivial.
Save.
Lemma coef_suma_Ttm: (f,h:pol)(full_term_pol f)->
(full_term_pol h)->(t:term)(term_in_pol f t)->
((t1:term)(term_in_pol h t1)->(Ttm (hterm f) t1))->
(eqQ (coef f t) (coef (suma_app f h) t)).
Intros.
Cut ~(equpol f vpol); Intros.
Apply eqQ_trans with (plusQ (coef f t) (coef h t)); Auto.
Apply eqQ_trans with (plusQ (coef f t) OQ); Auto.
Apply plusQ_comp; Trivial.
(Elim (eq_tm_dec t (hterm f)); Intros).
Rewrite <- a in H2.
Apply eqQ_sym.
Change (no_term_in_pol h t).
(Elim (dec_term_in_pol h t); Trivial).
Intros.
Cut (Ttm t t); Intros.
Cut ~t=t; Intros.
(Elim H5; Auto).
Apply Ttm_strict with n; Trivial.
(Apply full_coef with h; Trivial).
(Apply full_coef with h; Trivial).
Auto.
(Cut (t1:term)(term_in_pol h t1)->(Ttm t t1); Intros).
Apply eqQ_sym.
Change (no_term_in_pol h t).
(Elim (dec_term_in_pol h t); Trivial).
Intros.
Cut (Ttm t t); Intros.
Cut ~t=t; Intros.
(Elim H6; Auto).
Apply Ttm_strict with n; Trivial.
(Apply full_coef with h; Trivial).
(Apply full_coef with h; Trivial).
Auto.
Apply Ttm_trans with (hterm f) n.
Auto.
Apply full_coef with f; Trivial.
Auto.
(Apply full_coef with h; Trivial).
Auto.
Apply term_in_pol_nvpol with t; Trivial.
Save.
Hints Resolve coef_suma_Ttm.
Lemma aux1_hterm_eq_suma_Ttm: (f,g:pol)(full_term_pol f)->
(full_term_pol g)->((hterm f)=(hterm g))->
(t:term)(term_in_pol (suma_app f g) t)->
(~(t=(hterm f)))->(Ttm t (hterm f)).
Intros.
(Elim term_in_sum with f g t; Trivial).
Auto.
Rewrite H1; Intros.
Rewrite H1 in H3; Auto.
Save.
Lemma aux2_hterm_eq_suma_Ttm: (f,g:pol)(full_term_pol f)->
(full_term_pol g)->((hterm f)=(hterm g))->
((hterm f)=(hterm (suma_app f g)))->
(eqQ (hcoef (suma_app f g)) (plusQ (hcoef f) (hcoef g))).
Intros.
Apply eqQ_trans with (coef (suma_app f g) (hterm (suma_app f g))).
Auto.
Apply eqQ_trans with (plusQ (coef f (hterm f)) (coef g (hterm g))).
Rewrite <- H2.
(Rewrite <- H1; Auto).
Auto.
Save.
Lemma hterm_eq_suma_Ttm:(f,g:pol)(full_term_pol f)->
(full_term_pol g)->(~(equpol (suma_app f g) vpol))->
(eqQ (hcoef f) (multQ_neg (hcoef g)))->
((hterm f)=(hterm g))->
(Ttm (hterm (suma_app f g)) (hterm f)).
Intros.
(Elim (eq_tm_dec (hterm (suma_app f g)) (hterm f)); Intros).
(Cut (eqQ (hcoef (suma_app f g)) (plusQ (hcoef f) (hcoef g))); Intros).
(Cut (eqQ (hcoef (suma_app f g)) OQ); Intros).
(Cut ~(eqQ (hcoef (suma_app f g)) OQ); Intros).
(Elim H6; Auto).
(Apply cond_ht_pol; Auto).
(Apply eqQ_trans with (plusQ (hcoef f) (hcoef g)); Auto).
(Apply aux2_hterm_eq_suma_Ttm; Auto).
(Apply aux1_hterm_eq_suma_Ttm with g; Trivial).
(Apply occ_n_vpol; Auto).
Save.
Lemma hcoef_no_eq_hterm: (f,g:pol)(full_term_pol f)->(full_term_pol g)->
~(equpol f vpol)->~(equpol g vpol)->(hterm f)=(hterm g)->
~(eqQ (hcoef f) (multQ_neg (hcoef g)))->(hterm f)=(hterm (suma_app f g)).
Intros.
Cut (term_in_pol (suma_app f g) (hterm f)); Intros.
Apply aux1_hterm_suma_Ttm; Auto; Intros.
Cut (term_in_pol f t')\/(term_in_pol g t'); Intros.
Elim H8; Intros; Clear H8; Auto.
Rewrite H3.
Rewrite H3 in H7; Auto.
Apply term_in_sum; Trivial.
Red.
Apply comp_nOQ with (plusQ (coef f (hterm f)) (coef g (hterm f))); Auto.
Apply comp_nOQ with (plusQ (coef f (hterm f)) (coef g (hterm g))).
Auto.
Apply comp_nOQ with (plusQ (hcoef f) (hcoef g)); Auto.
Save.
Lemma Ttm_suma_hterm: (f,g:pol)(t:term)(full_term_pol f)->(full_term_pol g)->
(full n t)->~(equpol (suma_app f g) vpol)->(Ttm (hterm f) t)->(Ttm (hterm g) t)->
(Ttm (hterm (suma_app f g)) t).
Intros.
Elim (vpol_dec_full_term f); Trivial; Intros.
Replace (hterm (suma_app f g)) with (hterm g); Trivial.
Apply eq_hterm; Auto.
Apply equpol_tran with (suma_app vpol g); Auto.
Elim (vpol_dec_full_term g); Trivial; Intros.
Replace (hterm (suma_app f g)) with (hterm f); Trivial.
Apply eq_hterm; Auto.
Apply equpol_tran with (suma_app f vpol); Auto.
Elim (Ttm_total (hterm f) (hterm g) n); Auto.
Intros ax1; Elim ax1; Intros; Clear ax1.
Replace (hterm (suma_app f g)) with (hterm g); Trivial.
Symmetry.
Transitivity (hterm (suma_app g f)); Auto.
Apply hterm_suma_Ttm; Trivial.
Replace (hterm (suma_app f g)) with (hterm f); Trivial.
Symmetry.
Apply hterm_suma_Ttm; Trivial.
Intros.
Elim (decQ_t (hcoef f) (multQ_neg (hcoef g))); Intros.
Apply Ttm_trans with (hterm f) n; Auto.
Apply hterm_eq_suma_Ttm; Auto.
Replace (hterm (suma_app f g)) with (hterm f); Trivial.
Apply hcoef_no_eq_hterm; Trivial.
Save.
Lemma fst_mult : (p:pol)
(full_term_pol p)->
~(equpol p vpol)->(m:monom)
(full_mon n m)->~(z_monom m)->
(equm (fst_term (mult_m p m))(mult_mon m (fst_term p))).
Induction p.
Intros fp xx; Elim xx; Auto.
Induction m; Intros c t fq hr fp nzp; Inversion fp;
Induction m0; Intros d u; Simpl; Auto.
Save.
Hints Resolve fst_mult.
Lemma hmonom_mult :
(p:pol)(full_term_pol p)->
~(equpol p vpol)->
(m:monom)(full_mon n m)->~(z_monom m)->
(equm (hmonom (mult_m p m))(mult_mon m (hmonom p))).
Intros p fp zp m fm zm.
Replace hmonom with [x:pol](fst_term (fun_can x)).
Apply equm_trans with (fst_term (mult_m (fun_can p) m)).
Auto.
(Apply fst_mult; Auto).
(Unfold not; Intros ee; Apply zp; Apply equpol_tran with (fun_can p);
Auto).
Trivial.
Save.
Hints Resolve hmonom_mult.
Lemma hcoef_mult: (f:pol)(full_term_pol f)->
(m:monom)(full_mon n m)->
(eqQ (hcoef (mult_m f m)) (multQ (hcoef f) (mon_coef m))).
Intros.
Elim (vpol_dec_full_term f); Trivial.
Intros.
Apply eqQ_trans with OQ.
Apply eqQ_trans with (hcoef (mult_m vpol m)).
Apply eq_hcoef; Auto.
Generalize H0.
Induction m; Intros; Apply full_mult_m; Trivial.
Apply eqQ_trans with (hcoef vpol); Auto.
Apply hcoef_vpol.
Apply eqQ_trans with (multQ (hcoef vpol) (mon_coef m)).
Apply eqQ_trans with (multQ OQ (mon_coef m)); Auto.
Apply multQ_comp_r.
Apply eqQ_sym; Apply hcoef_vpol.
Apply multQ_comp_r.
Apply eq_hcoef; Auto.
Elim (z_monom_dec m).
Generalize m H0.
Clear H0 m.
Induction m; Intros.
Simpl.
Unfold z_monom in a0.
Apply eqQ_trans with (multQ (hcoef f) OQ); Auto.
Apply eqQ_trans with (hcoef (mult_m f (OQ,b))).
Auto.
Apply eqQ_trans with OQ; Auto.
Apply eqQ_trans with (hcoef vpol).
Apply eq_hcoef; Auto.
Apply hcoef_vpol.
Intros.
Cut (equm (hmonom (mult_m f m)) (mult_mon (hmonom f) m)); Intros.
Replace hcoef with [x:pol](mon_coef (hmonom x)); Auto.
Inversion H1.
Replace (multQ (mon_coef (hmonom f)) (mon_coef m)) with (mon_coef (c',t)); Auto.
Rewrite H3.
Elim (hmonom f); Elim m; Simpl; Auto.
Apply equm_trans with (mult_mon m (hmonom f)); Auto.
Generalize H0; Cut (full_mon n (hmonom f)).
Elim m; Elim (hmonom f); Simpl; Intros.
Replace (term_mult b2 b1) with (term_mult b1 b2); Auto.
Replace (hmonom f) with ((hcoef f),(hterm f)); Auto.
Save.
Lemma hterm_mult_m:(f:pol)(full_term_pol f)->
(m:monom)(full_mon n m)->
(~(equpol f vpol))->(~(z_monom m))->
(hterm (mult_m f m))=(term_mult (hterm f) (mon_term m)).
(Intros f ff m fm zf zm;
Cut (equm (hmonom (mult_m f m)) (mult_mon (hmonom f) m))).
Replace hterm with [x:pol](mon_term (hmonom x)).
(Intros e; Inversion e).
Replace (term_mult (mon_term (hmonom f)) (mon_term m))
with (mon_term (c',t)).
(Simpl; Auto).
Rewrite H0.
(Elim m; Elim (hmonom f); Simpl; Auto).
Auto.
(Apply equm_trans with (mult_mon m (hmonom f)); Auto).
Generalize fm; Cut (full_mon n (hmonom f)).
Elim m; Elim (hmonom f); Simpl; Intros.
Replace (term_mult b0 b) with (term_mult b b0).
Apply equmoni; Auto.
Auto.
Replace (hmonom f) with ((hcoef f),(hterm f)).
Simpl; Auto.
Symmetry; Apply hmct_Leib.
Save.
Lemma hterm_pol_m_opp:
(f:pol)
(full_term_pol f)
->(m:monom)
(full_mon n m)
->~(equpol f vpol)
->~(z_monom m)
->(hterm (mult_m f m))
=(hterm (mult_m f (monom_op m))).
Intros f ff m fm zf zm.
Transitivity (term_mult (hterm f) (mon_term m)).
(Apply hterm_mult_m; Trivial).
(Replace (mon_term m) with (mon_term (monom_op m)); Auto).
(Symmetry; Apply hterm_mult_m; Trivial).
(Generalize fm; Elim m; Auto).
(Generalize zm; Elim m; Simpl; Intros; Auto).
Save.
Hints Resolve hterm_pol_m_opp.
Lemma term_div_hterm: (p:pol)(full_term_pol p)->
(m:monom) ~(z_monom m)->
(full_mon n m)->
~(equpol p vpol)->
(term_div (hterm p) (hterm (mult_m p m))).
Intros p fp m zm fm zp.
Replace (hterm (mult_m p m)) with (term_mult (hterm p) (mon_term m)).
Auto.
Symmetry.
(Apply hterm_mult_m; Auto).
Save.
Hints Resolve term_div_hterm.
Lemma div_term_hterm: (f:pol)(full_term_pol f)->
~(equpol f vpol)->(y:Q)(y0:term)(full n y0)->
~(z_monom (y,y0))->y0=
(div_term (hterm (mult_m f (y,y0))) (hterm f)).
Intros.
(Replace (hterm (mult_m f (y,y0))) with (term_mult (hterm f) y0); Auto).
Symmetry.
(Apply div_mult_mon_inv with n; Auto).
Symmetry.
(Transitivity (term_mult (hterm f) (mon_term (y,y0))); Auto).
(Apply hterm_mult_m; Auto).
Save.
Hints Resolve div_term_hterm.
Lemma hterm_mult_m2: (f:pol)(full_term_pol f)->
(~(equpol f vpol))->(k:Q)(~(eqQ k OQ))->
(t:term)(full n t)->(term_div (hterm f) t)->
(hterm (mult_m f (k,(div_term t (hterm f)))))=t.
Intros.
Transitivity (term_mult (hterm f) (mon_term (k,(div_term t (hterm f))))).
Apply hterm_mult_m; Auto.
Simpl.
Symmetry.
(Apply divis_im_divt with n; Auto).
Save.
Lemma hcoef_mult2: (f:pol)(full_term_pol f)->
(t:term)(full n t)->(k:Q) (eqQ (hcoef (mult_m f (k,(div_term t (hterm f)))))
(multQ (hcoef f) (mon_coef (k,(div_term t (hterm f)))))).
Intros.
Apply eqQ_trans with (multQ (hcoef f) (mon_coef (k,(div_term t (hterm f))))); Auto.
Apply hcoef_mult; Auto.
Save.
Lemma term_in_Ttm: (fj:pol)(t,t',t0:term)(a:Q)(~(eqQ a OQ))->
(full_term_pol fj)->(full n t)->(full n t')->(full n t0)->
(~(equpol fj vpol))->(Ttm t0 t)->(term_div (hterm fj) t0)->
(term_in_pol (mult_m fj
((divQ a (hcoef fj)),(div_term t0 (hterm fj)))) t')->
(Ttm t' t).
Intros.
Cut (hterm (mult_m fj ((divQ a (hcoef fj)),(div_term t0 (hterm fj)))))=t0; Intros.
Elim (eq_tm_dec t' (hterm
(mult_m fj ((divQ a (hcoef fj)),(div_term t0 (hterm fj)))))); Intros.
Rewrite a0.
Rewrite H8; Trivial.
Cut (Ttm t' (hterm
(mult_m fj ((divQ a (hcoef fj)),(div_term t0 (hterm fj)))))); Intros; Auto.
Apply Ttm_trans with t0 n; Trivial.
Rewrite <- H8; Trivial.
Apply hterm_mult_m2; Trivial.
Apply no_divQ_zero; Auto.
Save.
Hints Resolve term_in_Ttm.
Index
This page has been generated by coqdoc