CODEWITHSUNDEEP
functiontypesstructurecoq
jaam
jaam

Reputation: 980

Structuring Coq code

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:

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

  2. Module- (or section-) specific definitions of A

  3. f must be computable in all sections (or modules)

What setup do you recommend me to use?

Upvotes: 1

Views: 100

Answers (1)

larsr
larsr

Reputation: 5811

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.

Upvotes: 3

Related Questions