Library Proofs_Subclassing

Proofs about Subclassing

Require Import Calculus.
Require Import Arith.

Module SetProgram(My_Program: Program).

Import My_Program.

Require Proofs_TypeOrdering.
Module My_Proofs_TypeOrdering := Proofs_TypeOrdering.SetProgram(My_Program).

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.

Hint Constructors Subclass.

Transitivity of subclassing
Lemma lemmaA19: forall (A B C: ClassSym),
  (Subclass A B) ->
  (Subclass B C) ->
  (Subclass A C).

Transitivity of subclassing
Lemma lemmaA20: forall (C C1 C2: ClassSym),
  (Subclass C C1) ->
  (Subclass C C2) ->
  (Subclass C1 C2) \/ (Subclass C2 C1).

Subclassing implies subtyping
Lemma lemmaA22:
  forall (C C': ClassSym) (G: Env),
    (Subclass C C') ->
    (Subtyping G (type_class C) (type_class C'))

Subtyping implies subclassing
Lemma lemmaA21:
  forall (C C': ClassSym) (G: Env),
    (Subtyping G (type_class C) (type_class C')) ->
    (Subclass C C')
eapply lemmaA21_aux. apply H. trivial. trivial.

End SetProgram.

This page has been generated by coqdoc