用於基礎本科微積分的Coquelicot庫

我在mathcomp/SSreflect之上安裝了Coquelicot。用於基礎本科微積分的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'是虞美人支柱，指出的功能f at x0 is f'的衍生物。

由於Coquelicot提供的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

來源

2017-02-09 FZed

你可能想看看[戒指策略]（https://coq.inria.fr/refman/Reference-Manual028.html）。 – gallais

@gallais：Thx。現場戰術在這個階段失敗。我想我必須擺脫「一」這個詞。我試圖展開，但這恐怕不是一個好主意。 – FZed

你嘗試過'環嗎？這裏你不需要'field'的全部功能。「一」展開的是什麼？我確實希望展開它是一個好主意。 – gallais

好吧，我花了一小會兒安裝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-09 16:32:15 gallais

OP已經知道'auto_derive'，但想讓他們的「手有點髒」。 ;） – gallais

Thx爲您的安裝和分析努力。欣賞它。留言Merci。 – FZed

不用麻煩，@FZed。我一直在閱讀新的[SSReflect書]（https://math-comp.github.io/mcb/），所以現在我找到了安裝所有東西的好藉口，我可能會嘗試解決這些練習。 :) – gallais

用於基礎本科微積分的Coquelicot庫

回答

相關問題