(* generated by Ott 0.10.17 from: common.ott common_type.ott common_typing.ott bool.ott bool_type.ott bool_typing.ott nat.ott nat_type.ott nat_typing.ott var.ott fun.ott fun_type.ott fun_typing.ott fix.ott typed_arith_fix_subst.ott *) Require Import Arith. Require Import Bool. Require Import List. Require Logic. Definition eq_var := beq_nat. (** syntax *) Definition label := nat. Definition index := nat. Definition var := nat. Inductive type : Set := | TyBool : type | TyNat : type | TyArrow : type -> type -> type. Inductive ctx : Set := | CtxEmpty : ctx | CtxExtend : ctx -> var -> type -> ctx. Inductive term : Set := | TmTrue : term | TmFalse : term | TmIf : term -> term -> term -> term | TmZero : term | TmSucc : term -> term | TmPred : term -> term | TmIszero : term -> term | TmVar : var -> term | TmAbs : var -> type -> term -> term | TmApp : term -> term -> term | TmFix : term -> term. Require Export notations. (** We use Coq's notations so we can use the standard syntax of terms even in Coq. However, since the syntax of the object languages is very similar to the syntax of Coq, some confusion may easily arise. In general, we use [true%tm] to denote an object language term (represented as the constructor [TmTrue] in Coq) to avoid confusing it with the ordinary boolean [true] that we use when programming directly in Coq. **) Delimit Scope term_scope with tm. Bind Scope term_scope with term. (** We use the special scope [ty_scope] for the types in our object language. This allows us to write [Bool%ty] instead of [TyBool]. **) Delimit Scope ty_scope with ty. Bind Scope ty_scope with type. Delimit Scope ctx_scope with ctx. Bind Scope ctx_scope with ctx. Arguments Scope CtxExtend [ctx_scope nat_scope ty_scope]. (** ** Typing contexts and variable lookup In TAPL the typing contexts are defined informally as simple sets of pairs of variables and types, and there is a convention that all variables in a typing context must be distinct. In practice this means that the same variable may not be bound twice in nested scopes. However, including these kinds of constraints in a Coq formalization would complicate the presentation, and the restriction is not even very realistic: in real-world programming languages, shadowing variables (i.e. defining a new variable with the same name as one that is already in scope) is allowed. So we here use a more formal definition of a typing context: a typing context is defined by the following grammar: G ::= empty | G, x : T So in practice it is a list of pairs of the form [x : T]. The relation [x : T in G] then means that the _rightmost_ occurrence of [x] in the context [G] is associated with the type [T]. This allows the same variable occur appear multiple times in the context, so we can then type terms like [\x:Bool. \x:Nat. x]. **) Arguments Scope TmIf [term_scope term_scope term_scope]. Notation "'true'" := (TmTrue) : term_scope. Notation "'false'" := (TmFalse) : term_scope. Notation "'if' t1 'then' t2 'else' t3" := ((TmIf t1 t2 t3)) : term_scope. Notation "'Bool'" := TyBool (at level 0, no associativity) : ty_scope. Notation "'succ' t" := ((TmSucc t)) : term_scope. Notation "'pred' t" := ((TmPred t)) : term_scope. Notation "0" := (TmZero) : term_scope. Notation "'iszero' t" := ((TmIszero t)) : term_scope. Notation "'Nat'" := TyNat (at level 0, no associativity) : ty_scope. Arguments Scope TmVar [nat_scope]. Arguments Scope TmAbs [_ ty_scope term_scope]. Arguments Scope TmApp [term_scope term_scope]. (** Since the stop [.] is a terminator of Coq commands, we cannot use it as the delimiter between the binder and the body of a lambda abstraction. We follow Coq's example and use the comma [,] here. **) Notation "\ x : T , t" := (TmAbs x T t) : term_scope. (** Plain juxtaposition is impossible to overload with Coq's notation mechanism. We resort to the syntax [t1 $ t2] to express an application of [t1] to the argument [t2]. The [$]-operator is left-associative, so we can write [t1 $ t2 $ t3] for [(t1 $ t2) $ t3]. **) Notation "t1 $ t2" := (TmApp t1 t2) : term_scope. (** We represent variable _identifiers_ with plain numbers. To get an expression representing a variable reference, we have to use the [TmVar] constructor. In informal presentations the distinction between a plain identifier and a variable reference is often ignored, and we just write [x] to mean a reference to the variable named [x]. However, since in our Coq formalization numbers and terms are different things, we express this distinction by writing ['x] for a variable reference. On the other hand, the identifier is unadorned when it appears in the binding position of a lambda abstraction. Hence we write the identity function for numbers as [\x:Nat, 'x]. **) Notation "' n" := (TmVar n) (at level 7, no associativity) : term_scope. Arguments Scope TyArrow [ty_scope ty_scope]. Notation "T -> U" := (TyArrow T U) : ty_scope. Notation "'fixx' t" := ((TmFix t)) : term_scope. (** ** General recursion We use the syntax [fixx t] for the fixpoint operator to avoid clashing with the built-in [fix] keyword of Coq. There are two evaluation rules for the fixpoint operator: the congruence rule [E_Fix] states that as long as [t1] can be evaluated further (i.e. it is not a value), it can be evaluated inside [fixx t1]. This rule is not needed very often, because the usual way of using the fixpoint operator is to give it a lambda abstraction directly as an argument. The computation rule [E_FixBeta] does the real work: if [t = fixx (\x:T1.t2)], then when [t] gets evaluated, then [x] is replaced by [t] in [t2]. Usually, [t2] is itself another lambda abstraction, which can then refer to itself with the variable [x]. **) Fixpoint subst x t' t := match t with | (TmVar y) => if beq_nat x y then t' else t | (t1 $ t2)%tm => (subst x t' t1 $ subst x t' t2)%tm | (\ y : T , t1)%tm => if beq_nat x y then t else (\ y : T, subst x t' t1)%tm | (fixx t1)%tm => (fixx (subst x t' t1))%tm | (if t1 then t2 else t3)%tm => (if (subst x t' t1) then (subst x t' t2) else (subst x t' t3))%tm | (succ t1)%tm => (succ (subst x t' t1))%tm | (pred t1)%tm => (pred (subst x t' t1))%tm | (iszero t1)%tm => (iszero (subst x t' t1))%tm | _ => t end. (** definitions *) (* defns Jtype *) Inductive bound : var -> type -> ctx -> Prop := (* defn bound *) | B_Here : forall (x:var) (T:type) (G:ctx), bound x T (CtxExtend G x T) | B_Next : forall (x:var) (T:type) (G:ctx) (y:var) (T':type), (Logic.not (x = y)) -> bound x T G -> bound x T (CtxExtend G y T') with fvs : term -> var -> Prop := (* defn fvs *) | FVS_If1 : forall (t1 t2 t3:term) (x:var), fvs t1 x -> fvs (TmIf t1 t2 t3) x | FVS_If2 : forall (t1 t2 t3:term) (x:var), fvs t2 x -> fvs (TmIf t1 t2 t3) x | FVS_If3 : forall (t1 t2 t3:term) (x:var), fvs t3 x -> fvs (TmIf t1 t2 t3) x | FVS_Var : forall (x:var), fvs (TmVar x) x | FVS_Abs : forall (y:var) (T:type) (t:term) (x:var), (Logic.not (x = y)) -> fvs t x -> fvs (TmAbs y T t) x | FVS_App1 : forall (t1 t2:term) (x:var), fvs t1 x -> fvs (TmApp t1 t2) x | FVS_App2 : forall (t1 t2:term) (x:var), fvs t2 x -> fvs (TmApp t1 t2) x with typing : ctx -> term -> type -> Prop := (* defn typing *) | T_True : forall (G:ctx), typing G TmTrue TyBool | T_False : forall (G:ctx), typing G TmFalse TyBool | T_If : forall (G:ctx) (t1 t2 t3:term) (T:type), typing G t1 TyBool -> typing G t2 T -> typing G t3 T -> typing G (TmIf t1 t2 t3) T | T_Zero : forall (G:ctx), typing G TmZero TyNat | T_Succ : forall (G:ctx) (t1:term), typing G t1 TyNat -> typing G (TmSucc t1) TyNat | T_Pred : forall (G:ctx) (t1:term), typing G t1 TyNat -> typing G (TmPred t1) TyNat | T_IsZero : forall (G:ctx) (t1:term), typing G t1 TyNat -> typing G (TmIszero t1) TyBool | T_Var : forall (G:ctx) (x:var) (T:type), bound x T G -> typing G (TmVar x) T | T_Abs : forall (G:ctx) (x:var) (T1:type) (t2:term) (T2:type), typing (CtxExtend G x T1) t2 T2 -> typing G (TmAbs x T1 t2) (TyArrow T1 T2) | T_App : forall (G:ctx) (t1 t2:term) (T12 T11:type), typing G t1 (TyArrow T11 T12) -> typing G t2 T11 -> typing G (TmApp t1 t2) T12 | T_Fix : forall (G:ctx) (t1:term) (T1:type), typing G t1 (TyArrow T1 T1) -> typing G (TmFix t1) T1. (* defns Jop *) Inductive nv : term -> Prop := (* defn nv *) | NV_Zero : nv TmZero | NV_Succ : forall (t:term), nv t -> nv (TmSucc t) with val : term -> Prop := (* defn val *) | Val_True : val TmTrue | Val_False : val TmFalse | Val_NV : forall (t:term), nv t -> val t | Val_Abs : forall (x:var) (T:type) (t:term), val (TmAbs x T t) with eval : term -> term -> Prop := (* defn eval *) | E_IfTrue : forall (t2 t3:term), eval (TmIf TmTrue t2 t3) t2 | E_IfFalse : forall (t2 t3:term), eval (TmIf TmFalse t2 t3) t3 | E_If : forall (t1 t2 t3 t1':term), eval t1 t1' -> eval (TmIf t1 t2 t3) (TmIf t1' t2 t3) | E_Succ : forall (t1 t1':term), eval t1 t1' -> eval (TmSucc t1) (TmSucc t1') | E_PredZero : eval (TmPred TmZero) TmZero | E_PredSucc : forall (t1:term), nv t1 -> eval (TmPred (TmSucc t1) ) t1 | E_Pred : forall (t1 t1':term), eval t1 t1' -> eval (TmPred t1) (TmPred t1') | E_IsZeroZero : eval (TmIszero TmZero) TmTrue | E_IsZeroSucc : forall (t1:term), nv t1 -> eval (TmIszero (TmSucc t1) ) TmFalse | E_IsZero : forall (t1 t1':term), eval t1 t1' -> eval (TmIszero t1) (TmIszero t1') | E_App1 : forall (t1 t2 t1':term), eval t1 t1' -> eval (TmApp t1 t2) (TmApp t1' t2) | E_App2 : forall (t1 t2 t2':term), val t1 -> eval t2 t2' -> eval (TmApp t1 t2) (TmApp t1 t2') | E_AppAbs : forall (x:var) (T:type) (t12 t2:term), val t2 -> eval (TmApp (TmAbs x T t12) t2) (subst x t2 t12 ) | E_FixBeta : forall (x:var) (T1:type) (t2:term), eval (TmFix (TmAbs x T1 t2) ) (subst x (TmFix (TmAbs x T1 t2) ) t2 ) | E_Fix : forall (t1 t1':term), eval t1 t1' -> eval (TmFix t1) (TmFix t1'). Notation "t1 --> t2" := (eval t1 t2) : type_scope. Notation "{}" := CtxEmpty : ctx_scope. Notation "{ G , x : T }" := ((CtxExtend G x T)) : ctx_scope. Notation "|- t : T" := (typing CtxEmpty t T) : type_scope. Notation "G |- t : T" := (typing G t T) : type_scope. Notation "[ x |-> t1 ] t2" := (subst x t1 t2 ) : term_scope.