구조화 Coq 코드

Question

나는 일반적인 설정을 가지고 있습니다. 먼저 몇 가지 유형을 정의한 다음 해당 유형의 일부 기능을 정의합니다. 그러나, 내가하는 일을 형식화하는 많은 방법이 있으므로, 나는 3 가지 버전으로 그것을 할 것입니다. 단순화 (그리고 개요를 유지하기 위해), 나는 하나의 파일에 내 코드를 원한다. 또한 반복 코드을 최소화하고 싶습니다.

1. 기능 f: A -> B의 일반적인 Definition, 접근 가능 : -이를 위해, 특정 물건과 그들의 앞에 일반적인 정의에 대한/3 Module의이 작동 할 수 승 설치 상황의 유형에 있지만은 설명 모든 섹션 (또는 모듈)

2. 모듈 - (또는 섹션 -) A

3. f 구체적인 정의의 모든 부분에서 계산할 수 있어야 (또는 모듈)

어떤 설정을 사용 하시겠습니까?

Answer 1

Require Import Arith. 

(* Create a module type for some type A with some general properties. *) 
Module Type ModA. 
    Parameter A: Type. 
    Axiom a_dec: forall a b:A, {a=b}+{a<>b}. 
End ModA. 

(* Define the function that uses the A type in another module 
    that imports a ModA type module *) 

Module FMod (AM: (ModA)). 
    Import AM. 
    Definition f (a1 a2:A) := if a_dec a1 a2 then 1 else 2. 
End FMod. 

(* Here's how to use f in another module *) 
Module FTheory (AM:ModA). 
    Module M := FMod AM. 
    Import M. 
    Import AM. 

    Theorem f_theorem: forall a, f a a = 1. 
    intros. compute. destruct (a_dec _ _). 
    auto. congruence. 
    Qed. 
End FTheory. 

(* Eventually, instatiate the type A in some way, 
    using subtyping '<:'. *) 

Module ModANat <: ModA. 
    Definition A := nat. 
    Theorem a_dec: forall a b:A, {a=b}+{a<>b}. 
    apply eq_nat_dec. 
    Qed. 
End ModANat. 

(* Here we use f for your particular type A *) 
Module FModNat := FMod ModANat. 

Compute (FModNat.f 3 4). 

Recursive Extraction FModNat.f. 

Goal FModNat.f 3 3 = 1. 
    Module M := FTheory ModANat. 
    apply M.f_theorem. 
Qed.