# Library Coqtail.Reals.Rsequence.Rsequence_tactics

Require Import Rsequence_def.
Require Import Rsequence_facts.
Require Import Rseries_def.
Require Export Reals.
Require Import Fourier.

Open Local Scope Rseq_scope.

# A tactic that constructs the limit of a sequence and the proof that this

limit is exact

Ltac neq := fun n
match goal with
| id : (n 0)%R |- _constr: id
| id : (n > 0) |- _constr: (Rgt_not_eq _ _ id)
| id : (n < 0) |- _constr: (Rlt_not_eq _ _ id)
| _
match constr:n with
| Rabs ?a
let H := neq a in constr: (Rabs_no_R0 _ H)
end
end.

Ltac rseq_fold Un := match constr:Un with
| ?Vn ?c ?Wnlet Vn' := rseq_fold Vn in let Wn' := rseq_fold Wn in constr:(Vn' c Wn')
| fun x : nat ⇒ ?Vn xrseq_fold Vn
| fun x : nat ⇒ (?Vn + ?Wn)%Ridtac "bla"

| _constr:Un
end.

Ltac rseq_lim := fun Unmatch goal with
Case 1: there exists a proof that the sequence converges in the hypothesis
| id : Rseq_cv Un ?l |- _constr:id
| id : Rseq_cv_pos_infty Un |- _constr:id
| id : Rseq_cv_neg_infty Un |- _constr:id
| _
Case 2: we have to deconstruct the sequence to infer the limit
match constr:Un with

| (Rseq_constant ?a) ⇒ constr:(Rseq_constant_cv a)

| (/ ?Vn) ⇒
let H1 := rseq_lim Vn in
match type of H1 with
| Rseq_cv Vn ?l
let H2 := neq l in
constr:(Rseq_cv_inv_compat _ _ H1 H2)
| Rseq_cv_pos_infty Vn
constr:(Rseq_cv_pos_infty_inv_compat _ H1)
| Rseq_cv_neg_infty Vn
constr:(Rseq_cv_neg_infty_inv_compat _ H1) end

| (?Vn/ ?Wn) ⇒
let H1 := rseq_lim Vn in
let H2 := rseq_lim Wn in
match type of H1 with
| Rseq_cv Vn ?lvmatch type of H2 with
| (Rseq_cv Wn ?lw) ⇒
let H3 := neq lw in constr:(Rseq_cv_div_compat _ _ _ _ H1 H2 H3)
| Rseq_cv_pos_infty Wn
constr:(Rseq_cv_pos_infty_div_compat _ _ _ H2 H1)
| Rseq_cv_neg_infty Wn
constr:(Rseq_cv_neg_infty_div_compat _ _ _ H2 H1) end
end

| (- ?Vn) ⇒
let H1 := rseq_lim Vn in
match type of H1 with
| Rseq_cv Vn ?lconstr:(Rseq_cv_opp_compat _ _ H1)
| Rseq_cv_pos_infty Vnconstr:(Rseq_cv_pos_infty_opp_compat _ H1)
| Rseq_cv_neg_infty Vnconstr:(Rseq_cv_neg_infty_opp_compat _ H1) end

| (?Vn + ?Wn) ⇒
let H1 := rseq_lim Vn in
let H2 := rseq_lim Wn in
match type of H1 with
| Rseq_cv Vn ?lvmatch type of H2 with
| Rseq_cv _ ?lwconstr:(Rseq_cv_plus_compat _ _ _ _ H1 H2)
| Rseq_cv_pos_infty _constr:(Rseq_cv_finite_plus_pos_infty_r _ _ _ H1 H2)
| Rseq_cv_neg_infty _constr:(Rseq_cv_finite_plus_neg_infty_r _ _ _ H1 H2) end
| Rseq_cv_pos_infty Vnmatch type of H2 with
| Rseq_cv _ ?lwconstr:(Rseq_cv_finite_plus_pos_infty_l _ _ _ H2 H1)
| Rseq_cv_pos_infty _constr:(Rseq_cv_pos_infty_plus_compat _ _ H1 H2) end

