Library orden_pol
Require Export Hmtc.
Require Export Relations.
Inductive Tpol_Lex3: pol -> pol -> Prop :=
Tpol_Lex3_v: (m:monom)(p:pol)(full_mon n m)->
(full_term_pol p)->
(Tpol_Lex3 vpol (cpol m p))
|Tpol_Lex3_car: (m1,m2:monom)(p1,p2:pol)(full_mon n m1)->
(full_mon n m2)->(full_term_pol p1)->(full_term_pol p2)->
(Ttm (mon_term m1) (mon_term m2))->
(Tpol_Lex3 (cpol m1 p1) (cpol m2 p2))
|Tpol_Lex3_cdr: (k1,k2:Q)(t:term)(p1,p2:pol)(full n t)->
(full_term_pol p1)->(full_term_pol p2)->
(Tpol_Lex3 p1 p2)->
(Tpol_Lex3 (cpol (k1,t) p1) (cpol (k2,t) p2)).
Hints Resolve Tpol_Lex3_v Tpol_Lex3_car Tpol_Lex3_cdr.
Lemma ext_l_Tpol_Lex3: (p,q:pol)(Tpol_Lex3 p q)->(full_pol p)->
(full_pol q)->(r:pol)(equpol p r)->(full_pol r)->(Tpol_Lex3 r q).
Intros p q.
Induction 1.
Induction m.
Induction r; Auto.
Induction m0; Intros.
Cut (cpol (a0,b0) p1)=vpol; Intros.
Rewrite H7; Auto.
Apply full_eq_vpol; Auto.
Induction m1; Induction m2.
Induction r; Auto.
Induction m; Intros.
Simpl in H4.
Cut b=b1; Intros.
Apply Tpol_Lex3_car; Auto.
Simpl.
Inversion H9; Auto.
Inversion H9; Auto.
Simpl.
Rewrite <- H10; Trivial.
Transitivity (hterm (cpol (a,b) p1)).
Symmetry; Auto.
Transitivity (hterm (cpol (a1,b1) p0)); Auto.
Induction r; Auto.
Induction m; Intros.
Cut t=b; Intros.
Rewrite H10.
Apply Tpol_Lex3_cdr; Trivial.
Inversion H9; Auto.
Inversion H9; Auto.
Apply H4.
Inversion H9; Auto.
Inversion H5; Auto.
Inversion H6; Auto.
Rewrite H10 in H8.
Cut (eqQ k1 a); Intros.
Apply eq_cpol with (a,b); Auto.
Apply equpol_tran with (cpol (k1,b) p1); Auto.
Apply eqQ_trans with (hcoef (cpol (k1,t) p1)); Auto.
Apply eqQ_trans with (hcoef (cpol (a,b) p0)); Auto.
Apply eq_hcoef; Auto.
Rewrite H10; Auto.
Inversion H9; Auto.
Transitivity (hterm (cpol (k1,t) p1)).
Symmetry; Auto.
Transitivity (hterm (cpol (a,b) p0)); Auto.
Save.
Lemma ext_r_Tpol_Lex3: (p,q:pol)(Tpol_Lex3 p q)->(full_pol p)->
(full_pol q)->(r:pol)(equpol q r)->(full_pol r)->(Tpol_Lex3 p r).
Intros p q.
Induction 1.
Induction m.
Induction r.
Intros.
Inversion H3.
Cut (eqQ a OQ); Intros.
Elim H9; Auto.
Apply eqQ_trans with (hcoef (cpol (a,b) p0)); Auto.
Cut (cpol (a,b) p0)=vpol; Intros.
Rewrite H13.
Apply hcoef_vpol.
Apply full_eq_vpol; Auto.
Induction m0; Intros.
Apply Tpol_Lex3_v.
Simpl.
Inversion H6; Auto.
Inversion H6; Auto.
Induction m1; Induction m2.
Induction r.
Intros.
Simpl in H4.
Cut (cpol (a0,b0) p2)=vpol; Intros.
Rewrite <- H9.
Apply Tpol_Lex3_car; Auto.
Apply full_eq_vpol; Auto.
Induction m; Intros.
Simpl in H4.
Cut b0=b1; Intros.
Rewrite <- H10.
Apply Tpol_Lex3_car; Auto.
Inversion H9; Auto.
Transitivity (hterm (cpol (a0,b0) p2)).
Symmetry; Auto.
Transitivity (hterm (cpol (a1,b1) p0)); Auto.
Induction r.
Intros.
Inversion H6.
Cut (eqQ k2 OQ); Intros.
Elim H12; Auto.
Apply eqQ_trans with (hcoef (cpol (k2,t) p2)); Auto.
Cut (cpol (k2,t) p2)=vpol; Intros.
Rewrite H16.
Apply hcoef_vpol.
Apply full_eq_vpol; Auto.
Induction m; Intros.
Cut t=b; Intros.
Rewrite H10.
Apply Tpol_Lex3_cdr; Auto.
Inversion H9; Auto.
Inversion H9; Auto.
Apply H4.
Inversion H5; Auto.
Inversion H6; Auto.
Rewrite H10 in H8.
Cut (eqQ k2 a); Intros.
Apply eq_cpol with (a,b); Auto.
Apply equpol_tran with (cpol (k2,b) p2); Auto.
Apply eqQ_trans with (hcoef (cpol (k2,t) p2)); Auto.
Apply eqQ_trans with (hcoef (cpol (a,b) p0)); Auto.
Apply eq_hcoef; Auto.
Rewrite H10; Auto.
Inversion H9; Auto.
Transitivity (hterm (cpol (k2,t) p2)).
Symmetry; Auto.
Transitivity (hterm (cpol (a,b) p0)); Auto.
Save.
Theorem Tpol_Lex3_no_refl: (p:pol) ~(Tpol_Lex3 p p).
Induction p.
Red; Intros H; Inversion H.
Intros m p0 H.
Red; Intros H1.
Simple Inversion H1.
Discriminate H3.
Injection H6.
Injection H7.
Intros H8 H9 H10 H11.
Rewrite H11.
Rewrite H9.
Induction m; Simpl; Intros.
Apply (Ttm_nonrefl b); Trivial.
Injection H5; Injection H6.
Intros H9 H10 H11 H12.
Rewrite H9.
Rewrite H11; Intros; Elim H; Trivial.
Save.
Hints Resolve Tpol_Lex3_no_refl.
Theorem Tpol_Lex3_tran: (p,q,r:pol)(Tpol_Lex3 p q) -> (Tpol_Lex3 q r) -> (Tpol_Lex3 p r).
Intros p q r H; Generalize r; Clear r; Elim H.
Induction m.
Intros a b p0 fb fp0 r; Case r.
Intros H1; Inversion H1.
Induction m0; Intros.
Apply Tpol_Lex3_v.
Inversion H0; Auto.
Inversion H0; Auto.
Induction m1; Induction m2; Intros.
Simple Inversion H5.
Discriminate H8.
Rewrite <- H12.
Generalize H11; Clear H11.
Elim m3; Elim m0; Intros.
Apply Tpol_Lex3_car; Auto.
Simpl.
Simpl in H10.
Simpl in H4.
Apply Ttm_trans with b0 n; Auto.
Injection H11; Intros.
Rewrite <- H14; Auto.
Rewrite <- H11; Intros.
Apply Tpol_Lex3_car; Auto.
Simpl.
Simpl in H4.
Injection H10; Intros.
Rewrite H13; Trivial.
Intros.
Simple Inversion H5.
Intros.
Discriminate H8.
Rewrite <- H12.
Generalize H11; Clear H11.
Induction m1; Induction m2; Intros.
Apply Tpol_Lex3_car; Auto.
Simpl.
Simpl in H10.
Injection H11; Intros.
Rewrite <- H14; Trivial.
Rewrite <- H11; Intros.
Injection H10; Intros.
Rewrite H13.
Apply Tpol_Lex3_cdr; Auto.
Apply H4.
Rewrite <- H12; Trivial.
Save.
Theorem ext_full_Tpol: (m:monom)(p:pol)(full_pol (cpol m p))->(Tpol_Lex3 p (cpol m vpol)).
Induction m.
Intros a b p; Induction p.
Intros.
Apply Tpol_Lex3_v; Auto.
Inversion H; Auto.
Elim m0; Intros.
Apply Tpol_Lex3_car; Trivial.
Inversion H.
Inversion H5; Auto.
Inversion H; Auto.
Inversion H.
Inversion H5; Auto.
Simpl.
Inversion H.
Inversion H6; Auto.
Save.
Theorem Tpol_tran_mon: (m,m1,m2:monom)(p,q:pol)(Tpol_Lex3 (cpol m p) (cpol m1 q))
->(full_mon n m2)->(Ttm (mon_term m1) (mon_term m2))->
(Ttm (mon_term m) (mon_term m2)).
Induction m; Induction m1; Induction m2.
Intros a1 b1 p q H.
Inversion H.
Intros.
Simpl.
Simpl in H8.
Simpl in H10.
Apply Ttm_trans with b0 n; Auto.
Intro fb1.
Simpl; Trivial.
Save.
Hints Resolve Tpol_tran_mon.
Theorem Tpol_cpol_full: (m:monom)(p:pol)(full_mon n m)->
(full_pol p)->~(z_monom m)->(Tpol_Lex3 p (cpol m vpol))->
(full_pol (cpol m p)).
Induction m; Intros.
Apply full_pol_cons; Auto.
Inversion H2; Auto.
Generalize m1 H10 H5; Clear H8 H10 H5 m1.
Induction m1; Auto.
Inversion H10; Auto.
Save.
Lemma s_l_ord_pol: (x,y,z:pol)(full_pol (suma_app x y))->(full_pol (suma_app x z))->
(Tpol_Lex3 (suma_app x y) (suma_app x z))->(Tpol_Lex3 y z).
Induction x.
Simpl; Trivial.
Induction m.
Simpl; Intros.
Inversion H2.
Simpl in H11.
Cut ~(Ttm b b); Intros; Auto.
Elim H12; Auto.
Apply H; Auto.
Inversion H0; Auto.
Inversion H1; Auto.
Save.
Lemma s_t_ord_p: (b,c:Q)(t,t':term)(x:pol)
(full_pol (suma_app x (cpol (b,t) vpol)))->(full_pol (suma_app x (cpol (c,t') vpol)))->
(Tpol_Lex3 (suma_app x (cpol (b,t) vpol)) (suma_app x (cpol (c,t') vpol)))->
(Ttm t t').
Intros.
Cut (Tpol_Lex3 (cpol (b,t) vpol) (cpol (c,t') vpol)); Intros.
Inversion H2.
Simpl in H11; Auto.
Cut ~(Tpol_Lex3 vpol vpol); Intros; Auto.
Elim H13; Auto.
Apply s_l_ord_pol with x; Auto.
Save.
Lemma auxiliar2: (b:Q)(t:term)(x,x0:pol)(full_pol (suma_app x x0))->
(full n t)->((t':term)(term_in_pol x t')->(Ttm t t'))->
((t':term)(term_in_pol x0 t')->(Ttm t' t))->
(Tpol_Lex3 (suma_app x x0) (suma_app x (cpol (b,t) vpol))).
Induction x.
Simpl.
Induction x0; Auto.
Induction m; Intros.
Apply Tpol_Lex3_car; Trivial.
Simpl.
Inversion H0; Auto.
Inversion H0; Auto.
Simpl.
Apply H3.
Red.
Red; Intros.
Cut (eqQ (coef (cpol (a,b0) p) b0) a); Intros.
Cut (eqQ OQ a); Intros.
Inversion H0; Auto.
Apply eqQ_trans with (coef (cpol (a,b0) p) b0); Auto.
Apply coef_first; Auto.
Induction m.
Induction x0.
Simpl; Intros.
Cut p=(suma_app p vpol); Intros; Auto.
Rewrite <- H4 in H0.
Inversion H0.
Apply Tpol_Lex3_cdr; Auto.
Apply H; Auto.
Rewrite <- H4; Auto.
Intros.
Apply H2.
Apply full_pol_cons_term; Auto.
Induction m0; Intros.
Cut (full_pol (cpol (a,b0) p)).
Simpl; Intros.
Simpl in H1.
Apply Tpol_Lex3_cdr; Auto.
Inversion H1; Auto.
Inversion H1; Auto.
Apply full_term_suma_app; Auto.
Inversion H5; Auto.
Apply H; Intros; Auto.
Inversion H1; Auto.
Apply H3; Auto.
Apply full_pol_cons_term; Auto.
Elim suma_app_full with (cpol (a,b0) p) (cpol (a0,b1) p0); Auto.
Save.
Definition pol_full := {p:pol | (full_pol p)}.
Definition Tpol_full: pol_full-> pol_full-> Prop :=
[a,b :pol_full ]
( <Prop> Case a of
[p : pol]
[H1 : (full_pol p)]
( <Prop> Case b of [q: pol] [H2: (full_pol q)] (Tpol_Lex3 p q) end )
end ).
Fixpoint pol_Lex_rec [p:pol]: (list term) := Cases p of
vpol => (nil ?)
|(cpol (k,t) p1) => (cons t (pol_Lex_rec p1))
end.
Lemma pol_rec_Tpol_lex3: (p,q: pol) (Tpol_Lex3 p q)->(Ltl ? Ttm (pol_Lex_rec p) (pol_Lex_rec q)).
Intros.
Elim H.
Induction m; Simpl; Intros.
Apply (Lt_nil term).
Induction m1; Induction m2; Simpl; Intros.
Apply (Lt_hd term); Trivial.
Simpl; Intros.
Apply (Lt_tl term); Trivial.
Save.
Hints Resolve pol_rec_Tpol_lex3.
Definition Listterm_desc:= [p:pol] (Desc term Ttm (pol_Lex_rec p)).
Lemma Desc_rev: (l:(list term))(t,b:term)(Ttm b t)->(Desc term Ttm (cons b l))->
(Desc term Ttm (cons t (cons b l))).
Cut (l':(list term))(b,t:term)
(Ttm b t)->
(Desc term Ttm l')->
(l:?) l'=(cons b l)->
(Desc term Ttm (cons t l')); EAuto.
Induction 2; Intros.
Discriminate H1.
Apply d_conc with x:=x y:=t l:=(nil term).
Injection H1; Intros.
Rewrite -> H3; Trivial.
Simpl; Constructor.
Apply d_conc with x:=x y:=y l:=(cons t l); Trivial.
Apply H3 with (tail (app l (cons y (nil ?)))).
NewDestruct l; Simpl; Simpl in H4.
Inversion H4; Trivial.
Inversion H4; Trivial.
Save.
Lemma Desc_rev_pol: (p:pol)(t,b:term)(Ttm b t)->(Desc term Ttm (cons b (pol_Lex_rec p)))->
(Desc term Ttm (cons t (cons b (pol_Lex_rec p)))).
Intros.
Apply Desc_rev; Auto.
Save.
Lemma ayuda_full_imp_lis_desc: (p:pol)(t:term)(full_pol p)->
(full n t)->(low_pol t p)->(Desc term Ttm (cons t (pol_Lex_rec p))).
Induction p.
Intros; Simpl.
Apply d_one.
Induction m; Intros; Simpl.
Apply Desc_rev_pol.
Inversion H2; Auto.
Apply H; Inversion H0; Auto.
Save.
Theorem full_imp_lis_desc: (p:pol)(full_pol p)->(Listterm_desc p).
Induction p.
Intros.
Red.
Simpl.
Apply d_nil.
Induction m; Intros.
Inversion H0.
Red.
Simpl.
Apply ayuda_full_imp_lis_desc; Auto.
Save.
Definition pol_recpol: pol_full->(Pow term Ttm) :=
[a: pol_full]
( <(Pow term Ttm)> Case a of
[p: pol]
[H: (full_pol p)] (exist (list term) (Desc term Ttm) (pol_Lex_rec p) (full_imp_lis_desc p H))
end).
Lemma pol_rec_Tpol:(p,q: pol_full)(Tpol_full p q)->
(lex_exp term Ttm (pol_recpol p)(pol_recpol q)).
Intros p q; Case p; Case q.
Unfold lex_exp; Simpl; Intros.
Apply pol_rec_Tpol_lex3; Trivial.
Save.
Theorem Tpol_full_wf: (well_founded pol_full Tpol_full).
LApply (wf_inverse_image pol_full (Pow term Ttm) (lex_exp term Ttm)
pol_recpol).
Intros H'3.
Apply wf_incl
with R2:=[x,y:pol_full]
(lex_exp term Ttm (pol_recpol x) (pol_recpol y)).
Red; Intros.
Apply pol_rec_Tpol; Trivial.
Auto.
Apply (wf_lex_exp term Ttm); Apply Ttm_wf.
Save.
Definition inc: pol_full -> pol :=
[p:pol_full] (Case p of
[q:pol][H:(full_pol q)] q
end).
Fixpoint inc_list [p:(list pol_full)]: (list pol) := Cases p of
nil => (nil ?)
|(cons p1 p2) => (cons (inc p1) (inc_list p2))
end.
Lemma ex_fpol:(f:pol_full){g:pol|(full_pol g)/\(equpol (inc f) g)}.
Induction f.
Simpl; Intros.
Split with x; Auto.
Save.
Lemma ex_fpol_eq:(f:pol)(full_pol f)->{g:pol_full|(equpol f (inc g))}.
Intros.
Split with (exist pol [x:pol](full_pol x) f H); Simpl; Auto.
Save.
Lemma pol_f_impl_f_pol:(f:pol_full)(full_pol (inc f)).
Induction f; Intros; Simpl; Trivial.
Save.
Hints Resolve pol_f_impl_f_pol.
Lemma pol_f_impl_f_term:(f:pol_full)(full_term_pol (inc f)).
Intros.
Cut (full_pol (inc f)); Intros; Auto.
Save.
Index
This page has been generated by coqdoc