I have installed Coquelicot on top of mathcomp/SSreflect.
I want to perform very basic real analysis with it even if I still do not master standard Coq.
This is my first lemma :
Definition fsquare (x : R) : R := x ^ 2.
Lemma deriv_x2 : forall y, is_derive (fsquare) y (2 * y).
is_derive f x0 f' is a Coquelicot Prop that states that the derivative of function f at x0 is f'.
I have already proved this lemma thanks to auto_derive tactic provided by Coquelicot.
If I want to get my hands a bit dirty, this is my attempt without 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.
And now I am stuck with this pending judgement :
1 subgoal
y : R_AbsRing
______________________________________(1/1)
2 * one * (y * 1) = 2 * y
How do I solve it ?
EDIT :
if I call ring, I get :
Error: Tactic failure: not a valid ring equation.
if I unfold one, I get :
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
Ok, it took me a little while to install ssreflect & Coquelicot and find the appropriate import statements but here we go.
The main point is that one is indeed just R1 under the hood but simpl is not aggressive enough to reveal that: you need to use compute instead. Once you only have raw elements in R and variables, ring takes care of the goal.
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.