Extending Declarative Subtyping (Extend.v)
This module takes a user-supplied extension relation and a declarative subtyping relation and creates an extended subtyping relation. Due to the explicit reflexivity and transitivity rules of the declarative subtyping relation, extended subtyping is still easily provably reflexive and transitive. This corresponds to Extended Subtyping in the paper.Require Import Common.
Require Import Tradition.
Module Type Extension (T : Typ) (Rule : Rules T).
Import T.
Import Rule.
Parameter Con : T -> T -> Prop.
End Extension.
Module ExtendedRules (T : Typ) (Rule : Rules T) (ERule : Extension T Rule) <: Rules T.
Import T.
Module Traditional := Traditional T Rule.
Inductive ECon (t t' : T) : Type
:= traditional : Traditional.TransRefl.Con t t' -> ECon t t'
| extended : ERule.Con t t' -> ECon t t'.
Arguments traditional [ t t' ].
Arguments extended [ t t' ].
Definition Con := ECon.
Definition Req {t t' : T} (con : Con t t') : Type
:= match con with
| traditional con => Traditional.TransRefl.Req con
| extended con => Empty
end.
Definition Ass {t t' : T} {con : Con t t'} : Req con -> Position -> T
:= match con as con return Req con -> Position -> T with
| traditional con => @Traditional.TransRefl.Ass _ _ con
| extended con => fun e => match e with end
end.
End ExtendedRules.
Module Extended (T : Typ) (Rule : Rules T) (ERule : Extension T Rule).
Import T.
Module ExtendedRules := ExtendedRules T Rule ERule.
Import ExtendedRules.
Module Traditional := ExtendedRules.Traditional.
Import Traditional.
Module Proof := Proofs T ExtendedRules.
Import Proof.
Definition Extended := Proof.
Lemma traditional_extended {t t' : T} : Traditional t t' -> Extended t t'.
intro tr. induction tr as [ t t' con _ rec ]. apply (proof (traditional con)). assumption.
Qed.
Lemma refl (t : T) : Extended t t.
apply traditional_extended. apply Traditional.refl.
Qed.
Lemma trans {t1 t2 t3 : T} : Extended t1 t2 -> Extended t2 t3 -> Extended t1 t3.
intros id id'. apply (proof (traditional (Traditional.TransRefl.trans t1 t2 t3))). intro req. destruct req; assumption.
Qed.
End Extended.
This page has been generated by coqdoc