4

我在 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，它声明了 function 的导数f at x0 is f'。

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

如果我想让我的手有点脏，这是我没有的尝试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
4

1 回答 1

6

好的，我花了一点时间来安装 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.
于 2017-02-09T16:32:15.387 回答