基礎学部計算のための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'は機能f at x0 is f'の派生と述べてCoquelicotプロップです。

私は既にこの補助定員を証明しました。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 

私は解決するにはどうすればよいですそれ ？

EDIT：

私はringを呼び出す場合、私が手：

Error: Tactic failure: not a valid ring equation. 

私は1つを展開すると、私が手：

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

は[OK]を、それは私に少し時間がかかりました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.