Library Coqtail.Reals.Ranalysis.Rfunction_facts


Require Import Reals.
Require Export Rfunction_def.

Open Scope Rfun_scope.

Compatibility of extensional equality

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 : RR.
Hypothesis Heq : f == g.

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

Lemma Rfun_continuity_eq_compat :
  continuity fcontinuity g.
intros H.
extensional_reflexivity H Heq.
Qed.

End Rfun_eq.