From ef92beece3147f8af0764521e22cb7fc9a3f32a3 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 24 Feb 2018 10:17:35 -0500 Subject: coqprime in COQPATH (closes #269) --- coqprime/Coqprime/Root.v | 239 ----------------------------------------------- 1 file changed, 239 deletions(-) delete mode 100644 coqprime/Coqprime/Root.v (limited to 'coqprime/Coqprime/Root.v') diff --git a/coqprime/Coqprime/Root.v b/coqprime/Coqprime/Root.v deleted file mode 100644 index 0b432b788..000000000 --- a/coqprime/Coqprime/Root.v +++ /dev/null @@ -1,239 +0,0 @@ - -(*************************************************************) -(* This file is distributed under the terms of the *) -(* GNU Lesser General Public License Version 2.1 *) -(*************************************************************) -(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) -(*************************************************************) - -(*********************************************************************** - Root.v - - Proof that a polynomial has at most n roots -************************************************************************) -Require Import ZArith. -Require Import List. -Require Import UList. -Require Import Tactic. -Require Import Permutation. - -Open Scope Z_scope. - -Section Root. - -Variable A: Set. -Variable P: A -> Prop. -Variable plus mult: A -> A -> A. -Variable op: A -> A. -Variable zero one: A. - - -Let pol := list A. - -Definition toA z := -match z with - Z0 => zero -| Zpos p => iter_pos _ (plus one) zero p -| Zneg p => op (iter_pos _ (plus one) zero p) -end. - -Fixpoint eval (p: pol) (x: A) {struct p} : A := -match p with - nil => zero -| a::p1 => plus a (mult x (eval p1 x)) -end. - -Fixpoint div (p: pol) (x: A) {struct p} : pol * A := -match p with - nil => (nil, zero) -| a::nil => (nil, a) -| a::p1 => - (snd (div p1 x)::fst (div p1 x), - (plus a (mult x (snd (div p1 x))))) -end. - -Hypothesis Pzero: P zero. -Hypothesis Pplus: forall x y, P x -> P y -> P (plus x y). -Hypothesis Pmult: forall x y, P x -> P y -> P (mult x y). -Hypothesis Pop: forall x, P x -> P (op x). -Hypothesis plus_zero: forall a, P a -> plus zero a = a. -Hypothesis plus_comm: forall a b, P a -> P b -> plus a b = plus b a. -Hypothesis plus_assoc: forall a b c, P a -> P b -> P c -> plus a (plus b c) = plus (plus a b) c. -Hypothesis mult_zero: forall a, P a -> mult zero a = zero. -Hypothesis mult_comm: forall a b, P a -> P b -> mult a b = mult b a. -Hypothesis mult_assoc: forall a b c, P a -> P b -> P c -> mult a (mult b c) = mult (mult a b) c. -Hypothesis mult_plus_distr: forall a b c, P a -> P b -> P c -> mult a (plus b c) = plus (mult a b) (mult a c). -Hypothesis plus_op_zero: forall a, P a -> plus a (op a) = zero. -Hypothesis mult_integral: forall a b, P a -> P b -> mult a b = zero -> a = zero \/ b = zero. -(* Not necessary in Set just handy *) -Hypothesis A_dec: forall a b: A, {a = b} + {a <> b}. - -Theorem eval_P: forall p a, P a -> (forall i, In i p -> P i) -> P (eval p a). -intros p a Pa; elim p; simpl; auto with datatypes. -intros a1 l1 Rec H; apply Pplus; auto. -Qed. - -Hint Resolve eval_P. - -Theorem div_P: forall p a, P a -> (forall i, In i p -> P i) -> (forall i, In i (fst (div p a)) -> P i) /\ P (snd (div p a)). -intros p a Pa; elim p; auto with datatypes. -intros a1 l1; case l1. -simpl; intuition. -intros a2 p2 Rec Hi; split. -case Rec; auto with datatypes. -intros H H1 i. -replace (In i (fst (div (a1 :: a2 :: p2) a))) with - (snd (div (a2::p2) a) = i \/ In i (fst (div (a2::p2) a))); auto. -intros [Hi1 | Hi1]; auto. -rewrite <- Hi1; auto. -change ( P (plus a1 (mult a (snd (div (a2::p2) a))))); auto with datatypes. -apply Pplus; auto with datatypes. -apply Pmult; auto with datatypes. -case Rec; auto with datatypes. -Qed. - - -Theorem div_correct: - forall p x y, P x -> P y -> (forall i, In i p -> P i) -> eval p y = plus (mult (eval (fst (div p x)) y) (plus y (op x))) (snd (div p x)). -intros p x y; elim p; simpl. -intros; rewrite mult_zero; try rewrite plus_zero; auto. -intros a l; case l; simpl; auto. -intros _ px py pa; rewrite (fun x => mult_comm x zero); repeat rewrite mult_zero; try apply plus_comm; auto. -intros a1 l1. -generalize (div_P (a1::l1) x); simpl. -match goal with |- context[fst ?A] => case A end; simpl. -intros q r Hd Rec px py pi. -assert (pr: P r). -case Hd; auto. -assert (pa1: P a1). -case Hd; auto. -assert (pey: P (eval q y)). -apply eval_P; auto. -case Hd; auto. -rewrite Rec; auto with datatypes. -rewrite (fun x y => plus_comm x (plus a y)); try rewrite <- plus_assoc; auto. -apply f_equal2 with (f := plus); auto. -repeat rewrite mult_plus_distr; auto. -repeat (rewrite (fun x y => (mult_comm (plus x y))) || rewrite mult_plus_distr); auto. -rewrite (fun x => (plus_comm x (mult y r))); auto. -repeat rewrite plus_assoc; try apply f_equal2 with (f := plus); auto. -2: repeat rewrite mult_assoc; try rewrite (fun y => mult_comm y (op x)); - repeat rewrite mult_assoc; auto. -rewrite (fun z => (plus_comm z (mult (op x) r))); auto. -repeat rewrite plus_assoc; try apply f_equal2 with (f := plus); auto. -2: apply f_equal2 with (f := mult); auto. -repeat rewrite (fun x => mult_comm x r); try rewrite <- mult_plus_distr; auto. -rewrite (plus_comm (op x)); try rewrite plus_op_zero; auto. -rewrite (fun x => mult_comm x zero); try rewrite mult_zero; try rewrite plus_zero; auto. -Qed. - -Theorem div_correct_factor: - forall p a, (forall i, In i p -> P i) -> P a -> - eval p a = zero -> forall x, P x -> eval p x = (mult (eval (fst (div p a)) x) (plus x (op a))). -intros p a Hp Ha H x px. -case (div_P p a); auto; intros Hd1 Hd2. -rewrite (div_correct p a x); auto. -generalize (div_correct p a a). -rewrite plus_op_zero; try rewrite (fun x => mult_comm x zero); try rewrite mult_zero; try rewrite plus_zero; try rewrite H; auto. -intros H1; rewrite <- H1; auto. -rewrite (fun x => plus_comm x zero); auto. -Qed. - -Theorem length_decrease: forall p x, p <> nil -> (length (fst (div p x)) < length p)%nat. -intros p x; elim p; simpl; auto. -intros H1; case H1; auto. -intros a l; case l; simpl; auto. -intros a1 l1. -match goal with |- context[fst ?A] => case A end; simpl; auto with zarith. -intros p1 _ H H1. -apply lt_n_S; apply H; intros; discriminate. -Qed. - -Theorem root_max: -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, P x -> eval p x = zero. -intros p l; generalize p; elim l; clear l p; simpl; auto. -intros p; case p; simpl; auto. -intros a p1 _ _ _ _ H; contradict H; auto with arith. -intros a p1 Rec p; case p. -simpl; auto. -intros a1 p2 H H1 H2 H3 H4 x px. -assert (Hu: eval (a1 :: p2) a = zero); auto with datatypes. -rewrite (div_correct_factor (a1 :: p2) a); auto with datatypes. -match goal with |- mult ?X _ = _ => replace X with zero end; try apply mult_zero; auto. -apply sym_equal; apply Rec; auto with datatypes. -apply ulist_inv with (1 := H). -intros i Hi; case (div_P (a1 :: p2) a); auto. -intros x1 H5; case (mult_integral (eval (fst (div (a1 :: p2) a)) x1) (plus x1 (op a))); auto. -apply eval_P; auto. -intros i Hi; case (div_P (a1 :: p2) a); auto. -rewrite <- div_correct_factor; auto. -intros H6; case (ulist_app_inv _ (a::nil) p1 x1); simpl; auto. -left. -apply trans_equal with (plus zero x1); auto. -rewrite <- (plus_op_zero a); try rewrite <- plus_assoc; auto. -rewrite (fun x => plus_comm (op x)); try rewrite H6; try rewrite plus_comm; auto. -apply sym_equal; apply plus_zero; auto. -apply lt_n_Sm_le;apply lt_le_trans with (length (a1 :: p2)); auto with zarith. -apply length_decrease; auto with datatypes. -Qed. - -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. -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. - -End Root. -- cgit v1.2.3