Library pol_can
Require Export coeficiente_tes.
Inductive low_pol : term -> pol -> Prop :=
low_nil : (t:term)(low_pol t vpol)
| low_cons : (t:term)(u:term)(x:Q)(p:pol)(Ttm u t)->
(low_pol t (cpol (x,u) p)).
Hints Resolve low_nil low_cons.
Lemma low_pol_cpol: (t,t':term)(c:Q)(p,p':pol)
(low_pol t (cpol (c,t') p))->(low_pol t (cpol (c,t') p')).
Intros.
Inversion H;Auto.
Save.
Hints Resolve low_pol_cpol.
Lemma low_trans : (t,u:term)
(full n t)->(full n u)->
(p:pol)
(full_term_pol p)->
(low_pol t p)->(Ttm t u)->(low_pol u p).
Induction p; Auto.
Induction m; Intros.
Inversion H3; Apply low_cons.
Inversion H2; Apply Ttm_trans with t n; Auto.
Save.
Hints Resolve low_trans.
Lemma low_opp: (t:term)(p:pol)(low_pol t p)->(low_pol t (pol_opp p)).
Induction p; Auto; Intros; Simpl.
Generalize H0.
Elim m; Intros.
Inversion H1; Auto.
Save.
Hints Resolve low_opp.
Lemma aux_suma_app_full: (t:term)(p,q:pol)(low_pol t (suma_app p q))->
(low_pol t p).
Induction p; Auto.
Induction m; Intros.
Simpl in H0.
Inversion H0.
Apply low_cons; Trivial.
Save.
Inductive full_pol : pol -> Prop :=
full_pol_nil: (full_pol vpol)
| full_pol_cons : (t:term)(a:Q)(P:pol) (~(eqQ a OQ))->(full n t)->
(full_pol P)->(low_pol t P)->(full_pol (cpol (a,t) P)).
Hints Resolve full_pol_nil full_pol_cons.
Lemma fullp_impl_fullt:(p:pol)(full_pol p)->
(full_term_pol p).
Induction p; Auto.
Induction m; Intros.
Inversion H0; Auto.
Save.
Hints Resolve fullp_impl_fullt.
Lemma full_monom: (m:monom)(~(z_monom m))->(full_mon n m)->
(full_pol (cpol m vpol)).
Induction m; Intros a c hz hf; Apply full_pol_cons; Auto.
Save.
Hints Resolve full_monom.
Lemma full_pol_mon: (m:monom)(p:pol)(full_pol (cpol m p))->(full_mon n m).
Induction m; Intros.
Inversion H; Auto.
Save.
Hints Resolve full_pol_mon.
Lemma full_opp: (p:pol)(full_pol p)->(full_pol (pol_opp p)).
Induction p; Auto; Intros; Simpl.
Generalize H0.
Elim m; Intros.
Inversion H1; Auto.
Save.
Hints Resolve full_opp.
Lemma suma_app_full: (p,q:pol)(full_pol (suma_app p q))->(full_pol p).
Induction p; Trivial.
Induction m; Intros.
Simpl in H0.
Inversion H0.
Apply full_pol_cons; Auto.
Apply H with q; Auto.
Apply aux_suma_app_full with q; Auto.
Save.
Lemma low_pol_term_mult: (c:Q)(t,t1:term)(p:pol)
(full n t)->(full n t1)->(full_pol p)->
(low_pol t1 p)->
(low_pol (term_mult t t1) (mult_m p (c,t))).
Induction p; Auto.
Induction m; Intros; Simpl.
Apply low_cons.
Inversion H2.
Inversion H3.
EAuto.
Save.
Hints Resolve low_pol_term_mult.
Lemma full_mult_mon: (c:Q)(t:term)(p:pol)(full n t)->(~(eqQ
c OQ))->
(full_pol p)->(full_pol (mult_m p (c,t))).
Induction p; Auto.
Induction m; Intros c1 t1 p0 HR ft eqn fcp.
Simpl.
Inversion fcp.
Apply full_pol_cons; Auto.
Save.
Hints Resolve full_mult_mon.
Lemma Low_Ttm_tran: (u,t:term)(p:pol)(full n u)->(full n t)->
(low_pol t p)->(Ttm t u)->(full_pol p)->(low_pol u p).
Intros.
Apply low_trans with t; Auto.
Save.
Hints Resolve Low_Ttm_tran.
Lemma coef_low_pol:(t:term)(p:pol)(low_pol t p)->
(full n t)->(full_pol p)->(eqQ (coef p t) OQ).
Induction p.
Auto.
Induction m; Intros.
Inversion H2.
Inversion H0.
Cut ~t=b; Intros.
Simpl.
Elim (eq_tm_dec t b); Intros.
Elim H15; Auto.
Clear b0.
Apply H; Trivial.
Apply Low_Ttm_tran with t:=b; Auto.
Unfold not; Intros; Absurd b=t; Auto.
Apply Ttm_strict with n:=n; Auto.
Save.
Hints Resolve coef_low_pol.
Lemma full_eq_vpol: (p:pol)(full_pol p)->(equpol p vpol)->p=vpol.
Induction 1; Auto; Intros.
Cut (eqQ a OQ); Intros.
Elim H0; Trivial.
Cut (eqQ (coef P t) OQ); Intros.
Clear H0 H p.
Apply eqQ_trans with (coef (cpol (a,t) P) t).
Simpl.
Elim (eq_tm_dec t t); Intros.
Apply eqQ_trans with (plusQ a OQ); Auto.
Elim b; Auto.
Change (no_term_in_pol (cpol (a,t) P) t).
Apply comp_no_term_in_pol with vpol; Auto.
Unfold no_term_in_pol; Auto.
Apply coef_low_pol; Trivial.
Save.
Lemma full_no_term: (y:Q)(y0:term)(p:pol)
(full_pol (cpol (y,y0) p))->(no_term_in_pol p y0).
Intros.
Red.
Inversion H.
Apply coef_low_pol; Auto.
Save.
Lemma coef_first : (p:pol)(c:Q)(t:term)
(full_pol (cpol (c,t) p))->
(eqQ (coef (cpol (c,t) p) t) c).
Intros p c t fp.
Simpl.
Elim (eq_tm_dec t t).
Intros XX; Clear XX.
Cut (eqQ (coef p t) OQ).
Intros e.
Apply eqQ_trans with (plusQ c OQ); Auto.
Inversion fp.
(Apply coef_low_pol; Trivial).
Intros XX; Elim XX; Trivial.
Save.
Lemma full_pol_cons_term: (a:Q)(t,t':term)(p:pol)(full_pol (cpol (a,t) p))->
(term_in_pol p t')->(term_in_pol (cpol (a,t) p) t').
Intros.
Red.
Red in H0.
Inversion H.
Red; Intros.
Apply H0.
Apply eqQ_trans with (coef (cpol (a,t) p) t'); Auto.
Apply eqQ_sym.
Apply coef_n_term.
Red; Intros.
Rewrite H9 in H8.
Cut (eqQ (coef (cpol (a,t) p) t) a); Intros.
Cut (eqQ a OQ); Intros.
Elim H4; Auto.
Apply eqQ_trans with (coef (cpol (a,t) p) t); Auto.
Apply coef_first; Auto.
Save.
Theorem no_mon_rep_full: (m:monom)(p:pol)~(full_pol (cpol m (cpol m p))).
Induction m; Intros; Red; Intro H.
Absurd (Ttm b b); Auto.
Inversion H.
Inversion H6; Auto.
Save.
Lemma full_cp_neq_vp : (p:pol)(m:monom)
(full_pol (cpol m p))->
~(equpol (cpol m p) vpol).
Induction m.
Intros c t.
Unfold not; Intros fp e.
Cut (eqQ c OQ).
Inversion fp; Assumption.
Apply eqQ_trans with (coef (cpol (c,t) p) t).
Apply eqQ_sym.
Apply coef_first; Trivial.
Apply eqQ_trans with (coef (cpol (c,t) p) t); Auto.
Replace OQ with (coef vpol t); Auto.
Save.
Lemma vpol_dec: (p:pol)(full_pol p)->
{(equpol p vpol)}+{~(equpol p vpol)}.
Induction p.
Left; Trivial.
Intros.
Right.
Apply full_cp_neq_vp; Trivial.
Save.
Hints Resolve vpol_dec.
Lemma term_in_Ttm_pol: (p:pol)(full_pol p)->(y0,t:term)(full n y0)->(low_pol y0 p)->
(term_in_pol p t)->(Ttm t y0).
Induction p.
Intros.
Elim H2; Auto.
Induction m; Intros.
Inversion H0; Inversion H2.
Elim (eq_tm_dec t b); Intros.
Rewrite a1; Trivial.
Apply Ttm_trans with b n; Trivial.
Apply H; Auto.
Cut t=b\/(term_in_pol p0 t); Intros.
Elim H16; Intros; Clear H16; Trivial.
Elim b0; Auto.
Apply split_term_in_pol_cons with a; Auto.
Apply full_coef with (cpol (a,b) p0); Auto.
Save.
Lemma insert : (m:monom)(full_mon n m)->(~(z_monom m))->
(p:pol)(full_pol p)->
{q:pol|(full_pol q)
/\(equpol q (cpol m p))
/\(t:term)(full n t)->(low_pol t p)->(Ttm (mon_term m) t)->
(low_pol t q)}.
Induction m; Intros x t fm zm; Induction p.
Intros; Split with (cpol (x,t) vpol); Auto.
Induction m0; Intros y u p' HR fuy.
Elim (Ttm_total t u n).
Induction 1; Intros fp.
Elim HR.
Intros q; Destruct 1; Intros fq; Destruct 1; Intros eq lq.
Split with (cpol (y,u) q).
Split.
Inversion fuy; Auto.
Split.
Apply equpol_tran with (cpol (y,u) (cpol (x,t) p')).
Auto.
Exact (equpol_cm (y,u) (cpol (x,t) vpol) p').
Intros v fv lv tv; Inversion lv; Auto.
Inversion fuy; Auto.
Split with (cpol (x,t) (cpol (y,u) p')); Auto.
Intros e; Elim (decQ (plusQ x y)).
Intros e1; Split with p'.
Split.
Inversion fuy; Trivial.
Split.
Rewrite e.
Apply equpol_tran with (cpol ((plusQ x y),u) p'); Auto.
(Intros v fv l i; Simpl in i; Inversion fuy; Inversion l;
Apply low_trans with u; Auto).
(Rewrite <- e; Intros neq; Split with (cpol ((plusQ x y),t) p');
Inversion fuy; Split).
(Apply full_pol_cons; Auto).
Rewrite e; Auto.
Split.
Auto.
(Intros v fv lv tv; Inversion lv; Apply low_cons; Auto).
Inversion fm; Auto.
Inversion fuy; Auto.
Save.
Lemma can_fun : (p:pol)(full_term_pol p)->
{q:pol|(full_pol q)/\(equpol p q)}.
Induction p.
Intros; Split with vpol; Auto.
Intros m p' HR fp.
Cut (full_term_pol p').
Intros fp'; Elim (HR fp'); Intros q; Destruct 1; Intros fq eq.
Elim (z_monom_dec m).
Intros zm; Split with q; Split; Trivial.
Apply equpol_tran with p'; Auto.
Intros nzm; Elim insert with m q; Trivial.
Intros q0; Destruct 1; Intros fq0; Destruct 1; Intros eq0 lq0; Split
with q0; Split;
[ Assumption | Apply equpol_tran with (cpol m q); Auto ].
Inversion fp; Auto.
Inversion fp; Auto.
Save.
Definition fun_can : pol -> pol.
Intros p; Elim (full_pol_tm_dec p).
Intros cp; Elim (can_fun p cp); Intros q; Intros; Exact q.
Intros ; Exact vpol.
Defined.
Transparent fun_can.
Lemma can_corr : (p:pol)(full_term_pol p)->
(equpol p (fun_can p)).
(Intros p fp; Unfold fun_can; Elim (full_pol_tm_dec p); Simpl).
(Clear fp; Intros fp; Elim (can_fun p fp); Simpl).
Tauto.
(Intros XX; Elim (XX fp)).
Save.
Hints Resolve can_corr.
Lemma can_is_full : (p:pol)(full_term_pol p)->(full_pol (fun_can p)).
(Intros p fp; Unfold fun_can; Elim (full_pol_tm_dec p); Simpl).
(Clear fp; Intros fp; Elim (can_fun p fp); Simpl).
Tauto.
(Intros XX; Elim (XX fp)).
Save.
Hints Resolve can_is_full.
Lemma vpol_dec_full_term: (p:pol)(full_term_pol p)->
{(equpol p vpol)}+{~(equpol p vpol)}.
Intros.
Elim (can_fun p H).
Intros q; Elim q; Simpl.
Destruct 1; Intros h1 h2; Left; Trivial.
Induction m.
Intros y y0 p0.
Intros.
Elim p1; Intros.
Right.
Apply eq_nvpol with (cpol (y,y0) p0); Auto.
Apply full_cp_neq_vp; Trivial.
Save.
Hints Resolve vpol_dec_full_term.
Lemma equpol_dec_full_term: (p,q:pol)(full_term_pol p)->(full_term_pol q)->
{(equpol p q)}+{~(equpol p q)}.
Intros.
Elim vpol_dec_full_term with (suma_app p (pol_opp q)); Auto.
Intros.
Left.
Apply equpol_tran with (pol_opp (pol_opp q)); Auto.
Intros.
Right.
Red; Intros.
Elim b.
Apply equpol_tran with (suma_app q (pol_opp q)); Auto.
Save.
Inductive same_pol : pol -> pol -> Prop :=
same_nil : (same_pol vpol vpol)
| same_cons : (t:term)(full n t)->(c1,c2:Q)(eqQ c1 c2)->(p1,p2:pol)
(same_pol p1 p2)->(same_pol (cpol (c1,t) p1)
(cpol (c2,t) p2)).
Hints Resolve same_nil same_cons. Lemma same_refl : (p:pol)(full_term_pol p)->(same_pol p p).
Induction 1; Auto.
Save.
Hints Resolve same_refl.
Lemma same_sym : (p,q:pol)(same_pol p q)->(same_pol q p).
Induction 1; Auto.
Save.
Hints Resolve same_sym.
Lemma same_trans : (p,q,r:pol)(same_pol p q)->(same_pol q r)->(same_pol p r).
Intros p q r s.
Generalize r.
Elim s.
Auto.
Intros.
(Inversion H3; Apply same_cons; Auto).
(Apply eqQ_trans with c2; Auto).
Save.
Hints Resolve same_trans.
Lemma same_length : (p1,p2:pol)(same_pol p1 p2)->(full_pol p1)->
((full_pol p2) /\ (u:term)(low_pol u p1)->(low_pol u p2)).
Induction 1; Auto.
Intros t f c1 c2 e q1 q2 s HR1 HR2; Split.
Inversion HR2.
Apply full_pol_cons; Trivial.
Apply comp_nOQ with c1; Trivial.
Elim HR1; Intros; Trivial.
Elim HR1; Auto.
Intros u HA; Inversion HA; Auto.
Save.
Hints Resolve same_length.
Lemma same_equpol: (p,q:pol)(same_pol p q)->(equpol p q).
Intros p q H.
Elim H; Auto.
Save.
Hints Resolve same_equpol.
Lemma full_same: (p1,p2:pol)(equpol p1 p2)->(full_pol p1)->
(full_pol p2)->(same_pol p1 p2).
Induction p1.
Induction p2; Auto.
Intros m2 q2 hr2 e fv fc.
Elim (full_cp_neq_vp q2 m2); Auto.
Induction m; Intros c1 t1 q1 hr1; Induction p2.
Intros e fp fv.
Elim (full_cp_neq_vp q1 (c1,t1)); Auto.
Induction m0; Intros c2 t2 q2 hr2 e f1 f2.
Inversion f1.
Inversion f2.
Elim Ttm_total with t2 t1 n; Trivial.
Destruct 1; Intros i; Clear a1.
Absurd (eqQ c1 OQ); Trivial.
Apply eqQ_trans with (coef (cpol (c2,t2) q2) t1); Auto.
Apply eqQ_sym.
Apply eqQ_trans with (coef (cpol (c1,t1) q1) t1); Auto.
Apply coef_first; Auto.
Absurd (eqQ c2 OQ); Trivial.
Apply eqQ_trans with (coef (cpol (c1,t1) q1) t2); Auto.
Apply eqQ_sym.
Apply eqQ_trans with (coef (cpol (c2,t2) q2) t2); Auto.
Apply coef_first; Auto.
Intros e0.
Cut t1=t2; Auto.
Clear e0; Intros e0.
Cut (eqQ c1 c2).
Intros e1.
Rewrite e0; Apply same_cons; Trivial.
Apply hr1; Trivial.
Apply equpol_tran
with (suma_app (pol_opp (cpol (c1,t1) vpol)) (cpol (c1,t1) q1)).
Simpl.
Apply equpol_tran with (cpol ((plusQ (multQ_neg c1) c1),t1) q1); Auto.
Apply equpol_sym.
Apply equpol_tran
with (suma_app (pol_opp (cpol (c2,t2) vpol)) (cpol (c2,t2) q2)).
Simpl.
Apply equpol_tran with (cpol ((plusQ (multQ_neg c2) c2),t2) q2); Auto.
Apply equpol_ss.
Simpl.
Apply equmon_cons; Auto.
Auto.
Apply eqQ_trans with (coef (cpol (c2,t2) q2) t1).
Rewrite e0.
Apply eqQ_sym.
Apply eqQ_trans with (coef (cpol (c1,t1) q1) t2); Auto.
Rewrite <- e0; Apply coef_first; Auto.
Rewrite e0; Apply coef_first; Auto.
Save.
Hints Resolve full_same.
Lemma same_can : (p,q:pol)(equpol p q)->
(full_term_pol p)->
(full_term_pol q)->(same_pol (fun_can p)(fun_can q)).
Intros p q e fp fq; Apply full_same.
Apply equpol_tran with p.
Auto.
(Apply equpol_tran with q; Auto).
Auto.
Auto.
Save.
Hints Resolve same_can.
Lemma comm_mult_can : (p:pol)
(full_term_pol p)->(m:monom)(full_mon n m)->
~(z_monom m)->
(same_pol (fun_can (mult_m p m))(mult_m (fun_can p) m)).
(Intros p fp; Induction m; Intros c t ft zc).
Apply full_same.
Apply equpol_tran with (mult_m p (c,t)).
(Apply equpol_sym; Auto).
Apply mult_pm_comp; Auto.
Auto.
Auto.
Save.
Hints Resolve comm_mult_can.
Lemma term_in_pol_same: (f,g:pol)(t:term)(same_pol f g)->
(term_in_pol f t)->(term_in_pol g t).
Unfold term_in_pol.
Intros f g t H tp.
Apply comp_nOQ with c:=(coef f t); Auto.
Save.
Hints Resolve term_in_pol_same.
Lemma pol_opp_mult :
(f:pol)(full_term_pol f)->
(same_pol (pol_opp f)
(mult_m f ((multQ_neg unQ),(n_term_O n)))).
Induction f.
Simpl; Auto.
Destruct m; Intros c t q hr fp.
Simpl.
Inversion fp.
Replace (term_mult (n_term_O n) t) with t.
Apply same_cons; Auto.
Apply eqQ_trans with (multQ c (multQ_neg unQ)); Auto.
Symmetry.
Transitivity (term_mult t (n_term_O n)); Auto.
Save.
Index
This page has been generated by coqdoc