proposition: Theorem well_typed_programs_are_safe: forall a t, nil ⊢ a ∈ t -> safe a.
proof: Proof. Abort. End Subtyping. From Coq Require Import FunctionalExtensionality. Module Intrinsic. Definition context := list type. Inductive var: context -> type -> Type := | V1: forall {E: context} {t: type}, var (t :: E) t | VS: forall {E: context} {t t': type}, var E t' -> var (t :: E) t'. Definition V2 {E: context} {t1 t2: type}: var (t1 :: t2 :: E) t2 := VS V1. Definition V3 {E: context} {t1 t2 t3: type}: var (t1 :: t2 :: t3 :: E) t3 := VS V2. Inductive term: context -> type -> Type := | Var: forall {E: context} {t: type}, var E t -> term E t | Abs: forall {E: context} {t t': type}, term (t :: E) t' -> term E (Fun t t') | App: forall {E: context} {t t': type}, term E (Fun t t') -> term E t -> term E t' | Const: forall {E: context} (b: bool), term E Bool | Cond: forall {E: context} {t: type}, term E Bool -> term E t -> term E t -> term E t. Definition t_negation : term nil (Bool --> Bool) := Abs (Cond (Var V1) (Const false) (Const true)). Definition t_compose (t1 t2 t3: type) : term nil ((t1 --> t2) --> (t2 --> t3) --> (t1 --> t3)) := Abs (Abs (Abs (App (Var V2) (App (Var V3) (Var V1))))). Fail Definition t_error : term nil Bool := Cond (Abs (Var V1)) (Const false) (Const true). Fixpoint dtype (t: type) : Type := match t with | Bool => bool | Fun t1 t2 => dtype t1 -> dtype t2 end. Fixpoint dcontext (E: context) : Type := match E with | nil => unit | t :: E => dtype t * dcontext E end. Fixpoint dvar {E: context} {t: type} (v: var E t): dcontext E -> dtype t := match v with | V1 => (fun e => fst e) | VS v => (fun e => dvar v (snd e)) end. Fixpoint dterm {E: context} {t: type} (a: term E t) : dcontext E -> dtype t := match a with | Var v => dvar v | Abs a => (fun e => (fun v => dterm a (v, e))) | App a1 a2 => (fun e => dterm a1 e (dterm a2 e)) | Const b => (fun e => b) | Cond a ifso ifnot => (fun e => if dterm a e then dterm ifso e else dterm ifnot e) end. Lemma dbeta: forall (E: context) (t t': type) (a: term (t :: E) t') (b: term E t), forall e, dterm (App (Abs a) b) e = dterm a (dterm b e, e). Proof. reflexivity. Qed.
imports: Coq(Bool String List Program.Equality) CDF(Sequences)