Coquelicot library for basic undergraduate calculus

Question

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

You probably want to look into the [ring tactic](https://coq.inria.fr/refman/Reference-Manual028.html). — gallais, Feb 09 '17 at 15:35
@gallais : Thx. field tactic fails at this stage. I suppose I have to get rid of the term "one". I have tried unfold but it is not a good idea I am afraid. — FZed, Feb 09 '17 at 15:49
Have you tried `ring`? You don't need the whole power of `field` here. What does `one` unfold to? I would indeed expect that it'd be a good idea to unfold it. — gallais, Feb 09 '17 at 15:53

score 6 · Accepted Answer · answered Feb 09 '17 at 16:32

6

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.

answered Feb 09 '17 at 16:32

gallais

11,823
2
30
63

OP already knows `auto_derive` but wanted to get their "hands a bit dirty". ;) – gallais Feb 09 '17 at 16:38
Thx for your efforts on installs & analysis. Appreciate it. Merci. – FZed Feb 09 '17 at 20:06
No bother, @FZed. I have been reading the new [SSReflect book](https://math-comp.github.io/mcb/) so now that I've found a good excuse to install everything, I might attempt to solve the exercises. :) – gallais Feb 13 '17 at 13:45

Coquelicot library for basic undergraduate calculus

1 Answers1