Require Import Setoid. Definition Is_true (b:bool) : Prop:= match b with |true => True |false => False end. Reserved Notation "x ++ y" (at level 50, left associativity). Reserved Notation "x -- y" (at level 50, left associativity). Reserved Notation "x ** y" (at level 40, left associativity). Reserved Notation "-- x" (at level 35, right associativity). Reserved Notation "x == y" (at level 70, no associativity). Reserved Notation "x ?== y" (at level 70, no associativity). Reserved Notation "x + y" (at level 50, left associativity). Reserved Notation "x -y" (at level 50, left associativity). Reserved Notation "x * y" (at level 40, left associativity). Reserved Notation "- x" (at level 35, right associativity). Reserved Notation " x != y "(at level 70, no associativity). Reserved Notation "x '+ y" (at level 50, left associativity). Reserved Notation "x '- y" (at level 50, left associativity). Reserved Notation "x '* y" (at level 40, left associativity). Reserved Notation "'- x" (at level 35, right associativity). Reserved Notation " x '= y "(at level 70, no associativity). Section COEF_RING. Variable C : Type. Record coef_set : Type := mk_cset{ CO : C; CI : C; Ceq : C -> C -> Prop; Cadd : C -> C -> C; Cmul : C -> C -> C; Csub : C -> C -> C; Copp : C -> C }. Variable coef : coef_set. Definition cadd := (Cadd coef). Definition cmul := (Cmul coef). Definition copp := (Copp coef). Definition csub := (Csub coef). Definition ceq := (Ceq coef). Notation "x ++ y" := (cadd x y). Notation "x ** y" := (cmul x y). Notation "x -- y" := (csub x y). Notation " -- x" := (copp x). Notation "x == y":=(ceq x y). Record coef_eq :Prop := mk_ceq{ Ceq_refl : forall x, x == x; Ceq_sym : forall x y, x == y -> y == x; Ceq_trans : forall x y z, x == y -> y == z -> x == z; Cadd_ext : forall x1 x2 y1 y2, x1 == x2 -> y1 == y2 -> x1 ++ y1 == x2 ++ y2; Cmul_ext : forall x1 x2 y1 y2, x1 == x2 -> y1 == y2 -> x1 ** y1 == x2 ** y2; Copp_ext : forall x1 x2, x1 == x2 -> -- x1 == -- x2 }. Variable eq_th : coef_eq. Definition ceq_refl := Ceq_refl eq_th. Definition ceq_sym := Ceq_sym eq_th. Definition ceq_trans := Ceq_trans eq_th. Definition cadd_ext := Cadd_ext eq_th. Definition cmul_ext := Cmul_ext eq_th. Definition copp_ext := Copp_ext eq_th. Definition cO := CO coef. Definition cI := CI coef. End COEF_RING. Section POL1 . Variable C:Type. Variable coef : coef_set C. Definition eqC:=(ceq C coef). Definition addC:=(cadd C coef). Definition mulC:=(cmul C coef). Definition oppC:= (copp C coef). Definition subC:=(csub C coef). Definition c0:=(cO C coef). Definition c1:=(cI C coef) . Notation "x ++ y" := (addC x y). Notation "x ** y" := (mulC x y). Notation "x -- y" := (subC x y). Notation " -- x" := (oppC x). Notation "x == y":=(eqC x y). (* Ring structure over coefficients*) Record coef_theory : Prop := mk_ct { Cadd_0_l : forall x, c0 ++ x == x; Cadd_sym : forall x y, x ++ y == y ++ x; Cadd_assoc : forall x y z, x ++ (y ++ z) == (x ++ y) ++ z; Cmul_1_l : forall x, c1** x == x; Cmul_sym : forall x y, x ** y == y ** x; Cmul_assoc : forall x y z, x ** (y ** z) == (x ** y) ** z; Cdistr_l : forall x y z, (x ++ y) ** z == (x ** z) ++ (y ** z); Csub_def : forall x y, x -- y == x ++ --y; Copp_def : forall x, x ++ (-- x) == c0 }. Variable CT : coef_theory . Definition cadd_0_l := (Cadd_0_l CT). Definition cadd_sym := (Cadd_sym CT). Definition cadd_assoc := (Cadd_assoc CT). Definition cmul_1_l := (Cmul_1_l CT). Definition cmul_sym := (Cmul_sym CT). Definition cmul_assoc := (Cmul_assoc CT). Definition cdistr_l := (Cdistr_l CT). Definition csub_def := (Csub_def CT). Definition copp_def := (Copp_def CT). Variable eq_th : coef_eq C coef. Lemma Coef_setoid : Setoid_Theory C eqC. Proof. constructor. exact (ceq_refl C coef eq_th). exact (ceq_sym C coef eq_th). exact (ceq_trans C coef eq_th). Qed. Add Setoid C eqC Coef_setoid. Add Morphism addC: cadd_ex. exact (Cadd_ext C coef (eq_th)). Qed. Add Morphism mulC: cmul_ex. exact (Cmul_ext C coef (eq_th)). Qed. Add Morphism oppC: copp_ex. exact (Copp_ext C coef (eq_th)). Qed. Hint Resolve ceq_sym ceq_trans ceq_refl cadd_ext cmul_ext copp_ext : ceq_spec. (*pour jouer : reecriture setoid a une occurence apres l'abstraction par pattern*) Ltac rewrite_pattern t := match goal with |- ?a ?b => let H := fresh "H" in (assert (H : forall c1 c2, c1==c2 -> (a c1)->(a c2)); intros;simpl in *; eauto with ceq_spec; apply (H _ _ t)) |_ => idtac "not an application" end. (*some lemmas about the ring structure of coefficients C*) Lemma copp_0 : -- c0==c0 . Proof. rewrite <- (cadd_0_l (--c0)). unfold eqC. unfold oppC;unfold c0. apply copp_def. Qed. Lemma cmul_0_l : forall x, c0 ** x == c0. Proof. intro x; setoid_replace (c0**x) with ((c0++c1)**x ++ --x). rewrite (cdistr_l c0 c1 x);rewrite (cmul_1_l x). rewrite <- (cadd_assoc (c0**x) x (--x)). rewrite (copp_def x);rewrite (cadd_sym (c0**x) c0). rewrite (cadd_0_l (c0**x));unfold eqC;apply ceq_refl;apply eq_th. rewrite (cadd_0_l c1); rewrite (CT.(Cmul_1_l) x). rewrite (copp_def x);unfold eqC;apply ceq_refl. apply eq_th. Qed. Lemma cmul_0_r : forall x, x**c0 == c0. Proof. intros;rewrite (cmul_sym x c0);apply cmul_0_l. Qed. Lemma cmul_1_r:forall x, x**c1==x. Proof. intros;rewrite (cmul_sym x c1);apply cmul_1_l. Qed. Lemma copp_mul_l : forall x y, --(x ** y) == --x ** y. Proof. intros x y;rewrite <-(cadd_0_l (-- x ** y)). rewrite (cadd_sym c0 (--x**y)). rewrite <-(copp_def (x**y)). rewrite (cadd_assoc (-- x ** y) (x**y) (--(x**y))). rewrite <- (cdistr_l (--x) x y). rewrite (cadd_sym (--x) x);rewrite (copp_def x). rewrite (cmul_0_l y);rewrite (cadd_0_l (--(x**y)));unfold eqC;apply ceq_refl;apply eq_th. Qed. Lemma copp_mul_r : forall x y, --(x**y) == x ** --y. Proof. intros. rewrite (cmul_sym x y);rewrite (cmul_sym x (-- y)). apply copp_mul_l. Qed. Lemma copp_add : forall x y, --(x ++ y) == --x ++ --y. Proof. intros x y;rewrite <- (cadd_0_l (--(x++y))). rewrite <- (copp_def x). rewrite <- (cadd_0_l (x ++ -- x ++ -- (x ++ y))). rewrite <- (copp_def y). rewrite (cadd_sym x (--x)). rewrite (cadd_sym y (--y)). rewrite <- (cadd_assoc (--y) y (-- x ++ x ++ -- (x ++ y))). rewrite <- (cadd_assoc (-- x) x (--(x ++ y))). rewrite (cadd_assoc y (-- x) (x ++ -- (x ++ y))). rewrite (cadd_sym y (--x)). rewrite <- (cadd_assoc (-- x) y (x ++ -- (x ++ y))). rewrite (cadd_assoc y x (--(x++y))). rewrite (cadd_sym y x);rewrite (copp_def (x++y)). rewrite (cadd_sym (--x) c0);rewrite (cadd_0_l (--x)). apply cadd_sym. Qed. Lemma cdistr_r : forall x y z, x**(y ++ z) == x**y ++ x**z. Proof. intros. rewrite (cmul_sym x (y++z));rewrite (cmul_sym x y);rewrite (cmul_sym x z); apply cdistr_l. Qed. Lemma cadd_0_r : forall x, x ++ c0 == x. Proof. intro; rewrite (cadd_sym x c0); apply cadd_0_l. Qed. Lemma cadd_assoc1 : forall x y z, (x ++ y) ++ z == (y ++ z) ++ x. Proof. intros;rewrite <-(cadd_assoc x y z). rewrite (cadd_sym x (y++z));unfold eqC;apply ceq_refl;apply eq_th. Qed. Lemma cadd_assoc2 : forall x y z, (y ++ x) ++ z == (y ++ z) ++ x. Proof. intros; rewrite <- (cadd_assoc y x z); rewrite (cadd_sym x z); apply cadd_assoc. Qed. Lemma cmul_assoc1 : forall x y z, (x ** y) ** z == (y ** z) ** x. Proof. intros;rewrite <-(cmul_assoc x y z). rewrite (cmul_sym x (y**z));unfold eqC;apply ceq_refl;apply eq_th. Qed. Lemma cmul_assoc2 : forall x y z, (y ** x) ** z == (y ** z) ** x. Proof. intros; rewrite <- (cmul_assoc y x z); rewrite (cmul_sym x z); apply cmul_assoc. Qed. Lemma copp_opp : forall x, -- --x == x. Proof. intros x; rewrite <- (Cadd_0_l CT (-- --x)). rewrite <- (Copp_def CT x). rewrite <- (Cadd_assoc CT x (--x) (-- --x)); rewrite (Copp_def CT (--x)). rewrite (Cadd_sym CT x c0);apply(Cadd_0_l CT x). Qed. (*Tactiques simplification des expressions dans C*) Ltac cgen := repeat (progress (match goal with | |- context [-- c0] => rewrite copp_0 | |- context [c0 ++ ?x] => rewrite (cadd_0_l x) | |- context [?x ++ c0] => rewrite (cadd_0_r x) | |- context [c1 ** ?x] => rewrite (cmul_1_l x) | |- context [ c0 ** ?x] => rewrite (cmul_0_l x) | |- context [?x ** c0] => rewrite (cmul_0_r x) | |- context [(copp ?x) ** ?y] => rewrite <- (copp_mul_l x y) | |- context [?x ** (--?y)] => rewrite <- (copp_mul_r x y) | |- context [-- ( ?x ++ ?y)] => rewrite (copp_add x y) | |- context [ ?x -- ?y] => rewrite (csub_def x y) | |- context [ ( ?x ++ ?y) ** ?z] => rewrite (cdistr_l x y z) | |- context [?z ** (?x ++ ?y)] => rewrite (cdistr_r x y z) | |- context [ ?x ++ (?y ++ ?z)] => rewrite (cadd_assoc x y z) | |- context [?x ** (?y ** ?z)] => rewrite (cmul_assoc x y z) | |- context [-- (-- ?x)] => rewrite (copp_opp x) | |- ?x == ?x => apply ceq_refl end)). Ltac cadd_push x := repeat (progress (match goal with | |- context [ (?y ++ x) ++ ?z] => rewrite (cadd_assoc2 x y z) | |- context [(x ++ ?y) ++ ?z] => rewrite (cadd_assoc1 x y z) end)). Ltac cmul_push x := repeat (progress (match goal with | |- context [(?y ** x) ** ?z] => rewrite (cmul_assoc2 x y z) | |- context [(x ** ?y) ** ?z] => rewrite (cmul_assoc1 x y z) end)). (* one variable polynomials over C*) (* PX P c=c+P*X *) Inductive Pol1:Type:= |Pc : C-> Pol1 |PX : Pol1 -> C -> Pol1. Definition PO:= (Pc c0). Definition PI:=(Pc c1). Fixpoint ev_Pol1(P:Pol1)(x:C){struct P}:C:= match P with |Pc c=>c |PX P1 c=>cadd C coef c (cmul C coef x (ev_Pol1 P1 x)) end. (*Equality over polynomials,not in normal forms*) Inductive Pol1Eq:Pol1 -> Pol1 -> Prop := |Eq1_Pc_Pc : forall p q: C, (eqC p q)->(Pol1Eq (Pc p) (Pc q)) |Eq1_Pc_PX : forall p q: C, forall Q1:Pol1, (eqC p q)->(Pol1Eq Q1 PO)->(Pol1Eq (Pc p) (PX Q1 q)) |Eq1_PX_Pc : forall p q: C, forall P1:Pol1, (eqC p q)->(Pol1Eq P1 PO)->(Pol1Eq (PX P1 p) (Pc q)) |Eq1_PX_PX : forall p q:C, forall P1 Q1 :Pol1, (eqC p q)->(Pol1Eq P1 Q1)->(Pol1Eq (PX P1 p) (PX Q1 q)). Axiom dec_EqPol:forall P Q,{Pol1Eq P Q}+{~(Pol1Eq P Q)}. Fixpoint degre1(P:Pol1):nat:=match P with |Pc _ =>O |PX P1 _=>match (dec_EqPol P1 PO) with left _=>O |right _=>S (degre1 P1) end end. Require Import max. (*Addition over polynomials*) Fixpoint Pol1_add(P Q:Pol1){struct P}:Pol1 := match P, Q with |Pc p, Pc q => Pc (p ++ q) |Pc p, PX Q1 q => PX Q1 (p ++ q) |PX P1 p, Pc q => PX P1 (p ++ q) |PX P1 p, PX Q1 q => PX (Pol1_add P1 Q1) (p ++ q) end. (*Product poly * cst*) Fixpoint Pol1_mulc(P:Pol1)(q:C){struct P}:Pol1:= match P with |Pc p => Pc (q** p) |PX P1 p => PX (Pol1_mulc P1 q) (p ** q) end. (*Product over polynomial*) Fixpoint Pol1_mul(P Q:Pol1){struct P}:Pol1 := match P with |Pc p => Pol1_mulc Q p |PX P1 p=> (Pol1_add (PX (Pol1_mul P1 Q) c0) (Pol1_mulc Q p)) end. (*Opposite *) Fixpoint Pol1_opp(P:Pol1):Pol1 := match P with |Pc p => Pc (-- p) |PX P1 p => PX (Pol1_opp P1) (-- p) end. (*Subtraction*) Definition Pol1_sub(P Q:Pol1):=(Pol1_add P (Pol1_opp Q)). (* Some notations *) Notation "x != y" := (Pol1Eq x y). Notation "x + y" := (Pol1_add x y). Notation "x * y" := (Pol1_mul x y). Notation "x - y" := (Pol1_sub x y). Notation "- x" := (Pol1_opp x). (*Pol1Eq is a setoid equality*) Lemma Pol1Eq_refl :forall P, P != P. Proof. induction P;constructor; unfold eqC;try apply ceq_refl;trivial. Qed. Lemma Pol1Eq_sym : forall P Q, P != Q -> Q != P. Proof. intros P Q; induction 1; constructor; unfold eqC;try apply ceq_sym;trivial. Qed. Lemma Pol1Eq_transO : forall P, P!=PO -> forall Q, P != Q-> Q != PO. Proof. induction P; inversion 1;subst; try constructor;try apply (ceq_trans c c0 q);trivial; intros;inversion H0;subst;unfold PO; constructor. unfold eqC;apply (ceq_trans C coef eq_th q c c0); auto; apply ceq_sym;auto. unfold eqC;apply (ceq_trans C coef eq_th q c c0); auto; apply ceq_sym;auto. auto. unfold eqC;apply (ceq_trans C coef eq_th q c c0); auto; apply ceq_sym;auto. unfold eqC;apply (ceq_trans C coef eq_th q c c0); auto; apply ceq_sym;auto. apply IHP; trivial;apply Pol1Eq_sym;trivial. Qed. Lemma Pol1Eq_trans : forall P Q, P != Q -> forall R, Q != R -> P != R. Proof. intros P Q;induction 1;intros; inversion H0;subst; try constructor; try apply (ceq_trans C coef eq_th p q q0);try apply eq_th;trivial;inversion H1; subst; constructor; try apply (ceq_trans C coef eq_th p q); trivial; try apply IHPol1Eq; trivial. apply (Pol1Eq_transO (Pc p0)); trivial. apply (Pol1Eq_transO (PX P1 p0));trivial. apply Pol1Eq_sym;trivial. apply Pol1Eq_sym;trivial. Qed. Axiom Pol1Eq_Pc_PX:forall (c c1:C) P, (Pc c) !=(PX P c1) ->P !=PO. Axiom Pol1Eq_PX_PX:forall (c c1:C) P Q,(PX Q c)!= (PX P c1) ->P !=Q. Axiom Pol1Eq_PX_PX_C:forall (c c1:C) P Q,(PX Q c)!=(PX P c1) ->c==c1. Axiom Pol1Eq_PC_Ceq:forall (c c1:C) , (Pc c) !=(Pc c1) ->c==c1. Axiom Pol1Eq_PX_Pc:forall (c c1:C) P, (Pc c) !=(PX P c1) ->c==c1. Variable degC:C->nat. Hypotheses degC_Pc:forall c c1,Pc c!=Pc c1->degC c=degC c1. Hypotheses degC_mul:forall c c1,degC (c**c1)=plus (degC c) (degC c1). Fixpoint deg1(P:Pol1):nat:= match P with |Pc c =>degC c |PX P1 c=>match (dec_EqPol P1 PO) with left _=>degC c |right _=>max_2_elt (S (deg1 P1)) (degC c) end end. Lemma Pol1Eq_deg_eq:forall p q,Pol1Eq p q->deg1 p=deg1 q. induction p ;induction q. simpl;intros;auto. simpl;intros. case (dec_EqPol q PO) . intro. assert (PX q c2!=Pc c2). apply Eq1_PX_Pc;try apply (ceq_refl C coef);try apply eq_th;auto. apply degC_Pc. apply Pol1Eq_trans with (PX q c2);auto. simpl;intros. absurd (Pol1Eq q PO ). auto. apply (Pol1Eq_Pc_PX c c2);auto. simpl;intros. case (dec_EqPol p PO ). intro;assert (PX p c!=Pc c). apply Eq1_PX_Pc;try apply (ceq_refl C coef);try apply eq_th;auto. apply degC_Pc. apply Pol1Eq_trans with (PX p c);auto. apply Pol1Eq_sym;auto. simpl;intros. absurd (Pol1Eq p PO ). auto. apply (Pol1Eq_Pc_PX c2 c);apply (Pol1Eq_sym);auto. simpl;intros. case (dec_EqPol p PO ). case (dec_EqPol q PO ). intros;assert (PX p c!=Pc c). apply Eq1_PX_Pc;try apply (ceq_refl C coef);try apply eq_th;auto. apply degC_Pc. apply Pol1Eq_trans with (PX p c);auto. apply Pol1Eq_sym;auto. assert (PX q c2!=Pc c2). apply Eq1_PX_Pc;try apply (ceq_refl C coef);try apply eq_th;auto. apply Pol1Eq_trans with (PX q c2);auto. intros. absurd (Pol1Eq q PO ). auto. apply Pol1Eq_trans with p. apply Pol1Eq_PX_PX with (c:=c)(c1:=c2);auto. auto. case (dec_EqPol q PO ). simpl;intros. absurd (Pol1Eq p PO). auto. apply Pol1Eq_trans with q. apply Pol1Eq_sym;try apply eq_th1. apply Pol1Eq_PX_PX with (c:=c)(c1:=c2);auto. auto. simpl;intros. rewrite IHp with q. rewrite degC_Pc with c c2. auto . apply Eq1_Pc_Pc;apply Pol1Eq_PX_PX_C with q p;auto. apply Pol1Eq_sym;try apply eq_th1. apply Pol1Eq_PX_PX with (c:=c)(c1:=c2);auto. Qed. Axiom eq_deg1_mulc:forall (c:C) p,deg1 (Pol1_mulc p c)=plus (degC c) (deg1 p). (* induction p. simpl;intros. apply degC_mul. simpl;intros. case (dec_EqPol (Pol1_mulc p c) PO). simpl;intros. case (dec_EqPol p PO). simpl;intros;rewrite Arith.Plus.plus_comm;apply degC_mul. *) (*equality over polynomials is a morphism*) Lemma Pol1_setoid : Setoid_Theory Pol1 Pol1Eq. Proof. constructor. exact Pol1Eq_refl. exact Pol1Eq_sym. intros; apply Pol1Eq_trans with y;trivial. Qed. Add Setoid Pol1 Pol1Eq Pol1_setoid. (*Pol1 constructors are morphisms *) Add Morphism PX : PX_ext. Proof. intros;constructor;trivial. Qed. Add Morphism Pc : Pc_ext. Proof. intros;constructor;trivial. Qed. Lemma Pol1add_sym : forall P Q, P+Q != Q+P. Proof. induction P;destruct Q;simpl;constructor;auto; try apply (Cadd_sym CT); apply Pol1Eq_refl. Qed. Lemma Pol1add_extO : forall P, P != PO -> forall Q R, Q != R -> Q != P + R. Proof. induction P; intros H Q R; inversion 1;inversion H;subst; unfold PO; simpl;constructor; try (assert (A : c == c0); trivial; rewrite A; clear A; cgen);trivial. apply Pol1Eq_sym ; apply IHP;trivial;apply Pol1Eq_sym;trivial. apply (Pol1Eq_trans P1 PO);trivial; apply Pol1Eq_sym;trivial. auto. Qed. Lemma Pol1add_extO': forall P, P != PO -> forall Q R, Q != R -> Q != R + P. Proof. intros. apply (Pol1Eq_trans Q (P+R)); [apply Pol1add_extO;trivial| apply Pol1add_sym]. Qed. Lemma Pol1add_0_l : forall P, PO+P != P. Proof. induction P;unfold PO;simpl;constructor;try apply (Cadd_0_l CT). apply Pol1Eq_refl. Qed. Lemma Pol1add_0_l' : forall P, P+PO!=P. Proof. intros. apply (Pol1Eq_trans (P +PO) (PO+P)); [apply Pol1add_sym|apply Pol1add_0_l]. Qed. Lemma Pol1add_ext: forall P1 P2, P1 != P2 -> forall Q1 Q2, Q1 != Q2 -> P1 + Q1 != P2 + Q2. Proof. induction 1; intros A1 A2;induction 1; subst;simpl; try constructor; unfold eqC;unfold addC;try apply cadd_ext;auto. apply (Pol1Eq_trans (Q1 + Q0) (PO + PO)); [auto | apply Pol1add_0_l]. apply (Pol1Eq_trans P1 PO);trivial;apply Pol1Eq_sym;trivial. apply (Pol1add_extO Q1);trivial. apply (Pol1Eq_trans P1 PO);trivial;apply Pol1Eq_sym;trivial. apply Pol1Eq_sym; apply Pol1add_extO;trivial;apply Pol1Eq_sym;trivial. apply Pol1Eq_sym; apply Pol1add_extO;trivial. apply Pol1Eq_sym; trivial. apply Pol1add_extO';trivial. apply Pol1Eq_sym; apply Pol1add_extO'; [trivial |apply Pol1Eq_sym;trivial]. Qed. (*Pol addition is a morphism*) Add Morphism Pol1_add : Pol1_add_ext. Proof. intros; apply Pol1add_ext;trivial. Qed. Lemma Pol1_mulc_spec : forall P c, Pol1_mulc P c != P * (Pc c). Proof. induction P;intros;simpl;constructor. apply (Cmul_sym CT). rewrite (cadd_0_l (c**c2)); unfold eqC;apply ceq_refl;apply eq_th. auto. Qed. Lemma Pol1_add_spec : forall P Q p q, (PX P p) + (PX Q q) != PX (P+Q) (p ++ q). Proof. induction P;destruct Q; simpl;constructor; try constructor;unfold eqC; try apply ceq_refl ;try apply eq_th; apply Pol1Eq_refl. Qed. Lemma Pol1add_assoc : forall P Q R, P + (Q + R) != (P+Q)+R. Proof. induction P;induction Q; destruct R; intros;simpl;constructor; try rewrite (cadd_assoc c c2 c3);unfold eqC; try apply ceq_refl;try apply eq_th;try apply Pol1Eq_refl. apply IHP. Qed. Lemma Pol1_distr_PX : forall P Q q, P*(PX Q q) != (PX (P*Q) c0) + (Pol1_mulc P q). Proof. induction P;destruct Q; intros; try (simpl;constructor; rewrite (Cadd_0_l CR (q**c)); apply ceq_refl;apply eq_th). simpl;constructor; [rewrite (Cadd_0_l CT (q ** c)) | constructor]; unfold eqC;apply ceq_refl;apply eq_th. simpl;constructor. rewrite (Cadd_0_l CT (q ** c)); unfold eqC;apply ceq_refl;apply eq_th. constructor. unfold eqC;apply ceq_refl;apply eq_th. apply Pol1Eq_refl. Opaque Pol1_add. simpl. rewrite (IHP (Pc c2) q). rewrite (Pol1_mulc_spec P q). rewrite (Pol1_add_spec (PX (P * Pc c2) c0 + P * Pc q) (Pc (c ** c2)) c0 (q ** c)). rewrite (Pol1_add_spec (PX (P * Pc c2) c0 + Pc (c ** c2)) (P * Pc q) c0 (c**q)). constructor. rewrite (Cmul_sym CT q c); unfold eqC;apply ceq_refl;apply eq_th. rewrite <- (Pol1add_assoc (PX (P * Pc c2) c0) (P * Pc q ) (Pc (c ** c2))). rewrite (Pol1add_sym (P*(Pc q)) (Pc (c ** c2))). rewrite (Pol1add_assoc (PX (P * Pc c2) c0) (Pc (c ** c2)) (P*(Pc q))). apply Pol1Eq_refl. Opaque Pol1_add. simpl. rewrite (IHP (PX Q c2) q). rewrite (Pol1_mulc_spec P q). rewrite (Pol1_mulc_spec Q c). rewrite (Pol1_add_spec (PX (P * PX Q c2) c0 + P * Pc q) (PX (Q *Pc c) (c2 ** c)) c0 (q**c)). rewrite (Pol1_add_spec (PX (P * PX Q c2) c0 + PX (Q * Pc c) (c2 ** c)) (P * Pc q) c0 (c**q)). constructor. rewrite (Cmul_sym CT q c); unfold eqC;apply ceq_refl;apply eq_th. rewrite <- (Pol1add_assoc (PX (P * PX Q c2) c0 ) (P * Pc q) (PX (Q * Pc c) (c2 ** c))). rewrite (Pol1add_sym (P * Pc q) (PX (Q * Pc c) (c2 ** c))). rewrite (Pol1add_assoc (PX (P * PX Q c2) c0 ) (PX (Q * Pc c) (c2** c)) (P*Pc q)). apply Pol1Eq_refl. Transparent Pol1_add. Qed. Lemma Pol1mul_sym : forall P Q, P*Q != Q*P. Proof. induction P;intros; destruct Q;simpl;constructor; try cgen; try apply cmul_sym;unfold eqC; try apply ceq_refl;try apply eq_th. apply Pol1_mulc_spec. apply Pol1Eq_sym;apply Pol1_mulc_spec. rewrite (Pol1_distr_PX P Q c2). rewrite (Pol1_distr_PX Q P c). rewrite (IHP Q). rewrite <- (Pol1add_assoc (PX (Q * P) c0) (Pol1_mulc Q c) (Pol1_mulc P c2)). rewrite (Pol1add_sym (Pol1_mulc Q c) (Pol1_mulc P c2)). rewrite (Pol1add_assoc (PX (Q * P) c0) (Pol1_mulc P c2) (Pol1_mulc Q c) ). apply Pol1Eq_refl. Qed. Lemma Pol1_distr_PX_r : forall Q q P, (PX Q q)*P != (PX (Q*P) c0) +(Pol1_mulc P q). Proof. intros. rewrite (Pol1mul_sym (PX Q q) P); rewrite (Pol1mul_sym Q P); apply Pol1_distr_PX. Qed. Add Morphism Pol1_mulc : Pol1_mulc_ext. induction 1;intros;simpl;constructor;unfold PO in *; try rewrite (cmul_sym p c);try rewrite (cmul_sym q c2); unfold eqC;unfold mulC; try apply cmul_ext;trivial. induction Q1;simpl;constructor; inversion_clear H0; subst; try rewrite H2;try apply cmul_0_l; try apply cmul_0_r. apply IHQ1;trivial;intros;simpl in *. assert (PX (Pol1_mulc Q1 c) (c3 ** c) != Pc (c2 ** c0));try exact (IHPol1Eq H1). inversion_clear H4. rewrite (cmul_0_r c2);auto. simpl in *. rewrite <- (cmul_0_r c2);auto. auto. Qed. Lemma Pol1mul_0_l : forall Q, (Pc c0) * Q != (Pc c0). Proof. induction Q; intros; simpl;constructor. apply cmul_0_l. apply cmul_0_r. rewrite (Pol1_mulc_spec Q c0). rewrite (Pol1mul_sym Q (Pc c0)). auto. Qed. Lemma Pol1mul_0_r : forall Q, Q*(Pc c0)!= Pc c0. Proof. intros; rewrite (Pol1mul_sym Q (Pc c0)); apply Pol1mul_0_l. Qed. Lemma Pol1mul_ext_0_l : forall P Q, P != (Pc c0) -> P *Q !=(Pc c0). Proof. induction P;destruct Q;intros;inversion H;subst; simpl;constructor; try rewrite H2; try apply cmul_0_l;try apply cmul_0_r. rewrite (Pol1_mulc_spec Q c0);apply Pol1mul_0_r. rewrite H3; rewrite (cmul_0_l c2); apply cadd_0_l. auto. rewrite (cadd_0_l (c2**c));rewrite H3; apply cmul_0_r. rewrite H3. rewrite (Pol1_mulc_spec Q c0). rewrite (Pol1mul_0_r Q). assert (P*PX Q c2 != Pc c0). auto. rewrite H0;simpl;rewrite (cadd_0_l c0); apply Pol1Eq_refl. Qed. Lemma Pol1mul_ext_0_r : forall P Q, P != (Pc c0) -> Q*P !=(Pc c0). Proof. intros. rewrite (Pol1mul_sym Q P). apply Pol1mul_ext_0_l;trivial. Qed. Lemma Pol1mul_ext : forall P1 P2, P1 != P2 -> forall Q1 Q2, Q1 != Q2 -> P1*Q1 != P2*Q2. Proof. induction 1; intros;unfold PO in *. rewrite (Pol1mul_sym (Pc p) Q1); rewrite (Pol1mul_sym (Pc q) Q2). rewrite <- (Pol1_mulc_spec Q1 p); rewrite <- (Pol1_mulc_spec Q2 q). rewrite H0;rewrite H; apply Pol1Eq_refl. rewrite (Pol1mul_sym (PX Q1 q ) Q2). rewrite (Pol1_distr_PX Q2 Q1 q). assert (PX (Q2 * Q1) c0 != Pc c0). constructor;unfold eqC;try apply ceq_refl;try apply eq_th. rewrite (Pol1mul_sym Q2 Q1). unfold PO in *;rewrite <- (Pol1mul_0_l Q2). apply (IHPol1Eq Q2 Q2 (Pol1Eq_refl Q2)). rewrite H2. rewrite (Pol1mul_sym (Pc p) Q0). rewrite <- (Pol1_mulc_spec Q0 p). rewrite H1;rewrite H;fold PO; apply Pol1Eq_sym;apply Pol1add_0_l. rewrite (Pol1mul_sym (PX P1 p) Q1). rewrite (Pol1_distr_PX Q1 P1 p). assert (PX (Q1*P1) c0!=Pc c0). constructor;unfold eqC;try apply ceq_refl;try apply eq_th. rewrite (Pol1mul_sym Q1 P1). unfold PO;rewrite <- (Pol1mul_0_l Q1). apply (IHPol1Eq Q1 Q1 (Pol1Eq_refl Q1)). rewrite (Pol1mul_sym (Pc q) Q2);rewrite <- (Pol1_mulc_spec Q2 q). rewrite H2;rewrite H1;rewrite H. apply Pol1add_0_l. rewrite (Pol1mul_sym (PX P1 p) Q0); rewrite (Pol1mul_sym (PX Q1 q) Q2). rewrite (Pol1_distr_PX Q0 P1 p); rewrite (Pol1_distr_PX Q2 Q1 q). apply Pol1_add_ext. constructor;unfold eqC;try apply ceq_refl;try apply eq_th. rewrite (Pol1mul_sym Q0 P1);rewrite (Pol1mul_sym Q2 Q1); apply (IHPol1Eq Q0 Q2);trivial. rewrite H1; rewrite H;apply Pol1Eq_refl. Qed. Add Morphism Pol1_mul : Pol1mul_ext_morph. intros; apply Pol1mul_ext; trivial. Qed. Lemma Pol1opp_def : forall P, P + -P != Pc c0. Proof. induction P;simpl;constructor;try apply copp_def. auto. Qed. Lemma Pol1opp_ext : forall P Q, P != Q -> -P != -Q. Proof. induction P;destruct Q;subst;simpl;constructor;try inversion H;subst;unfold eqC;unfold oppC; try apply copp_ext;trivial. inversion_clear H4;simpl;unfold PO in *; constructor;try rewrite H0; try apply copp_0;unfold PO in *. rewrite <- (Pol1add_0_l (-P1)); fold PO in H1; rewrite <- H1; apply Pol1opp_def. rewrite <- (Pol1add_0_l (-P)). rewrite <- H4. rewrite (Pol1opp_def P);apply Pol1Eq_sym;auto. auto. Qed. Add Morphism Pol1_opp : Pol1opp_ext_morph. intros;apply Pol1opp_ext;trivial. Qed. Lemma Pol1_mulc_add : forall P Q c, Pol1_mulc(P + Q) c !=(Pol1_mulc P c) + (Pol1_mulc Q c). Proof. induction P;destruct Q;intros;simpl;constructor;try apply Pol1Eq_refl; try apply cdistr_l;try apply cdistr_r. rewrite (cmul_sym c3 c);apply cdistr_l. rewrite (cmul_sym c3 c2);apply cdistr_l. auto. Qed. Lemma Pol1_assoc_sym : forall a b c d, a + b + (c +d) != (a+c) +(b+d). Proof. intros. rewrite <- (Pol1add_assoc a b (c+d)). rewrite (Pol1add_assoc b c d). rewrite (Pol1add_sym b c). rewrite <- (Pol1add_assoc c b d). rewrite (Pol1add_assoc a c (b+d)). apply Pol1Eq_refl. Qed. Lemma Pol1distr_l : forall R P Q, (P+Q)*R != P*R + Q*R. Proof. induction R. induction P;destruct Q;intros; simpl;constructor; cgen;unfold eqC;try apply ceq_refl;try apply eq_th; try apply Pol1Eq_refl. auto. intros. rewrite (Pol1_distr_PX (P + Q) R c). rewrite (IHR P Q). assert (PX (P*R + Q*R) (c0++c0) != (PX (P*R) c0)+(PX (Q*R) c0)). apply Pol1Eq_sym. apply (Pol1_add_spec (P*R) (Q*R) c0 c0). generalize H;rewrite (cadd_0_l c0). intro. clear H. rewrite H0;rewrite (Pol1_mulc_add P Q c). rewrite (Pol1_assoc_sym (PX (P * R) c0) (PX (Q * R) c0) (Pol1_mulc P c) (Pol1_mulc Q c)). rewrite <- (Pol1_distr_PX P R c). rewrite <- (Pol1_distr_PX Q R c). apply Pol1Eq_refl. Qed. Lemma Pol1distr_r : forall P Q R, P*(Q + R) != P*Q + P*R. Proof. intros. rewrite (Pol1mul_sym P Q); rewrite (Pol1mul_sym P R); rewrite (Pol1mul_sym P (Q+R)); apply Pol1distr_l. Qed. Lemma Pol1mul_1_l : forall P, PI * P != P. Proof. induction P;intros;unfold PI in *;simpl;constructor; try rewrite (cmul_sym c c1); try apply cmul_1_l. rewrite (Pol1_mulc_spec P c1). rewrite (Pol1mul_sym P (Pc c1));trivial. Qed. Lemma Pol1mul_1_r : forall P, P *PI!= P. Proof. induction P;intros;unfold PI in *;simpl;constructor; try rewrite (cmul_sym c c1); try apply cmul_1_l. cgen;apply (ceq_refl C coef eq_th c). auto. Qed. Lemma Pol1mulc_comp : forall P c1 c2, (Pol1_mulc (Pol1_mulc P c1) c2) !=(Pol1_mulc P (c2**c1)). Proof. induction P;intros;simpl;constructor. apply cmul_assoc. rewrite (cmul_sym c3 c2);unfold eqC;apply ceq_sym;try apply eq_th; apply cmul_assoc. trivial. Qed. Lemma Pol1mul_Pc_PX : forall c P p, (Pc c)*(PX P p) != PX (Pol1_mulc P c) (c**p). Proof. destruct P;intros;simpl;rewrite (cmul_sym c p); apply Pol1Eq_refl. Qed. Lemma Pol1mul_PX_Pc : forall P p c, (PX P p)*(Pc c) != PX (Pol1_mulc P c) (p**c). Proof. intros; rewrite (Pol1mul_sym (PX P p) (Pc c)); rewrite (cmul_sym p c); apply Pol1mul_Pc_PX. Qed. Lemma Pol1mulc_assoc : forall P Q c, (Pol1_mulc (P*Q) c) != (Pol1_mulc P c)*Q. Proof. induction P;destruct Q;intros;simpl;constructor;cgen; try (cmul_push c1;unfold eqC;apply ceq_refl;try apply eq_th). rewrite (cmul_assoc2 c c2 c3);unfold eqC;apply ceq_refl;try apply eq_th. apply (Pol1mulc_comp Q c c3). rewrite (cmul_assoc2 c2 c c3);unfold eqC;apply ceq_refl;try apply eq_th. rewrite (Pol1mul_sym P (Pc c2)). unfold Pol1_mul at 1. rewrite (Pol1mulc_comp P c2 c3). rewrite (Pol1mul_sym (Pol1_mulc P c3) (Pc c2));simpl. rewrite (Pol1mulc_comp P c3 c2). rewrite (cmul_sym c2 c3);apply Pol1Eq_refl. assert (Pol1_mulc (P * PX Q c2 + Pol1_mulc Q c) c3 != (Pol1_mulc (P * PX Q c2) c3) + (Pol1_mulc (Pol1_mulc Q c) c3)). fold (Pc c3 * (P * PX Q c2 + Pol1_mulc Q c)). rewrite (Pol1distr_r (Pc c3) (P * PX Q c2) ( Pol1_mulc Q c)). unfold Pol1_mul at 1 3; apply Pol1Eq_refl. rewrite H. rewrite (IHP (PX Q c2) c3). rewrite (Pol1mulc_comp Q c c3). rewrite (cmul_sym c c3); apply (Pol1Eq_refl). Qed. Lemma Pol1mul_assoc : forall P Q R, P *(Q*R) != (P*Q)*R. Proof. induction P; destruct Q;intros. simpl; apply Pol1mulc_comp. assert (Pc c * (PX Q c2 * R) != Pol1_mulc (PX Q c2 * R) c). simpl;apply Pol1Eq_refl. rewrite H. rewrite (Pol1mulc_assoc (PX Q c2 ) R c). simpl;apply Pol1Eq_refl. rewrite (Pol1_distr_PX_r P c (Pc c2* R)). rewrite (IHP (Pc c2) R). destruct R;simpl;constructor;cgen;cmul_push c;unfold eqC;try apply ceq_refl;try apply eq_th. apply Pol1Eq_refl. rewrite (Pol1mulc_comp R c2 c);apply Pol1Eq_refl. rewrite (Pol1_distr_PX_r P c (PX Q c2 * R) ). rewrite (IHP (PX Q c2) R). rewrite (Pol1mulc_assoc (PX Q c2) R c). assert (PX (P * PX Q c2 * R) c0 != PX (P*PX Q c2) c0 * R). rewrite (Pol1_distr_PX_r (P * (PX Q c2)) c0 R). fold ((Pc c0)*R). rewrite (Pol1mul_0_l R). fold PO;rewrite (Pol1add_0_l' (PX (P * PX Q c2 * R) c0)). apply Pol1Eq_refl. rewrite H. rewrite <- (Pol1distr_l R (PX (P * PX Q c2) c0) (Pol1_mulc (PX Q c2) c)). simpl;apply Pol1Eq_refl. Qed. Lemma Pol1_mulc_0 : forall P c, c==c0->Pol1_mulc P c != PO. Proof. intros. unfold PO. apply Pol1Eq_trans with (P*(Pc c)). apply Pol1_mulc_spec. apply Pol1Eq_trans with (P*(Pc c0)). apply Pol1mul_ext. apply Pol1Eq_refl. apply Eq1_Pc_Pc;auto. apply Pol1mul_0_r. Qed. Axiom dec_eqPol:forall a b:Pol1,{Pol1Eq a b}+{~(Pol1Eq a b)}. Require Import listT. (*P=fst (mk_couple P)+snd (mk_couple P) P(x1,.,xn+1) =p'(x1, ,xn+1)+pt(x1, ,xn)xn+1^t *) Fixpoint mk_couple(P:Pol1):(prodT Pol1 Pol1):= match P with Pc c=>(pairT (Pc c) (Pc c0)) |PX Q c=>(pairT (PX (fstT (mk_couple Q)) c0) (match dec_eqPol (sndT (mk_couple Q)) PO with left _=>Pc c |right _=>PX (sndT (mk_couple Q)) c end)) end. (* renvoie X^t *) Fixpoint mk_Xt(t:nat):Pol1:=match t with O=>Pc c1 |S m=>PX (mk_Xt m) c0 end. Axiom deg1_mk_Xt:forall t:nat,deg1 (mk_Xt t)=t. (*renvoie pt et p' *) Fixpoint mk_prod(P:Pol1):(prodT C Pol1):= match P with Pc c=>(pairT c (Pc c0)) |PX Q c=>(pairT (fstT (mk_prod Q)) (match dec_eqPol (sndT (mk_prod Q)) PO with left _=>Pc c |right _=>PX (sndT (mk_prod Q)) c end)) end. Axiom p0_deg0_mul:forall (p :Pol1)(Q:C),Pol1Eq p PO->Pol1Eq (Pol1_mulc (mk_Xt (degre1 p)) Q) PO. Axiom p0_mk0:forall p:Pol1,Pol1Eq p PO-> (fstT (mk_prod p))**c1==c0. Lemma eq_p_add_mk:forall p:Pol1,Pol1Eq p (Pol1_add (Pol1_mulc (mk_Xt (degre1 p)) (fstT (mk_prod p))) (sndT (mk_prod p))). induction p. simpl. apply Eq1_Pc_Pc. cgen. apply (ceq_sym C coef eq_th);apply cmul_1_r. simpl. case (dec_EqPol p PO). case (dec_eqPol (sndT (mk_prod p)) PO). simpl;intros. apply Eq1_PX_Pc. cgen. apply (ceq_trans C coef eq_th) with (c0++c). apply (ceq_sym C coef eq_th);apply cadd_0_l. apply (cadd_ext C coef eq_th). apply (ceq_sym C coef eq_th);apply p0_mk0;auto. apply (ceq_refl C coef eq_th). auto. simpl;intros. apply Eq1_PX_PX. cgen. apply (ceq_trans C coef eq_th) with (c0++c). apply (ceq_sym C coef eq_th);apply cadd_0_l. apply (cadd_ext C coef eq_th). apply (ceq_sym C coef eq_th);apply p0_mk0;auto. apply (ceq_refl C coef eq_th). apply Pol1Eq_trans with (Pol1_mulc (mk_Xt (degre1 p)) (fstT (mk_prod p)) + sndT (mk_prod p)). auto. apply Pol1Eq_trans with (PO + sndT (mk_prod p)). apply Pol1_add_ext. apply p0_deg0_mul;auto. apply Pol1Eq_refl. apply Pol1add_0_l. case (dec_eqPol (sndT (mk_prod p)) PO). simpl;intros. apply Eq1_PX_PX. cgen. apply (ceq_refl C coef eq_th). auto. apply Pol1Eq_trans with (Pol1_mulc (mk_Xt (degre1 p)) (fstT (mk_prod p)) + sndT (mk_prod p)). auto. apply Pol1Eq_trans with (Pol1_mulc (mk_Xt (degre1 p)) (fstT (mk_prod p)) + PO). apply Pol1_add_ext. apply Pol1Eq_refl. auto. apply Pol1add_0_l'. simpl;intros. apply Eq1_PX_PX. cgen. apply (ceq_refl C coef eq_th). auto. Qed. Lemma eq_p_mk:forall p:Pol1,Pol1Eq p (Pol1_add (fstT (mk_couple p)) (sndT (mk_couple p))). induction p. simpl;apply Eq1_Pc_Pc;cgen. apply (ceq_refl C coef eq_th). simpl. case (dec_eqPol (sndT (mk_couple p)) PO). simpl;intros. apply Eq1_PX_PX. cgen;apply (ceq_refl C coef eq_th). apply Pol1Eq_trans with (fstT (mk_couple p) + sndT (mk_couple p));auto. apply Pol1Eq_trans with (fstT (mk_couple p) +PO). apply Pol1add_ext. apply Pol1Eq_refl. auto. apply Pol1add_0_l'. simpl;intros. apply Eq1_PX_PX. cgen;apply (ceq_refl C coef eq_th). auto. Qed. Lemma le_deg1_add:forall p q,(forall c1 c2:C,degC (c1++c2)<=max_2_elt (degC c1) (degC c2))-> deg1 (Pol1_add p q)<=max_2_elt (deg1 p) (deg1 q). induction p;induction q. simpl;intros;auto. simpl;intros. case (dec_EqPol q PO). simpl;intros;auto. simpl;intros. rewrite max2_sym with (b:=degC c2). rewrite <-max_2_ass. rewrite max2_sym with (b:=S (deg1 q)). apply max2_le;auto with *. simpl;intros. case (dec_EqPol p PO). simpl;intros;auto. simpl;intros. rewrite max_2_ass. apply max2_le;auto with *. simpl;intros. case (dec_EqPol (p+q) PO). case (dec_EqPol p PO). case (dec_EqPol q PO). simpl;intros;auto. simpl;intros. assert (q != PO). apply Pol1Eq_trans with (PO+q). apply Pol1Eq_sym;apply Pol1add_0_l. apply Pol1Eq_trans with (p+q). apply Pol1add_ext;auto. apply Pol1Eq_sym;auto. apply Pol1Eq_refl. auto. intuition. simpl;intros. case (dec_EqPol q PO). simpl;intros. assert (p != PO). apply Pol1Eq_trans with (p+PO). apply Pol1Eq_sym;apply Pol1add_0_l'. apply Pol1Eq_trans with (p+q). apply Pol1add_ext;auto. apply Pol1Eq_refl. apply Pol1Eq_sym;auto. auto. intuition. simpl;intros. rewrite max_2_ass. rewrite max2_sym with (b:=degC c2). rewrite<-max_2_ass with (a:=degC c). rewrite max2_sym with (b:=S (deg1 q)). rewrite <-max_2_ass. apply max_2_le. auto. simpl;intros. case (dec_EqPol p PO). case (dec_EqPol q PO). simpl;intros;auto. simpl;intros. absurd (p+q != PO). auto. apply Pol1Eq_trans with (PO+PO). apply Pol1add_ext;auto. apply Pol1add_0_l'. simpl;intros. rewrite max2_sym with (b:=degC c2). rewrite <-max_2_ass. rewrite max2_sym with (b:=S (deg1 q)). assert (p+q !=q). apply Pol1Eq_trans with (PO+q). apply Pol1add_ext;auto. apply Pol1Eq_refl. apply Pol1add_0_l. rewrite (Pol1Eq_deg_eq (p+q) q H0). apply max2_le. auto. case (dec_EqPol q PO). simpl;intros. rewrite max_2_ass. assert (p+q !=p). apply Pol1Eq_trans with (p+PO). apply Pol1add_ext;auto. apply Pol1Eq_refl. apply Pol1add_0_l'. rewrite (Pol1Eq_deg_eq (p+q) p H0). apply max2_le. auto. simpl;intros. rewrite<-max_2_ass . rewrite max2_sym with (b:=degC c2). rewrite<-max_2_ass . rewrite max2_sym with (b:=degC c). rewrite<-max_2_ass . rewrite max2_sym with (b:=S (deg1 q)). rewrite max2_sym with (b:=S (deg1 p)). rewrite<-max_2_ass . rewrite max2_sym with (b:=degC c). apply max_2_le_le. rewrite max2_sym. apply Le.le_trans with (S (max_2_elt (deg1 p) (deg1 q))). apply Le.le_n_S;apply IHp;auto. apply le_max2_S. auto. Qed. End POL1. Section CALL. Variable C:Type. Record CALL:Type:=mk_Call{ COp:coef_set C; CEq:coef_eq C COp; Cth:coef_theory C COp }. End CALL. Section Pol1. Variable C:Type. Variable Call:CALL C. Definition coef1 :coef_set C. apply (COp C Call). Defined. Definition eq_th1 : coef_eq C coef1 . apply (CEq C Call). Defined. Definition CT1: coef_theory C coef1. apply (Cth C Call). Defined. Definition P1Set:coef_set (Pol1 C). apply mk_cset. apply (PO C);apply coef1. apply (PI C);apply coef1. apply (Pol1Eq C);apply coef1. apply (Pol1_add C);apply coef1. apply (Pol1_mul C);apply coef1. apply (Pol1_sub C);apply coef1. apply (Pol1_opp C);apply coef1. Defined. Definition P1Eq:coef_eq (Pol1 C) P1Set. apply mk_ceq. simpl;intros;apply (Pol1Eq_refl C). apply eq_th1. simpl;intros;apply (Pol1Eq_sym C). apply eq_th1. apply H. simpl;intros;apply (Pol1Eq_trans C coef1 eq_th1 x y H z H0);apply coef1. simpl;intros. apply (Pol1_add_ext C coef1);auto. apply CT1. apply eq_th1. simpl;intros. apply (Pol1mul_ext C (coef1));auto. apply CT1. apply eq_th1. simpl;intros. apply (Pol1opp_ext C coef1 );auto. apply CT1. apply eq_th1. Defined. Definition P1th:coef_theory (Pol1 C) P1Set . apply mk_ct. simpl;intros. generalize (Pol1add_0_l C coef1 CT1 eq_th1 x). simpl;intros;auto. simpl;intros;apply (Pol1add_sym C coef1 CT1 eq_th1 ) . simpl;intros;apply (Pol1add_assoc C coef1 CT1 eq_th1 ) . simpl;intros. generalize (Pol1mul_1_r C coef1 CT1 eq_th1 x). unfold PI;simpl;intros. apply Pol1Eq_trans with (Q:=(Pol1_mul C coef1 x (Pc C (c1 C coef1)))). apply eq_th1. apply (Pol1_mulc_spec C coef1 CT1 eq_th1 x (c1 C coef1)). auto. simpl;intros;apply (Pol1mul_sym C coef1 CT1 eq_th1 ). simpl;intros;apply (Pol1mul_assoc C coef1 CT1 eq_th1 ) . simpl;intros;apply (Pol1distr_l C coef1 CT1 eq_th1 ) . simpl;intros;unfold Pol1_sub;apply (Pol1Eq_refl C coef1 eq_th1 ). simpl;intros;apply (Pol1opp_def C coef1 CT1 ) . Defined. Definition mk_Pol1:CALL (Pol1 C). apply (mk_Call (Pol1 C ) P1Set P1Eq P1th). Defined. Variable C':Type. Fixpoint Pol1map(f:C->C')(p:Pol1 C){struct p}:Pol1 C':=match p with Pc c=>Pc C' (f c) |PX P c=>PX C' (Pol1map f P) (f c) end. End Pol1. Section POLn. Variable C:Type. Variable Call:CALL C. (*polynomes a n variables *) Fixpoint Pol(n:nat){struct n}:Type:=match n with |0=>C |(S m)=>Pol1 (Pol m) end. Fixpoint CPol(n:nat):CALL (Pol n):=match n return (CALL (Pol n)) with O=>Call |S m=>mk_Pol1 (Pol m) (CPol m) end. Fixpoint degre(n:nat){struct n}:(Pol n)->nat:= match n return (Pol n)->nat with |O =>fun c:C=>O |(S m)=>deg1 (Pol m) (COp (Pol m) (CPol m)) (degre m) end . Lemma degre_Pc_eq:forall (n:nat)(c:Pol n),degre (S n) (Pc _ c)=degre n c. induction n. simpl;intros;auto. simpl;intros;auto. Qed. Definition degr1(n:nat)(p:Pol n):nat. induction n. intro;exact O. simpl;intro. apply (degre1 (Pol n) (COp _ (CPol n)) p). Defined. Lemma degP0:forall n:nat,degre n (c0 (Pol n) (COp (Pol n) (CPol n )))=0. induction n. simpl;auto. simpl;auto. Qed. Definition PolnEq(n:nat):Pol n->Pol n->Prop:=eqC (Pol n) (COp (Pol n) (CPol n)) . Lemma Poln_Pol1_eq:forall (n:nat) p q,PolnEq (S n) p q->Pol1Eq (Pol n) (COp (Pol n) (CPol n)) p q. unfold PolnEq;induction n. simpl;intros;auto. simpl;intros. auto. Qed. Lemma PolnEq_deg_eq:forall (n:nat) p q,PolnEq n p q->degre n p=degre n q. induction n. simpl;intros;auto. simpl;intros. apply Pol1Eq_deg_eq. apply (CEq (Pol n) (CPol n)). simpl;intros. apply IHn. unfold PolnEq. apply Pol1Eq_PC_Ceq;auto. unfold PolnEq in H. apply Poln_Pol1_eq;auto. Qed. Definition Poln_add(n:nat):Pol n->Pol n->Pol n:=cadd (Pol n) (COp (Pol n) (CPol n)). Definition Poln_mul(n:nat):Pol n->Pol n->Pol n:=cmul (Pol n) (COp (Pol n) (CPol n)). Definition Poln_sub(n:nat):Pol n->Pol n->Pol n:=csub (Pol n) (COp (Pol n) (CPol n)). Definition Poln_opp(n:nat):Pol n->Pol n:=copp (Pol n) (COp (Pol n) (CPol n)). Lemma le_deg_add:forall (n:nat) p q,degre n (Poln_add n p q)<=max_2_elt (degre n p) (degre n q). induction n. simpl;intros. rewrite max_0_r;auto. simpl;intros. unfold Poln_add;simpl. apply (le_deg1_add (Pol n) (COp (Pol n) (CPol n)) (Cth (Pol n) (CPol n)) (CEq (Pol n) (CPol n)) (degre n)). simpl;intros. apply PolnEq_deg_eq. unfold PolnEq;simpl. apply Pol1Eq_PC_Ceq;auto. simpl;intros. unfold Poln_add in IHn. auto with *. Qed. (* Definition mk_cple(n:nat)(p:Pol n):(prodT (Pol n) (Pol n)):= match n return (prodT (Pol n) (Pol n)) with O=>(pairT (c0 _ (coef1 C Call)) p) |(S m)=>mk_couple p end. *) Definition mk_cple(n:nat)(p:Pol n):(prodT (Pol n) (Pol n)). induction n. intro. exact (pairT (c0 _ (coef1 C Call)) p). intros. apply (mk_couple (Pol n) (COp _ (CPol n)) p). Defined. Definition mk_prodn(n:nat)(p:Pol n):(prodT (Pol (pred n)) (Pol n)). induction n. intro. exact (pairT (c0 _ (coef1 C Call)) p). intros. apply (mk_prod (Pol n) (COp _ (CPol n)) p). Defined. Lemma eq_pn_mk:forall (n:nat)(p:Pol n), PolnEq n p (Poln_add n (fstT (mk_cple n p)) (sndT (mk_cple n p))). induction n. simpl;intros. unfold PolnEq;unfold Poln_add;simpl. apply ceq_sym. apply CEq. apply cadd_0_l. apply Cth. simpl;intros. unfold PolnEq;unfold Poln_add;simpl. apply eq_p_mk. apply Cth. apply CEq. Qed. (* c vu comme un elt de type (Pol n) *) Fixpoint inject(n:nat)(c:C){struct n}:Pol n:= match n return (Pol n) with O=>c |S m=>Pc (Pol m) (inject m c) end. Definition Poln_mulc(n:nat)(c:C)(p:Pol n):Pol n:=Poln_mul n (inject n c) p. Definition mk_Xtn(t:nat)(n:nat):Pol n. induction n. apply c1. apply COp. apply Call. simpl. apply (mk_Xt (Pol n) (COp _ (CPol n)) t). Defined. Definition Poln_mulcn(n:nat)(c:Pol (pred n))(p:Pol n):Pol n. induction n. simpl;apply cmul. apply COp. apply Call. simpl. intros. apply (Pol1_mulc (Pol n) (COp _ (CPol n)) p c). Defined. Lemma eq_p_mkn:forall (n:nat)(p:Pol n), PolnEq n p (Poln_add n (Poln_mulcn n (fstT (mk_prodn n p)) (mk_Xtn (degr1 n p) n)) (sndT (mk_prodn n p))). induction n. simpl;intros. unfold PolnEq;unfold Poln_add;simpl. apply ceq_sym. apply CEq. apply ceq_trans with (cadd C (COp C Call) (c0 C (coef1 C Call)) p). apply CEq. apply cadd_ext;try apply CEq. apply cmul_0_l;try apply Cth;try apply CEq. apply ceq_refl;try apply CEq. apply cadd_0_l. apply Cth. simpl;intros. unfold PolnEq;unfold Poln_add;simpl. apply eq_p_add_mk. apply Cth. apply CEq. Qed. Fixpoint restrict_Pol(n:nat)(p:Pol (S n)){struct p}:Pol n:=match p with Pc c=>c |PX P c=>Poln_add n (restrict_Pol n P) c end. Definition P0(n:nat):Pol n:=cO (Pol n) (COp (Pol n) (CPol n)). Definition P1(n:nat):Pol n:=cI (Pol n) (COp (Pol n) (CPol n)). (*the list 1,x1,...,xn *) Fixpoint ListVar_(n:nat){struct n}:listT (Pol n):= match n return (listT (Pol n)) with O => consT (P1 0) (nilT _) |S m => let l:=(ListVar_ m) in let listm:=(mapT (fun p:Pol m=>Pc _ p) l) in consT (PX _ (P1 (S m)) (P0 m)) listm end. (* Fixpoint ListVar(n:nat){struct n}:listT (Pol n):= match n return (listT (Pol n)) with O => nilT _ | S O =>consT (PX _ (Pc _ (P1 0)) (P0 0)) (nilT _) |S m => let l:=(ListVar m) in let listm:=(mapT (fun p:Pol m=>Pc _ p) l) in consT (PX _ (P1 (S m)) (P0 m)) listm end. *) Definition ListVar(n:nat):=tailT (ListVar_ n). Axiom eq_p_restr_snd: forall (n : nat) (p : Pol (S n)), PolnEq n (fstT (mk_prodn (S n) p)) (P0 n) -> PolnEq (S n) p (Pc _ (restrict_Pol n (sndT (mk_prodn (S n) p)))). Axiom le_deg_plus: forall (n : nat) (p : Pol (S n)), (degre n (fstT (mk_prodn (S n) p)) + degre1 (Pol n) (COp (Pol n) (CPol n)) p <= degre (S n) p). Require Import listT. Fixpoint ev_pol1(n:nat)(P:Pol (S n))(x:C){struct P}:Pol n:= match P with Pc c=>c |PX P1 c=>Poln_add n c (Poln_mulc n x (ev_pol1 n P1 x)) end. (* l=ln...l1 *) Fixpoint eval_Pol(n:nat):(Pol n)->(listT C)->C:= match n as x return (Pol x)->(listT C)->C with O=>fun p:C=>(fun l:(listT C)=>p) |S m=>fun p:Pol (S m)=>(fun l:(listT C)=>eval_Pol m (ev_pol1 m p (headT (c0 C (coef1 C Call)) l)) (tailT l) )end. Definition eval(n:nat)(l:listT C)(p:Pol n):C:=eval_Pol n p l. Definition eval_coef(n:nat)(p:Pol (S n))(l:listT C):Pol1 C:=Pol1map (Pol n) C (eval n l) p. Axiom eq_pol_ev1_eq:forall (n:nat) (l: C) (p q:Pol1 (Pol n)),Pol1Eq _ (COp _ (CPol n)) p q-> PolnEq n (ev_pol1 n p l) (ev_pol1 n q l). Lemma eq_pol_ev_eq:forall (n:nat) (l:listT C) (p q:Pol n),PolnEq n p q-> ceq C (COp C Call) (eval_Pol n p l) (eval_Pol n q l). induction n;unfold PolnEq;simpl;intros. auto. apply IHn. apply eq_pol_ev1_eq;auto. Qed. Axiom eq_p_ev_coef_eq:forall (n:nat)(p q:Pol (S n))(l:listT C),PolnEq (S n) p q-> Pol1Eq C (coef1 C Call) (eval_coef n p l) (eval_coef n q l) . Lemma ev_P0:forall (n:nat) (l:listT C),ceq C (coef1 C Call) (eval n l (P0 n)) (c0 C (coef1 C Call) ). unfold P0;simpl;unfold PO;simpl. unfold eval;simpl. induction n. simpl;intros. apply ceq_refl;try apply Cth;try apply CEq. simpl;intros. apply IHn. Qed. Axiom ev_pol1_add_eq: forall (n : nat) (p r : Pol (S n) ) (a0 : C), PolnEq n (ev_pol1 n (Poln_add (S n) p r) a0) ( Poln_add n (ev_pol1 n p a0) (ev_pol1 n r a0)). Lemma ev_pol_add_eq: forall (n : nat) (p r : Pol n ) (a0 : listT C), ceq C (coef1 C Call) (eval_Pol n (Poln_add n p r) a0) (cadd C (coef1 C Call) (eval_Pol n p a0) (eval_Pol n r a0)). induction n. simpl;intros. unfold Poln_add;simpl. apply ceq_refl;try apply CEq. simpl;intros. apply ceq_trans with (eval_Pol n (Poln_add n (ev_pol1 n p (headT (c0 C (coef1 C Call) ) a0)) (ev_pol1 n r (headT (c0 C (coef1 C Call) ) a0))) (tailT a0)). apply CEq. apply eq_pol_ev_eq. apply ev_pol1_add_eq. apply IHn. Qed. Axiom ev_pol1_mulc_eq: forall (n : nat) (p : Pol (S n) ) (a a0 : C), PolnEq n (ev_pol1 n (Poln_mulc (S n) a p) a0) ( Poln_mulc n a (ev_pol1 n p a0)). Lemma ev_pol_mulc_eq: forall (n : nat) (p : Pol n) (a : C) (a0 : listT C), ceq C (coef1 C Call) (eval_Pol n (Poln_mulc n a p) a0) (cmul C (coef1 C Call) a (eval_Pol n p a0)). induction n. simpl;intros. unfold Poln_mulc;simpl. unfold Poln_mul;simpl. apply ceq_refl;try apply CEq. simpl;intros. apply ceq_trans with (eval_Pol n (Poln_mulc n a (ev_pol1 n p (headT (c0 C (coef1 C Call) ) a0))) (tailT a0)). apply CEq. apply eq_pol_ev_eq. apply ev_pol1_mulc_eq. apply IHn. Qed. Lemma ev_coef_p0:forall (n:nat)(p:Pol (S n))(l:listT C),PolnEq (S n) p (P0 (S n))->Pol1Eq C (coef1 C Call) (eval_coef n p l) (P0 1). intros. apply Pol1Eq_trans with (eval_coef n (P0 (S n)) l). apply CEq. apply eq_p_ev_coef_eq;auto. unfold eval_coef;simpl. unfold P0;simpl;unfold PO;simpl. apply Eq1_Pc_Pc. generalize (ev_P0 n l);unfold P0;simpl;unfold PO;simpl;intro;auto. Qed. (*PolnEq is a setoid equality*) Lemma PolnEq_refl:forall (n:nat) P,(PolnEq n P P). Proof. induction n. simpl;intro. unfold PolnEq;apply ceq_refl;apply eq_th1. simpl;intros. unfold PolnEq;apply ceq_refl;apply (CEq (Pol (S n)) (CPol (S n))). Qed. Lemma PolnEq_sym:forall (n:nat) P Q,(PolnEq n P Q)->(PolnEq n Q P). Proof. induction n. simpl;intro. unfold PolnEq;apply ceq_sym;apply eq_th1. simpl;intros. unfold PolnEq;apply ceq_sym;auto;apply (CEq (Pol (S n)) (CPol (S n))). Qed. Lemma PolnEq_trans:forall (n:nat) P Q R,(PolnEq n P Q)->(PolnEq n Q R)->(PolnEq n P R). Proof. induction n. simpl;intros;apply (ceq_trans C (coef1 C Call) (eq_th1 C Call) P Q R);auto. simpl;intros;apply (Pol1Eq_trans (Pol n) (COp (Pol n) (CPol n)) ((CEq (Pol n) (CPol n)) ) P Q H R H0);auto. Qed. Lemma Polnadd_sym : forall (n:nat) P Q, (PolnEq n (Poln_add n P Q ) (Poln_add n Q P)). Proof. simpl;intros. unfold PolnEq;unfold Poln_add;apply cadd_sym. apply Cth. Qed. Axiom Poln_mulc_p0:forall (n:nat)(c:C)(p:Pol n),PolnEq n p (P0 n)-> PolnEq n (Poln_mulc n c p) (P0 n). Axiom Poln_mulc_ext: forall (n:nat) P1 P2 c1 c2,(PolnEq n P1 P2) -> ceq C (COp C Call) c1 c2 -> PolnEq n (Poln_mulc n c1 P1) (Poln_mulc n c2 P2) . Lemma Polnadd_0_l : forall (n:nat) P, (PolnEq n (Poln_add n (P0 n) P) P). Proof. simpl;intros;unfold PolnEq;unfold Poln_add. unfold P0;apply cadd_0_l;auto. apply Cth;apply Call. Qed. Lemma Polnadd_0_r : forall (n:nat) P, (PolnEq n (Poln_add n P (P0 n)) P). Proof. simpl;intros;unfold PolnEq;unfold Poln_add. unfold P0;apply cadd_0_r;auto. apply Cth;apply Call. apply CEq;apply Call. Qed. Lemma Polnadd_ext: forall (n:nat) P1 P2,(PolnEq n P1 P2) -> forall Q1 Q2, (PolnEq n Q1 Q2 )-> (PolnEq n (Poln_add n P1 Q1 ) (Poln_add n P2 Q2)). Proof. simpl;intros;unfold PolnEq;unfold Poln_add. apply cadd_ext;auto. apply CEq. Qed. Lemma Polnadd_assoc : forall (n:nat) P Q R, (PolnEq n (Poln_add n P (Poln_add n Q R) ) (Poln_add n (Poln_add n P Q) R)). Proof. simpl;intros;unfold PolnEq;unfold Poln_add. apply cadd_assoc;auto. apply Cth. Qed. Lemma Polnmul_sym : forall (n:nat) P Q, (PolnEq n (Poln_mul n P Q ) (Poln_mul n Q P)). Proof. simpl;intros;unfold PolnEq;unfold Poln_mul. apply cmul_sym;auto. apply Cth. Qed. Lemma Polnmul_ext : forall (n:nat) P1 P2, (PolnEq n P1 P2)-> forall Q1 Q2, (PolnEq n Q1 Q2) -> (PolnEq n (Poln_mul n P1 Q1 ) (Poln_mul n P2 Q2)). Proof. simpl;intros;unfold PolnEq;unfold Poln_mul. apply cmul_ext;auto. apply CEq. Qed. Lemma Polnopp_ext : forall (n:nat) P Q, (PolnEq n P Q )-> (PolnEq n (Poln_opp n P) (Poln_opp n Q)). Proof. simpl;intros;unfold PolnEq;unfold Poln_opp. apply copp_ext;auto. apply CEq. Qed. Lemma Polnopp_def : forall (n:nat) P, (PolnEq n (Poln_add n P (Poln_opp n P) ) (P0 n)). Proof. simpl;intros;unfold PolnEq;unfold Poln_opp;unfold Poln_add. unfold P0;apply copp_def;auto. apply Cth. Qed. Lemma Polndistr_l : forall (n:nat) R P Q, (PolnEq n (Poln_mul n (Poln_add n P Q) R) (Poln_add n (Poln_mul n P R) (Poln_mul n Q R))). Proof. simpl;intros;unfold PolnEq;unfold Poln_mul;unfold Poln_add. apply cdistr_l;auto. apply Cth. Qed. Lemma Polndistr_r : forall (n:nat) R P Q, (PolnEq n (Poln_mul n R (Poln_add n P Q)) (Poln_add n (Poln_mul n R P) (Poln_mul n R Q ))). Proof. simpl;intros;unfold PolnEq;unfold Poln_mul;unfold Poln_add. apply cdistr_r;auto. apply Cth. apply CEq. Qed. Lemma Polnmul_1_l : forall (n:nat) P, (PolnEq n (Poln_mul n (P1 n) P) P). Proof. simpl;intros;unfold PolnEq;unfold Poln_mul. unfold P1;apply cmul_1_l;auto. apply Cth. Qed. Lemma Polnmul_1_r : forall (n:nat) P, (PolnEq n (Poln_mul n P (P1 n) ) P). Proof. simpl;intros;unfold PolnEq;unfold Poln_mul;unfold P1. apply cmul_1_r;auto. apply Cth. apply CEq. Qed. Lemma Polnmul_assoc : forall (n:nat) P Q R, (PolnEq n (Poln_mul n P (Poln_mul n Q R)) (Poln_mul n (Poln_mul n P Q) R)). Proof. simpl;intros;unfold PolnEq;unfold Poln_mul. apply cmul_assoc;auto. apply Cth. Qed. Fixpoint mk_cte(n:nat)(c:C){struct n}:(Pol n):=match n return (Pol n) with O=>c |(S m)=>Pc (Pol m) (mk_cte m c) end. End POLn.