proposition: 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)).
proof: Proof. 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.
imports: ZArith List UList Tactic Permutation