# Library Coqtail.Reals.Rsequence.Rsequence_tactics_reflection

Require Import Rbase MyRIneq.
Require Import Rsequence_def Rsequence_facts Rsequence_cv_facts.

Require Import List.
Require Import Option.
Require Import Ass_handling.

Inductive rseq :=
| rseq_cst : (r : R), rseq
| rseq_var : (n : nat), rseq
| rseq_opp : (r : rseq), rseq
| rseq_plus : (rl rr : rseq), rseq
| rseq_minus : (rl rr : rseq), rseq.

Inductive rseq_limit :=
| minus_inf : rseq_limit
| finite : (l : R), rseq_limit
| plus_inf : rseq_limit.

Definition is_limit r l := match l with
| minus_infRseq_cv_neg_infty r
| finite lRseq_cv r l
| plus_infRseq_cv_pos_infty r
end.

Lemma is_limit_ext : r s k l,
is_limit r k
r == sk = l
is_limit s l.
Proof.
intros r s k [] Hrk Hrs Hkl ;
[ eapply Rseq_cv_neg_infty_eq_compat
| eapply Rseq_cv_eq_compat ; [symmetry |]
| eapply Rseq_cv_pos_infty_eq_compat ]
; subst ; eassumption.
Qed.

Definition Rseq_with_limit := {r : Rseq & {l : rseq_limit | is_limit r l}}.

Definition rseq_limit_opp l := match l with
| minus_infplus_inf
| finite ufinite (- u)
| plus_infminus_inf
end.

Lemma rseq_limit_opp_is_limit : r l,
is_limit r l
is_limit (- r) (rseq_limit_opp l).
Proof.
intros r [] Hl ; simpl ;
[ apply Rseq_cv_neg_infty_opp_compat
| apply Rseq_cv_opp_compat
| apply Rseq_cv_pos_infty_opp_compat] ;
assumption.
Qed.

Definition rseq_limit_add ll lr := match ll, lr with
| minus_inf, plus_infNone
| plus_inf , minus_infNone
| minus_inf, _Some minus_inf
| _ , minus_infSome minus_inf
| plus_inf , _Some plus_inf
| _ , plus_infSome plus_inf
| finite u , finite vSome (finite (u + v))
end.

Fixpoint comp_limit (r : rseq) (env : list Rseq_with_limit) : option rseq_limit :=
match r with
| rseq_cst rReturn (finite r)
| rseq_var nBind (nth_error env n) (fun xReturn (projT1 (projT2 x)))
| rseq_opp rBind (comp_limit r env) (fun lSome (rseq_limit_opp l))
| rseq_plus rl rrBind (comp_limit rl env) (fun ll
Bind (comp_limit rr env) (fun lrrseq_limit_add ll lr))
| rseq_minus rl rrBind (comp_limit rl env) (fun ll
Bind (comp_limit rr env) (fun lrrseq_limit_add ll (rseq_limit_opp lr)))
end.

Fixpoint comp_rseq (r : rseq) (env : list Rseq_with_limit) := match r with
| rseq_cst rReturn (Rseq_constant r)
| rseq_var nBind (nth_error env n) (fun unSome (projT1 un))
| rseq_opp rBind (comp_rseq r env) (fun unSome (Rseq_opp un))
| rseq_plus rl rrBind (comp_rseq rl env) (fun un
Bind (comp_rseq rr env) (fun vnSome (Rseq_plus un vn)))
| rseq_minus rl rrBind (comp_rseq rl env) (fun un
Bind (comp_rseq rr env) (fun vnSome (Rseq_minus un vn)))
end.

Ltac fold_is_limit := match goal with
| |- Rseq_cv ?r ?lfold (is_limit r (finite l))
| |- Rseq_cv_neg_infty ?rfold (is_limit r minus_inf)
| |- Rseq_cv_pos_infty ?rfold (is_limit r plus_inf)
end.

