CODEWITHSUNDEEP
logiccoq
TomR
TomR

Reputation: 3036

How to declare constant of some inductive type in Coq?

I am following https://github.com/brunofx86/LL/blob/master/FOLL/LL/SyntaxLL.v and there the inductive type is defined (parametrized Higher Order Abstract Syntax - PHOAS is used here):

(** Closed Terms *)
  Inductive ClosedT : Term -> Prop :=
  | cl_cte: forall C, ClosedT (Cte C)
  | cl_fc1: forall n t1, ClosedT t1 -> ClosedT (FC1 n t1)
  | cl_fc2: forall n t1 t2, ClosedT t1 -> ClosedT t2 -> ClosedT (FC2 n t1 t2).

My question is - how can I define constant John to be of type ClosedT using constructor cl_cte?

And additional question: there can be situations when I would like to define more types, e.g. John : Person and Bruno : Tortoise so - should I created new type, e.g. ClosedT_Tortoise for the new type? ClosedT is the base type upon which the object logic is built, so, maybe I should not proceed with multisort logic?

As I understand, then this formalization of the Linear Logic which I am using, is applied in the another Coq project http://subsell.logic.at/bio-CTC/ and it may be possible that the constants are defined there. But skimming source I can not find them.

Upvotes: 0

Views: 123

Answers (1)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23582

Strictly speaking, your question is ill-stated: ClosedT is not a type, but a family of propositions indexed by elements of the type Term. Based on the file, I imagine that ClosedT t means that the term t : Term is closed, and that you want to do the following:

  • Define a type of constants T that has an element John : T.

  • Instantiate the definitions of the development with T. For this, you need to wrap T in a module of type Eqset_dec_pol along with a proof that T has decidable equality, and apply the functor Syntax_LL that appears at the beginning of the file to this module.

  • Embed John in the syntax of terms using the Cte "constructor" of Term. (This is not a constructor in the proper Coq sense of the word, but just a handy wrapper to build elements of type Term.)

  • Prove that this term is closed; that is, prove ClosedT (Cte John). This should just be a matter of applying the constructor cl_cte.

Is this more-or-less along the lines of what you want to do?

Upvotes: 3

Related Questions