Library Somme_poly_tes
Require Export Polynomes_tes.
Fixpoint suma_app [p:pol]: pol -> pol :=
[q:pol]Cases p of
vpol => q
| (cpol m1 p1) => (cpol m1 (suma_app p1 q))
end.
Lemma vpol_suma_leibn: (p:pol) (suma_app vpol p)=p.
Auto.
Save.
Hints Resolve vpol_suma_leibn.
Lemma suma_vpol_leibn: (p:pol) (suma_app p vpol)=p.
(Induction p; Auto).
Intros.
Simpl.
(Rewrite -> H; Auto).
Save.
Hints Resolve suma_vpol_leibn.
Inductive equpol: pol->pol->Prop :=
equpol_refl: (p:pol)(equpol p p)
| equpol_sym: (p,q:pol)(equpol p q)->(equpol q p)
| equpol_tran: (p,q,r:pol)(equpol p q)->(equpol q r)->(equpol p r)
| equpol_cm: (m:monom)(p,q:pol)
(equpol (cpol m (suma_app p q)) (suma_app p (cpol m q)))
| equpol_ss: (p,p',q,q':pol)(equpol p p')->(equpol q q')->
(equpol (suma_app p q) (suma_app p' q'))
| equpol_smt: (k,k':Q)(t:term)(p:pol)
(equpol (cpol (k,t) (cpol (k',t) p)) (cpol ((plusQ k k'),t) p))
| equpol_elim: (m:monom)(p:pol)(z_monom m)->(equpol (cpol m p) p).
Hints Resolve equpol_refl equpol_sym equpol_tran equpol_cm equpol_ss equpol_smt equpol_elim.
Lemma equpol_cpol: (m:monom)(p,q:pol)(equpol p q)->
(equpol (cpol m p) (cpol m q)).
Intros m p q H.
Change (equpol (suma_app (cpol m vpol) p)
(suma_app (cpol m vpol) q)).
Auto.
Save.
Hints Resolve equpol_cpol.
Lemma sym_mon : (m:monom)(p:pol) (equpol (cpol (monom_op m) (cpol m p)) p).
Intros; Elim m; Intros.
Unfold monom_op.
Simpl.
Apply equpol_tran with (cpol ((plusQ (multQ_neg a) a),b) p); Auto.
Save.
Hints Resolve sym_mon.
Lemma eq_cpol: (m:monom)(p,q:pol)(equpol (cpol m p) (cpol m q))->
(equpol p q).
Intros.
Generalize (equpol_cpol (monom_op m) (cpol m p) (cpol m q)); Intros.
Generalize (H0 H); Intro.
Generalize (sym_mon m p) ; Intro.
Generalize (sym_mon m q) ; Intro.
Generalize (equpol_sym (cpol (monom_op m) (cpol m p)) p H2); Intro.
Generalize (H0 H) ; Clear H0; Intros.
Generalize (equpol_tran p (cpol (monom_op m) (cpol m p)) q H4).
Intros.
Apply H5.
Apply equpol_tran with (cpol (monom_op m) (cpol m q)); Trivial.
Save.
Hints Resolve eq_cpol.
Lemma equmon_cons : (m,m':monom)(equmon m m')->
(equpol (cpol m vpol)(cpol m' vpol)).
(Induction m; Intros c t; Induction m'; Intros c' t'; Induction 1).
(Induction 1; Intros e1 e2).
(Apply equpol_tran with vpol; Auto).
(Induction 1; Intros e1 e2).
Rewrite <- e1.
Apply equpol_tran
with (cpol ((plusQ c (multQ_neg c')),t) (cpol (c',t) vpol)).
Apply equpol_tran
with (cpol (c,t) (cpol ((multQ_neg c'),t) (cpol (c',t) vpol))).
Apply equpol_tran
with (suma_app (cpol ((multQ_neg c'),t) (cpol (c',t) vpol))
(cpol (c,t) vpol)).
Apply equpol_tran
with (cpol ((plusQ (multQ_neg c') c'),t) (cpol (c,t) vpol)).
(Apply equpol_sym; Apply equpol_elim).
Simpl.
Auto.
Simpl.
(Apply equpol_sym; Apply equpol_smt).
Replace (cpol ((multQ_neg c'),t) (cpol (c',t) vpol))
with (suma_app (cpol ((multQ_neg c'),t) (cpol (c',t) vpol)) vpol).
(Apply equpol_sym; Apply equpol_cm).
Trivial.
Apply equpol_smt.
Apply equpol_elim.
Unfold z_monom.
Apply eqQ_trans with (plusQ (multQ_neg c') c).
Auto.
Apply suma_op.
Auto.
Save.
Hints Resolve equmon_cons.
Lemma eq_mon_cpol: (m,m':monom)(equmon m m')->
(p:pol)(equpol (cpol m p) (cpol m' p)).
Intros.
Change (equpol (suma_app (cpol m vpol) p) (suma_app (cpol m' vpol) p)).
EAuto.
Save.
Hints Resolve eq_mon_cpol.
Lemma mon_Q_cpol: (a,b:Q)(eqQ a b)->
(p:pol)(y:term)(equpol (cpol (a,y) p) (cpol (b,y) p)).
Auto.
Save.
Hints Resolve mon_Q_cpol.
Lemma equpol_cpol2: (m,m':monom)(equmon m m')->(p,p':pol)(equpol p p')->
(equpol (cpol m p) (cpol m' p')).
Intros.
Change (equpol (suma_app (cpol m vpol) p) (suma_app (cpol m' vpol) p')).
Auto.
Save.
Hints Resolve equpol_cpol2.
Lemma eq_nvpol:(p,q:pol)(equpol p q)->~(equpol p vpol)->~(equpol q vpol).
Intros.
(Unfold not; Intros).
Apply H0.
Apply equpol_tran with q; Trivial.
Save.
Hints Resolve eq_nvpol.
Lemma full_term_suma_app: (p:pol)(full_term_pol p)->
(q:pol)(full_term_pol q)->(full_term_pol (suma_app p q)).
Induction p; Auto.
Induction m.
Induction q.
Intros.
Replace (suma_app (cpol (a,b) p0) vpol) with (cpol (a,b) p0); Auto.
Induction m0; Intros.
Simpl.
Apply full_term_pol_cons.
Inversion H0; Auto.
Apply H with q:=(cpol (a0,b0) p1); Auto.
Inversion H0; Auto.
Save.
Hints Resolve full_term_suma_app.
Theorem asoc_mon_pol : (m:monom)(p,q:pol)
(equpol (suma_app (suma_app (cpol m vpol) p) q)
(suma_app (cpol m vpol) (suma_app p q))).
Auto.
Save.
Hints Resolve asoc_mon_pol.
Theorem vpol_suma : (q:pol) (equpol (suma_app vpol q) q).
Auto.
Save.
Hints Resolve vpol_suma.
Theorem suma_vpol : (q:pol) (equpol (suma_app q vpol) q).
Intros.
Replace (suma_app q vpol) with q; Auto.
Save.
Hints Resolve suma_vpol.
Theorem conmt_suma : (p,q:pol)(equpol (suma_app p q) (suma_app q p)).
Induction p; Auto.
Intros m p' HR q'; Simpl.
Apply equpol_tran with (cpol m (suma_app q' p')); Auto.
Save.
Hints Resolve conmt_suma.
Theorem asoc_suma: (p,q,r:pol)(equpol (suma_app (suma_app p q) r)
(suma_app p (suma_app q r))).
Induction p; Auto.
Intros m p' HR q' r'; Simpl; Auto.
Save.
Hints Resolve asoc_suma.
Lemma suma_cpol: (m,n:monom)(p,q:pol)(equpol (suma_app (cpol m p) (cpol n q))
(cpol m (cpol n (suma_app p q)))).
Simpl; Auto.
Save.
Hints Resolve suma_cpol.
Lemma permut_suma_app:(p,q,r:pol)(equpol (suma_app p (suma_app q r))
(suma_app q (suma_app p r))).
Intros.
Apply equpol_tran with (suma_app (suma_app p q) r); Auto.
Apply equpol_tran with (suma_app (suma_app q p) r); Auto.
Save.
Hints Resolve permut_suma_app.
Theorem monot_suma: (p,q,r:pol)(equpol p q)->
(equpol (suma_app p r) (suma_app q r)).
Auto.
Save.
Hints Resolve monot_suma.
Lemma monot_suma_l: (p,q,r:pol)(equpol p q)->
(equpol (suma_app r p) (suma_app r q)).
Auto.
Save.
Hints Resolve monot_suma_l.
Lemma sumcpol_l: (m:monom)(p,q:pol)((cpol m (suma_app p q))=
(suma_app (cpol m p) q)).
Auto.
Save.
Hints Resolve sumcpol_l.
Fixpoint pol_opp [p:pol]: pol:=
Cases p of
vpol => vpol
| (cpol (c,t) p) => (cpol ((multQ_neg c),t) (pol_opp p))
end.
Lemma suma_opp: (p:pol)(equpol (suma_app p (pol_opp p)) vpol).
Induction p; Auto.
Intro m; Elim m; Intros.
Simpl.
Apply equpol_tran with
(cpol (a,b) (cpol ((multQ_neg a),b) (suma_app p0 (pol_opp p0)))).
Auto.
Apply equpol_tran with (cpol (a,b) (cpol ((multQ_neg a),b) vpol)).
Auto.
Apply equpol_tran with (cpol ((plusQ a (multQ_neg a)),b) vpol);
Auto.
Save.
Hints Resolve suma_opp.
Lemma sym_mon1: (m:monom)(equpol (cpol m (pol_opp (cpol m vpol))) vpol).
Intros; Elim m; Intros.
Simpl.
Apply equpol_tran with (cpol ((plusQ a (multQ_neg a)),b) vpol);
Auto.
Save.
Hints Resolve sym_mon1.
Lemma sum_vpol_opp: (p,q:pol)(equpol (suma_app p q) vpol)->
(equpol p (pol_opp q)).
Intros.
Apply equpol_tran with (suma_app p (suma_app q (pol_opp q))).
(Apply equpol_tran with (suma_app p vpol); Auto).
Apply equpol_tran with (suma_app (suma_app p q) (pol_opp q)).
Auto.
Apply equpol_tran with (suma_app vpol (pol_opp q)).
Auto.
Auto.
Save.
Hints Resolve sum_vpol_opp.
Lemma sum_vpol_opp_inv: (p,q:pol)(equpol p (pol_opp q))->
(equpol (suma_app p q) vpol).
Intros.
Apply equpol_tran with (suma_app (pol_opp q) q).
Auto.
(Apply equpol_tran with (suma_app q (pol_opp q)); Auto).
Save.
Hints Resolve sum_vpol_opp_inv.
Lemma opp_comp: (f,g:pol)(equpol f g)->(equpol (pol_opp f) (pol_opp g)).
Intros.
Apply sum_vpol_opp with p:=(pol_opp f) q:=g.
Apply equpol_tran with (suma_app (pol_opp f) f).
Apply equpol_ss.
Auto.
Auto.
Auto.
Save.
Hints Resolve opp_comp.
Lemma opp_vpol: (p:pol)(equpol p vpol)->(equpol (pol_opp p) vpol).
Intros.
Apply equpol_tran with (pol_opp vpol); Auto.
Save.
Hints Resolve opp_vpol.
Lemma eq_pol_opp_no_zero: (f:pol)
(equpol (pol_opp f) vpol)->(equpol f vpol).
Intros.
Apply equpol_tran with (pol_opp vpol).
Apply equpol_tran with (pol_opp (pol_opp f)); Auto.
Auto.
Save.
Hints Resolve eq_pol_opp_no_zero.
Lemma mult_sum_opp3: (f,g:pol)(equpol (pol_opp (suma_app f g))
(suma_app (pol_opp f) (pol_opp g))).
Intros.
Apply equpol_sym.
Apply sum_vpol_opp.
(Apply equpol_tran with (suma_app (pol_opp f)
(suma_app (pol_opp g) (suma_app f g)));
Auto).
(Apply equpol_tran with (suma_app (pol_opp f)
(suma_app (pol_opp g) (suma_app g f)));
Auto).
(Apply equpol_tran with (suma_app (pol_opp f)
(suma_app (suma_app (pol_opp g) g) f));
Auto).
(Apply equpol_tran with (suma_app (pol_opp f) (suma_app vpol f)); Auto).
Save.
Hints Resolve mult_sum_opp3.
Lemma no_eq_no_vpol_opp: (f:pol)
~(equpol f vpol)->~(equpol (pol_opp f) vpol).
Red.
Intros.
(Cut (equpol f vpol); Intros).
(Elim H0; Auto).
Auto.
Save.
Hints Resolve no_eq_no_vpol_opp.
Lemma full_term_opp: (p:pol)(full_term_pol p)->(full_term_pol (pol_opp p)).
(Induction p; Auto).
Induction m.
Intros.
Simpl.
(Inversion H0; Auto).
Save.
Hints Resolve full_term_opp.
Index
This page has been generated by coqdoc