Coq Coquelicot库中是否有rewrite类战术可改写is_lim内的函数

解决方案 #

你要的效果完全可以通过ssreflect的under战术结合Coquelicot自带的is_lim_ext_loc引理实现，不需要手动指定改写后的目标函数，修改后的证明代码如下：

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.
  (* 直接在is_lim的函数参数位置做局部等价改写 *)
  under [is_lim (fun x => _) _ _]eq_rel apply is_lim_ext_loc => y.
  - case: (Req_dec y 1) => [/= -> | Hyneq1].
    + right. (* 极限点处的函数值不影响极限，不需要相等 *)
    + left. field. lra.
  (* 后续正常证明x+1在1处的极限为2即可 *)
  - apply is_lim_plus'; [apply is_lim_id | apply is_lim_const].
Qed.

说明 #

• under战术的[is_lim (fun x => _) _ _]模式定位到了你需要改写的函数位置，eq_rel声明本次改写是保持命题等价的关系变换，刚好匹配is_lim_ext_loc的性质：只要两个函数在极限点的去心邻域内处处相等，二者的极限性质完全一致。
• 这套写法不需要你手动展开邻域定义、手动指定邻域半径，is_lim_ext_loc已经自动封装了邻域存在性的逻辑，你只需要证明对所有不等于极限点1的点，两个函数值相等即可。

如果你愿意引入mathcomp-analysis库，封装好的极限战术可以进一步简化证明：

From mathcomp Require Import all_ssreflect all_algebra classical_sets reals.
From mathcomp.analysis Require Import functions topology normedtype realfun.

Lemma lim_1_2 : lim (x:=1) (fun x:R => (x^2 - 1)/(x - 1)) = 2.
Proof. by apply: eq_lim => x x_ne1; field_simplify (x - 1 != 0) => //; ring. Qed.

内容的提问来源于stack exchange，提问作者Yosuke Ito