코 큐식에서 자연체에서 자연수로 조각 별 함수를 정의하는 방법

Question

x가 0이면 f (x) = 0을 어떻게 정의 할 수 있습니까? 그렇지 않으면 Coq에서 f (x) = 1이됩니다. <

나는,

Definition test (i:nat):nat := 
    if i < 5 then 0 else 1. 

이

Error: The term i < 5 has type Prop which is not a (co-)inductive type.

Answer 1

당신은 (i < 5 논리 또는 제적 버전 비교의 decidable 버전을 사용할 필요가 있다는 불평 OСaml처럼 뭔가를 할 경우 그것은 당신이 계산할 수 없다). 이 표준 라이브러리에 있습니다 부울하지만 돌아 미만

Require Import Arith. 
Check lt_dec. 

Definition test (i:nat) : nat := if lt_dec i 5 then 0 else 1. 

표준 라이브러리의 테스트 실제로 두 경우 모두 교정이 증거는 사용하지 않는 이동 (함수가 무엇을 당신에게 포함하는 sumbool, 당신의 예를 들어, test에 대해 뭔가를 증명하고 싶다면 편리 할 것입니다. lt_dec 님의 타입은 sumbool (n < m) (~n < m)입니다.

교정에 대해 신경 쓰지 않았다면 다른 함수 Nat.ltb을 사용하여 부울을 반환 할 수 있습니다. 표준 라이브러리뿐만 아니라이 기능을 편리 표기법을 포함

Require Import Arith. 

Definition test (i:nat) : nat := if i <? 5 then 0 else 1. 

당신이 증거에두고 작업 할 때, 당신은 무엇 i <? 5 반환에 대해 추론하기 위하여 Nat.ltb_lt 같은 이론을 적용해야합니다.

Coq의 if b then .. else ...은 b이 bool 또는 sumbool 중 하나임을 유의하십시오. 사실 두 개의 생성자가있는 유도 형을 지원하며 첫 번째 생성자에 then 분기를 사용하고 두 번째 생성자에 else 분기를 사용합니다. bool 및 sumbool에 대한 정의는 생성자에게 if 문이 예상대로 동작하도록하기 위해주의해야합니다.