構建Coq代碼

Question

我有一個通常的設置：首先定義一些類型，然後定義這些類型的一些函數。然而，由於有很多方法來形式化我所做的事情，我會在3個版本中做到這一點。爲了簡單（並保持概述），我希望我的代碼在一個文件中。 我也想盡量減少重複代碼。

1. 的功能f: A -> B一般Definition，可訪問： - 要爲此，設置W/3 Module S代表具體的東西，在他們面前的一般定義可能會奏效，但不是在形勢的類型如下所述在所有 部分（或模塊）

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.