Skip to Content.
Sympa Menu

coq-club - [Coq-Club] newbie: dependent types

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] newbie: dependent types


chronological Thread 
  • From: Ramana Kumar <ramana.kumar AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] newbie: dependent types
  • Date: Tue, 8 Nov 2011 17:36:06 +0000

Dear Coq Club

I am writing my first (semi-)serious Coq file, and I'd like to get
help from anyone willing to improve my style and tell me about things
in the libraries I don't know about yet (and fix my errors...).

I am trying to define the terms (and types) of simple type theory (aka
higher-order logic) as an inductive datatype in Coq using dependent
types to ensure that all terms are well-typed from the start. Is that
possible?

At the bottom of my file (attached) is the attempt to do it from the
start. Above it, I also tried a more convoluted way where I first
define preterms (which may not be well-typed) then try to take a
subset of them. But I am running into problems with testing equality
(among other things).

A specific side-question: Is there a better way to get dependently
typed lists than the way I have defined ilist?
Any other comments on style are welcome.

I look forward to any replies :)

Thanks
Ramana
Require Import String.

Definition identifier : Set := string.

Record type_operator : Set := mk_type_operator {
  op_name  : identifier;
  op_arity : nat
}.

Section ilist.
  Variable A : Set.

  Inductive ilist : nat -> Set :=
  | nil  : ilist 0
  | cons : forall n, A -> ilist n -> ilist (S n).
End ilist.

Implicit Arguments cons [n A].
Implicit Arguments nil [A].

Inductive type : Set :=
| TyVar : identifier -> type
| TyApp (op : type_operator) : ilist type (op_arity op) -> type.

Local Open Scope string_scope.

Definition fun_tyop := mk_type_operator "->" 2.

Definition fun_type x y := TyApp fun_tyop (cons x (cons y nil)).

Record constant : Set := mk_constant {
  const_name : identifier;
  const_type : type
}.

Inductive preterm : Set :=
| Var   : identifier -> type -> preterm
| Const : constant -> preterm
| App   : preterm -> preterm -> preterm
| Abs   : preterm -> preterm -> preterm.

Require Import Coq.Bool.Bool.
Require Import Coq.Program.Program.

(*

I know I probably need to ensure type_operator and type have decidable equality, before the following will work.
But how do I do that?

Program Fixpoint type_of (tm : preterm) : option type :=
match tm with
  | (Var _ ty)  => Some ty
  | (Const c)   => Some (const_type c)
  | (App t1 t2) => match (type_of t1, type_of t2) with
                     | (Some (TyApp op (cons 1 x (cons 0 y nil))), Some x') => 
                         if (op = fun_tyop) && (x = x') then Some y else None
                     | _ => None
                   end
  | (Abs ((Var _ ty) as x) b) => match type_of b with
                                   | Some tb => Some (fun_type ty tb)
                                   | None => None
                                 end
  | (Abs _ _)   => None
end.

Definition term : Set := {tm : preterm | exists ty, type_of tm = Some ty}

(* Can I define terms at once without preterms?

Inductive term : Set :=
| Var   : identifier -> type -> term
| Const : constant -> term
| App   : forall x y, {t1 : term | has_type t1 (fun_type x y) } -> {t2 : term | has_type t2 x} -> term
| Abs   : identifier -> type -> term -> term
with has_type : term -> type -> Prop :=
| Var_has_type   : has_type (Var _ ty) ty
| Const_has_type : has_type (Const c) (const_type c)
| App_has_type   : forall x y, has_type t1 (fun_type x y) -> has_type t2 x -> has_type (App t1 t2) y.
*)

(* What about defining terms and type_of at once, without has_type? *)



Archive powered by MhonArc 2.6.16.

Top of Page