本科基础微积分的 Coquelicot 库

Question

我已安装 Coquelicot在 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'是一个 Coquelicot Prop，说明函数 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

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.