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 ?c ⇒ constr:(Rint_constant c a b)
    | (?g + ?h)%F ⇒ let 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)%F ⇒ let 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)%F ⇒ let H := Rint_constr h a b in
                     constr:(Rint_scalar_mult_compat_l h a b H)
    | (?h × (fct_cte ?c))%F ⇒ let 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 ?x ⇒ assumption
  | |- Rint ?f ?a ?a ⇒ apply Rint_singleton
  | |- Rint ?f ?a ?b ?x ⇒ let H := Rint_constr f a b in match type of H with
         Rint f a b ?y ⇒ replace x with y ; [apply H | subst; try reflexivity; try field; intuition] end
end.