Coquelicot-Bibliothek für grundlegende Bachelor-Kalkül

Question

Ich habe Coquelicot oben auf Mathcomp/SSreflect installiert.

Ich möchte sehr grundlegende echte Analyse damit durchführen, auch wenn ich Standard-Coq noch nicht meistern.

Dies ist mein erstes Lemma:

Definition fsquare (x : R) : R := x^2. 
Lemma deriv_x2 : forall y, is_derive (fsquare) y (2 * y). 

is_derive f x0 f' ist ein Coquelicot Prop, die besagt, dass die Ableitung der Funktion f at x0 is f'.

Ich habe dieses Lemma bereits dank auto_derive Taktik von Coquelicot bewiesen.

Wenn ich möchte, dass meine Hände ein wenig schmutzig machen, das ist mein Versuch, ohne 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. 

Und jetzt bin ich mit diesem bis zur Entscheidung fest:

1 subgoal 
y : R_AbsRing 
______________________________________(1/1) 
2 * one * (y * 1) = 2 * y 

Wie löse ich es?

EDIT:

wenn ich ring nennen, die ich erhalten:

Error: Tactic failure: not a valid ring equation. 

wenn ich eine entfalten, erhalte ich:

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, es hat mich eine Weile installieren Sie ssreflect & Coquelicot und finden Sie die entsprechenden Import-Anweisungen, aber hier gehen wir.

Der wichtigste Punkt ist, dass one ist in der Tat nur R1 unter der Haube aber simpl ist nicht aggressiv genug, das offenbaren: Sie müssen compute stattdessen verwenden. Sobald Sie nur Rohelemente in R und Variablen haben, kümmert sich ring um das Ziel.

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.