Library Monomes_tes
Require Export divisib_tes.
Require Export Corps_tes.
Definition monom := Q*term.
Definition z_monom := [m:monom]Cases m of
(pair q t) => (eqQ q OQ) end.
Hints Unfold z_monom.
Definition equmon :=[m,m':monom]
Cases m m' of
(pair c t)(pair c' t') => ((eqQ c OQ)/\(eqQ c' OQ))
\/((t=t')/\(eqQ c c'))
end.
Hints Unfold equmon.
Lemma equmon_refl: (m:monom) (equmon m m).
Intro m; Elim m; Auto.
Save.
Hints Resolve equmon_refl.
Lemma equmon_sym: (m,m':monom)(equmon m m')->(equmon m' m).
Intros m m'; Elim m; Elim m'.
Intros.
Inversion H.
Red.
Red in H.
Left.
Elim H0; Auto.
Red.
Right.
Elim H0; Auto.
Save.
Hints Resolve equmon_sym.
Lemma equmon_trans: (m1,m2,m3:monom) (equmon m1 m2)->(equmon m2 m3)->
(equmon m1 m3).
Intros m1 m2 m3; Elim m1; Elim m2; Elim m3.
Intros.
Red.
Red in H; Red in H0.
Elim H; Elim H0; Intros.
Left.
Elim H1; Elim H2; Auto.
Left.
Elim H1; Elim H2.
Split; Auto.
Apply eqQ_trans with a0; Auto.
Left.
Elim H1; Elim H2.
Split; Auto.
Apply eqQ_trans with a0; Auto.
Right.
Elim H1; Elim H2; Intros.
Split.
Transitivity b0; Assumption.
Apply eqQ_trans with a0; Trivial.
Save.
Hints Resolve equmon_trans.
Lemma equmon_z: (m,m':monom)(z_monom m)->(equmon m m')->(z_monom m').
Intros m m'; Red.
Case m'.
Unfold z_monom.
Case m; Intros.
Inversion H0.
Elim H1; Trivial.
Elim H1; Intros.
Apply eqQ_trans with q; Auto.
Save.
Hints Resolve equmon_z.
Lemma z_equmon:(m,m':monom)(z_monom m)->(z_monom m')->(equmon m m').
Intros m m'; Unfold z_monom.
Case m; Case m'; Auto.
Save.
Hints Resolve z_equmon.
Definition mon_coef := [m:monom]<Q> Case m of
[q:Q][t:term]q end.
Hints Unfold mon_coef.
Definition mon_term := [m:monom]<term> Case m of
[q:Q][t:term]t end.
Hints Unfold mon_term.
Definition monom_op := [m:monom]((multQ_neg (mon_coef m)),(mon_term m)).
Hints Unfold monom_op.
Definition mult_mon:= [m1,m2:monom]Cases m1 m2 of
(pair k1 t1) (pair k2 t2) => (pair ? ? (multQ k1 k2) (term_mult t1 t2))
end.
Hints Unfold mult_mon.
Definition full_mon: nat->monom -> Prop :=
[n:nat][m:monom]
Cases m of
(pair c t) => (full n t)
end.
Hints Unfold full_mon.
Lemma mul_mon_full: (m,m':monom)(n:nat)(full_mon n m)->(full_mon n m')->
(full_mon n (mult_mon m m')).
Intros m m'.
(Elim m; Elim m'; Intros).
Simpl.
Auto.
Save.
Hints Resolve mul_mon_full.
Lemma mult_mon_conm: (m,m':monom)
(equmon (mult_mon m m') (mult_mon m' m)).
Intros m m'.
Elim m.
Elim m'.
Intros.
Simpl; Auto.
Save.
Hints Resolve mult_mon_conm.
Lemma mult_mon_asoc: (m,m1,m2:monom)
(equmon (mult_mon m (mult_mon m1 m2)) (mult_mon (mult_mon m m1) m2)).
Intros m m1 m2.
(Elim m; Elim m1; Elim m2).
Intros.
Simpl.
Right; Auto.
Save.
Hints Resolve mult_mon_asoc.
Lemma mult_mon_comp_l: (m,m1,m2:monom)(equmon m1 m2)->
(equmon (mult_mon m1 m) (mult_mon m2 m)).
Intros m m1 m2.
(Elim m; Elim m1; Elim m2; Intros).
Red in H.
Simpl.
(Elim H; Intros).
Left.
(Elim H0; Intros).
Auto.
Right.
(Elim H0; Intros).
Split.
(Rewrite -> H1; Auto).
Auto.
Save.
Hints Resolve mult_mon_comp_l.
Lemma mult_mon_perm: (m,m1,m2:monom)
(equmon (mult_mon (mult_mon m m1) m2) (mult_mon m1 (mult_mon m m2))).
Intros.
Apply equmon_trans with (mult_mon (mult_mon m1 m) m2); Auto.
Save.
Hints Resolve mult_mon_perm.
Definition mult_Q_monom:= [c:Q][m:monom]Cases m of
(pair c1 t) => (pair ? ? (multQ c c1) t) end.
Hints Unfold mult_Q_monom.
Lemma monot_zmonom: (m,m':monom)((z_monom m)\/(z_monom m'))->
(z_monom (mult_mon m m')).
Intros m m'.
Elim m.
Elim m'.
Intros y y0 y1 y2.
Induction 1.
Intros.
Simpl.
Auto.
Unfold z_monom.
Simpl.
Auto.
Save.
Hints Resolve monot_zmonom.
Lemma monot_no_zmonom: (m,m':monom)(~(z_monom m)/\~(z_monom m'))->
(~(z_monom (mult_mon m m'))).
Intros m m'.
Elim m.
Elim m'.
Intros y y0 y1 y2.
Induction 1.
Intros.
Simpl.
Auto.
Save.
Hints Resolve monot_no_zmonom.
Definition div_mon:= [m1,m2:monom]Cases m1 m2 of
(k1,t1) (k2,t2) => ((divQ k1 k2),(div_term t1 t2))
end.
Lemma z_monom_dec: (m:monom){z_monom m}+{~(z_monom m)}.
(Induction m; Intros).
(Elim (decQ a); Auto).
Save.
Hints Resolve z_monom_dec.
Lemma dec_coef_monom: (m:monom){(eqQ (mon_coef m) OQ)}+
{~(eqQ (mon_coef m) OQ)}.
Auto.
Save.
Hints Resolve dec_coef_monom.
Lemma mon_opp_term : (m:monom)
(mon_term m)=(mon_term (monom_op m)).
Induction m; Simpl;Trivial.
Save.
Index
This page has been generated by coqdoc