Declarative Subtyping (Tradition.v)

Given some user-defined subtyping rules as defined in Common.v, this module adds reflexivity and transitivity rules, and, based in them provides (straightforward) proofs of reflexivity and transitivity of the resulting subtyping relation Traditional. This corresponds to the definition of Declarative Subtyping in the paper.

Require Import Common.

Module Traditional (T : Typ) (Rule : Rules T).
Import T.

Module TransRefl <: Rules T.
Inductive TRCon : T -> T -> Type
:= refl (t : T) : TRCon t t
 | trans (t1 t2 t3 : T) : TRCon t1 t3
 | tcon (t t' : T) : Rule.Con t t' -> TRCon t t'.
Arguments tcon [t t'].
Definition Con := TRCon.
Definition Req : forall {t t' : T}, Con t t' -> Type
:= fun t t' con => match con with
                   | refl t => Empty
                   | trans t1 t2 t3 => Position
                   | tcon con => Rule.Req con
                   end.
Definition Ass : forall {t t' : T} {con : Con t t'}, Req con -> Position -> T
:= fun t t' con => match con as con in TRCon t t' return Req con -> Position -> T with
                   | refl t => fun req => match req with end
                   | trans t1 t2 t3 => fun req => match req with
                                                  | left => fun p => match p with left => t1 | right => t2 end
                                                  | right => fun p => match p with left => t2 | right => t3 end
                                                  end
                   | @tcon t t' con => @Rule.Ass t t' con
                   end.
End TransRefl.

Import TransRefl.
Module Proof := Proofs T TransRefl.
Import Proof.
Definition Traditional := Proof.

Lemma refl (t : T) : Traditional t t.
apply (proof (refl t)). intro req. destruct req.
Qed.
Lemma trans {t1 t2 t3 : T} : Traditional t1 t2 -> Traditional t2 t3 -> Traditional t1 t3.
intros p p'. apply (proof (trans t1 t2 t3)). intro req. destruct req; assumption.
Qed.

End Traditional.

This page has been generated by coqdoc