基本本科微积分的 Coquelicot 图书馆

Question

我在 mathcomp/SSreflect 之上安装了 Coquelicot。

即使我还不掌握标准 Coq，我也想用它执行非常基本的实际分析。

这是我的第一个引理：

Definition fsquare (x : R) : R := x ^ 2.
Lemma deriv_x2 : forall y, is_derive (fsquare) y (2 * y).

is_derive f x0 f' 是一个 Coquelicot Prop，声明函数 f at x0 is f'.

的导数

由于 Coquelicot 提供的 auto_derive 策略，我已经证明了这个引理。

如果我想让自己的手有点脏，这是我没有 auto_derive 的尝试：

Lemma deriv_x2 : forall y, is_derive (fsquare) y (2 * y).
Proof.
  move => y.
  unfold fsquare.
  evar_last.
  apply is_derive_pow.
  apply is_derive_id.
  simpl.

现在我被这个悬而未决的判断困住了：

1 subgoal
y : R_AbsRing
______________________________________(1/1)
2 * one * (y * 1) = 2 * y

我该如何解决？

编辑：

如果我调用 ring，我得到：

Error: Tactic failure: not a valid ring equation.

如果我展开一个，我得到：

1 subgoal
y : R_AbsRing
______________________________________(1/1)
2 *
Ring.one
  (AbelianGroup.Pack R_AbsRing (Ring.class R_AbsRing) R_AbsRing)
  (Ring.class R_AbsRing) * (y * 1) = 2 * y

Answer 1

好的，我花了一些时间来安装 ssreflect & Coquelicot 并找到合适的导入语句，但我们开始吧。

要点是 one 确实只是 R1 在幕后，但 simpl 不够激进以揭示这一点：你需要使用 compute .一旦您在 R 和变量中只有原始元素，ring 就会处理目标。

Require Import Reals.
Require Import Coquelicot.Coquelicot.
Require Import mathcomp.ssreflect.ssreflect.

Definition fsquare (x : R) : R := x ^ 2.

Lemma deriv_x2 : forall y, is_derive (fsquare) y (2 * y).
Proof.
  move => y.
  unfold fsquare.
  evar_last.
  apply is_derive_pow.
  apply is_derive_id.
  compute.
  ring.
Qed.

基本本科微积分的 Coquelicot 图书馆

Coquelicot library for basic undergraduate calculus

coq

real-number