"is_lim"中的函数有什么办法重写吗？

Question

我正在使用 Coq 和 Coquelicot 库，我想知道一种更好的方法来轻松处理限制。当我想证明 \lim_{x \to 1} (x^2-1)/(x-1) = 2 时，我的代码如下。

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.

在这个例子中，我明确地写了目标词(fun x:R => x + 1)。有什么方法可以像 rewrite 策略那样将 (fun x:R => (x^2 - 1)/(x - 1)) 转换为 (fun x:R => x + 1) 吗？换句话说，我正在寻找与 under for eq_big_nat.

类似的策略

Answer 1

Coquelicot 针对易用性进行了优化，并尽可能使用全部功能而不是依赖限制 - 例如您可以写下一个积分而无需证明它存在，但据我所知这不会扩展到被零除。为了使你的上述等式有效，需要一个除法的定义，它可以以某种方式处理你得到的 x=1 的 0/0。可以为函数（多项式）定义一个除法，它可以以一种合理的方式处理这个问题——这就是你隐式使用的，声明这是有道理的，但是不能为可以处理 0/0 的单个实数定义除法你想要的方式。但是您在上面使用的除法运算符是对单个数字而不是多项式的除法。在非正式数学中，有时人们对这些事情有点草率。

除了 0/0 问题之外，您还必须使用函数外延性公理，该公理指出两个函数相等，以防它们在每个点上都相等。

这是 Coq 的一个片段，它显示了可以做什么以及问题所在：

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.

总而言之，从 dom 到 Real 的隐式强制转换并没有那么糟糕，尽管该函数实际上比看起来更复杂，因为每个 x 都是从dom 到 R.

还可以有一个函数外延性公理，如果一个函数的 domain 是另一个函数的 domain 的子集，则该公理有效。不过，我不确定这是否一致，而且它还需要一个非标准的相等定义，因为通常的相等只有相同类型的东西才能相等。这将允许您将多项式分数与完整 R 上的多项式相等。

我希望这能解释为什么事情是这样的。 Coquelicot 依赖于标准库中的除法运算符，如果分母为零，则您无法证明任何事情。这有时很不方便，但据我所知（这不是很广泛 - 我是物理学家而不是数学家）到目前为止还没有人提出除法的定义，让你可以轻松地做你想做的事。

"is_lim"中的函数有什么办法重写吗？

Is there any way to rewrite the function in "is_lim"?

coq

coq-tactic