Coquelicot图书馆为基础本科微积分

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'是一个Coquelicot Prop,它说明了函数的导数f at x0 is f'.

由于auto_deriveCoquelicot提供的策略,我已经证明了这个引理.

如果我想让我的手有点脏,这是我的尝试没有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并找到合适的import语句但是我们走了.

重点是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.