Library Coqtail.Reals.Rintegral.Rintegral_tactic


Require Import Reals.
Require Import Rintegral.
Require Import Rintegral_usual.
Ltac Rint_constr f a b := match goal with
  | id : Rint f a b ?x |- _constr:id
  | id : Rint f b a ?x |- _constr:(Rint_reverse_1 f b a x)
  | _match constr:f with
    | fct_cte ?cconstr:(Rint_constant c a b)
    | (?g + ?h)%Flet H1 := Rint_constr g a b in let H2 := Rint_constr h a b in
                     constr:(Rint_plus g h a b H1 H2)
    | (?g - ?h)%Flet H1 := Rint_constr g a b in let H2 := Rint_constr h a b in
                     constr:(Rint_minus g h a b H1 H2)
    | ((fct_cte ?c) × ?h)%Flet H := Rint_constr h a b in
                     constr:(Rint_scalar_mult_compat_l h a b H)
    | (?h × (fct_cte ?c))%Flet H := Rint_constr h a b in
                     constr:(Rint_scalar_mult_compat_r h a b H)
  end

end.

Ltac rint_tac := match goal with
  | id : Rint ?f ?a ?b ?x |- Rint ?f ?a ?b ?xassumption
  | |- Rint ?f ?a ?aapply Rint_singleton
  | |- Rint ?f ?a ?b ?xlet H := Rint_constr f a b in match type of H with
         Rint f a b ?yreplace x with y ; [apply H | subst; try reflexivity; try field; intuition] end
end.