(* generated by Ott 0.10.14 from: common.ott common_index.ott common_labels.ott common_typing.ott bool.ott bool_typing.ott nat.ott nat_typing.ott arrow_typing.ott basety.ott unit.ott seq.ott ascribe.ott let.ott product.ott sum.ott fix.ott tuple.ott record.ott variant.ott *) Require Import Arith. Require Import Bool. Require Import List. Require Import ott_list_core. Require Import ott_list. (* for [all_distinct] *) (** syntax *) Definition index := nat. Definition label := nat. Lemma eq_label: forall (x y : label), {x = y} + {x <> y}. Proof. decide equality; auto with ott_coq_equality arith. Defined. Hint Resolve eq_label : ott_coq_equality. Definition termvar := nat. Lemma eq_termvar: forall (x y : termvar), {x = y} + {x <> y}. Proof. decide equality; auto with ott_coq_equality arith. Defined. Hint Resolve eq_termvar : ott_coq_equality. Definition basetype := nat. Lemma eq_basetype: forall (x y : basetype), {x = y} + {x <> y}. Proof. decide equality; auto with ott_coq_equality arith. Defined. Hint Resolve eq_basetype : ott_coq_equality. Inductive T : Set := TyBool : T | TyNat : T | TyArr : T -> T -> T | TyId : basetype -> T | TyUnit : T | TyPair : T -> T -> T | TySum : T -> T -> T | TyTuple : list T -> T | TyRecord : list (label*T) -> T | TyVariant : list (label*T) -> T . Inductive C : Set := CCase : label -> termvar -> t -> C with t : Set := TmTrue : t | TmFalse : t | TmIf : t -> t -> t -> t | TmZero : t | TmSucc : t -> t | TmPred : t -> t | TmIszero : t -> t | TmVar : termvar -> t | TmAbs : termvar -> T -> t -> t | TmApp : t -> t -> t | TmUnit : t | TmSeq : t -> t -> t | TmAscribe : t -> T -> t | TmLet : termvar -> t -> t -> t | TmPair : t -> t -> t | TmProj1 : t -> t | TmProj2 : t -> t | TmInl : t -> t | TmInr : t -> t | TmCaseSm : t -> termvar -> t -> termvar -> t -> t | TmFix : t -> t | TmTuple : list t -> t | TmProjTp : t -> index -> t | TmRecord : list (label*t) -> t | TmProj : t -> label -> t | TmVariant : label -> t -> T -> t | TmCase : t -> list C -> t . Definition G : Set := list (termvar*T) . Inductive labels : Set := labels_seq : list label -> labels . (** subrules *) Fixpoint is_v_of_t (t__6:t) : bool := match t__6 with | TmTrue => (true) | TmFalse => (true) | (TmIf t1 t2 t3) => false | TmZero => (true) | (TmSucc t5) => ((is_v_of_t t5)) | (TmPred t5) => false | (TmIszero t5) => false | (TmVar x) => false | (TmAbs x T5 t5) => (true) | (TmApp t1 t2) => false | TmUnit => (true) | (TmSeq t1 t2) => false | (TmAscribe t5 T5) => false | (TmLet x t5 t') => false | (TmPair t1 t2) => ((is_v_of_t t1) && (is_v_of_t t2)) | (TmProj1 t5) => false | (TmProj2 t5) => false | (TmInl t5) => ((is_v_of_t t5)) | (TmInr t5) => ((is_v_of_t t5)) | (TmCaseSm t_5 x1 t1 x2 t2) => false | (TmFix t5) => false | (TmTuple t_list) => ((forall_list (fun (t_:t) => (is_v_of_t t_)) t_list)) | (TmProjTp t5 i) => false | (TmRecord l_t_list) => ((forall_list (fun (pat_:(label*t)) => match pat_ with (l_,t_) => (is_v_of_t t_) end) l_t_list)) | (TmProj t5 l) => false | (TmVariant l t5 T5) => ((is_v_of_t t5)) | (TmCase t5 C_list) => false end. (** free variables *) Fixpoint fv_C (C5:C) : list termvar := match C5 with | (CCase l x t5) => ((list_minus eq_termvar (fv_t t5) (cons x nil))) end with fv_t (t__6:t) : list termvar := match t__6 with | TmTrue => nil | TmFalse => nil | (TmIf t1 t2 t3) => (app (fv_t t1) (app (fv_t t2) (fv_t t3))) | TmZero => nil | (TmSucc t5) => ((fv_t t5)) | (TmPred t5) => ((fv_t t5)) | (TmIszero t5) => ((fv_t t5)) | (TmVar x) => (cons x nil) | (TmAbs x T5 t5) => ((list_minus eq_termvar (fv_t t5) (cons x nil))) | (TmApp t1 t2) => (app (fv_t t1) (fv_t t2)) | TmUnit => nil | (TmSeq t1 t2) => (app (fv_t t1) (fv_t t2)) | (TmAscribe t5 T5) => ((fv_t t5)) | (TmLet x t5 t') => (app (fv_t t5) (list_minus eq_termvar (fv_t t') (cons x nil))) | (TmPair t1 t2) => (app (fv_t t1) (fv_t t2)) | (TmProj1 t5) => ((fv_t t5)) | (TmProj2 t5) => ((fv_t t5)) | (TmInl t5) => ((fv_t t5)) | (TmInr t5) => ((fv_t t5)) | (TmCaseSm t_5 x1 t1 x2 t2) => (app (fv_t t_5) (app (list_minus eq_termvar (fv_t t1) (cons x1 nil)) (list_minus eq_termvar (fv_t t2) (cons x2 nil)))) | (TmFix t5) => ((fv_t t5)) | (TmTuple t_list) => ((flat_map (fun (t_:t) => (fv_t t_)) t_list)) | (TmProjTp t5 i) => ((fv_t t5)) | (TmRecord l_t_list) => ((flat_map (fun (pat_:(label*t)) => match pat_ with (l_,t_) => (fv_t t_) end) l_t_list)) | (TmProj t5 l) => ((fv_t t5)) | (TmVariant l t5 T5) => ((fv_t t5)) | (TmCase t5 C_list) => (app (fv_t t5) (flat_map (fun (C_:C) => (fv_C C_)) C_list)) end. (** substitutions *) Fixpoint subst_C (t_6:t) (x5:termvar) (C5:C) {struct C5} : C := match C5 with | (CCase l x t5) => CCase l x (if list_mem eq_termvar x5 (cons x nil) then t5 else (subst_t t_6 x5 t5)) end with subst_t (t__6:t) (x_5:termvar) (t___7:t) {struct t___7} : t := match t___7 with | TmTrue => TmTrue | TmFalse => TmFalse | (TmIf t1 t2 t3) => TmIf (subst_t t__6 x_5 t1) (subst_t t__6 x_5 t2) (subst_t t__6 x_5 t3) | TmZero => TmZero | (TmSucc t5) => TmSucc (subst_t t__6 x_5 t5) | (TmPred t5) => TmPred (subst_t t__6 x_5 t5) | (TmIszero t5) => TmIszero (subst_t t__6 x_5 t5) | (TmVar x) => (if eq_termvar x x_5 then t__6 else (TmVar x)) | (TmAbs x T5 t5) => TmAbs x T5 (if list_mem eq_termvar x_5 (cons x nil) then t5 else (subst_t t__6 x_5 t5)) | (TmApp t1 t2) => TmApp (subst_t t__6 x_5 t1) (subst_t t__6 x_5 t2) | TmUnit => TmUnit | (TmSeq t1 t2) => TmSeq (subst_t t__6 x_5 t1) (subst_t t__6 x_5 t2) | (TmAscribe t5 T5) => TmAscribe (subst_t t__6 x_5 t5) T5 | (TmLet x t5 t') => TmLet x (subst_t t__6 x_5 t5) (if list_mem eq_termvar x_5 (cons x nil) then t' else (subst_t t__6 x_5 t')) | (TmPair t1 t2) => TmPair (subst_t t__6 x_5 t1) (subst_t t__6 x_5 t2) | (TmProj1 t5) => TmProj1 (subst_t t__6 x_5 t5) | (TmProj2 t5) => TmProj2 (subst_t t__6 x_5 t5) | (TmInl t5) => TmInl (subst_t t__6 x_5 t5) | (TmInr t5) => TmInr (subst_t t__6 x_5 t5) | (TmCaseSm t_5 x1 t1 x2 t2) => TmCaseSm (subst_t t__6 x_5 t_5) x1 (if list_mem eq_termvar x_5 (cons x1 nil) then t1 else (subst_t t__6 x_5 t1)) x2 (if list_mem eq_termvar x_5 (cons x2 nil) then t2 else (subst_t t__6 x_5 t2)) | (TmFix t5) => TmFix (subst_t t__6 x_5 t5) | (TmTuple t_list) => TmTuple (map (fun (t_:t) => (subst_t t__6 x_5 t_)) t_list) | (TmProjTp t5 i) => TmProjTp (subst_t t__6 x_5 t5) i | (TmRecord l_t_list) => TmRecord (map (fun (pat_:(label*t)) => match pat_ with (l_,t_) => (l_,(subst_t t__6 x_5 t_)) end) l_t_list) | (TmProj t5 l) => TmProj (subst_t t__6 x_5 t5) l | (TmVariant l t5 T5) => TmVariant l (subst_t t__6 x_5 t5) T5 | (TmCase t5 C_list) => TmCase (subst_t t__6 x_5 t5) (map (fun (C_:C) => (subst_C t__6 x_5 C_)) C_list) end. (* These definitions are a hack to make [unmake_list'T] (and similarly [unmake_list't]) work whether native lists or specific lists are generated by ott. We use [unmake_list'T] in homs, and that should be a function that converts from whatever type ott uses to represent lists of [T] to standard lists of [T]. The type [list'T] is defined just so as to express the argument type of [unmake_list'T]. *) Definition list'T : Set. exact list_T || exact (list T). Defined. Definition unmake_list'T : list'T -> list T. exact unmake_list_T || exact (fun x => x). Defined. Definition list't : Set. exact list_t || exact (list t). Defined. Definition unmake_list't : list't -> list t. exact unmake_list_t || exact (fun x => x). Defined. Definition list'label : Set. exact list_label || exact (list label). Defined. Definition unmake_list'label : list'label -> list label. exact unmake_list_label || exact (fun x => x). Defined. Definition bound x T0 G := exists G1, exists G2, (G = G1 ++ (x,T0)::G2)%list /\ ~In x (List.map (@fst termvar T) G1). (** definitions *) (* defns Jop *) Inductive (* defn red *) red : t -> t -> Prop := | E_IfTrue : forall (t2:t) (t3:t), red (TmIf TmTrue t2 t3) t2 | E_IfFalse : forall (t2:t) (t3:t), red (TmIf TmFalse t2 t3) t3 | E_If : forall (t1:t) (t2:t) (t3:t) (t1':t), red t1 t1' -> red (TmIf t1 t2 t3) (TmIf t1' t2 t3) | E_Succ : forall (t1:t) (t1':t), red t1 t1' -> red (TmSucc t1) (TmSucc t1') | E_PredZero : red (TmPred TmZero) TmZero | E_PredSucc : forall (v1:t), Is_true (is_v_of_t v1) -> red (TmPred (TmSucc v1) ) v1 | E_Pred : forall (t1:t) (t1':t), red t1 t1' -> red (TmPred t1) (TmPred t1') | E_IsZeroZero : red (TmIszero TmZero) TmTrue | E_IsZeroSucc : forall (v1:t), Is_true (is_v_of_t v1) -> red (TmIszero (TmSucc v1) ) TmFalse | E_IsZero : forall (t1:t) (t1':t), red t1 t1' -> red (TmIszero t1) (TmIszero t1') | E_App1 : forall (t1:t) (t2:t) (t1':t), red t1 t1' -> red (TmApp t1 t2) (TmApp t1' t2) | E_App2 : forall (v1:t) (t2:t) (t2':t), Is_true (is_v_of_t v1) -> red t2 t2' -> red (TmApp v1 t2) (TmApp v1 t2') | E_AppAbs : forall (x:termvar) (T5:T) (t12:t) (v2:t), Is_true (is_v_of_t v2) -> red (TmApp (TmAbs x T5 t12) v2) (subst_t v2 x t12 ) | E_Seq : forall (t1:t) (t2:t) (t1':t), red t1 t1' -> red (TmSeq t1 t2) (TmSeq t1' t2) | E_SeqNext : forall (t2:t), red (TmSeq TmUnit t2) t2 | E_Ascribe : forall (v1:t) (T5:T), Is_true (is_v_of_t v1) -> red (TmAscribe v1 T5) v1 | E_Ascribe1 : forall (t1:t) (T5:T) (t1':t), red t1 t1' -> red (TmAscribe t1 T5) (TmAscribe t1' T5) | E_LetV : forall (x:termvar) (v1:t) (t2:t), Is_true (is_v_of_t v1) -> red (TmLet x v1 t2) (subst_t v1 x t2 ) | E_Let : forall (x:termvar) (t1:t) (t2:t) (t1':t), red t1 t1' -> red (TmLet x t1 t2) (TmLet x t1' t2) | E_PairBeta1 : forall (v1:t) (v2:t), Is_true (is_v_of_t v1) -> Is_true (is_v_of_t v2) -> red (TmProj1 (TmPair v1 v2)) v1 | E_PairBeta2 : forall (v1:t) (v2:t), Is_true (is_v_of_t v1) -> Is_true (is_v_of_t v2) -> red (TmProj2 (TmPair v1 v2)) v2 | E_Proj1 : forall (t1:t) (t1':t), red t1 t1' -> red (TmProj1 t1) (TmProj1 t1') | E_Proj2 : forall (t1:t) (t1':t), red t1 t1' -> red (TmProj2 t1) (TmProj2 t1') | E_Pair1 : forall (t1:t) (t2:t) (t1':t), red t1 t1' -> red (TmPair t1 t2) (TmPair t1' t2) | E_Pair2 : forall (v1:t) (t2:t) (t2':t), Is_true (is_v_of_t v1) -> red t2 t2' -> red (TmPair v1 t2) (TmPair v1 t2') | E_CaseInl : forall (v0:t) (x1:termvar) (t1:t) (x2:termvar) (t2:t), Is_true (is_v_of_t v0) -> red (TmCaseSm (TmInl v0) x1 t1 x2 t2) (subst_t v0 x1 t1 ) | E_CaseInr : forall (v0:t) (x1:termvar) (t1:t) (x2:termvar) (t2:t), Is_true (is_v_of_t v0) -> red (TmCaseSm (TmInr v0) x1 t1 x2 t2) (subst_t v0 x2 t2 ) | E_CaseSm : forall (t0:t) (x1:termvar) (t1:t) (x2:termvar) (t2:t) (t0':t), red t0 t0' -> red (TmCaseSm t0 x1 t1 x2 t2) (TmCaseSm t0' x1 t1 x2 t2) | E_Inl : forall (t1:t) (t1':t), red t1 t1' -> red (TmInl t1) (TmInl t1') | E_Inr : forall (t1:t) (t1':t), red t1 t1' -> red (TmInr t1) (TmInr t1') | E_FixBeta : forall (x:termvar) (T1:T) (t2:t), red (TmFix (TmAbs x T1 t2) ) (subst_t (TmFix (TmAbs x T1 t2) ) x t2 ) | E_Fix : forall (t1:t) (t1':t), red t1 t1' -> red (TmFix t1) (TmFix t1') | E_ProjTuple : forall (v_list:list t) (j:index) (t101:t), nth_error v_list (j - 1) = Some t101 -> (Forall_list (fun (v_:t) => Is_true (is_v_of_t v_)) v_list) -> (1 <= j /\ j <= length (unmake_list't v_list )) -> red (TmProjTp (TmTuple v_list) j) t101 | E_ProjTp : forall (t1:t) (i:index) (t1':t), red t1 t1' -> red (TmProjTp t1 i) (TmProjTp t1' i) | E_Tuple : forall (t_list:list t) (v_list:list t) (t_5:t) (t':t), (Forall_list (fun (v_:t) => Is_true (is_v_of_t v_)) v_list) -> red t_5 t' -> red (TmTuple ((app v_list (app (cons t_5 nil) (app t_list nil))))) (TmTuple ((app v_list (app (cons t' nil) (app t_list nil))))) | E_ProjRcd : forall (l_v_list:list (label*t)) (j:index) (t102:(label*t)) (t103:(label*t)), nth_error l_v_list (j - 1) = Some t102 -> nth_error l_v_list (j - 1) = Some t103 -> (Forall_list (fun (tmp_:(label*t)) => match tmp_ with (l_,v_) => Is_true (is_v_of_t v_) end) l_v_list) -> red (TmProj (TmRecord l_v_list) (match t103 with (l_,v_) => l_ end)) (match t102 with (l_,v_) => v_ end) | E_Proj : forall (t1:t) (l:label) (t1':t), red t1 t1' -> red (TmProj t1 l) (TmProj t1' l) | E_Rcd : forall (l'_t_list:list (label*t)) (l_v_list:list (label*t)) (l:label) (t_5:t) (t':t), (Forall_list (fun (tmp_:(label*t)) => match tmp_ with (l_,v_) => Is_true (is_v_of_t v_) end) l_v_list) -> red t_5 t' -> red (TmRecord ((app l_v_list (app (cons (l,t_5) nil) (app l'_t_list nil))))) (TmRecord ((app l_v_list (app (cons (l,t') nil) (app l'_t_list nil))))) | E_CaseVariant : forall (l_x_t_list:list (label*termvar*t)) (v5:t) (T5:T) (j:index) (t104:(label*termvar*t)) (t105:(label*termvar*t)) (t106:(label*termvar*t)), nth_error l_x_t_list (j - 1) = Some t104 -> nth_error l_x_t_list (j - 1) = Some t105 -> nth_error l_x_t_list (j - 1) = Some t106 -> Is_true (is_v_of_t v5) -> (1 <= j /\ j <= length (unmake_list't (map (fun (pat_:(label*termvar*t)) => match pat_ with (l_,x_,t_) => t_ end ) l_x_t_list) )) -> red (TmCase (TmVariant (match t106 with (l_,x_,t_) => l_ end) v5 T5) (map (fun (pat_:(label*termvar*t)) => match pat_ with (l_,x_,t_) => (CCase l_ x_ t_) end ) l_x_t_list)) (subst_t v5 (match t105 with (l_,x_,t_) => x_ end) (match t104 with (l_,x_,t_) => t_ end) ) | E_Case : forall (l_x_t_list:list (label*termvar*t)) (t_5:t) (t':t), red t_5 t' -> red (TmCase t_5 (map (fun (pat_:(label*termvar*t)) => match pat_ with (l_,x_,t_) => (CCase l_ x_ t_) end ) l_x_t_list)) (TmCase t' (map (fun (pat_:(label*termvar*t)) => match pat_ with (l_,x_,t_) => (CCase l_ x_ t_) end ) l_x_t_list)) | E_Variant : forall (li:label) (ti:t) (T5:T) (ti':t), red ti ti' -> red (TmVariant li ti T5) (TmVariant li ti' T5) . (* defns Jtype *) Inductive (* defn typing *) typing : G -> t -> T -> Prop := | T_True : forall (G5:G), typing G5 TmTrue TyBool | T_False : forall (G5:G), typing G5 TmFalse TyBool | T_If : forall (G5:G) (t1:t) (t2:t) (t3:t) (T5:T), typing G5 t1 TyBool -> typing G5 t2 T5 -> typing G5 t3 T5 -> typing G5 (TmIf t1 t2 t3) T5 | T_Zero : forall (G5:G), typing G5 TmZero TyNat | T_Succ : forall (G5:G) (t1:t), typing G5 t1 TyNat -> typing G5 (TmSucc t1) TyNat | T_Pred : forall (G5:G) (t1:t), typing G5 t1 TyNat -> typing G5 (TmPred t1) TyNat | T_IsZero : forall (G5:G) (t1:t), typing G5 t1 TyNat -> typing G5 (TmIszero t1) TyBool | T_Var : forall (G5:G) (x:termvar) (T5:T), (bound x T5 G5 ) -> typing G5 (TmVar x) T5 | T_Abs : forall (G5:G) (x:termvar) (T1:T) (t2:t) (T2:T), typing (cons ( x , T1 ) G5 ) t2 T2 -> typing G5 (TmAbs x T1 t2) (TyArr T1 T2) | T_App : forall (G5:G) (t1:t) (t2:t) (T12:T) (T11:T), typing G5 t1 (TyArr T11 T12) -> typing G5 t2 T11 -> typing G5 (TmApp t1 t2) T12 | T_Unit : forall (G5:G), typing G5 TmUnit TyUnit | T_Seq : forall (G5:G) (t1:t) (t2:t) (T2:T), typing G5 t1 TyUnit -> typing G5 t2 T2 -> typing G5 (TmSeq t1 t2) T2 | T_Ascribe : forall (G5:G) (t1:t) (T5:T), typing G5 t1 T5 -> typing G5 (TmAscribe t1 T5) T5 | T_Let : forall (G5:G) (x:termvar) (t1:t) (t2:t) (T2:T) (T1:T), typing G5 t1 T1 -> typing (cons ( x , T1 ) G5 ) t2 T2 -> typing G5 (TmLet x t1 t2) T2 | T_Pair : forall (G5:G) (t1:t) (t2:t) (T1:T) (T2:T), typing G5 t1 T1 -> typing G5 t2 T2 -> typing G5 (TmPair t1 t2) (TyPair T1 T2) | T_Proj1 : forall (G5:G) (t1:t) (T1:T) (T2:T), typing G5 t1 (TyPair T1 T2) -> typing G5 (TmProj1 t1) T1 | T_Proj2 : forall (G5:G) (t1:t) (T2:T) (T1:T), typing G5 t1 (TyPair T1 T2) -> typing G5 (TmProj2 t1) T2 | T_Inl : forall (G5:G) (t1:t) (T1:T) (T2:T), typing G5 t1 T1 -> typing G5 (TmInl t1) (TySum T1 T2) | T_Inr : forall (G5:G) (t1:t) (T1:T) (T2:T), typing G5 t1 T2 -> typing G5 (TmInr t1) (TySum T1 T2) | T_CaseSm : forall (G5:G) (t0:t) (x1:termvar) (t1:t) (x2:termvar) (t2:t) (T_5:T) (T1:T) (T2:T), typing G5 t0 (TySum T1 T2) -> typing (cons ( x1 , T1 ) G5 ) t1 T_5 -> typing (cons ( x2 , T2 ) G5 ) t2 T_5 -> typing G5 (TmCaseSm t0 x1 t1 x2 t2) T_5 | T_Fix : forall (G5:G) (t1:t) (T1:T), typing G5 t1 (TyArr T1 T1) -> typing G5 (TmFix t1) T1 | T_Tuple : forall (t_T_list:list (t*T)) (G5:G), (forall (t_:t) (T_:T), In (G5,t_,T_) (map (fun (pat_:t*T) => match pat_ with (t_,T_) => (G5,t_,T_) end) t_T_list) -> (typing G5 t_ T_)) -> typing G5 (TmTuple (map (fun (pat_:(t*T)) => match pat_ with (t_,T_) => t_ end ) t_T_list)) (TyTuple (map (fun (pat_:(t*T)) => match pat_ with (t_,T_) => T_ end ) t_T_list)) | T_ProjTp : forall (T_list:list T) (G5:G) (t1:t) (j:index) (t107:T), nth_error T_list (j - 1) = Some t107 -> typing G5 t1 (TyTuple T_list) -> (1 <= j /\ j <= length (unmake_list'T T_list )) -> typing G5 (TmProjTp t1 j) t107 | T_Rcd : forall (l_t_T_list:list (label*t*T)) (G5:G), (forall (t_:t) (T_:T), In (G5,t_,T_) (map (fun (pat_:label*t*T) => match pat_ with (l_,t_,T_) => (G5,t_,T_) end) l_t_T_list) -> (typing G5 t_ T_)) -> (Is_true (all_distinct eq_label (unmake_list'label (map (fun (pat_:(label*t*T)) => match pat_ with (l_,t_,T_) => l_ end ) l_t_T_list) ))) -> typing G5 (TmRecord (map (fun (pat_:(label*t*T)) => match pat_ with (l_,t_,T_) => (l_,t_) end ) l_t_T_list)) (TyRecord (map (fun (pat_:(label*t*T)) => match pat_ with (l_,t_,T_) => (l_,T_) end ) l_t_T_list)) | T_Proj : forall (l_T_list:list (label*T)) (j:index) (G5:G) (t1:t) (t108:(label*T)) (t109:(label*T)), nth_error l_T_list (j - 1) = Some t108 -> nth_error l_T_list (j - 1) = Some t109 -> typing G5 t1 (TyRecord l_T_list) -> typing G5 (TmProj t1 (match t109 with (l_,T_) => l_ end)) (match t108 with (l_,T_) => T_ end) | T_Variant : forall (l_T_list:list (label*T)) (G5:G) (t5:t) (j:index) (t110:(label*T)) (t111:(label*T)), nth_error l_T_list (j - 1) = Some t110 -> nth_error l_T_list (j - 1) = Some t111 -> typing G5 t5 (match t110 with (l_,T_) => T_ end) -> (1 <= j /\ j <= length (unmake_list'T (map (fun (pat_:(label*T)) => match pat_ with (l_,T_) => T_ end ) l_T_list) )) -> typing G5 (TmVariant (match t111 with (l_,T_) => l_ end) t5 (TyVariant l_T_list)) (TyVariant l_T_list) | T_Case : forall (l_x_t_T_list:list (label*termvar*t*T)) (G5:G) (t_5:t) (T_5:T), typing G5 t_5 (TyVariant (map (fun (pat_:(label*termvar*t*T)) => match pat_ with (l_,x_,t_,T_) => (l_,T_) end ) l_x_t_T_list)) -> (forall (x_:termvar) (T_:T) (t_:t), In ( (cons ( x_ , T_ ) G5 ) ,t_,T_5) (map (fun (pat_:label*termvar*t*T) => match pat_ with (l_,x_,t_,T_) => ( (cons ( x_ , T_ ) G5 ) ,t_,T_5) end) l_x_t_T_list) -> (typing (cons ( x_ , T_ ) G5 ) t_ T_5)) -> (Is_true (all_distinct eq_label (unmake_list'label (map (fun (pat_:(label*termvar*t*T)) => match pat_ with (l_,x_,t_,T_) => l_ end ) l_x_t_T_list) ))) -> typing G5 (TmCase t_5 (map (fun (pat_:(label*termvar*t*T)) => match pat_ with (l_,x_,t_,T_) => (CCase l_ x_ t_) end ) l_x_t_T_list)) T_5 . (** induction principles *) Section T_rect. Variables (P_T : T -> Prop) (P_list_T : list T -> Prop) (P_list_label_T : list (label*T) -> Prop). Hypothesis (H_TyBool : P_T TyBool) (H_TyNat : P_T TyNat) (H_TyArr : forall (T5:T), P_T T5 -> forall (T':T), P_T T' -> P_T (TyArr T5 T')) (H_TyId : forall (A:basetype), P_T (TyId A)) (H_TyUnit : P_T TyUnit) (H_TyPair : forall (T1:T), P_T T1 -> forall (T2:T), P_T T2 -> P_T (TyPair T1 T2)) (H_TySum : forall (T1:T), P_T T1 -> forall (T2:T), P_T T2 -> P_T (TySum T1 T2)) (H_TyTuple : forall (T_list:list T), P_list_T T_list -> P_T (TyTuple T_list)) (H_TyRecord : forall (l_T_list:list (label*T)), P_list_label_T l_T_list -> P_T (TyRecord l_T_list)) (H_TyVariant : forall (l_T_list:list (label*T)), P_list_label_T l_T_list -> P_T (TyVariant l_T_list)) (H_list_T_nil : P_list_T nil) (H_list_T_cons : forall (T0:T), P_T T0 -> forall (T_l:list T), P_list_T T_l -> P_list_T (cons T0 T_l)) (H_list_label_T_nil : P_list_label_T nil) (H_list_label_T_cons : forall (label0:label), forall (T1:T), P_T T1 -> forall (label_T_l:list (label*T)), P_list_label_T label_T_l -> P_list_label_T (cons (label0,T1) label_T_l)). Fixpoint T_ott_ind (n:T) : P_T n := match n as x return P_T x with | TyBool => H_TyBool | TyNat => H_TyNat | (TyArr T5 T') => H_TyArr T5 (T_ott_ind T5) T' (T_ott_ind T') | (TyId A) => H_TyId A | TyUnit => H_TyUnit | (TyPair T1 T2) => H_TyPair T1 (T_ott_ind T1) T2 (T_ott_ind T2) | (TySum T1 T2) => H_TySum T1 (T_ott_ind T1) T2 (T_ott_ind T2) | (TyTuple T_list) => H_TyTuple T_list (((fix T_list_ott_ind (T_l:list T) : P_list_T T_l := match T_l as x return P_list_T x with nil => H_list_T_nil | cons T2 xl => H_list_T_cons T2(T_ott_ind T2)xl (T_list_ott_ind xl) end)) T_list) | (TyRecord l_T_list) => H_TyRecord l_T_list (((fix l_T_list_ott_ind (label_T_l:list (label*T)) : P_list_label_T label_T_l := match label_T_l as x return P_list_label_T x with nil => H_list_label_T_nil | cons (label1,T3) xl => H_list_label_T_cons label1 T3(T_ott_ind T3)xl (l_T_list_ott_ind xl) end)) l_T_list) | (TyVariant l_T_list) => H_TyVariant l_T_list (((fix l_T_list_ott_ind (label_T_l:list (label*T)) : P_list_label_T label_T_l := match label_T_l as x return P_list_label_T x with nil => H_list_label_T_nil | cons (label2,T4) xl => H_list_label_T_cons label2 T4(T_ott_ind T4)xl (l_T_list_ott_ind xl) end)) l_T_list) end. End T_rect. Section C_t_rect. Variables (P_C : C -> Prop) (P_list_t : list t -> Prop) (P_list_label_t : list (label*t) -> Prop) (P_t : t -> Prop) (P_list_C : list C -> Prop). Hypothesis (H_CCase : forall (l:label), forall (x:termvar), forall (t5:t), P_t t5 -> P_C (CCase l x t5)) (H_TmTrue : P_t TmTrue) (H_TmFalse : P_t TmFalse) (H_TmIf : forall (t1:t), P_t t1 -> forall (t2:t), P_t t2 -> forall (t3:t), P_t t3 -> P_t (TmIf t1 t2 t3)) (H_TmZero : P_t TmZero) (H_TmSucc : forall (t5:t), P_t t5 -> P_t (TmSucc t5)) (H_TmPred : forall (t5:t), P_t t5 -> P_t (TmPred t5)) (H_TmIszero : forall (t5:t), P_t t5 -> P_t (TmIszero t5)) (H_TmVar : forall (x:termvar), P_t (TmVar x)) (H_TmAbs : forall (x:termvar), forall (T5:T), forall (t5:t), P_t t5 -> P_t (TmAbs x T5 t5)) (H_TmApp : forall (t1:t), P_t t1 -> forall (t2:t), P_t t2 -> P_t (TmApp t1 t2)) (H_TmUnit : P_t TmUnit) (H_TmSeq : forall (t1:t), P_t t1 -> forall (t2:t), P_t t2 -> P_t (TmSeq t1 t2)) (H_TmAscribe : forall (t5:t), P_t t5 -> forall (T5:T), P_t (TmAscribe t5 T5)) (H_TmLet : forall (x:termvar), forall (t5:t), P_t t5 -> forall (t':t), P_t t' -> P_t (TmLet x t5 t')) (H_TmPair : forall (t1:t), P_t t1 -> forall (t2:t), P_t t2 -> P_t (TmPair t1 t2)) (H_TmProj1 : forall (t5:t), P_t t5 -> P_t (TmProj1 t5)) (H_TmProj2 : forall (t5:t), P_t t5 -> P_t (TmProj2 t5)) (H_TmInl : forall (t5:t), P_t t5 -> P_t (TmInl t5)) (H_TmInr : forall (t5:t), P_t t5 -> P_t (TmInr t5)) (H_TmCaseSm : forall (t_5:t), P_t t_5 -> forall (x1:termvar), forall (t1:t), P_t t1 -> forall (x2:termvar), forall (t2:t), P_t t2 -> P_t (TmCaseSm t_5 x1 t1 x2 t2)) (H_TmFix : forall (t5:t), P_t t5 -> P_t (TmFix t5)) (H_TmTuple : forall (t_list:list t), P_list_t t_list -> P_t (TmTuple t_list)) (H_TmProjTp : forall (t5:t), P_t t5 -> forall (i:index), P_t (TmProjTp t5 i)) (H_TmRecord : forall (l_t_list:list (label*t)), P_list_label_t l_t_list -> P_t (TmRecord l_t_list)) (H_TmProj : forall (t5:t), P_t t5 -> forall (l:label), P_t (TmProj t5 l)) (H_TmVariant : forall (l:label), forall (t5:t), P_t t5 -> forall (T5:T), P_t (TmVariant l t5 T5)) (H_TmCase : forall (C_list:list C), P_list_C C_list -> forall (t5:t), P_t t5 -> P_t (TmCase t5 C_list)) (H_list_t_nil : P_list_t nil) (H_list_t_cons : forall (t0:t), P_t t0 -> forall (t_l:list t), P_list_t t_l -> P_list_t (cons t0 t_l)) (H_list_label_t_nil : P_list_label_t nil) (H_list_label_t_cons : forall (label0:label), forall (t1:t), P_t t1 -> forall (label_t_l:list (label*t)), P_list_label_t label_t_l -> P_list_label_t (cons (label0,t1) label_t_l)) (H_list_C_nil : P_list_C nil) (H_list_C_cons : forall (C0:C), P_C C0 -> forall (C_l:list C), P_list_C C_l -> P_list_C (cons C0 C_l)). Fixpoint t_ott_ind (n:t) : P_t n := match n as x return P_t x with | TmTrue => H_TmTrue | TmFalse => H_TmFalse | (TmIf t1 t2 t3) => H_TmIf t1 (t_ott_ind t1) t2 (t_ott_ind t2) t3 (t_ott_ind t3) | TmZero => H_TmZero | (TmSucc t5) => H_TmSucc t5 (t_ott_ind t5) | (TmPred t5) => H_TmPred t5 (t_ott_ind t5) | (TmIszero t5) => H_TmIszero t5 (t_ott_ind t5) | (TmVar x) => H_TmVar x | (TmAbs x T5 t5) => H_TmAbs x T5 t5 (t_ott_ind t5) | (TmApp t1 t2) => H_TmApp t1 (t_ott_ind t1) t2 (t_ott_ind t2) | TmUnit => H_TmUnit | (TmSeq t1 t2) => H_TmSeq t1 (t_ott_ind t1) t2 (t_ott_ind t2) | (TmAscribe t5 T5) => H_TmAscribe t5 (t_ott_ind t5) T5 | (TmLet x t5 t') => H_TmLet x t5 (t_ott_ind t5) t' (t_ott_ind t') | (TmPair t1 t2) => H_TmPair t1 (t_ott_ind t1) t2 (t_ott_ind t2) | (TmProj1 t5) => H_TmProj1 t5 (t_ott_ind t5) | (TmProj2 t5) => H_TmProj2 t5 (t_ott_ind t5) | (TmInl t5) => H_TmInl t5 (t_ott_ind t5) | (TmInr t5) => H_TmInr t5 (t_ott_ind t5) | (TmCaseSm t_5 x1 t1 x2 t2) => H_TmCaseSm t_5 (t_ott_ind t_5) x1 t1 (t_ott_ind t1) x2 t2 (t_ott_ind t2) | (TmFix t5) => H_TmFix t5 (t_ott_ind t5) | (TmTuple t_list) => H_TmTuple t_list (((fix t_list_ott_ind (t_l:list t) : P_list_t t_l := match t_l as x return P_list_t x with nil => H_list_t_nil | cons t2 xl => H_list_t_cons t2(t_ott_ind t2)xl (t_list_ott_ind xl) end)) t_list) | (TmProjTp t5 i) => H_TmProjTp t5 (t_ott_ind t5) i | (TmRecord l_t_list) => H_TmRecord l_t_list (((fix l_t_list_ott_ind (label_t_l:list (label*t)) : P_list_label_t label_t_l := match label_t_l as x return P_list_label_t x with nil => H_list_label_t_nil | cons (label1,t3) xl => H_list_label_t_cons label1 t3(t_ott_ind t3)xl (l_t_list_ott_ind xl) end)) l_t_list) | (TmProj t5 l) => H_TmProj t5 (t_ott_ind t5) l | (TmVariant l t5 T5) => H_TmVariant l t5 (t_ott_ind t5) T5 | (TmCase t5 C_list) => H_TmCase C_list (((fix C_list_ott_ind (C_l:list C) : P_list_C C_l := match C_l as x return P_list_C x with nil => H_list_C_nil | cons C1 xl => H_list_C_cons C1(C_ott_ind C1)xl (C_list_ott_ind xl) end)) C_list) t5 (t_ott_ind t5) end with C_ott_ind (n:C) : P_C n := match n as x return P_C x with | (CCase l x t5) => H_CCase l x t5 (t_ott_ind t5) end. End C_t_rect.