Library Polynomes_tes


Require Export Monomes_tes.




Parameter n:nat.




Inductive pol : Set :=

  vpol : pol

| cpol : monom -> pol->pol. 




Inductive full_term_pol: pol -> Prop :=

  full_term_pol_nil: (full_term_pol vpol)

 | full_term_pol_cons : (t:term)(a:Q)(p:pol)(full n t)->

   (full_term_pol p)->(full_term_pol (cpol (a,t) p)).

Hints Resolve full_term_pol_nil full_term_pol_cons.




Fixpoint mult_Q_pol [c:Q;p:pol]: pol:=

   Cases p of

      vpol   =>   vpol

    | (cpol m1 p1) => (cpol (mult_Q_monom c m1) (mult_Q_pol c p1)) 

   end.




Lemma full_term_cpol: (m:monom)(full_mon n m)->

   (full_term_pol (cpol m vpol)).

Induction m; Intros.

Apply full_term_pol_cons; Auto.

Save.

Hints Resolve full_term_cpol.




Lemma full_term_pol_mon: (m:monom)(p:pol)(full_term_pol (cpol m p))->

   (full_mon n m).

Intros m.

Elim m; Intros.

Red.

Inversion H; Auto.

Save.

Hints Resolve full_term_pol_mon.




Lemma full_tm_dec : (t:term){(full n t)}+{~(full n t)}.

Intros t ; Elim (eq_nat_dec n (length t));

   [Left; Auto | Right; Unfold full; Auto].

Save.




Lemma full_pol_tm_dec : (p:pol){(full_term_pol p)}+{~(full_term_pol p)}.

Induction p.

Left; Auto.

Induction m; Intros c t p' HR.

Elim (full_tm_dec t).

Intros vrai; Elim HR.

Intros v2; Left; Auto.

(Intros f2; Right ; Unfold not; Intros f3).

(Apply f2; Inversion f3; Auto).




(Intros f2; Right ; Unfold not; Intros f3; Apply f2; Inversion f3; Auto).




Save.
Index
This page has been generated by coqdoc