```(*************************************************************************** * Calculus of Constructions - Definitions * * Arthur Charguéraud, April 2007, Coq v8.1 * ***************************************************************************) Set Implicit Arguments. Require Import Metatheory. (* ********************************************************************** *) (** ** Description of the Language *) (* ********************************************************************** *) (** Grammar of pre-terms of the calculus of constructions *) Inductive trm : Set := | trm_bvar : nat -> trm | trm_fvar : var -> trm | trm_type : nat -> trm | trm_app : trm -> trm -> trm | trm_abs : trm -> trm -> trm | trm_prod : trm -> trm -> trm. (* ********************************************************************** *) (** Open operation *) Fixpoint open_rec (k : nat) (u : trm) (t : trm) {struct t} : trm := match t with | trm_bvar i => if k === i then u else (trm_bvar i) | trm_fvar x => trm_fvar x | trm_type n => trm_type n | trm_app t1 t2 => trm_app (open_rec k u t1) (open_rec k u t2) | trm_abs t1 t2 => trm_abs (open_rec k u t1) (open_rec (S k) u t2) | trm_prod t1 t2 => trm_prod (open_rec k u t1) (open_rec (S k) u t2) end. Definition open t u := open_rec 0 u t. Notation "{ k ~> u } t" := (open_rec k u t) (at level 67). Notation "t ^^ u" := (open t u) (at level 67). Notation "t ^ x" := (open t (trm_fvar x)). (* ********************************************************************** *) (** Terms as locally closed pre-terms *) Inductive term : trm -> Prop := | term_var : forall x, term (trm_fvar x) | term_app : forall t1 t2, term t1 -> term t2 -> term (trm_app t1 t2) | term_type : forall n, term (trm_type n) | term_abs : forall L t1 t2, term t1 -> (forall x, x \notin L -> term (t2 ^ x)) -> term (trm_abs t1 t2) | term_prod : forall L t1 t2, term t1 -> (forall x, x \notin L -> term (t2 ^ x)) -> term (trm_prod t1 t2). (* ********************************************************************** *) (** Closedness of the body of an abstraction *) Definition body t := exists L, forall x, x \notin L -> term (t ^ x). (* ********************************************************************** *) (** Definition of a relation on terms *) Definition relation := trm -> trm -> Prop. (* ********************************************************************** *) (** Definition of the beta relation *) Inductive beta : relation := | beta_red : forall t1 t2 u, term (trm_abs t1 t2) -> term u -> beta (trm_app (trm_abs t1 t2) u) (t2 ^^ u) | beta_app1 : forall t1 t1' t2, term t2 -> beta t1 t1' -> beta (trm_app t1 t2) (trm_app t1' t2) | beta_app2 : forall t1 t2 t2', term t1 -> beta t2 t2' -> beta (trm_app t1 t2) (trm_app t1 t2') | beta_abs1 : forall t1 t1' t2, body t2 -> beta t1 t1' -> beta (trm_abs t1 t2) (trm_abs t1' t2) | beta_abs2 : forall L t1 t2 t2', term t1 -> (forall x, x \notin L -> beta (t2 ^ x) (t2' ^ x)) -> beta (trm_abs t1 t2) (trm_abs t1 t2') | beta_prod1 : forall t1 t1' t2, body t2 -> beta t1 t1' -> beta (trm_prod t1 t2) (trm_prod t1' t2) | beta_prod2 : forall L t1 t2 t2', term t1 -> (forall x, x \notin L -> beta (t2 ^ x) (t2' ^ x)) -> beta (trm_prod t1 t2) (trm_prod t1 t2'). (* ********************************************************************** *) (** Definition of the reflexive-transitive closure of a relation *) Inductive star_ (R : relation) : relation := | star_refl : forall t, term t -> star_ R t t | star_trans : forall t2 t1 t3, star_ R t1 t2 -> star_ R t2 t3 -> star_ R t1 t3 | star_step : forall t t', R t t' -> star_ R t t'. Notation "R 'star'" := (star_ R) (at level 69). (* ********************************************************************** *) (** Definition of the reflexive-symmetric-transitive closure of a relation *) Inductive equiv_ (R : relation) : relation := | equiv_refl : forall t, term t -> equiv_ R t t | equiv_sym: forall t t', equiv_ R t t' -> equiv_ R t' t | equiv_trans : forall t2 t1 t3, equiv_ R t1 t2 -> equiv_ R t2 t3 -> equiv_ R t1 t3 | equiv_step : forall t t', R t t' -> equiv_ R t t'. Notation "R 'equiv'" := (equiv_ R) (at level 69). (* ********************************************************************** *) (** Conversion relation *) Definition conv := beta equiv. (* ********************************************************************** *) (** Subtyping relation *) Inductive less : relation := | less_conv : forall t1 t2, conv t1 t2 -> less t1 t2 | less_univ : forall i j, i <= j -> less (trm_type i) (trm_type j) | less_prod : forall L U U' T T', conv U U' -> (forall x, x \notin L -> less (T ^ x) (T' ^ x) ) -> less (trm_prod U T) (trm_prod U' T') | less_refl : forall T, term T -> less T T | less_trans : forall U T V, less T U -> less U V -> less T V. (* ********************************************************************** *) (** Environment for typing *) Definition env := Env.env trm. (* ********************************************************************** *) (** Typing relation for terms *) Inductive typing : env -> relation := | typing_type : forall E i, wf E -> typing E (trm_type i) (trm_type (i+1)) | typing_var : forall E x U, wf E -> binds x U E -> typing E (trm_fvar x) U | typing_prod : forall k L i E U T, typing E U (trm_type k) -> (forall x, x \notin L -> typing (E & x ~ U) (T ^ x) (trm_type i)) -> (i = k \/ i = 0) -> typing E (trm_prod U T) (trm_type i) | typing_abs : forall i L E U t T, typing E (trm_prod U T) (trm_type i) -> (forall x, x \notin L -> typing (E & x ~ U) (t ^ x) (T ^ x)) -> typing E (trm_abs U t) (trm_prod U T) | typing_app : forall E t u T U, typing E t (trm_prod U T) -> typing E u U -> typing E (trm_app t u) (T ^^ u) | typing_sub : forall T i E t U, less T U -> typing E t T -> typing E U (trm_type i) -> typing E t U (* ********************************************************************** *) (** Typing relation for contexts *) with wf : env -> Prop := | wf_nil : wf empty | wf_cons : forall i E x U, x # E -> typing E U (trm_type i) -> wf (E & x ~ U). (* ********************************************************************** *) (** ** Description of our Goals *) (** Confluence property (proved for beta star) *) Definition confluence (R : relation) := forall M S T, R M S -> R M T -> exists P : trm, R S P /\ R T P. (** Church-Rosser property (proved for beta) *) Definition church_rosser (R : relation) := forall t1 t2, (R equiv) t1 t2 -> exists t, (R star) t1 t /\ (R star) t2 t. (** Subject relation (proved for beta and beta star) *) Definition subject_reduction (R : relation) := forall E t t' T, R t t' -> typing E t T -> typing E t' T. ```