coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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? *)
- [Coq-Club] newbie: dependent types, Ramana Kumar
- Re: [Coq-Club] newbie: dependent types, gallais @ ensl.org
- Re: [Coq-Club] newbie: dependent types, Benedikt Ahrens
Archive powered by MhonArc 2.6.16.