Library congr_y_red2_tes
Require Export reduccion2_tes.
Inductive equiv_Id [F:(list pol);f:pol]: pol->Prop :=
equiv_Id_cons: (g:pol)(full_fam F)->(full_term_pol f)->
(full_term_pol g)->(Ideal (suma_app f (pol_opp g)) F)
->(equiv_Id F f g).
Hints Resolve equiv_Id_cons.
Lemma equiv_id_trans :
(F:(list pol))(f,g,h:pol)(equiv_Id F f g)->
(equiv_Id F g h)->(equiv_Id F f h).
Induction 1.
Induction 5; Intros.
Apply equiv_Id_cons; Trivial.
Apply pol_eq_id_eg
with (suma_app (suma_app f (pol_opp g0)) (suma_app g0 (pol_opp g1))).
Apply suma_p_id; Trivial.
Auto.
Auto.
Save.
Inductive Red_equiv [F:(list pol)] : pol->pol->Prop :=
Red_equiv_eq: (g,h:pol)(full_fam F)->(full_term_pol g)->
(full_term_pol h)->(equpol g h)->(Red_equiv F g h)
|Red_equiv_step: (g,h:pol)(full_fam F)->(full_term_pol g)->
(full_term_pol h)->(Red1 F g h)->(Red_equiv F g h)
|Red_equiv_sym: (g,h:pol)(full_fam F)->(full_term_pol g)->
(full_term_pol h)->(Red_equiv F g h)->
(Red_equiv F h g)
|Red_equiv_trans: (g,f,h:pol)(full_fam F)->
(full_term_pol g)->(full_term_pol f)->
(full_term_pol h)->(Red_equiv F g f)->(Red_equiv F f h)->
(Red_equiv F g h).
Hints Resolve Red_equiv_eq Red_equiv_step Red_equiv_sym Red_equiv_trans.
Lemma Red_equiv_ext: (G : (list pol))(g,h:pol)(Red_equiv G g h)->
(g':pol)(equpol g g')->(full_term_pol g')->(Red_equiv G g' h).
Intros G g h.
Induction 1; Intros.
Apply Red_equiv_eq; Auto.
Apply equpol_tran with g0; Auto.
Apply Red_equiv_step; Auto.
Apply Red1_ext2 with g0; Auto.
Apply Red_equiv_trans with h0; Auto.
Apply Red_equiv_trans with f; Auto.
Save.
Lemma Red3_equiv : (f,g:pol)(F:(list pol))
(Red3 F f g)->(Red_equiv F f g).
(Intros f g F r; Elim r).
Auto.
Auto.
(Intros g' f' h'; Intros; Apply Red_equiv_trans with f';
Auto).
Save.
Hints Resolve Red3_equiv.
Lemma Red_equiv_full_l :
(f,g:pol)(F:(list pol))(Red_equiv F f g)->
(full_term_pol f).
Intros f g F r; Inversion r; Auto.
Save.
Lemma Red_equiv_full_r :
(f,g:pol)(F:(list pol))(Red_equiv F f g)->
(full_term_pol g).
Intros f g F r; Inversion r; Auto.
Save.
Hints Resolve Red_equiv_full_r Red_equiv_full_l.
Lemma Red_equiv_tran : (f,g,h:pol)(F:(list pol))
(Red_equiv F f g)->(Red_equiv F g h)->
(Red_equiv F f h).
(Intros f g h F r1 r2; Apply Red_equiv_trans with g; Auto).
(Inversion r1; Auto).
(Inversion r1; Auto).
(Inversion r1; Auto).
(Inversion r2; Auto).
Save.
Lemma Red_equiv_sy : (f,g:pol)(F:(list pol))
(Red_equiv F f g)->(Red_equiv F g f).
(Intros f g F r; Inversion r; Apply Red_equiv_sym; Auto).
Save.
Hints Resolve Red_equiv_sy.
Lemma con_red_cong: (f,g:pol)(F:(list pol))(Red_equiv F f g)->
(Ideal (suma_app f (pol_opp g)) F).
Induction 1; Intros.
Apply ideal_vpol.
Auto.
Apply sum_vpol_opp_inv.
Apply equpol_tran with h; Auto.
Apply Red1_dif_id; Trivial.
Apply pol_eq_id_eg with f:=(pol_opp (suma_app g0 (pol_opp h))); Auto.
Apply pol_eq_id_eg
with f:=(suma_app (suma_app g0 (pol_opp f0)) (suma_app f0 (pol_opp h)));
Trivial.
Apply suma_p_id; Trivial.
Auto.
Save.
Hints Resolve con_red_cong.
Lemma conv_congr :
(F:(list pol))(f,g:pol)(Red_equiv F f g)->
(equiv_Id F f g).
Induction 1.
Auto.
Auto.
Auto.
Intros g1 f1 h fF fg1 ff1 fh Rgf.
(Intros; Apply equiv_id_trans with f1; Auto).
Save.
Hints Resolve conv_congr.
Index
This page has been generated by coqdoc