Coq는 선택 모나드가 응용 프로그램과 모나드임을 증명합니다.

Question

저는 coq에 처음 접했고 지금까지 손으로 증명할 수있는 것들만 증명할 수있었습니다. 그래서 셀렉션 모나드를 만나서 그것을 haskell에서 구현하기로 결정했을 때, 좋은 운동이 될 것이라고 생각했지만 붙어있었습니다. 누군가가 coq에서 선택 모나드가 응용 프로그램이자 모나드라는 증거를 보여줄 수 있습니까? 다음은 functor의 haskell 구현입니다.

또한 모나드 법을 입증 할 수 있다면 감사드립니다.

편집 :

Definition sel (R A : Type) := (A -> R) -> A. 

Theorem functor_exists : forall (R A B : Type), 
    (A -> B) -> sel R A -> sel R B. 
    intros R A B. unfold sel. intros AB ARA BR. 
    apply AB. apply ARA. intro. apply BR. apply AB. exact X. 
    Qed. 

Answer 1

당신이 COQ 때문에 전술을 사용할 필요가 없습니다 : 당신은 상당히 유사한 방식으로 프로그래밍 언어로 사용할 수 있습니다 여기에 펑의 존재를 내 증거입니다 하스켈. R 변수이 섹션의 모든 시간을 제시 될 것입니다 때문에

첫째, 우리는 한 번 언급하여 조금 더 가벼운 표기법을 만들 수 있습니다 및 모든 :

Section SelMon. 
Variable (R : Type). 

우리는 복제 할 수 있습니다 sel의 정의 (이미 컨텍스트에 있기 때문에 R 변수가 없음). 그리고 좋은 정의보다는 전술을 사용하여 증거로 fmap 쓰기 :

Definition sel (A : Type) := (A -> R) -> A. 

Definition fmap {A B : Type} (f : A -> B) (s : sel A) : sel B := 
    fun br => f (s (fun a => br (f a))). 

다음 단계는 당신이 실용적이 pure 방법을 제공하는 것이다 가지고 증명. 우리는 상수 함수를 사용할 수 있습니다.

Definition pure {A : Type} (a : A) : sel A := 
    fun _ => a. 

그런 다음 약간 털이납니다. 당신이 다음에 완료되면

Definition join {A : Type} (ssa : sel (sel A)) : sel A. 
Admitted. 

Definition bind {A B : Type} (sa : sel A) (asb : A -> sel B) : sel B. 
Admitted. 

Definition app {A B : Type} (sab : sel (A -> B)) (sa : sel A) : sel B. 
Admitted. 

, 당신이 섹션 닫을 수 및 R과 같이 추가됩니다 : 나는 join 시작 후 bind (그리고 그것에서 app) 정규 구조를 사용을 유도하기 위해 조언을 것 모든 정의에 대한 매개 변수. I는 제 COQ 사용하기 시작하면

End SelMon.