Miscellaneous properties |
Require Import Calculus.
Require Import List.
Require Import ListSet.
Require Import MatchCompNat.
Require Import Util.
Require Import Omega.
Module SetProgram(My_Program: Program).
Import My_Program.
Require WellFormedness.
Module My_WellFormedness := WellFormedness.SetProgram(My_Program).
Import My_WellFormedness.
Import My_Semantics.
Import My_Typing.
Import My_TypeOrdering.
Import My_DeBruijn.
Import My_Substitutions.
Import My_Subclassing.
| The program is well-formed |
Axiom program_is_well_formed_proof: WF_program.
Lemma symRel_is_well_founded_proof: symRel_is_well_founded.
Lemma classes_smaller_than_types_proof: classes_smaller_than_types.
Lemma classes_are_well_formed_proof: classes_are_well_formed.
Lemma no_method_overriding_proof: no_method_overriding.
Lemma no_type_overriding_proof: no_type_overriding.
Lemma main_term_is_well_typed: (exists T: type, (Typing rootEnv main T)).
Lemma typeVal_subtype_of_upperBound:
forall (L: TypeSym) (C: ClassSym) (S T: type),
(typeUpperBound L) = T ->
(typeValue L C) = (Some S) ->
(Subtyping (classEnv C) S T)
.
Lemma typeVal_supertype_of_lowerBound:
forall (L: TypeSym) (C: ClassSym) (S T: type),
(typeLowerBound L) = (Some T) ->
(typeValue L C) = (Some S) ->
(Subtyping (classEnv C) T S)
.
Lemma methodBody_of_type_methodType:
forall (m: MethodSym) (C: ClassSym) (t: Term) (T: type),
(methodValue m C) = (Some t) ->
(methodType m) = T ->
(Typing (Env_mk (Owner_class C) (method_parameters m) nil) t T)
.
Lemma param_types_are_well_formed:
forall (x: ParamSym) (T: type) (m: MethodSym) (C: ClassSym),
(paramType x) = T ->
(paramOwner x) = m ->
(methodOwner m) = C ->
(Kinding (classEnv C) T)
.
Lemma methodTypes_are_well_formed:
forall (m: MethodSym) (C: ClassSym) (T: type),
(methodOwner m) = C ->
(methodType m) = T ->
(Kinding (classEnv C) T)
.
Lemma fieldTypes_are_well_formed:
forall (f: FieldSym) (C: ClassSym) (T: type),
(fieldOwner f) = C ->
(fieldType f) = T ->
(Kinding (classEnv C) T)
.
Lemma typeUpperBounds_are_well_formed:
forall (L: TypeSym) (C: ClassSym) (T: type),
(typeOwner L) = C ->
(typeUpperBound L) = T ->
(Kinding (classEnv C) T)
.
Lemma typeLowerBounds_are_well_formed:
forall (L: TypeSym) (C: ClassSym) (T: type),
(typeOwner L) = C ->
(typeLowerBound L) = (Some T) ->
(Kinding (classEnv C) T)
.
Lemma typeValues_are_well_formed:
forall (L: TypeSym) (C: ClassSym) (T: type),
(typeValue L C) = (Some T) ->
(Kinding (classEnv C) T)
.
| Admissibility of subsumption |
Lemma lemmaA1:
forall (G: Env) (t: Term) (T U: type),
(Typing G t T) ->
(Gen_Subtyping G T U) ->
(Typing G t U)
.
| Self in self substitution |
Lemma lemmaA2_1:
forall (p q: Path),
(this_in_path (thisSubst_in_path q p)) ->
(this_in_path p)
.
| Self in self substitution |
Lemma lemmaA2_2:
forall (p: Path) (T: type),
(this_in_type (thisSubst_in_type T p)) ->
(this_in_path p)
.
Lemma lemmaA24_aux:
forall (p: Path) (T: type),
~(this_in_path p) ->
~(this_in_type (thisSubst_in_type T p))
.
| ??? |
Lemma free_parameters_and_lifting_aux_0:
forall (p: Path) (n k: nat),
(fp_in_path (lift_at_depth_in_path p n k)) = (fp_in_path p)
.
Lemma free_parameters_and_lifting_aux_2:
forall (T: type) (n k: nat),
(fp_in_type (lift_at_depth_in_type T n k)) = (fp_in_type T)
.
Lemma free_parameters_and_lifting_0:
forall (p: Path) (n: nat),
(fp_in_path (lift_in_path p n)) = (fp_in_path p)
.
Lemma free_parameters_and_lifting_2:
forall (T: type) (n: nat),
(fp_in_type (lift_in_type T n)) = (fp_in_type T)
.
| Free parameters are in the context |
| Function: first projection of a list of typed parameters |
Definition paramTypeList_to_paramList (xTs: ParamTypeList): (list ParamSym) :=
(map (fun a => match a with (x, T) => x end) xTs)
.
Lemma lemmaA3_aux_1:
forall (x: ParamSym) (T: type) (xTs: ParamTypeList),
(In (x, T) xTs) ->
(In x (paramTypeList_to_paramList xTs))
.
Definition lemmaA3_prop1 (G: Env) (p: Path) (T: type) (H: (Gen_PathTyping G p T)): Prop :=
forall (O: Owner) (xTs: ParamTypeList) (Us: TypeList),
G = (Env_mk O xTs Us) ->
forall (x: ParamSym),
(paramset_In x (paramset_union (fp_in_path p) (fp_in_type T))) ->
(In x (paramTypeList_to_paramList xTs))
.
Definition lemmaA3_prop2 (G: Env) (T U: type) (H: (Gen_Subtyping G T U)): Prop :=
forall (O: Owner) (xTs: ParamTypeList) (Us: TypeList),
G = (Env_mk O xTs Us) ->
forall (x: ParamSym),
(paramset_In x (paramset_union (fp_in_type T) (fp_in_type U))) ->
(In x (paramTypeList_to_paramList xTs))
.
| Free parameters are in the context -- subtyping |
Lemma lemmaA3_2:
forall (O: Owner) (xTs: ParamTypeList) (Us: TypeList) (T U: type),
(Gen_Subtyping (Env_mk O xTs Us) T U) ->
forall (x: ParamSym),
(paramset_In x (paramset_union (fp_in_type T) (fp_in_type U))) ->
(In x (paramTypeList_to_paramList xTs))
.
| Free parameters are in the context -- path typing |
Lemma lemmaA3_0:
forall (O: Owner) (xTs: ParamTypeList) (Us: TypeList) (p: Path) (T: type),
(Gen_PathTyping (Env_mk O xTs Us) p T) ->
forall (x: ParamSym),
(paramset_In x (paramset_union (fp_in_path p) (fp_in_type T))) ->
(In x (paramTypeList_to_paramList xTs))
.
| Free parameters are in the context -- type well-formedness |
Lemma lemmaA3_3:
forall (O: Owner) (xTs: ParamTypeList) (Us: TypeList) (T: type),
(Kinding (Env_mk O xTs Us) T) ->
forall (x: ParamSym),
(paramset_In x (fp_in_type T)) ->
(In x (paramTypeList_to_paramList xTs))
.
Lemma lemmaA3_3_corollary:
forall (C: ClassSym) (T: type),
(Kinding (classEnv C) T) ->
forall (x: ParamSym), ~(paramset_In x (fp_in_type T))
.
| Free variables are in the context |
Definition lemmaA4_prop1 (G: Env) (p: Path) (T: type) (H: (Gen_PathTyping G p T)): Prop :=
forall (O: Owner) (xTs: ParamTypeList) (Us: TypeList),
G = (Env_mk O xTs Us) ->
forall (d: nat),
d <= (length Us) ->
forall (k: VarSym),
(varset_In k (varset_union (fv_at_depth_in_path p d) (fv_at_depth_in_type T d))) ->
(k < (length Us) - d)
.
Definition lemmaA4_prop2 (G: Env) (T U: type) (H: (Gen_Subtyping G T U)): Prop :=
forall (O: Owner) (xTs: ParamTypeList) (Us: TypeList),
G = (Env_mk O xTs Us) ->
forall (d: nat),
d <= (length Us) ->
forall (k: VarSym),
(varset_In k (varset_union (fv_at_depth_in_type T d) (fv_at_depth_in_type U d))) ->
(k < (length Us) - d)
.
| Free variables are in the context -- subtyping |
Lemma lemmaA4_2':
forall (O: Owner) (xTs: ParamTypeList) (Us: TypeList) (T U: type),
(Gen_Subtyping (Env_mk O xTs Us) T U) ->
forall (d: nat),
d <= (length Us) ->
forall (k: VarSym),
(varset_In k (varset_union (fv_at_depth_in_type T d) (fv_at_depth_in_type U d))) ->
(k < (length Us) - d)
.
| Free variables are in the context -- path typing |
Lemma lemmaA4_0':
forall (O: Owner) (xTs: ParamTypeList) (Us: TypeList) (p: Path) (T: type),
(Gen_PathTyping (Env_mk O xTs Us) p T) ->
forall (d: nat),
d <= (length Us) ->
forall (k: VarSym),
(varset_In k (varset_union (fv_at_depth_in_path p d) (fv_at_depth_in_type T d))) ->
(k < (length Us) - d)
.
| Free variables are in the context -- type well-formedness |
Lemma lemmaA4_3':
forall (O: Owner) (xTs: ParamTypeList) (Us: TypeList) (T: type),
(Kinding (Env_mk O xTs Us) T) ->
forall (d: nat),
d <= (length Us) ->
forall (k: VarSym),
(varset_In k (fv_at_depth_in_type T d)) ->
(k < (length Us) - d)
.
Lemma lemmaA4_0:
forall (O: Owner) (xTs: ParamTypeList) (Us: TypeList) (p: Path) (T: type),
(Gen_PathTyping (Env_mk O xTs Us) p T) ->
forall (n: VarSym),
(varset_In n (varset_union (fv_in_path p) (fv_in_type T))) ->
(n < (length Us))
.
Lemma lemmaA4_2:
forall (O: Owner) (xTs: ParamTypeList) (Us: TypeList) (T U: type),
(Gen_Subtyping (Env_mk O xTs Us) T U) ->
forall (n: VarSym),
(varset_In n (varset_union (fv_in_type T) (fv_in_type U))) ->
(n < (length Us))
.
Lemma lemmaA4_3:
forall (O: Owner) (xTs: ParamTypeList) (Us: TypeList) (T: type),
(Kinding (Env_mk O xTs Us) T) ->
forall (n: VarSym),
(varset_In n (fv_in_type T)) ->
(n < (length Us))
.
Lemma lemmaA4_3_corollary:
forall (C: ClassSym) (T: type),
(Kinding (classEnv C) T) ->
(forall (n: nat), ~(varset_In n (fv_in_type T)))
.
Lemma lemmaA4_0_corollary:
forall (v: Value) (T: type),
(Gen_PathTyping rootEnv (Path_value v) T) ->
forall (n: VarSym), ~(varset_In n (fv_in_type T))
.
Definition lemmaA4_1_prop1 (G: Env) (t: Term) (T: type) (H: (Typing G t T)): Prop :=
forall (O: Owner) (xTs: ParamTypeList) (Us: TypeList),
G = (Env_mk O xTs Us) ->
forall (d: nat),
d <= (length Us) ->
forall (k: VarSym),
(varset_In k (varset_union (fv_at_depth_in_term t d) (fv_at_depth_in_type T d))) ->
(k < (length Us) - d)
.
Definition lemmaA4_1_prop2 (G: Env) (p: Path) (m: MethodSym) (xts: ParamTermList)
(H: (ParamTermListTyping G p m xts)): Prop :=
forall (O: Owner) (xTs: ParamTypeList) (Us: TypeList),
G = (Env_mk O xTs Us) ->
forall (d: nat),
d <= (length Us) ->
forall (k: VarSym),
(varset_In k (fv_at_depth_in_paramTermList xts d)) ->
(k < (length Us) - d)
.
Definition lemmaA4_1_prop3 (G: Env) (C: ClassSym) (fts: FieldTermList)
(H: (FieldTermListTyping G C fts)): Prop :=
forall (O: Owner) (xTs: ParamTypeList) (Us: TypeList),
G = (Env_mk O xTs Us) ->
forall (d: nat),
d <= (length Us) ->
forall (k: VarSym),
(varset_In k (fv_at_depth_in_fieldTermList fts d)) ->
(k < (length Us) - d)
.
Lemma lemmaA4_1:
forall (O: Owner) (xTs: ParamTypeList) (Us: TypeList) (t: Term) (T: type),
(Typing (Env_mk O xTs Us) t T) ->
forall (n: VarSym),
(varset_In n (varset_union (fv_in_term t) (fv_in_type T))) ->
(n < (length Us))
.
Lemma param_in_classEnv:
forall (C: ClassSym) (x: ParamSym) (T: type),
~(PathTyping (classEnv C) (Path_param x) T)
.
Lemma var_in_classEnv:
forall (C: ClassSym ) (n: VarSym) (T: type),
~(PathTyping (classEnv C) (Path_var n) T)
.
Lemma path_in_classEnv:
forall (C: ClassSym) (p: Path) (T: type),
(PathTyping (classEnv C) p T) ->
(p = Path_this) \/
exists v: Value, p = (Path_value v)
.
| Chaining self substitutions |
Lemma lemmaA8_1:
forall (p1 p2 q: Path),
(thisSubst_in_path (thisSubst_in_path q p1) p2) =
(thisSubst_in_path q (thisSubst_in_path p1 p2))
.
| Chaining self substitutions |
Lemma lemmaA8_2:
forall (p1 p2: Path) (T: type),
(thisSubst_in_type (thisSubst_in_type T p1) p2) =
(thisSubst_in_type T (thisSubst_in_path p1 p2))
.
Definition lemmaA5_P1 (t: Term): Prop :=
forall (v: Value) (t': Term),
(value_to_term v) = t ->
~(Red_term t t').
Definition lemmaA5_P2 (fts: FieldTermList): Prop :=
forall (fvs: FieldValueList) (fts': FieldTermList),
(fieldValueList_to_fieldTermList fvs) = fts ->
~(Red_fieldTermList fts fts').
Lemma lemmaA5: forall (t : Term), (lemmaA5_P1 t).
| Some terms are not typable in empty context - 1 |
Lemma lemmaA6_1:
forall (T: type),
~(PathTyping rootEnv Path_this T)
.
| Some terms are not typable in empty context - 1 |
Lemma lemmaA6_1':
forall (T: type),
~(Gen_PathTyping rootEnv Path_this T)
.
| Some terms are not typable in empty context - 2 |
Lemma lemmaA6_2:
forall (x: ParamSym) (T: type),
~(PathTyping rootEnv (Path_param x) T)
.
| Some terms are not typable in empty context - 2 |
Lemma lemmaA6_2':
forall (x: ParamSym) (T: type),
~(Gen_PathTyping rootEnv (Path_param x) T)
.
| Some terms are not typable in empty context - 3 |
Lemma lemmaA6_3:
forall (n: VarSym) (T: type),
~(PathTyping rootEnv (Path_var n) T)
.
| Some terms are not typable in empty context - 3 |
Lemma lemmaA6_3':
forall (n: VarSym) (T: type),
~(Gen_PathTyping rootEnv (Path_var n) T)
.
| Paths typable in empty context are values |
Lemma lemmaA7:
forall (p: Path) (T: type),
(PathTyping rootEnv p T) ->
exists v: Value, p = (Path_value v)
.
| Paths typable in empty context are values |
Lemma lemmaA7':
forall (p: Path) (T: type),
(Gen_PathTyping rootEnv p T) ->
exists v: Value, p = (Path_value v)
.
| Decidability of equality for values |
Definition Value_eqdec' (v: Value): Set := forall (v' : Value), { v = v' }+{ v <> v' }.
Definition FieldValueList_eqdec' (fvs: FieldValueList): Set := forall (fvs': FieldValueList), { fvs = fvs' }+{ fvs <> fvs' }.
Lemma Value_eqdec: forall (v: Value), (Value_eqdec' v).
| Decidability of equality for paths |
Lemma Path_eqdec: forall (p q : Path), { p = q }+{ p <> q }.
| Decidability of equality for types |
Lemma Type_eqdec : forall (T U : type), { T = U }+{ T <> U }.
Definition paramValueList_to_paramList (xvs: ParamValueList): (list ParamSym) :=
(map (fun a => match a with (x, v) => x end) xvs)
.
Lemma lemmaA9_aux_0:
forall (x: ParamSym) (xvs: ParamValueList),
~(In x (paramValueList_to_paramList xvs)) ->
(map_paramSubst_in_path (Path_param x) xvs) = (Path_param x)
.
Lemma lemmaA9_0:
forall (q: Path) (p: Path) (xvs: ParamValueList),
(forall (x: ParamSym), (In x (paramValueList_to_paramList xvs)) -> ~(param_in_path x q)) ->
(map_paramSubst_in_path (thisSubst_in_path q p) xvs) =
(thisSubst_in_path q (map_paramSubst_in_path p xvs))
.
Lemma lemmaA9_2:
forall (T: type) (p: Path) (xvs: ParamValueList),
(forall (x: ParamSym), (In x (paramValueList_to_paramList xvs)) -> ~(param_in_type x T)) ->
(map_paramSubst_in_type (thisSubst_in_type T p) xvs) =
(thisSubst_in_type T (map_paramSubst_in_path p xvs))
.
Lemma lemmaA10_0:
forall (q: Path) (p: Path) (k: nat) (v: Value),
(fv_in_path q) = empty_varset ->
(varSubst_in_path (thisSubst_in_path q p) k v) =
(thisSubst_in_path q (varSubst_in_path p k v))
.
Lemma lemmaA10_2:
forall (T: type) (p: Path) (k: nat) (v: Value),
(fv_in_type T) = empty_varset ->
(varSubst_in_type (thisSubst_in_type T p) k v) =
(thisSubst_in_type T (varSubst_in_path p k v))
.
Lemma new_lemma1_0:
forall (p: Path) (q: Path),
~(this_in_path p) ->
(thisSubst_in_path p q) = p
.
Lemma new_lemma1_2:
forall (T: type) (q: Path),
~(this_in_type T) ->
(thisSubst_in_type T q) = T
.
Lemma new_lemma2_0:
forall (q: Path),
(fp_in_path q) = empty_paramset ->
forall (p: Path),
(fp_in_path (thisSubst_in_path p q)) = (fp_in_path p)
.
Lemma new_lemma2_2:
forall (q: Path),
(fp_in_path q) = empty_paramset ->
forall (T: type),
(fp_in_type (thisSubst_in_type T q)) = (fp_in_type T)
.
Lemma fp_and_paramSubst_in_path:
forall (p: Path) (xvs: ParamValueList),
(fp_in_path p) = empty_paramset ->
(map_paramSubst_in_path p xvs) = p
.
Lemma fp_and_paramSubst_in_type:
forall (T: type) (xvs: ParamValueList),
(fp_in_type T) = empty_paramset ->
(map_paramSubst_in_type T xvs) = T
.
Lemma fv_and_paramSubst_in_path:
forall (p: Path) (xvs: ParamValueList),
(fv_in_path (map_paramSubst_in_path p xvs)) = (fv_in_path p)
.
Lemma fv_and_paramSubst_in_type:
forall (T: type) (xvs: ParamValueList),
(fv_in_type (map_paramSubst_in_type T xvs)) = (fv_in_type T)
.
End SetProgram.