기본 학부 계산을위한 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 소유입니다 기능 f at x0 is f'의 파생.

나는이 보조 정리를 이미 Coquelicot이 제공 한 auto_derive 전술 덕분에 증명했습니다.

내 손에 더러운 조금을 얻고 싶은 경우에

,이 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 

가 어떻게 해결합니까 그거야?

편집 : 나는 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을 설치하고 적절한 import 문을 찾으면됩니다.

주요 포인트는 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.