Library Coqtail.Reals.Rsequence.Rsequence_rewrite_facts
Unfolding Rseq_sum
Lemma Rseq_sum_simpl : ∀ Un n,
(Rseq_sum Un (S n) = Rseq_sum Un n + Un (S n))%R.
Proof.
intros ; reflexivity.
Qed.
Rseq_shift(s) simplification rules
Lemma Rseq_shifts_0 : ∀ Un,
Rseq_shifts Un 0 == Un.
Proof.
intros Un n ; unfold Rseq_shifts ; rewrite plus_0_l ;
reflexivity.
Qed.
Lemma Rseq_shifts_O : ∀ Un k,
Rseq_shifts Un k O = Un k.
Proof.
intros Un k ; unfold Rseq_shifts ; rewrite plus_0_r ;
reflexivity.
Qed.
Lemma Rseq_shift_shifts: ∀ Un n,
Rseq_shifts Un (S n) == Rseq_shift (Rseq_shifts Un n).
Proof.
intros Un n k ; unfold Rseq_shift, Rseq_shifts ;
f_equal ; apply plus_n_Sm.
Qed.
Lemma Rseq_shifts_shift: ∀ Un n,
Rseq_shifts Un (S n) == Rseq_shifts (Rseq_shift Un) n.
Proof.
intros Un n k ; reflexivity.
Qed.
Lemma Rseq_shifts_fusion : ∀ An k m,
(Rseq_shifts (Rseq_shifts An k) m == Rseq_shifts An (k + m))%Rseq.
Proof.
intros ; unfold Rseq_shifts ; intro ; rewrite plus_assoc ; reflexivity.
Qed.
Unfolding definitions
Lemma Rseq_minus_simpl : ∀ Un Vn,
Un - Vn == Un + - Vn.
Proof.
intros Un Vn n ; unfold Rseq_minus, Rminus ; reflexivity.
Qed.
Lemma Rseq_div_simpl : ∀ Un Vn,
Un / Vn == Un × / Vn.
Proof.
intros Un Vn n ; unfold Rseq_div, Rdiv ; reflexivity.
Qed.
Lemma Rseq_fact_simpl : ∀ n,
Rseq_fact (S n) = (INR (S n) × Rseq_fact n)%R.
Proof.
intro n ; unfold Rseq_fact ;
rewrite fact_simpl, mult_INR ;
reflexivity.
Qed.
Shifts and common operations
Lemma Rseq_shifts_opp_compat : ∀ An k,
Rseq_shifts (- An) k == - Rseq_shifts An k.
Proof.
intros ; unfold Rseq_shifts ; intro n ; reflexivity.
Qed.
Lemma Rseq_shifts_plus_compat : ∀ An Bn k,
Rseq_shifts (An + Bn) k == Rseq_shifts An k + Rseq_shifts Bn k.
Proof.
intros ; unfold Rseq_shifts ; intro n ; reflexivity.
Qed.
Lemma Rseq_shifts_mult_compat : ∀ An Bn k,
Rseq_shifts (An × Bn) k == Rseq_shifts An k × Rseq_shifts Bn k.
Proof.
intros ; unfold Rseq_shifts ; intro n ; reflexivity.
Qed.
Lemma Rseq_shifts_div_compat : ∀ An Bn k,
Rseq_shifts (An / Bn) k == Rseq_shifts An k / Rseq_shifts Bn k.
Proof.
intros ; unfold Rseq_shifts ; intro n ; reflexivity.
Qed.
Lemma Rseq_shifts_inv_compat : ∀ An k,
Rseq_shifts (/ An) k == / Rseq_shifts An k.
Proof.
intros ; unfold Rseq_shifts ; intro n ; reflexivity.
Qed.
Lemma Rseq_shifts_scal_compat : ∀ (c : R) An k,
Rseq_shifts (c × An) k == c × Rseq_shifts An k.
Proof.
intros ; unfold Rseq_shifts ; intro n ; reflexivity.
Qed.
Action of Rseq_abs on different operations
Lemma Rseq_abs_idempotent : ∀ An,
Rseq_abs (Rseq_abs An) == Rseq_abs An.
Proof.
intros An n ; unfold Rseq_abs ; apply Rabs_Rabsolu.
Qed.
Lemma Rseq_abs_mult : ∀ An Bn,
Rseq_abs (An × Bn) == Rseq_abs An × Rseq_abs Bn.
Proof.
intros An Bn n ; apply Rabs_mult.
Qed.
Lemma Rseq_abs_pow : ∀ r,
Rseq_abs (Rseq_pow r) == Rseq_pow (Rabs r).
Proof.
intros r n ; symmetry ; apply RPow_abs.
Qed.
Lemma Rseq_abs_alt : ∀ An,
Rseq_abs (Rseq_alt An) == Rseq_abs An.
Proof.
intros An n ; unfold Rseq_alt, Rseq_pow ;
rewrite Rseq_abs_mult ; unfold Rseq_mult, Rseq_abs ;
rewrite Rabs_opp1 ; apply Rmult_1_l.
Qed.
Lemma Rseq_abs_zip : ∀ An Bn,
Rseq_abs (Rseq_zip An Bn) == Rseq_zip (Rseq_abs An) (Rseq_abs Bn).
Proof.
intros An Bn n ; unfold Rseq_abs, Rseq_zip ; case (n_modulo_2 n) ;
intros [p Hp] ; reflexivity.
Qed.
Action of Rseq_alt on common operations
Lemma Rseq_alt_involutive : ∀ An,
Rseq_alt (Rseq_alt An) == An.
Proof.
intros An n ; unfold Rseq_alt, Rseq_mult, Rseq_pow.
rewrite <- Rmult_assoc, <- pow_add ;
replace (n + n)%nat with (2 × n)%nat by ring ;
rewrite pow_1_even ; apply Rmult_1_l.
Qed.
Lemma Rseq_alt_scal_l : ∀ An (l : R),
Rseq_alt (l × An) == l × Rseq_alt An.
Proof.
intros An l n ; unfold Rseq_alt, Rseq_mult, Rseq_constant ; ring.
Qed.
Lemma Rseq_alt_scal_r : ∀ An (l : R),
Rseq_alt (An × l) == Rseq_alt An × l.
Proof.
intros An l n ; unfold Rseq_alt, Rseq_mult, Rseq_constant ; ring.
Qed.
Lemma Rseq_alt_opp : ∀ An,
Rseq_alt (- An) == - Rseq_alt An.
Proof.
intros An n ; unfold Rseq_alt, Rseq_mult, Rseq_opp ; ring.
Qed.
Lemma Rseq_alt_plus : ∀ An Bn,
Rseq_alt (An + Bn) == Rseq_alt An + Rseq_alt Bn.
Proof.
intros An Bn n ; unfold Rseq_alt, Rseq_mult, Rseq_plus ; ring.
Qed.
Lemma Rseq_alt_minus : ∀ An Bn,
Rseq_alt (An - Bn) == Rseq_alt An - Rseq_alt Bn.
Proof.
intros An Bn n ; unfold Rseq_alt, Rseq_mult, Rseq_minus ; ring.
Qed.
Lemma Rseq_alt_mult_l : ∀ An Bn,
Rseq_alt (An × Bn) == Rseq_alt An × Bn.
Proof.
intros An Bn n ; unfold Rseq_alt, Rseq_mult ; ring.
Qed.
Lemma Rseq_alt_mult_r : ∀ An Bn,
Rseq_alt (An × Bn) == An × Rseq_alt Bn.
Proof.
intros An Bn n ; unfold Rseq_alt, Rseq_mult ; ring.
Qed.
Lemma Rseq_alt_zip : ∀ An Bn,
Rseq_alt (Rseq_zip An Bn) == Rseq_zip An (- Bn).
Proof.
intros An Bn n ; unfold Rseq_alt, Rseq_zip, Rseq_mult, Rseq_opp, Rseq_pow ;
case (n_modulo_2 n) ; intros [p Hp] ; subst.
rewrite pow_1_even ; apply Rmult_1_l.
rewrite pow_1_odd ; ring.
Qed.
Action of Rseq_zip over simple operations
Lemma Rseq_zip_opp : ∀ An Bn,
- Rseq_zip An Bn == Rseq_zip (- An) (- Bn).
Proof.
intros An Bn n ; unfold Rseq_zip, Rseq_opp ;
case (n_modulo_2 n) ; intros [p Hp] ; reflexivity.
Qed.
Lemma Rseq_zip_scal_l : ∀ An Bn (l : R),
l × Rseq_zip An Bn == Rseq_zip (l × An) (l × Bn).
Proof.
intros An Bn l n ; unfold Rseq_mult, Rseq_constant, Rseq_zip ;
case (n_modulo_2 n) ; intros [p Hp] ; reflexivity.
Qed.
Link with stdlib