의존 함수 재 작성

이진 자연수 (비트 목록)에 대한 선행 함수를 정의하려고합니다. 나는 내 함수의 입력을 자르거나 (0을 갖지 않고) 양수인 숫자로 제한하고자한다. 그래서 이전의 0을 걱정할 필요가 없다. 나는 그것을 해결하는 방법을 모른다,의존 함수 재 작성

nat1: Nat 
H1: is_trim nat1 = True 
H2: is_pos nat1 H1 = True 
H3: Empt = nat1 
______________________________________(1/1) 
Nat

그러나 :

Program Fixpoint pred (nat1: Nat) (H1: is_trim nat1 = True) (H2: is_pos nat1 H1 = True): Nat := 
    match nat1 with 
    | Empt => _ 
    | Fill Zer nat2 => Fill One (pred nat2 H1 H2) 
    | Fill One nat2 => Fill Zer nat2 
    end.

나의 첫번째 의무는 다음과 같다 : 여기

운영자 pred의 정의입니다.

모순은 분명히 H2에 있습니다. 하지만, H1에 따라 다르므로 을 Empt으로 설정 한 다음 (is_pos Empt H1)을 False으로 설정할 수 없습니다.

어떻게 증명해야합니까?

출처

2012-11-24 user1494846

또한 'dependent-types'는 태그 여야합니다. – user1494846

'dependent-type' (단수)은 태그입니다. – sepp2k

방금이 목표가 '사소한'것으로 나타났습니다. (-_- ') 그래도 나는 비슷하지만 좀 더 복잡한 것으로 비틀 거린 경우를 대비해서 손으로 해결하는 법을 알고 싶다. – user1494846

Empt 경우의 자연수를 반환 할 수 있다는 점에서이 목표는 참으로 사소한 것이므로 처음에는 적절한 H2 : is_pos nat1 H1을 전달해야하므로 아무도 해당 숫자에 도달 할 수 없다는 점에서 안심하십시오.

입니다

Program Fixpoint pred (nat1: Nat) (H1: is_trim nat1 = True) (H2: is_pos nat1 H1 = True): Nat := 
    match nat1 as nat1' return is_pos nat1' H1 -> Nat with 
    | Empt => fun isposEmpt => 
     (* hopefully, is_pos Empt H1 immediately reduces to False, and you can do this: *) 
     False_rec Nat isposEmpt 
    | Fill Zer nat2 => fun _ => Fill One (pred nat2 H1 H2) 
    | Fill One nat2 => fun _ => Fill Zer nat2 
    end H2.

, 당신은 nat1이 긍정적임을 증명이 필요합니다

나는 그런 일을 해결하기 위해 다음 "올바른"방법의 라인에 종속 패턴 일치를 사용하는 것입니다 생각 당신의 시합에 대한 논쟁, 그리고 Empt 사건에서 증거가 가짜라고 결론을 짓기 때문에 가짜를 돌려 줄 수 있습니다.

이 기능이 유용 할 수도 있습니다. 다음에 사람들이 귀하의 모범을 보일 수 있도록 필요한 정의를 제공하십시오.

출처

2012-11-25 17:27:01 Ptival

의존 함수 재 작성

답변

관련 문제