proposition: Theorem root_max_is_zero: forall p l, ulist l -> (forall i, In i p -> P i) -> (forall i, In i l -> P i) -> (forall x, In x l -> eval p x = zero) -> (length p <= length l)%nat -> forall x, (In x p) -> x = zero.
proof: Proof. intros p l; generalize p; elim l; clear l p; simpl; auto. intros p; case p; simpl; auto. intros _ _ _ _ _ x H; case H. intros a p1 _ _ _ _ H; contradict H; auto with arith. intros a p1 Rec p; case p. simpl; auto. intros _ _ _ _ _ x H; case H. simpl; intros a1 p2 H H1 H2 H3 H4 x H5. assert (Ha1: a1 = zero). assert (Hu: (eval (a1::p2) zero = zero)). apply root_max with (l := a :: p1); auto. rewrite <- Hu; simpl; rewrite mult_zero; try rewrite plus_comm; sauto. case H5; clear H5; intros H5; subst; auto. apply Rec with p2; auto with arith. apply ulist_inv with (1 := H). intros x1 Hx1. case (In_dec A_dec zero p1); intros Hz. case (in_permutation_ex _ zero p1); auto; intros p3 Hp3. apply root_max with (l := a::p3); auto. apply ulist_inv with zero. apply ulist_perm with (a::p1); auto. apply permutation_trans with (a:: (zero:: p3)); auto. apply permutation_skip; auto. apply permutation_sym; auto. simpl; intros x2 [Hx2 | Hx2]; subst; auto. apply H2; right; apply permutation_in with (1 := Hp3); auto with datatypes. simpl; intros x2 [Hx2 | Hx2]; subst. case (mult_integral x2 (eval p2 x2)); auto. rewrite <- H3 with x2; sauto. rewrite plus_zero; auto. intros H6; case (ulist_app_inv _ (x2::nil) p1 x2) ; auto with datatypes. rewrite H6; apply permutation_in with (1 := Hp3); auto with datatypes. case (mult_integral x2 (eval p2 x2)); auto. apply H2; right; apply permutation_in with (1 := Hp3); auto with datatypes. apply eval_P; auto. apply H2; right; apply permutation_in with (1 := Hp3); auto with datatypes. rewrite <- H3 with x2; sauto; try right. apply sym_equal; apply plus_zero; auto. apply Pmult; auto. apply H2; right; apply permutation_in with (1 := Hp3); auto with datatypes. apply eval_P; auto. apply H2; right; apply permutation_in with (1 := Hp3); auto with datatypes. apply permutation_in with (1 := Hp3); auto with datatypes. intros H6; case (ulist_app_inv _ (zero::nil) p3 x2) ; auto with datatypes. simpl; apply ulist_perm with (1:= (permutation_sym _ _ _ Hp3)). apply ulist_inv with (1 := H). rewrite H6; auto with datatypes. replace (length (a :: p3)) with (length (zero::p3)); auto. rewrite permutation_length with (1 := Hp3); auto with arith. case (mult_integral x1 (eval p2 x1)); auto. rewrite <- H3 with x1; sauto; try right. apply sym_equal; apply plus_zero; auto. intros HH; case Hz; rewrite <- HH; auto. Qed.
imports: ZArith List UList Tactic Permutation