Haskellで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'') 

どのように私はコックで受け入れ同様の定義を得ることができますか？

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`式の2つのバインディングが相互に再帰的であるため、

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.