Proofs about Type Ordering |
Require Import Calculus.
Require Import WellFoundation.
Module SetProgram(My_Program: Program).
Import My_Program.
Require Proofs_Miscellaneous.
Module My_Proofs_Miscellaneous := Proofs_Miscellaneous.SetProgram(My_Program).
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.
| Interpretation and substitution of a value |
Lemma lemmaA12:
forall (T: type) (v: Value),
(symbol_of_type (thisSubst_in_type T (Path_value v))) = (symbol_of_type T)
.
| Interpretation and substitution of a path |
Lemma lemmaA12':
forall (T: type) (p: Path),
(symbol_of_type (thisSubst_in_type T p)) = (symbol_of_type T)
.
| typeRel is a function extension of symRel |
Lemma typeRel_is_fun_extension:
typeRel = (fun_extension type Sym symbol_of_type symRel)
.
| Type ordering and substitution of a value |
Lemma lemmaA14:
forall (T U: type) (v: Value),
(typeRel T U) ->
(typeRel (thisSubst_in_type T (Path_value v)) (thisSubst_in_type U (Path_value v))).
| Type ordering is well-founded |
Lemma lemmaA17: (well_founded typeRel).
| Facts about type ordering - 1 |
Lemma lemmaA15_1: forall (T: type) (C: ClassSym),
(typeRel T (type_class C)) ->
exists C': ClassSym, T = (type_class C')
.
| Facts about type ordering - 2 |
Lemma lemmaA15_2: forall (C: ClassSym) (p: Path) (L: TypeSym),
(typeRel (type_class C) (type_virtual p L))
.
| Declarations and type ordering |
Lemma lemmaA13_1:
forall (L: TypeSym) (T: type) (p: Path),
(typeUpperBound L) = T ->
(typeRel (thisSubst_in_type T p) (type_virtual p L))
.
| Declarations and type ordering |
Lemma lemmaA13_1':
forall (L: TypeSym) (U: type) (p: Path),
(typeLowerBound L) = (Some U) ->
(typeRel (thisSubst_in_type U p) (type_virtual p L))
.
| Declarations and type ordering |
Lemma lemmaA13_2:
forall (L: TypeSym) (C: ClassSym) (T: type) (p: Path),
(typeValue L C) = (Some T) ->
(typeRel (thisSubst_in_type T p) (type_virtual p L))
.
| Declarations and type ordering |
Lemma lemmaA13_3:
forall (C C': ClassSym),
(classSuper C) = (Some C') ->
(typeRel (type_class C') (type_class C))
.
Require Import Multiset.
Require Import MultisetCore.
Require Import MultisetList.
Require Import RelExtras.
Require Import Setoid.
Require Import MultisetOrder.
Require Import MultisetTheory.
Module Type_Eqset: Eqset
with Definition A := type
with Definition eqA := fun (T U: type) => T = U
.
Definition A : Set := type.
Definition eqA : A -> A -> Prop := fun (T U: type) => T = U.
Lemma sid_theoryA: Setoid_Theory A eqA.
End Type_Eqset.
Module Type_Eqset_dec: Eqset_dec
with Module ESM := Type_Eqset
with Definition eqA_dec := Type_eqdec.
Module ESM := Type_Eqset.
Import ESM.
Definition eqA_dec: forall (x y: A), { (eqA x y) } + { ~(eqA x y) } := Type_eqdec.
End Type_Eqset_dec.
Module Type_Multiset: FiniteMultisetCore
with Module Sid := Type_Eqset_dec
:= FiniteMultisetList(Type_Eqset_dec).
Import Type_Multiset.
Module Type_MultisetOrder := MultisetOrder(Type_Multiset).
Import Type_MultisetOrder.
Import MSet.
| Multiset extension of typeRel |
Definition typeRelMul: Multiset -> Multiset -> Prop := MultisetLt (transp _ typeRel).
Lemma lemmaA18_aux_1: forall (A: Set) (R: A -> A -> Prop) (x: A),
(Acc R x) ->
(Acc (fun (x y: A) => (R x y)) x).
Lemma lemmaA18_aux_2: forall (A: Set) (R: A -> A -> Prop),
(well_founded R) ->
(well_founded (fun (x y: A) => (R x y))).
| The multiset extension of type ordering is well-founded |
Lemma lemmaA18:
well_founded typeRelMul.
| Some useful multiset inequalities |
Lemma typeRelMul1:
forall (T T' S U: type),
(typeRel T T') ->
(typeRelMul
({{T}} + {{S}} + {{U}})
({{T'}} + {{S}} + {{U}})
)
.
Lemma typeRelMul3:
forall (T S S' U: type),
(typeRel S S') ->
(typeRelMul
({{T}} + {{S}} + {{U}})
({{T}} + {{S'}} + {{U}})
)
.
Lemma typeRelMul2:
forall (T S S1 S2 U: type),
(typeRel S1 S) ->
(typeRel S2 S) ->
(typeRelMul
({{T}} + {{S1}} + {{S2}})
({{T}} + {{S}} + {{U}})
)
.
Lemma typeRelMul4:
forall (T S U U': type),
(typeRel U U') ->
(typeRelMul
({{T}} + {{S}} + {{U}})
({{T}} + {{S}} + {{U'}})
)
.
End SetProgram.