Library nueva_equiv2_tes
Require Export lemma_cong_red2_tes.
Inductive suma_pol_mon [F:(list pol); f:pol] : pol->Prop :=
suma_pol_mon1: (f0:pol)(full_fam F)->
(full_term_pol f)
->(full_term_pol f0)
->(equpol f f0)->(suma_pol_mon F f f0)
| suma_pol_mon2: (g0:pol)
(g:pol)(full_fam F)->
(full_term_pol f)
->(full_term_pol g0)
->(full_term_pol g)
->(suma_pol_mon F f g)
->(m:monom)
(full_mon n m)
->(fi:pol)
(pol_In_ensemb fi F)
->(equpol g0
(suma_app g (mult_m fi m)))
->(suma_pol_mon F f g0).
Hints Resolve suma_pol_mon1 suma_pol_mon2.
Lemma equpol_Id_sum2: (p,q,p':pol)(F:(list pol))(equpol p q)->
(suma_pol_mon F p p')->(full_term_pol q)->(suma_pol_mon F q p').
Induction 2; Intros.
Apply suma_pol_mon1; Trivial.
Apply equpol_tran with p; Auto.
Apply suma_pol_mon2 with g:=g m:=m fi:=fi; Auto.
Save.
Hints Resolve equpol_Id_sum2.
Lemma equpol_Id_sum2_op: (p,q,p':pol)(F:(list pol))(suma_pol_mon F p' p)->
(full_term_pol q)->(equpol p q)->(suma_pol_mon F p' q).
Induction 1; Intros.
Apply suma_pol_mon1; Trivial.
Apply equpol_tran with f0; Trivial.
Apply suma_pol_mon2 with g:=g m:=m fi:=fi; Trivial.
Apply equpol_tran with g0; Auto.
Save.
Hints Resolve equpol_Id_sum2_op.
Lemma trans_equiv_Id2: (f,g,h:pol)(F:(list pol))(suma_pol_mon F f g)->
(suma_pol_mon F g h)->(suma_pol_mon F f h).
Induction 1.
Intros.
Apply equpol_Id_sum2 with p:=f0; Auto.
Intros.
Generalize H9.
Induction 1.
Intros.
(Apply suma_pol_mon2 with g:=g1 m:=m fi:=fi; Trivial).
Apply equpol_tran with g0; Auto.
Intros.
(Apply suma_pol_mon2 with g:=g3 m:=m0 fi:=fi0; Auto).
Save.
Hints Resolve trans_equiv_Id2.
Lemma sym_equiv_Id2: (f,g:pol)(F:(list pol))(suma_pol_mon F f g)->(suma_pol_mon F g f).
Induction 1.
Auto.
Intros.
Apply trans_equiv_Id2 with g1; Trivial.
Apply suma_pol_mon2 with g:=g0 fi:=fi m:=(monom_op m); Trivial.
Auto.
Generalize m H6.
Induction m0; Auto.
Apply ch_m_plus.
Apply equpol_tran with (suma_app g1 (mult_m fi m)); Auto.
Save.
Lemma equat_equiv_Id: (f,g,p:pol)(F:(list pol))(full_term_pol f)->(full_term_pol g)->
(suma_pol_mon F (suma_app f (pol_opp g)) p)->(suma_pol_mon F f (suma_app p g)).
Induction 3; Intros.
Apply suma_pol_mon1; Trivial.
Apply full_term_suma_app; Trivial.
Apply equpol_tran with (suma_app f (suma_app (pol_opp g) g)).
Apply equpol_tran with (suma_app f vpol).
Auto.
Apply equpol_ss; Auto.
Apply equpol_tran with (suma_app (suma_app f (pol_opp g)) g); Auto.
Apply suma_pol_mon2 with g:=(suma_app g1 g) m:=m fi:=fi; Trivial.
Apply full_term_suma_app; Trivial.
Apply full_term_suma_app; Trivial.
Apply equpol_tran with (suma_app g1 (suma_app g (mult_m fi m))).
Apply equpol_tran with (suma_app g1 (suma_app (mult_m fi m) g)).
Apply equpol_tran with (suma_app (suma_app g1 (mult_m fi m)) g); Auto.
Auto.
Auto.
Save.
Hints Resolve equat_equiv_Id.
Lemma equiv_Id_cpol: (f,p:pol)(F:(list pol))(full_term_pol p)->
(~(equpol p vpol))->(suma_pol_mon F f vpol)->(suma_pol_mon (cons p F) f vpol).
Induction 3; Intros; Auto.
Apply suma_pol_mon2 with g:=g m:=m fi:=fi; Auto.
Save.
Hints Resolve equiv_Id_cpol.
Lemma equiv_m: (F:(list pol))(f,g:pol)(m:monom)(full_mon n m)->
(suma_pol_mon F f g)->(suma_pol_mon F (cpol m f) (cpol m g)).
Induction 2.
Intros.
Apply suma_pol_mon1; Auto.
Generalize H.
Induction m; Intros.
Apply full_term_pol_cons; Auto.
Generalize H.
Induction m; Intros.
Apply full_term_pol_cons; Auto.
Intros.
Apply suma_pol_mon2 with g:=(cpol m g1) m:=m0 fi:=fi; Trivial.
Generalize H.
Induction m; Intros.
Apply full_term_pol_cons; Auto.
Generalize H.
Induction m; Intros.
Apply full_term_pol_cons; Auto.
Generalize H.
Induction m; Intros.
Apply full_term_pol_cons; Auto.
Simpl.
Auto.
Save.
Lemma monot_suma_pol_mon: (F:(list pol))(f,g,h:pol)(full_term_pol h)->(suma_pol_mon F f g)->(suma_pol_mon F (suma_app h f) (suma_app h g)).
Induction h; Intros; Auto.
Cut (suma_pol_mon F (suma_app p f) (suma_app p g)); Intros.
Simpl.
Apply equiv_m; Trivial.
Inversion H0; Auto.
Apply H; Auto.
Inversion H0; Auto.
Save.
Lemma split_pol_mon: (F:(list pol))(f,g,h :pol)(full_term_pol g)->(full_term_pol h)->(full_fam F)->
(suma_pol_mon (cons g F) f (mult_p g h))->(suma_pol_mon (cons g F)f vpol).
Induction h; Intros.
Apply equpol_Id_sum2_op with (mult_p g vpol); Auto.
Cut (full_term_pol p); Intros.
Cut (full_fam (cons g F)); Intros.
Cut (full_term_pol (mult_m g m)); Intros.
Cut (full_term_pol (mult_p g p)); Intros.
Cut (full_term_pol (suma_app (mult_m g m) (mult_p g p))); Intros.
Cut (suma_pol_mon (cons g F) (mult_m g m) vpol); Intros.
Cut (suma_pol_mon (cons g F) (suma_app (mult_m g m) (mult_p g p))
(mult_p g p)); Intros.
Cut (suma_pol_mon (cons g F) f (mult_p g p)); Intros.
Apply H; Auto.
Apply trans_equiv_Id2 with (suma_app (mult_m g m) (mult_p g p)); Auto.
Apply trans_equiv_Id2 with (mult_p g (cpol m p)); Auto.
Apply equpol_Id_sum2 with (suma_app (mult_p g p) (mult_m g m)); Auto.
Apply equpol_Id_sum2_op with (suma_app (mult_p g p) vpol); Auto.
Apply monot_suma_pol_mon; Auto.
Apply suma_pol_mon2 with g:=(mult_m g m) m:=(monom_op m) fi:=g; Auto.
Inversion H1; Auto.
Apply full_term_suma_app; Auto.
Apply full_term_mult_p; Trivial.
Generalize m H1.
Induction m0; Intros.
Apply full_mult_m; Trivial.
Inversion H6; Auto.
Inversion H3; Auto.
Inversion H1; Auto.
Save.
Lemma split_mon_mon: (F:(list pol))(f,g:pol)(m:monom)(full_term_pol g)->
(~(equpol g vpol))->(full_mon n m)->(suma_pol_mon F f vpol)->
(suma_pol_mon (cons g F) (suma_app (mult_m g m) f) vpol).
Intros.
Cut (full_term_pol (mult_m g m)); Intros.
Cut (suma_pol_mon (cons g F) f vpol); Intros.
Cut (full_fam (cons g F)); Intros.
Cut (suma_pol_mon (cons g F) (suma_app (mult_m g m) f) (mult_m g m)); Intros.
Cut (suma_pol_mon (cons g F) (mult_m g m) vpol); Intros.
Apply trans_equiv_Id2 with (mult_m g m); Auto.
Apply suma_pol_mon2 with g:=(mult_m g m) m:=(monom_op m) fi:=g; Auto.
Generalize m H1.
Induction m0; Intros; Auto.
Apply equpol_Id_sum2_op with (suma_app (mult_m g m) vpol); Auto.
Apply monot_suma_pol_mon; Auto.
Inversion H4; Auto.
Apply equiv_Id_cpol; Auto.
Generalize m H1.
Induction m0; Intros.
Apply full_mult_m; Auto.
Save.
Lemma equiv_Id2_equiv_Id: (f,g:pol)(F:(list pol))(suma_pol_mon F f g)->
(equiv_Id F f g).
Induction 1.
Auto.
Intros.
Apply equiv_Id_cons; Trivial.
Inversion H5.
Apply pol_eq_id_eg
with (suma_app (suma_app f (pol_opp g1)) (pol_opp (mult_m fi m))).
Apply suma_p_id; Auto.
Apply opp_p_id.
Apply pol_F_idmult; Auto.
Apply elem_full with F; Trivial.
Apply equpol_tran
with (suma_app f (suma_app (pol_opp g1) (pol_opp (mult_m fi m)))).
Auto.
Apply equpol_ss; Trivial.
Apply equpol_sym.
Apply equpol_tran with (pol_opp (suma_app g1 (mult_m fi m))).
Auto.
Auto.
Auto.
Save.
Hints Resolve equiv_Id2_equiv_Id.
Lemma imp_equiv_Id2_opp: (h,g,f,fi:pol)(F:(list pol))
(full_fam F)->(pol_In_ensemb fi F)->(full_term_pol h) ->
(full_term_pol g)->(full_term_pol f)->
(equpol g (suma_app f (mult_p h fi)))->(suma_pol_mon F f g).
Induction h.
Intros.
(Apply suma_pol_mon1; Trivial).
Apply equpol_sym.
Apply equpol_tran with (suma_app f vpol); Auto.
Intros.
Simpl in H5.
Apply trans_equiv_Id2 with (suma_app g (pol_opp (mult_p p fi))).
(Apply suma_pol_mon2 with g:=f m:=m fi:=fi; Trivial).
(Apply full_term_suma_app; Trivial).
Apply full_term_opp.
(Apply full_term_mult_p; Trivial).
(Inversion H2; Auto).
(Apply elem_full with F; Auto).
Auto.
(Inversion H2; Auto).
Apply equpol_tran
with (suma_app (suma_app f (mult_m fi m))
(suma_app (mult_p p fi) (pol_opp (mult_p p fi)))).
Apply equpol_tran
with (suma_app (suma_app (suma_app f (mult_m fi m)) (mult_p p fi))
(pol_opp (mult_p p fi))).
Apply monot_suma.
Apply equpol_tran
with (suma_app f (suma_app (mult_m fi m) (mult_p p fi))); Auto.
Auto.
Apply equpol_tran with (suma_app (suma_app f (mult_m fi m)) vpol).
Auto.
Auto.
(Apply H with fi:=fi; Trivial).
(Inversion H2; Auto).
Apply full_term_suma_app; Trivial.
Apply full_term_opp.
Apply full_term_mult_p; Trivial.
Inversion H2; Auto.
Apply elem_full with F; Auto.
Apply equpol_tran
with (suma_app g (suma_app (pol_opp (mult_p p fi)) (mult_p p fi))).
Apply equpol_tran with (suma_app g vpol).
Auto.
Auto.
Auto.
Save.
Hints Resolve imp_equiv_Id2_opp.
Lemma ideal_suma_pol_mon: (F:(list pol))(f,g:pol)(full_term_pol f)->
(full_term_pol g)->(full_fam F)->
(Ideal (suma_app f (pol_opp g)) F)->
(suma_pol_mon F f g).
Intros.
Apply equpol_Id_sum2_op with (suma_app vpol g); Trivial.
Apply equat_equiv_Id; Trivial.
Generalize F f g H H0 H2 H1.
Clear H H0 H2 H1 F f g.
Induction 3; Intros.
Apply suma_pol_mon1; Auto.
Cut (full_term_pol q); Intros.
Cut ~(equpol q vpol); Intros.
Cut (full_fam F0); Intros.
Cut (suma_pol_mon F0 p' vpol); Intros.
Induction q'; Intros.
Apply trans_equiv_Id2 with p'.
Apply suma_pol_mon1; Trivial.
Inversion H4; Auto.
Apply equpol_tran with (suma_app vpol p'); Trivial.
Apply equpol_tran with (suma_app (mult_p q vpol) p'); Auto.
Apply equiv_Id_cpol; Auto.
Cut (full_term_pol q'); Intros.
Cut (suma_pol_mon (cons q F0) (suma_app (mult_m q m) p') vpol); Intros.
Cut (suma_pol_mon (cons q F0)
(suma_app (mult_p q q') (suma_app (mult_m q m) p')) (mult_p q q')); Intros.
Apply split_pol_mon with h:=q'; Trivial.
Apply equpol_Id_sum2 with (suma_app (mult_p q q') (suma_app (mult_m q m) p'));
Trivial.
Apply equpol_tran with (suma_app (mult_p q (cpol m q')) p').
Apply equpol_tran with (suma_app (suma_app (mult_p q q') (mult_m q m)) p').
Auto.
Apply equpol_ss; Trivial.
Apply equpol_sym.
Apply equpol_tran with (suma_app (mult_m q m) (mult_p q q')); Auto.
Auto.
Apply equpol_Id_sum2_op with (suma_app (mult_p q q') vpol); Trivial.
Apply monot_suma_pol_mon; Auto.
Auto.
Apply split_mon_mon; Trivial.
Inversion H3; Auto.
Inversion H3; Auto.
Apply H5; Auto.
Inversion H7; Auto.
Inversion H7.
Elim H11; Auto.
Inversion H7.
Elim H10; Auto.
Save.
Lemma equiv_Id_equiv_Id2: (f,g:pol)(F:(list pol))(equiv_Id F f g)->
(suma_pol_mon F f g).
Induction 1.
Intros.
Apply ideal_suma_pol_mon; Auto.
Save.
Hints Resolve equiv_Id_equiv_Id2.
Index
This page has been generated by coqdoc