Bibliothèque Coquelicot pour le calcul de base de premier cycle

Question

J'ai installé Coquelicot sur mathcomp/SSreflect.

Je veux effectuer une analyse réelle très basique même si je ne maîtrise pas encore le standard Coq.

Ceci est mon premier lemme:

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

is_derive f x0 f' est un Coquelicot Prop qui indique que la dérivée de la fonction f at x0 is f'.

J'ai déjà prouvé ce lemme grâce à la tactique auto_derive fournie par Coquelicot.

Si je veux obtenir mes mains un peu sale, c'est ma tentative sans 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. 

Et maintenant, je suis coincé avec cet arrêt en cours:

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

Comment puis-je résoudre il ?

EDIT:

si je l'appelle ring, je reçois:

Error: Tactic failure: not a valid ring equation. 

si je déplie un, je reçois:

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, il m'a fallu un peu de temps pour installer ssreflect & Coquelicot et trouver les déclarations d'importation appropriées, mais c'est parti.

Le point principal est que one est en effet juste R1 sous le capot, mais simpl ne suffit pas agressive pour révéler que: vous devez utiliser compute à la place. Une fois que vous avez seulement des éléments bruts dans R et des variables, ring prend soin de l'objectif.

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.