COQ에서 미분 연산자를 구현할 수 있습니까?

Question

COQ에서 미분 연산자를 구현할 수 있습니까? 즉, x^2과 같은 대수 함수를 사용하여 그 파생물을 반환하는 연산자입니다. 이 경우 2x.

Answer 1

임의의 기능을 수행하는 연산자, 즉 Z -> Z 유형의 연산자를 사용하고 그 파생어를 구성한다면 나는 불가능하다고 생각합니다.

하지만 특정 클래스의 함수를 모델로 만들 수는 있지만 해당 클래스에 이러한 연산자를 구현할 수 있어야합니다.

최종 목표와 동기 부여에 대해 알아두면 도움이 될 것입니다.