Proofs about Admissibility of Transitivity for Subtyping |
Require Import Calculus.
Module SetProgram(My_Program: Program).
Import My_Program.
Require Proofs_Subclassing.
Module My_Proofs_Subclassing := Proofs_Subclassing.SetProgram(My_Program).
Import My_Proofs_Subclassing.
Import My_Proofs_TypeOrdering.
Import My_Proofs_Miscellaneous.
Import My_WellFormedness.
Import My_Semantics.
Import My_Typing.
Import My_TypeOrdering.
Import My_DeBruijn.
Import My_Substitutions.
Import My_Subclassing.
Definition lemmaA23_prop1 (G: Env) (p: Path) (T: type) (H: (PathTyping G p T)): Prop :=
(Gen_PathTyping G p T)
.
Definition lemmaA23_prop2 (G: Env) (T: type) (U: type) (H: (Subtyping G T U)): Prop :=
(Gen_Subtyping G T U)
.
Definition lemmaA23_prop3 (G: Env) (C: ClassSym) (fvs: FieldValueList) (H: (FieldValueListTyping G C fvs)): Prop :=
(Gen_FieldValueListTyping G C fvs)
.
| Unstructuring derivations |
Lemma lemmaA23_2:
forall (G: Env) (T: type) (U: type),
(Subtyping G T U) ->
(Gen_Subtyping G T U)
.
| Unstructuring derivations |
Lemma lemmaA23_1:
forall (G: Env) (p: Path) (T: type),
(PathTyping G p T) ->
(Gen_PathTyping G p T)
.
Definition lemmaA24_prop_1 (G: Env) (TA T: type) (H: (Subtyping G TA T)): Prop :=
forall (C A: ClassSym),
G = (classEnv C) ->
TA = (type_class A) ->
~(this_in_type T) ->
(Subtyping rootEnv (type_class A) T)
.
Definition lemmaA24_prop_2 (G: Env) (p: Path) (T: type) (H: (PathTyping G p T)): Prop :=
forall (C: ClassSym) (v: Value),
G = (classEnv C) ->
p = (Path_value v) ->
~(this_in_type T) ->
(PathTyping rootEnv (Path_value v) T)
.
Definition lemmaA24_prop_3 (G: Env) (B: ClassSym) (fvs: FieldValueList) (H: (FieldValueListTyping G B fvs)): Prop :=
forall (C: ClassSym),
G = (classEnv C) ->
(FieldValueListTyping rootEnv B fvs)
.
| Strengthening - 2 |
Lemma lemmaA24_2_aux:
forall (G: Env) (p: Path) (T: type) (H: PathTyping G p T),
(lemmaA24_prop_2 G p T H)
.
| Strengthening - 2 |
Lemma lemmaA24_2:
forall (C: ClassSym) (v: Value) (T: type),
(PathTyping (classEnv C) (Path_value v) T) ->
~(this_in_type T) ->
(PathTyping rootEnv (Path_value v) T)
.
| Admissibility of transitivity for class type subtyping |
Lemma lemmaA25:
forall (G G' G'': Env) (A B C: ClassSym),
(Subtyping G (type_class A) (type_class B)) ->
(Subtyping G' (type_class B) (type_class C)) ->
(Subtyping G'' (type_class A) (type_class C))
.
| Substitution for self in structured derivations - 1 |
Definition lemmaA26_prop_1 (G: Env) (p: Path) (T: type) (H: (PathTyping G p T)): Prop :=
forall (v: Value) (C A: ClassSym),
(PathTyping rootEnv (Path_value v) (type_class C)) ->
G = (classEnv C) ->
T = (type_class A) ->
(PathTyping rootEnv (thisSubst_in_path p (Path_value v)) (type_class A))
.
| Substitution for self in structured derivations - 2 |
Definition lemmaA26_prop_2 (G: Env) (T U: type) (H: (Subtyping G T U)): Prop :=
forall (v: Value) (C: ClassSym),
(PathTyping rootEnv (Path_value v) (type_class C)) ->
G = (classEnv C) ->
(Subtyping rootEnv (thisSubst_in_type T (Path_value v)) (thisSubst_in_type U (Path_value v)))
.
| Substitution for self in structured derivations - 1 |
Lemma lemmaA26_1_aux:
forall (G: Env) (p: Path) (T: type) (H: (PathTyping G p T)),
(lemmaA26_prop_1 G p T H).
| Substitution for self in structured derivations - 1 |
Lemma lemmaA26_1:
forall (v: Value) (C: ClassSym),
(PathTyping rootEnv (Path_value v) (type_class C)) ->
forall (A: ClassSym) (p: Path),
(PathTyping (classEnv C) p (type_class A)) ->
(PathTyping rootEnv (thisSubst_in_path p (Path_value v)) (type_class A))
.
| Substitution for self in structured derivations - 2 |
Lemma lemmaA26_2_aux:
forall (G: Env) (T U: type) (H: (Subtyping G T U)),
(lemmaA26_prop_2 G T U H).
| Substitution for self in structured derivations - 2 |
Lemma lemmaA26_2:
forall (v: Value) (C: ClassSym) (T U: type),
(PathTyping rootEnv (Path_value v) (type_class C)) ->
(Subtyping (classEnv C) T U) ->
(Subtyping rootEnv (thisSubst_in_type T (Path_value v)) (thisSubst_in_type U (Path_value v)))
.
Import Type_Multiset.
Import Type_MultisetOrder.
Import MSet.
Definition lemmaA27_prop (tm: Type_Multiset.Multiset): Prop :=
forall (T S U: type),
tm = ({{T}} + {{S}} + {{U}}) ->
(Subtyping rootEnv T S) ->
(Subtyping rootEnv S U) ->
(Subtyping rootEnv T U)
.
| Admissibility of transitivity for structured subtyping |
Lemma lemmaA27:
forall (T S U: type),
(Subtyping rootEnv T S) ->
(Subtyping rootEnv S U) ->
(Subtyping rootEnv T U)
.
Definition lemmaA28_prop1 (G: Env) (p: Path) (T: type) (H: (Gen_PathTyping G p T)): Prop :=
forall (v: Value),
(G = rootEnv) ->
(p = (Path_value v)) ->
(PathTyping rootEnv p T)
.
Definition lemmaA28_prop2 (G: Env) (T: type) (U: type) (H: (Gen_Subtyping G T U)): Prop :=
(G = rootEnv) ->
(Subtyping rootEnv T U)
.
Definition lemmaA28_prop3 (G: Env) (C: ClassSym) (fvs: FieldValueList) (H: (Gen_FieldValueListTyping G C fvs)): Prop :=
(G = rootEnv) ->
(FieldValueListTyping rootEnv C fvs)
.
| Structuring derivations -- subtyping |
Lemma lemmaA28_2:
forall (T: type) (U: type),
(Gen_Subtyping rootEnv T U) ->
(Subtyping rootEnv T U)
.
| Structuring derivations -- path typing |
Lemma lemmaA28_1:
forall (v: Value) (T: type),
(Gen_PathTyping rootEnv (Path_value v) T) ->
(PathTyping rootEnv (Path_value v) T)
.
End SetProgram.