Coq nats에서 스택 오버 플로우 또는 세그먼트 화 오류를 방지하려면 어떻게합니까?

Question

저는 현재 vellvm과 함께 작업하고 있습니다. 나는 코퀴인 초보자입니다. 이 경고는 서명을 계산 생성

Warning: Stack overflow or segmentation fault happens when working with large numbers in nat (observed threshold may vary from 5000 to 70000 depending on your system limits and on the command executed).

내 기능 :

프로그래밍 동안, 나는 다음과 같은 경고에 직면했다. 서명은 상위 비트와 하위 비트로 나뉩니다. 상위 비트와 하위 비트를 나타내는 두 개의 n1과 n2가 주어지면 (n1 * 65536) + n2가 계산됩니다. 이것은 16 비트의 2 진수를 나란히 배치 한 추상화입니다.

매우 놀랍습니다. 왜냐하면 coq nat 정의가 S 생성자 덕택에 외부에서 큰 int를 처리하기 때문에 나타납니다.

coq에서이 경고/큰 숫자를 어떻게 사용해야합니까? 구현을 nat에서 일종의 이진 구조로 변경했습니다.

감사합니다.

Answer 1

Coq에 nat 유형을 사용하는 대신 부호 양 쌍 표현을 사용하는 정수의 형식화 인 Z 유형을 사용하는 것이 더 좋습니다 (큰 숫자를 조작해야하는 경우). 단점은 교정이 약간 더 복잡해질 수 있다는 것입니다. nat은 매우 간단하므로 간단한 증명 원칙을 인정합니다.

그러나 Coq에는 정의, 정리 및 증명을 작성하는 데 간단한 표기법이 사용됩니다. Coq는 극히 작은 커널을 가지고 있습니다 (우리는 증명 검사기가 정확할 것으로 믿을 수 있기를 원하기 때문에 이것을 원합니다. 읽을 수 있습니다). 그러나 사물의 표현이 다양하고 좋은 기호가 몇 개 있기 때문에 일반적으로 기호가 충돌합니다. 이 문제를 극복하기 위해 coq는 interpretation scopes을 사용하여 기호를 모호하게 만들고 이름을 "+"는 add, plus 등을 의미하기 때문에 해결합니다.

Z_scope을 사용하여 올바른지 확인하십시오. plus에 대한 +은 Z입니다.