обратное состояние монады в Coq

Question

В Haskell, следующее определение затруднительное принимается:

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

Это включает в себя вычисление фиксированной точкой для g, который вообще невозможно в Coq из-за возможного отсутствия прекращения.

Как Дэвид Янг упоминает выше, если что-то вроде bind выполнимо в Coq, оно должно быть расширено с помощью доказательств, доказывающих, что эта рекурсия завершается. Это усовершенствование нетривиально.

Answer 2

bind нуждается в доказательстве того, что функции действительно вернутся. Если вы добавите аргумент H с таким типом, который зависит от фактических значений sf, f и s, вы можете извлечь нужную сумму (b, s'') из этого «сертифицированного» термина H.

Обратите внимание, что как на самом деле вычислить в sf и f функции должно быть объяснено в строительстве H, для конкретного sf, f и s.

(Там могут быть и другие/более эффективные способы achieveing ​​это. Надеюсь, кто-то может добавить к этой теме.)

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.