I'm using Coq and Coquelicot Library, and I'd like to know a better way to handle limit easily. When I want to prove \lim_{x \to 1} (x^2-1)/(x-1) = 2, I code as follows.
Require Import Reals Lra.
From mathcomp Require Import all_ssreflect.
From Coquelicot Require Import Coquelicot.
Lemma lim_1_2 : is_lim (fun x:R => (x^2 - 1)/(x - 1)) 1 2.
Proof.
apply (is_lim_ext_loc (fun x:R => x + 1)).
- rewrite /Rbar_locally' /locally' /within /locally.
exists (mkposreal 1 Rlt_0_1).
move => y Hyball Hyneq1.
field; lra.
- apply is_lim_plus'; [apply is_lim_id | apply is_lim_const].
Qed.
In this example, I explicitly write the goal term (fun x:R => x + 1). Is there any way to transform (fun x:R => (x^2 - 1)/(x - 1)) to (fun x:R => x + 1) like rewrite tactic? In other words, I'm looking for a similar tactic as under for eq_big_nat.
Coquelicot is optimized for ease of use and uses total functions rather than dependent restrictions wherever possible - e.g. you can write down an integral without having a prove that it exists, but as far as I know this does not extend to division by zero. To make your above equation work, one would need a definition of division, which somehow can handle the 0/0 you get for x=1. One can define a division for functions (polynomials) which can handle this in a reasonable way - and this is what you are using implicitly by stating that this makes sense, but one cannot define division for individual real numbers which can handle 0/0 in the way you would like. But the division operator you use above is a division on individual numbers and not on polynomials. In informal mathematics one is sometimes a bit sloppy about such things.
Besides the 0/0 issue, you also would have to use the axiom of functional extensionality, which states that two functions are equal in case they are equal for each point.
Here is a snippet of Coq which shows what one can be done and where the issues are :
Require Import Reals.
Require Import Lra.
Require Import FunctionalExtensionality.
Open Scope R.
Definition dom := {x : R | x<>1}.
Definition dom2R (x : dom) : R := proj1_sig x.
Coercion dom2R : dom >-> R.
Example Example:
(fun x : dom => (x^2 - 1)/(x - 1))
= (fun x : dom => x + 1).
Proof.
apply functional_extensionality.
intros [x xH].
cbv.
field.
lra.
Qed.
All in all it is not that bad with the implicit coercion from dom to Real, although the function is in reality more complicated than it looks since each x is an implicit coercion projecting from dom to R.
Also one could have an axiom of functional extensionality, which works if the domain of one function is a subset of the domain of the other function. I am not sure if this would be consistent, though and it would also require a non standard definition of equality because with the usual equality only things of the same type can be equal. This would allow you to equate the polynomial fraction with the polynomial on the full R.
I hope this explains why things are as they are. Coquelicot relies on the division operator from the standard library, for which you can't prove anything in case the denominator is zero. This is sometimes inconvenient, but to my knowledge (which is not very extensive - I am physicist not mathematician) up to now nobody came up with a definition of division which allows you to easily do what you want.