Library examples.cime_trace.ring_extention
Require Import ZArith.
Require Import ZArithRing.
Require Import Ring_polynom.
Require Import Bool.
Require Import List.
Function all_coef_pos (p:Pol Z) : bool :=
match p with
| Pc c => match Zcompare 0 c with
| Gt => false
| _ => true
end
| Pinj _ p => all_coef_pos p
| PX p _ q => andb (all_coef_pos p) (all_coef_pos q)
end.
Function all_mem_pos (l:list Z) : Prop :=
match l with
| nil => True
| c::l => (0<=c)%Z /\ all_mem_pos l
end.
Open Scope Z_scope.
Import InitialRing.
Import BinList.
Functional Scheme jump_ind := Induction for jump Sort Prop.
Open Scope Z_scope.
Lemma all_mem_pos_def : forall l, (forall c, In c l -> 0<= c) <-> all_mem_pos l.
Proof.
intro l;split;intro H.
induction l. simpl. trivial.
simpl.
split.
apply H;simpl;auto.
apply IHl;intro;simpl in H;auto.
functional induction (all_mem_pos l).
simpl;tauto.
destruct H;simpl.
intros x H';simpl in H';destruct H'.
subst.
assumption.
auto.
Qed.
Lemma tail_in : forall A (l:list A) x, In x (tail l) -> In x l.
Proof.
induction l.
simpl;tauto.
simpl.
auto.
Qed.
Lemma jump_in : forall A n l (x:A), In x (jump n l) -> @In A x l.
Proof.
intros a n l;functional induction (jump n l).
intros;apply tail_in;eauto.
eauto.
intros;apply tail_in;auto.
Qed.
Lemma pos_expr_if_all_pos_aux :
forall (p:Pol Z), all_coef_pos p = true -> forall l, all_mem_pos l ->
0<=Pphi 0 Zplus Zmult (IDphi (R:=Z)) l p.
Proof.
intros p;functional induction (all_coef_pos p).
intro;discriminate.
intros _.
simpl.
destruct c;simpl in y;try discriminate;simpl;auto with zarith.
unfold IDphi;auto with zarith.
simpl.
intros H l H0.
apply IHb.
exact H.
rewrite <- all_mem_pos_def in H0|-*.
intros c H1.
apply H0.
apply jump_in with _x;exact H1.
simpl.
intros H l H0.
assert (0<=hd 0 l).
clear - H0.
induction l.
simpl;omega.
simpl.
rewrite <- all_mem_pos_def in H0;simpl in H0;eauto.
assert (0<= pow_pos Zmult (hd 0 l) _x).
set (u:=hd 0 l) in *;clearbody u.
clear - H1.
induction _x.
simpl; auto with zarith.
simpl; auto with zarith.
simpl; auto with zarith.
assert (0 <=
Pphi 0 Zplus Zmult (IDphi (R:=Z)) l p0).
apply IHb.
symmetry in H.
destruct (@andb_true_eq _ _ H);auto.
assumption.
assert (0<=Pphi 0 Zplus Zmult (IDphi (R:=Z)) (tail l) q).
apply IHb0.
symmetry in H;destruct (@andb_true_eq _ _ H);auto.
rewrite <- all_mem_pos_def in H0|-*.
intros c H4; apply H0;apply tail_in;exact H4.
auto with zarith.
Qed.
Lemma pos_expr_if_all_pos_aux' :
forall (p:Pol Z), all_coef_pos p = true -> forall l, all_mem_pos l ->
0<=
@Pphi_pow _ 0 1 Zplus Zmult Zminus Zopp _ 0 1 Zeq_bool (IDphi (R:=Z)) _ Z_of_N Zpower (get_sign_None (C:=Z)) l p.
Proof.
intros p H l H0.
replace ( @Pphi_pow _ 0 1 Zplus Zmult Zminus Zopp _ 0 1 Zeq_bool (IDphi (R:=Z)) _ Z_of_N Zpower (get_sign_None (C:=Z)) l p)
with (Pphi 0 Zplus Zmult (@IDphi Z) l p).
apply pos_expr_if_all_pos_aux;assumption.
symmetry;eapply Pphi_pow_ok with (1:=InitialRing.Zsth) (C:= Z).
exact InitialRing.Zeqe.
exact (@Rth_ARth _ _ _ _ _ _ _ _ InitialRing.Zsth InitialRing.Zeqe InitialRing.Zth).
eexact (@IDmorph Z Z0 1 Zplus Zmult Zminus Zopp _ InitialRing.Zsth Zeq_bool InitialRing.Zeqb_ok).
exact Zpower_theory.
constructor.
destruct c;simpl;try (intros;discriminate).
Qed.
Lemma pos_expr_if_all_pos' :
forall pe,
all_coef_pos
(norm_subst 0 1 Zplus Zmult Zminus Zopp Zeq_bool ring_subst_niter nil pe) = true ->
forall l, all_mem_pos l ->
0<= ( PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower l pe) .
Proof.
intros p H l H0.
rewrite Zr_ring_lemma2 with (n:=ring_subst_niter) (lH:=@nil (PExpr Z * PExpr Z)) (l:=l)
(lmp:=@nil (Mon * Pol Z)) (pe:=p) (npe:=norm_subst 0 1 Zplus Zmult Zminus Zopp Zeq_bool ring_subst_niter nil
p).
apply pos_expr_if_all_pos_aux';assumption.
vm_compute;exact I.
vm_compute;reflexivity.
reflexivity.
Qed.
Lemma pos_expr_if_all_pos :
forall pe1 pe2,
all_coef_pos ( norm_subst 0 1 Zplus Zmult Zminus Zopp Zeq_bool ring_subst_niter nil (PEsub pe2 pe1)) = true ->
forall l, all_mem_pos l ->
PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower l pe1 <=
PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower l pe2 .
Proof.
intros pe1 pe2 H l H0.
assert (0<= PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower l (PEsub pe2 pe1)).
apply pos_expr_if_all_pos'.
assumption.
assumption.
simpl in H1;auto with zarith.
Qed.
Lemma jump_nil : forall p, jump p (@nil Z) = nil .
Proof.
induction p;simpl.
do 2 rewrite IHp;reflexivity.
do 2 rewrite IHp;reflexivity.
reflexivity.
Qed.
Lemma Pphi_nil : forall p,
Pphi 0 Zplus Zmult (IDphi (R:=Z)) nil p =
match p with
| Pc c => c
| Pinj _ p => Pphi 0 Zplus Zmult (IDphi (R:=Z)) nil p
| PX _ _ p => Pphi 0 Zplus Zmult (IDphi (R:=Z)) nil p
end.
Proof.
destruct p.
simpl;unfold IDphi;reflexivity.
simpl.
rewrite jump_nil;reflexivity.
simpl.
replace (pow_pos Zmult 0 p2) with 0.
ring.
clear;induction p2;simpl;auto with zarith.
rewrite <- IHp2;reflexivity.
Qed.
Lemma strict_pos_expr_if_all_pos_aux :
forall (p:Pol Z), all_coef_pos p = true -> forall l, all_mem_pos l ->
0 < Pphi 0 Zplus Zmult (IDphi (R:=Z)) (@nil _) p ->
0< Pphi 0 Zplus Zmult (IDphi (R:=Z)) l p.
Proof.
intro p;
rewrite Pphi_nil.
induction p;simpl.
tauto.
intros H l H0 H1.
apply IHp.
assumption.
rewrite <- all_mem_pos_def in H0|-*.
intros c H2.
apply H0.
apply jump_in with (1:=H2).
destruct p0;simpl in H1.
unfold IDphi;assumption.
rewrite jump_nil in H1;assumption.
replace (pow_pos Zmult 0 p0) with 0 in H1.
rewrite Zmult_comm in H1; simpl in H1;assumption.
clear;induction p0;simpl;auto.
rewrite <- IHp0;auto.
intros H l H0 H1.
assert (0<=hd 0 l).
clear - H0.
induction l.
simpl;omega.
simpl.
rewrite <- all_mem_pos_def in H0;simpl in H0;eauto.
assert (0<=pow_pos Zmult (hd 0 l) p2).
set (u:=hd 0 l) in *;clearbody u.
clear - H2.
induction p2; simpl; auto with zarith.
assert (0<= Pphi 0 Zplus Zmult (IDphi (R:=Z)) l p1).
eapply pos_expr_if_all_pos_aux.
symmetry in H.
destruct (@andb_true_eq _ _ H);auto.
assumption.
assert (0 < Pphi 0 Zplus Zmult (IDphi (R:=Z)) (tail l) p3).
apply IHp2.
symmetry in H.
destruct (@andb_true_eq _ _ H);auto.
rewrite <- all_mem_pos_def in H0|-*.
intros c H5.
apply H0. destruct l;simpl in H5|-*. tauto. auto.
clear - H1; destruct p3;simpl in H1.
exact H1.
rewrite jump_nil in H1;assumption.
replace (pow_pos Zmult 0 p) with 0 in H1.
rewrite Zmult_comm in H1; simpl in H1;assumption.
clear;induction p;simpl;auto.
rewrite <- IHp;auto.
set (u:=pow_pos Zmult (hd 0 l) p2) in *;clearbody u.
set (v:=Pphi 0 Zplus Zmult (IDphi (R:=Z)) l p1) in *;clearbody v.
set (w:=Pphi 0 Zplus Zmult (IDphi (R:=Z)) (tail l) p3) in *;clearbody w.
clear - H3 H4 H5.
assert (0<= v*u) by auto with zarith.
auto with zarith.
Qed.
Lemma strict_pos_expr_if_all_pos_aux' :
forall (p:Pol Z), all_coef_pos p = true -> forall l, all_mem_pos l ->
0< @Pphi_pow _ 0 1 Zplus Zmult Zminus Zopp _ 0 1 Zeq_bool (IDphi (R:=Z)) _ Z_of_N Zpower (get_sign_None (C:=Z)) nil p ->
0< @Pphi_pow _ 0 1 Zplus Zmult Zminus Zopp _ 0 1 Zeq_bool (IDphi (R:=Z)) _ Z_of_N Zpower (get_sign_None (C:=Z)) l p.
Proof.
intros p H l H0.
replace ( @Pphi_pow _ 0 1 Zplus Zmult Zminus Zopp _ 0 1 Zeq_bool (IDphi (R:=Z)) _ Z_of_N Zpower (get_sign_None (C:=Z)) l p)
with (Pphi 0 Zplus Zmult (@IDphi Z) l p).
replace (Pphi_pow 0 1 Zplus Zmult Zminus Zopp 0 1 Zeq_bool
(IDphi (R:=Z)) Z_of_N Zpower (get_sign_None (C:=Z)) nil p)
with (Pphi 0 Zplus Zmult (@IDphi Z) nil p).
intro.
apply strict_pos_expr_if_all_pos_aux;assumption.
symmetry;eapply Pphi_pow_ok with (1:=InitialRing.Zsth) (C:= Z).
exact InitialRing.Zeqe.
exact (@Rth_ARth _ _ _ _ _ _ _ _ InitialRing.Zsth InitialRing.Zeqe InitialRing.Zth).
eexact (@IDmorph Z Z0 1 Zplus Zmult Zminus Zopp _ InitialRing.Zsth Zeq_bool InitialRing.Zeqb_ok).
exact Zpower_theory.
constructor.
destruct c;simpl;try (intros;discriminate).
symmetry;eapply Pphi_pow_ok with (1:=InitialRing.Zsth) (C:= Z).
exact InitialRing.Zeqe.
exact (@Rth_ARth _ _ _ _ _ _ _ _ InitialRing.Zsth InitialRing.Zeqe InitialRing.Zth).
eexact (@IDmorph Z Z0 1 Zplus Zmult Zminus Zopp _ InitialRing.Zsth Zeq_bool InitialRing.Zeqb_ok).
exact Zpower_theory.
constructor.
destruct c;simpl;try (intros;discriminate).
Qed.
Lemma strict_pos_expr_if_all_pos' :
forall pe, all_coef_pos (norm_subst 0 1 Zplus Zmult Zminus Zopp Zeq_bool ring_subst_niter nil pe) = true ->
forall l, all_mem_pos l ->
0 < PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower (@nil Z) pe ->
0< ( PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower l pe) .
Proof.
intros p H l H0.
rewrite Zr_ring_lemma2 with (n:=ring_subst_niter) (lH:=@nil (PExpr Z * PExpr Z))
(lmp:=@nil (Mon * Pol Z)) (pe:=p) (npe:=norm_subst 0 1 Zplus Zmult Zminus Zopp Zeq_bool ring_subst_niter nil
p).
rewrite Zr_ring_lemma2 with (n:=ring_subst_niter) (lH:=@nil (PExpr Z * PExpr Z))
(lmp:=@nil (Mon * Pol Z)) (pe:=p) (npe:=norm_subst 0 1 Zplus Zmult Zminus Zopp Zeq_bool ring_subst_niter nil
p).
apply strict_pos_expr_if_all_pos_aux';assumption.
vm_compute;exact I.
vm_compute;reflexivity.
reflexivity.
vm_compute;exact I.
vm_compute;reflexivity.
reflexivity.
Qed.
Lemma strict_pos_expr_if_all_pos : forall pe1 pe2,
all_coef_pos (norm_subst 0 1 Zplus Zmult Zminus Zopp Zeq_bool ring_subst_niter nil (PEsub pe2 pe1)) = true ->
forall l, all_mem_pos l ->
PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower (@nil Z) pe1 < PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower (@nil Z) pe2 ->
PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower l pe1 < ( PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower l pe2) .
Proof.
intros pe1 pe2 H l H0 H1.
assert (0< PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower l pe2 -
PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower l pe1).
replace (PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower l pe2 -
PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower l pe1) with
(PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower l (PEsub pe2 pe1)) by (vm_compute;reflexivity).
apply strict_pos_expr_if_all_pos'.
assumption.
assumption.
simpl. auto with zarith.
auto with zarith.
Qed.
Ltac ring_ineq :=
match goal with
| |- ?p <= ?q =>
let mkFV := FV Zcst Zpow_tac Zplus Zmult Zminus Zopp Zpower in
let mkPol := mkPolexpr Z Zcst Zpow_tac Zplus Zmult Zminus Zopp Zpower in
let fv := mkFV p (@List.nil Z) in
let fv := mkFV q fv in
let pe := mkPol p fv in
let qe := mkPol q fv in
let p' := constr:(PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower fv pe) in
let q' := constr:(PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower fv qe) in
let H:= fresh "H" in
(assert (H':p' <= q');[
apply pos_expr_if_all_pos;
[vm_compute;reflexivity|
simpl;repeat split;assumption]
| vm_compute in H';exact H'
])
| |- ?p < ?q =>
let mkFV := FV Zcst Zpow_tac Zplus Zmult Zminus Zopp Zpower in
let mkPol := mkPolexpr Z Zcst Zpow_tac Zplus Zmult Zminus Zopp Zpower in
let fv := mkFV p (@List.nil Z) in
let fv := mkFV q fv in
let pe := mkPol p fv in
let qe := mkPol q fv in
let p' := constr:(PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower fv pe) in
let q' := constr:(PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower fv qe) in
let H:= fresh "H" in
(assert (H':p' < q');[
apply strict_pos_expr_if_all_pos;
[vm_compute;reflexivity|
simpl;repeat split;assumption| vm_compute;reflexivity]
| vm_compute in H';exact H'
])
end.
Function all_le (l1 l2:list Z) {struct l1}: Prop :=
match l1 with
| nil =>
match l2 with
| nil => True
| _ => False
end
| x::l1 =>
match l2 with
| nil => False
| y::l2 =>
x <= y /\ all_le l1 l2
end
end
.
Lemma all_le_def : forall l1 l2, all_le l1 l2 <-> (length l1 = length l2 /\ forall x y, In (x,y) (combine l1 l2) -> x <= y).
Proof.
intros l1 l2;functional induction (all_le l1 l2).
simpl;tauto.
simpl.
destruct l2.
split;try tauto.
split;try tauto.
simpl;inversion 1;discriminate.
simpl.
split;try tauto.
simpl;inversion 1;discriminate.
simpl.
destruct IHP as [lhs rhs].
split.
intros [H1 H2].
destruct (lhs H2) as [Heq Hforall];split.
f_equal.
exact Heq.
intros x' y' [h|h].
injection h;clear h;intros;subst;exact H1.
auto.
clear lhs.
intros [H1 H2].
split;auto.
Qed.
Lemma jump_length : forall A n (l1 l2:list A), length l1 = length l2 -> length (jump n l1) = length (jump n l2).
Proof.
induction n;simpl;intros l1 l2 Hlenght.
do 2 apply IHn.
destruct l1;destruct l2;simpl in Hlenght;try discriminate.
reflexivity.
simpl. injection Hlenght;auto.
do 2 apply IHn.
assumption.
destruct l1;destruct l2;simpl in Hlenght;try discriminate.
reflexivity.
simpl. injection Hlenght;auto.
Qed.
Lemma jump_combine :
forall A n (l1 l2:list A), jump n (combine l1 l2) = combine (jump n l1) (jump n l2).
Proof.
induction n; simpl.
intros l1 l2.
do 2 rewrite <- IHn.
do 2 f_equal.
destruct l1;destruct l2;simpl;try reflexivity.
destruct l1;simpl; reflexivity.
intros l1 l2.
do 2 rewrite <- IHn.
do 2 f_equal.
intros l1 l2.
destruct l1;destruct l2;simpl;try reflexivity.
destruct l1;simpl; reflexivity.
Qed.
Lemma pos_pol_incr :
forall (p:Pol Z), all_coef_pos p = true ->
forall l1 l2, all_le l1 l2 -> all_mem_pos l1 ->
0<=Pphi 0 Zplus Zmult (IDphi (R:=Z)) l1 p <= Pphi 0 Zplus Zmult (IDphi (R:=Z)) l2 p.
Proof.
intros p;functional induction (all_coef_pos p).
intro;discriminate.
intros _.
simpl.
destruct c;simpl in y;try discriminate;simpl;split;unfold IDphi;auto with zarith.
simpl.
intros H l1 l2 H0 H1.
apply IHb.
exact H.
rewrite all_le_def in H0|-*.
destruct H0 as [Hlength Hforall].
split.
apply jump_length;exact Hlength.
intros x y H0;apply Hforall;apply jump_in with _x.
rewrite jump_combine;assumption.
rewrite <- all_mem_pos_def in H1|-*.
intros c H2;apply H1;apply jump_in with _x;assumption.
simpl.
intros H l1 l2 H0 H1.
assert (0<=pow_pos Zmult (hd 0 l1) _x <= pow_pos Zmult (hd 0 l2) _x).
destruct l1;destruct l2;simpl in H0;try tauto;simpl;auto with zarith.
clear;induction _x;simpl;auto with zarith.
destruct H0.
simpl in H1;destruct H1 as [ H1 _ ].
clear - H0 H1.
assert (0<=z0);auto with zarith.
generalize dependent z0;generalize dependent z.
induction _x;simpl;intros.
assert (0<=pow_pos Zmult z _x) by (clear -H1;induction _x;simpl;auto with zarith).
assert (z*pow_pos Zmult z _x <= z0 * pow_pos Zmult z0 _x).
destruct (IH_x _ H1 _ H0 H);apply Zle_trans with (z0*pow_pos Zmult z _x);
auto with zarith.
split.
auto with zarith.
destruct (IH_x _ H1 _ H0 H).
do 2 rewrite Zmult_assoc.
apply Zle_trans with (z*pow_pos Zmult z _x * pow_pos Zmult z0 _x);auto with zarith.
destruct (IH_x _ H1 _ H0 H).
split;auto with zarith.
assert (0<= pow_pos Zmult z0 _x).
apply Zle_trans with (pow_pos Zmult z _x);auto with zarith.
apply Zle_trans with (pow_pos Zmult z _x*pow_pos Zmult z0 _x);auto with zarith.
auto with zarith.
assert (0 <= Pphi 0 Zplus Zmult (IDphi (R:=Z)) l1 p0 <= Pphi 0 Zplus Zmult (IDphi (R:=Z)) l2 p0).
apply IHb.
symmetry in H.
destruct (@andb_true_eq _ _ H);auto.
assumption.
assumption.
assert (0<=Pphi 0 Zplus Zmult (IDphi (R:=Z)) (tail l1) q <= Pphi 0 Zplus Zmult (IDphi (R:=Z)) (tail l2) q).
apply IHb0.
symmetry in H;destruct (@andb_true_eq _ _ H);auto.
destruct l1;destruct l2;simpl in H0;simpl;auto;try tauto.
rewrite <- all_mem_pos_def in H1|-*.
intros c H4; apply H1;apply tail_in;exact H4.
destruct H2;destruct H3;destruct H4;split;auto with zarith.
assert (0<=Pphi 0 Zplus Zmult (IDphi (R:=Z)) l2 p0) by
(apply Zle_trans with (Pphi 0 Zplus Zmult (IDphi (R:=Z)) l1 p0);auto with zarith).
assert (0<=Pphi 0 Zplus Zmult (IDphi (R:=Z)) (tail l2) q) by
(apply Zle_trans with (Pphi 0 Zplus Zmult (IDphi (R:=Z)) (tail l1) q);auto with zarith).
assert (0 <= pow_pos Zmult (hd 0 l2) _x) by
(apply Zle_trans with (pow_pos Zmult (hd 0 l1) _x);auto with zarith).
assert (Pphi 0 Zplus Zmult (IDphi (R:=Z)) l1 p0 * pow_pos Zmult (hd 0 l1) _x <=
Pphi 0 Zplus Zmult (IDphi (R:=Z)) l2 p0 * pow_pos Zmult (hd 0 l2) _x)
by (apply Zle_trans with (Pphi 0 Zplus Zmult (IDphi (R:=Z)) l2 p0 * pow_pos Zmult (hd 0 l1) _x);auto with zarith).
auto with zarith.
Qed.
Lemma pos_pol_incr' :
forall (p:Pol Z), all_coef_pos p = true ->
forall l1 l2, all_le l1 l2 -> all_mem_pos l1 ->
0<=@Pphi_pow _ 0 1 Zplus Zmult Zminus Zopp _ 0 1 Zeq_bool (IDphi (R:=Z)) _ Z_of_N Zpower (get_sign_None (C:=Z)) l1 p <=
@Pphi_pow _ 0 1 Zplus Zmult Zminus Zopp _ 0 1 Zeq_bool (IDphi (R:=Z)) _ Z_of_N Zpower (get_sign_None (C:=Z)) l2 p.
Proof.
intros p H l1 l2 H0 H1.
replace (@Pphi_pow _ 0 1 Zplus Zmult Zminus Zopp _ 0 1 Zeq_bool (IDphi (R:=Z)) _ Z_of_N Zpower (get_sign_None (C:=Z)) l1 p)
with (Pphi 0 Zplus Zmult (@IDphi Z) l1 p).
replace (Pphi_pow 0 1 Zplus Zmult Zminus Zopp 0 1 Zeq_bool
(IDphi (R:=Z)) Z_of_N Zpower (get_sign_None (C:=Z)) l2 p)
with (Pphi 0 Zplus Zmult (@IDphi Z) l2 p).
apply pos_pol_incr;assumption.
symmetry;eapply Pphi_pow_ok with (1:=InitialRing.Zsth) (C:= Z).
exact InitialRing.Zeqe.
exact (@Rth_ARth _ _ _ _ _ _ _ _ InitialRing.Zsth InitialRing.Zeqe InitialRing.Zth).
eexact (@IDmorph Z Z0 1 Zplus Zmult Zminus Zopp _ InitialRing.Zsth Zeq_bool InitialRing.Zeqb_ok).
exact Zpower_theory.
constructor.
destruct c;simpl;try (intros;discriminate).
symmetry;eapply Pphi_pow_ok with (1:=InitialRing.Zsth) (C:= Z).
exact InitialRing.Zeqe.
exact (@Rth_ARth _ _ _ _ _ _ _ _ InitialRing.Zsth InitialRing.Zeqe InitialRing.Zth).
eexact (@IDmorph Z Z0 1 Zplus Zmult Zminus Zopp _ InitialRing.Zsth Zeq_bool InitialRing.Zeqb_ok).
exact Zpower_theory.
constructor.
destruct c;simpl;try (intros;discriminate).
Qed.
Lemma pos_expr_incr_aux :
forall pe,
all_coef_pos (norm_subst 0 1 Zplus Zmult Zminus Zopp Zeq_bool ring_subst_niter nil pe) = true ->
forall l1 l2, all_le l1 l2 -> all_mem_pos l1 ->
0 <= PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower l1 pe
<= ( PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower l2 pe) .
Proof.
intros pe H l1 l2 H0 H1.
rewrite Zr_ring_lemma2 with (n:=ring_subst_niter) (lH:=@nil (PExpr Z * PExpr Z))
(lmp:=@nil (Mon * Pol Z)) (pe:=pe) (npe:=norm_subst 0 1 Zplus Zmult Zminus Zopp Zeq_bool ring_subst_niter nil
pe).
rewrite Zr_ring_lemma2 with (n:=ring_subst_niter) (lH:=@nil (PExpr Z * PExpr Z))
(lmp:=@nil (Mon * Pol Z)) (pe:=pe) (npe:=norm_subst 0 1 Zplus Zmult Zminus Zopp Zeq_bool ring_subst_niter nil
pe).
apply pos_pol_incr';assumption.
vm_compute;exact I.
vm_compute;reflexivity.
reflexivity.
vm_compute;exact I.
vm_compute;reflexivity.
reflexivity.
Qed.
Lemma pos_expr_incr :
forall pe,
all_coef_pos (norm_subst 0 1 Zplus Zmult Zminus Zopp Zeq_bool ring_subst_niter nil pe) = true ->
forall l1 l2, all_le l1 l2 -> all_mem_pos l1 ->
PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower l1 pe
<= ( PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower l2 pe) .
Proof.
intros pe H l1 l2 H0 H1.
destruct (pos_expr_incr_aux pe H l1 l2 H0 H1) as [_ h];exact h.
Qed.
Ltac modify_FV H l :=
match l with
| nil => constr:(@nil Z)
| ?x::?l =>
match type of H with
| ?p <= x =>
match p with
| 0 => fail 1
| _ =>
constr:(p::l)
end
end
| ?y::?l =>
let fv' := modify_FV H l in
constr:(y::fv')
end.
Ltac set_as_var_if_needed p :=
let set_as_var :=
let x := fresh "x" in
assert (0<=p) by ring_ineq
in
match p with
| context [Zplus _ _] => set_as_var
| context [Zmult _ _] => set_as_var
| context [Zminus _ _] => set_as_var
| context [Zopp _] => set_as_var
| _ => idtac
end
.
Ltac ring_ineq_same_pol H :=
try exact H;
match type of H with
| ?p <= ?q =>
(set_as_var_if_needed p;
set_as_var_if_needed q)
end;
match goal with
| |- ?p <= ?q =>
let mkFV := FV Zcst Zpow_tac Zplus Zmult Zminus Zopp Zpower in
let mkPol := mkPolexpr Z Zcst Zpow_tac Zplus Zmult Zminus Zopp Zpower in
let fv2 := mkFV q (@List.nil Z) in
let fv1 := modify_FV H fv2 in
let qe := mkPol q fv2 in
let p' := constr:(Ring_polynom.PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower fv1 qe) in
let q' := constr:(Ring_polynom.PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) Z_of_N Zpower fv2 qe) in
let H':= fresh "H" in
(assert (H':p' <= q');[
apply pos_expr_incr;
[vm_compute;reflexivity|
cbv beta iota zeta delta [all_le all_mem_pos];
repeat split;auto with zarith|
cbv beta iota zeta delta [all_le all_mem_pos];
repeat split;auto with zarith
]
| vm_compute in H'|-*;exact H'
])
end
.
Ltac prove_ineq :=
match goal with
| H:?p <= ?x |- context C [ ?x ] =>
match p with
| 0 => fail 1
| _ =>
let e := context C [ x ] in
match e with
| _ <= ?e =>
let e' := eval pattern x in e in
match e' with
?f _ =>
apply Zle_trans with (f p);
[clear H;prove_ineq|
let H' := fresh "H" in
assert (H':forall a b, 0 <= a -> a <= b -> f a <= f b);
[
let h := fresh "h" in
(cbv beta;do 3 intro;intro h;ring_ineq_same_pol h)
|
cbv beta in H'; refine (H' _ _ _ H);ring_ineq
]
]
end
| _ < ?e =>
let e' := eval pattern x in e in
match e' with
?f _ =>
apply Zlt_le_trans with (f p);
[clear H;prove_ineq|
let H' := fresh "H" in
assert (H':forall a b, 0 <= a -> a <= b -> f a <= f b);
[
let h := fresh "h" in
(cbv beta;do 3 intro;intro h;ring_ineq_same_pol h)
|
cbv beta in H'; refine (H' _ _ _ H);ring_ineq
]
]
end
end
end
| _ => ring_ineq
end.
Ltac soft_prove_ineq :=
match goal with
| H:?p <= ?x |- context C [ ?x ] =>
match p with
| 0 => fail 1
| _ =>
let e := context C [ x ] in
match e with
| _ <= ?e =>
let e' := eval pattern x in e in
match e' with
?f _ =>
apply Zle_trans with (f p);
[clear H;soft_prove_ineq| try ring_ineq_same_pol H]
end
| _ < ?e =>
let e' := eval pattern x in e in
match e' with
?f _ =>
apply Zlt_le_trans with (f p);
[clear H;soft_prove_ineq| try ring_ineq_same_pol H
]
end
end
end
| _ => try ring_ineq
end.
Ltac check_pos p :=
match p with
| xH => constr:true
| xI ?p => check_pos p
| xO ?p => check_pos p
| _ => constr:false
end.
Ltac check_Z n :=
match n with
| Z0 => constr:false
| Zpos ?p => check_pos p
| Zneg ?p => check_pos p
| _ => constr:false
end.
Ltac simplify_one_ineq H :=
match type of H with
?p <= ?x =>
match p with
| 0 => fail 1 | 1 => fail 1
| ?n =>
match check_Z n with
| true =>
match type of H with
?p <= ?x =>
let e := eval pattern p in x in
match e with
?f _ =>
let f' := let f'' := eval cbv beta in (f 1) in constr:f'' in
let prov := fresh "prov" in
let H' := fresh "H" in
(assert (prov:x = p*f') by ring;
assert (H':1<= f') by omega; clear prov H;repeat rewrite Zmult_1_l in H' )||fail 1
end
end
| false => fail 0
end
end
end
.
Ltac simplify_ineq := repeat (match goal with H: _ <= _ |- _ => simplify_one_ineq H end).