Library Proofs_TypeOrdering

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') ->
      ({{T}} + {{S}} + {{U}})
      ({{T'}} + {{S}} + {{U}})

Lemma typeRelMul3:
  forall (T S S' U: type),
    (typeRel S S') ->
      ({{T}} + {{S}} + {{U}})
      ({{T}} + {{S'}} + {{U}})

Lemma typeRelMul2:
  forall (T S S1 S2 U: type),
    (typeRel S1 S) ->
    (typeRel S2 S) ->
      ({{T}} + {{S1}} + {{S2}})
      ({{T}} + {{S}} + {{U}})

Lemma typeRelMul4:
  forall (T S U U': type),
    (typeRel U U') ->
      ({{T}} + {{S}} + {{U}})
      ({{T}} + {{S}} + {{U'}})

End SetProgram.

This page has been generated by coqdoc