Библиотека Coquelicot для базового студенческого исчисления

Question

Я установил Coquelicot поверх mathcomp/SSreflect.

Я хочу выполнить очень простой реальный анализ с ним, даже если я до сих пор не владею стандартным Coq.

Это моя первая лемма:

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

is_derive f x0 f' является Coquelicot Prop, который гласит, что производная функции f at x0 is f'.

Я уже доказал эту лемму благодаря тактике auto_derive, предоставленной Coquelicot.

Если я хочу, чтобы мои руки немного грязный, это моя попытка без 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 

Как решить Это ?

EDIT:

, если я позвоню 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 

Answer 1

Хорошо, что мне потребовалось некоторое время, для установки 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.