构建 Coq 代码

Question

我有通常的设置：首先我定义了一些类型，然后是这些类型的一些函数。但是，由于有很多方法可以将我做的事情形式化，所以我会分 3 个版本来做。为简单起见（并保持概述），我希望我的代码在一个文件中。 我也想尽量减少重复代码。为此，针对特定内容和前面的一般定义设置 w/3 Modules 可能会起作用——但不适用于下面描述的情况类型：

函数f: A -> B的一般Definition，在所有部分（或模块）
A
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.

构建 Coq 代码

Structuring Coq code

function

types

structure

coq