基础本科微积分库

Question

我已经将考奎罗安装在mathcomp/SSreflect之上。

我想用它执行非常基本的实际分析，即使我仍然没有掌握标准Coq。

这是我的第一个引理：

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

is_derive f x0 f'是一种函数f at x0 is f'的导数。

我已经证明了这个引理，多亏了科奎斯特提供的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

好的，我花了一小段时间安装import & 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.