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')
.
intros.
eapply lemmaA21_aux. apply H. trivial. trivial.
Qed.
End SetProgram.