COQ

Question

하스켈에서

의 반대 상태 모나드는, 바인드의 다음과 같은 정의가 허용됩니다 :

type RState s a = s -> (a, s) 

bind :: RState s a -> (a -> RState s b) -> RState s b 
bind sf f = \s -> 
    let (a, s'') = sf s' 
     (b, s') = f a s 
    in (b, s'') 

어떻게 COQ에 의해 허용 유사한 정의를 얻을 수 있나요?

Definition RState (S A : Type) : Type := S -> A * S. 

Definition bind (S A B : Type) (sf : RState S A) (f : A -> RState S B) : RState S B := 
    fun s => 
    let (a, s'') := sf s' in 
    let (b, s') := f a s in 
    (b, s''). 

그러나 다음과 같은 오류 메시지와 함께 실패합니다 : 내 시도는

Error: The reference s' was not found in the current environment. 

Answer 1

는 g :: s -> s을 가정합니다.

sf :: RState s s 
sf = get = \s -> (s, s) 

f :: s -> RState s s 
f = put . g = \a _ -> ((), g a) 

우리가 얻을 고려 :

bind sf f = \s -> 
    let (a, s'') = sf s' 
     (b, s') = f a s 
    in (b, s'') 
      = \s -> 
    let (a, s'') = (s', s') 
     (b, s') = ((), g a) 
    in (b, s'') 
      = \s -> 
    let (b, s') = ((), g s') 
    in (b, s') 
      = \s -> 
    let s' = g s' in ((), s') 

이 포함 인해 종단의 가능한 부족으로 COQ 불가능 일반적이다 g을위한 고정 소수점을 계산.

David Young이 위에서 언급 한 것처럼 bind과 같은 것이 Coq에서 실행 가능하다면이 재귀가 종료됨을 증명하는 증명 조건으로 개선되어야합니다. 이 향상은 중요하지 않습니다.

Answer 2

bind은 함수가 실제로 반환한다는 증거가 필요합니다. 실제로 sf, f 및 s 값에 따라이 효과에 유형이 지정된 H 인수를 추가하면 "인증 된"용어 H에서 원하는 (b, s'') 쌍을 추출 할 수 있습니다. 실제로sf 및 f 함수를 계산하는 방법

참고 특정 sf, f 및 s 들어 H의 구성에 대하여 설명한다.

은`let` 표현의 두 바인딩이 상호 재귀 때문에

Definition RState (S A : Type) : Type := S -> A * S. 

Section Bind. 
    Variables S A B:Type. 

    (* define a type that a proof should have *) 
    Definition sf_f_s_are_ok (sf : RState S A) (f : A -> RState S B) (s:S) := 
    {x | exists a s'' b s', x = (a, s'', b, s') /\ 
     (a, s'') = sf s' /\ (b, s') = f a s}. 

    (* bind just returns the values we were interested in *) 
    Definition bind sf f (s:S) (H : sf_f_s_are_ok sf f s) := 
    match H with exist _ (a, s'', b, s') _ => (b, s'') end. 

    (* make sure bind is ok *) 
    Lemma bind_is_ok: forall sf f s H b s'', 
     bind sf f s H = (b, s'') -> exists a s', (a,s'') = sf s' /\ (b,s') = f a s. 
    Proof. 
    intros sf f s [[[[a s''0] b0] s'] [a0 [b1 [s'0 [s''1 [Ha [Hb Hc]]]]]]] b s'' H0. 
    simpl in H0; generalize H0 Ha Hb Hc; do 4 inversion 1; subst; eauto. 
    Qed. 
End Bind.