Lemma comp_rseq_limit_compat : r env un l,
comp_rseq r env = Some un
comp_limit r env = Some l
is_limit un l.
Proof.
intros r env ; induction r ; intros un l Hun Hl ; simpl in ×.
inversion Hun ; inversion Hl ; apply Rseq_constant_cv.
destruct (nth_error env n) as [Hget |].
inversion Hun ; inversion Hl ; apply (projT2 (projT2 Hget)).
inversion Hl.
destruct (comp_rseq r env) as [vn |] ; [| inversion Hun] ;
destruct (comp_limit r env) as [lo |] ; [| inversion Hl] ;
inversion Hun ; inversion Hl.
apply rseq_limit_opp_is_limit, IHr ; reflexivity.
destruct (comp_rseq r1 env) as [vn |] ; [| inversion Hun] ;
destruct (comp_limit r1 env) as [ll |] ; [| inversion Hl] ;
destruct (comp_rseq r2 env) as [wn |] ; [| inversion Hun] ;
destruct (comp_limit r2 env) as [lr |] ; [| inversion Hl].
destruct ll ; destruct lr ; inversion Hun ; inversion Hl ;
subst.
apply Rseq_cv_neg_infty_plus_compat ; fold_is_limit ;
[apply IHr1 | apply IHr2] ; reflexivity.
eapply Rseq_cv_finite_plus_neg_infty_l ; fold_is_limit ;
[apply IHr1 | apply IHr2] ; reflexivity.
eapply Rseq_cv_finite_plus_neg_infty_r ; fold_is_limit ;
[apply IHr1 | apply IHr2] ; reflexivity.
eapply Rseq_cv_plus_compat ; fold_is_limit ;
[apply IHr1 | apply IHr2] ; reflexivity.
eapply Rseq_cv_finite_plus_pos_infty_r ; fold_is_limit ;
[apply IHr1 | apply IHr2] ; reflexivity.
eapply Rseq_cv_finite_plus_pos_infty_l ; fold_is_limit ;
[apply IHr1 | apply IHr2] ; reflexivity.
apply Rseq_cv_pos_infty_plus_compat ; fold_is_limit ;
[apply IHr1 | apply IHr2] ; reflexivity.
destruct (comp_rseq r1 env) as [vn |] ; [| inversion Hun] ;
destruct (comp_limit r1 env) as [ll |] ; [| inversion Hl] ;
destruct (comp_rseq r2 env) as [wn |] ; [| inversion Hun] ;
destruct (comp_limit r2 env) as [lr |] ; [| inversion Hl].
inversion Hun ; eapply (is_limit_ext (Rseq_plus vn (Rseq_opp wn))) ;
[| intro n ; unfold Rseq_plus, Rseq_minus, Rseq_opp ; ring | reflexivity].
destruct ll ; destruct lr ; inversion Hl ; subst.
apply Rseq_cv_finite_plus_neg_infty_l with (- l0)%R ; fold_is_limit ;
[apply IHr1 | fold (rseq_limit_opp (finite l0)) ;
apply rseq_limit_opp_is_limit, IHr2] ; reflexivity.
apply Rseq_cv_neg_infty_plus_compat ; fold_is_limit ;
[apply IHr1 | fold (rseq_limit_opp plus_inf) ;
apply rseq_limit_opp_is_limit, IHr2] ; reflexivity.
apply Rseq_cv_finite_plus_pos_infty_r with l0 ; fold_is_limit ;
[apply IHr1 | fold (rseq_limit_opp minus_inf) ;
apply rseq_limit_opp_is_limit, IHr2] ; reflexivity.
apply Rseq_cv_plus_compat ; fold_is_limit ;
[apply IHr1 | fold (rseq_limit_opp (finite l1)) ;
apply rseq_limit_opp_is_limit, IHr2] ; reflexivity.
eapply Rseq_cv_finite_plus_neg_infty_r ; fold_is_limit ;
[apply IHr1 | fold (rseq_limit_opp plus_inf) ;
apply rseq_limit_opp_is_limit, IHr2] ; reflexivity.
apply Rseq_cv_pos_infty_plus_compat ; fold_is_limit ;
[apply IHr1 | fold (rseq_limit_opp minus_inf) ;
apply rseq_limit_opp_is_limit, IHr2] ; reflexivity.
apply Rseq_cv_finite_plus_pos_infty_l with (- l0)%R ; fold_is_limit ;
[apply IHr1 | fold (rseq_limit_opp (finite l0)) ;
apply rseq_limit_opp_is_limit, IHr2] ; reflexivity.
Qed.

Definition rseq_precondition r env un l :=
match comp_rseq r env with
| NoneFalse
| Some vn
match comp_limit r env with
| NoneFalse
| Some v(un == vn) (l = v)
end
end.

Lemma tactic_correctness : r env un l,
rseq_precondition r env un l
is_limit un l.
Proof.
unfold rseq_precondition ; intros r env un l ;
destruct_eq (comp_rseq r env) ;
destruct_eq (comp_limit r env) ;
intros [].
intros ; eapply is_limit_ext ;
[ eapply comp_rseq_limit_compat | |] ;
symmetry ; eassumption.
Qed.