构造Coq代码(Structuring Coq code)

构造Coq代码(Structuring Coq code)

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

函数f: A -> B一般Definition f: A -> B ，可在所有部分（或模块）中访问

A的模块（或部分）特定定义

f必须在所有部分（或模块）中可计算

你建议我使用什么设置？

I have the usual setup: first I define some types, then some functions from those types. However, since there are many ways to formalize the thing I do, I will do it in 3 versions. For simplicity (and to maintain an overview), I want my code in one file. I also want to minimize repetitive code. To this end, a setup w/ 3 Modules for specific stuff and general definitions in front of them might work -- but not in the type of situation described below:

A general Definition of function f: A -> B, accessible in all sections (or modules)

Module- (or section-) specific definitions of A

f must be computable in all sections (or modules)

What setup do you recommend me to use?

最满意答案

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. 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.