Library Coqtail.Reals.Ranalysis.Rfunction_facts

Require Import Reals.
Require Export Rfunction_def.

Open Scope Rfun_scope.

Ltac extensional_reflexivity H Heq :=
let swap H1 H2 :=
  clear H1;
  assert (H1 := H2);
  clear H2
in
let rec refl_aux H :=
match goal with
| |- ∀ x, _ ⇒
  let x := fresh "x" in
  let nH := fresh in
  intros x;
  assert (nH := H x);
  swap H nH;
  refl_aux H
| |- ∃ x, _ ⇒
  let x := fresh "x" in
  destruct H as [x H];
  ∃ x;
  refl_aux H
| |- ?P ∧ ?Q ⇒
  let Hl := fresh "H" in
  let Hr := fresh "H" in
  destruct H as [Hl Hr];
  split; [refl_aux Hl|refl_aux Hr]
| |- ?P ∨ ?Q ⇒
  let Hl := fresh "H" in
  let Hr := fresh "H" in
  destruct H as [Hl|Hr];
  [refl_aux Hl|refl_aux Hr]
| _ ⇒
  repeat (rewrite <- Heq); apply H
end in
compute in H |- *; refl_aux H.

Section Rfun_eq.

Variables f g : R → R.
Hypothesis Heq : f == g.

Lemma Rfun_continuity_pt_eq_compat :
  ∀ x, continuity_pt f x → continuity_pt g x.
Proof.
intros x Hct.
extensional_reflexivity Hct Heq.
Qed.

Lemma Rfun_continuity_eq_compat :
  continuity f → continuity g.
intros H.
extensional_reflexivity H Heq.
Qed.

End Rfun_eq.