| Rseq_cv_neg_infty Vnmatch type of H2 with
| Rseq_cv _ ?lwconstr:(Rseq_cv_finite_plus_neg_infty_l _ _ _ H2 H1)
| Rseq_cv_neg_infty _constr:(Rseq_cv_neg_infty_plus_compat _ _ H1 H2)
end
end

| (?Vn - ?Wn) ⇒
let H1 := rseq_lim Vn in
let H2 := rseq_lim Wn in
match type of H1 with
| Rseq_cv Vn ?lvmatch type of H2 with
| (Rseq_cv Wn ?lw) ⇒ constr:(Rseq_cv_minus_compat _ _ _ _ H1 H2)
| Rseq_cv_pos_infty Wnconstr:(Rseq_cv_finite_minus_pos_infty _ _ _ H1 H2)
| Rseq_cv_neg_infty Wnconstr:(Rseq_cv_finite_plus_neg_infty_r _ _ _ H1 H2) end
| Rseq_cv_pos_infty Vnmatch type of H2 with
| (Rseq_cv Wn ?lw) ⇒ constr:(Rseq_cv_finite_minus_pos_infty _ _ _ H2 H1)

| Rseq_cv_neg_infty Wnconstr:(Rseq_cv_pos_minus_neg_infty _ _ H1 H2) end
| Rseq_cv_neg_infty Vnmatch type of H2 with
| (Rseq_cv Wn ?lw) ⇒ constr:(Rseq_cv_finite_minus_neg_infty _ _ _ H2 H1)
| Rseq_cv_pos_infty Wnconstr:(Rseq_cv_neg_minus_pos_infty _ _ H1 H2) end

end

| (?Vn × ?Wn) ⇒
let H1 := rseq_lim Vn in
let H2 := rseq_lim Wn in
match type of H1 with
| Rseq_cv Vn ?lvmatch type of H2 with
| (Rseq_cv Wn ?lw) ⇒ constr:(Rseq_cv_mult_compat _ _ _ _ H1 H2)
end
| Rseq_cv_pos_infty Vnmatch type of H2 with

| Rseq_cv_pos_infty Wnconstr:(Rseq_cv_pos_pos_infty_mult _ _ H1 H2)
| Rseq_cv_neg_infty Wnconstr:(Rseq_cv_pos_neg_infty_mult _ _ H1 H2) end
| Rseq_cv_neg_infty Vnmatch type of H2 with

| Rseq_cv_pos_infty Wnconstr:(Rseq_cv_neg_pos_infty_mult _ _ H1 H2) end
| Rseq_cv_neg_infty Wnconstr:(Rseq_cv_neg_neg_infty_mult _ _ H1 H2)
end

| |?Vn|
let H := rseq_lim Vn in fail

end
end.

Ltac rser_lim := fun Unmatch goal with
| id : Rser_cv Un ?l |- _constr:id
| id : Rser_cv_pos_infty Un |- _constr:id
| id : Rser_cv_neg_infty Un |- _constr:id
| _match constr:Un with
| _idtac
end
end.

Ltac rseq_cv_construct := intros; match goal with
| |- {l | Rseq_cv ?Un l}
let H := rseq_lim Un in
match type of H with
| Rseq_cv _ ?l l ; apply H
end
| |- {l | Rser_cv ?Un l}
let H := rser_lim Un in
match type of H with
| Rser_cv _ ?l l ; apply H
end
| |- Rseq_cv ?Un ?l
let H := rseq_lim Un in
match type of H with
| Rseq_cv _ ?l'replace l with l' ; [apply H | subst; try reflexivity; try field; intuition]
end
| |- Rser_cv ?Un ?l
let H := rser_lim Un in
match type of H with
| Rser_cv _ ?l'replace l with l' ; [apply H | subst; try reflexivity; try field; intuition]
end
| |- Rseq_cv_pos_infty ?Unlet H := rseq_lim Un in apply H
| |- Rseq_cv_neg_infty ?Unlet H := rseq_lim Un in apply H
end.