Commit a990090b authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

Replace the inductive subtyping relation by incusion because it has

better transitivity properties.
parent 47be8555
...@@ -43,7 +43,7 @@ def label := string. ...@@ -43,7 +43,7 @@ def label := string.
def type := dk_type.type. (; type := list (label * type) ;) def type := dk_type.type. (; type := list (label * type) ;)
def Ot_nil := dk_type.tnil. def Ot_nil := dk_type.tnil.
def Ot_cons := dk_type.tcons. def Ot_cons := dk_type.tcons.
def Ot_st := dk_type.st. def Ot_st := dk_type.sub.
def Ot_domain_subtype := dk_type.domain_subtype. def Ot_domain_subtype := dk_type.domain_subtype.
def pos := dk_type.pos. def pos := dk_type.pos.
...@@ -204,17 +204,18 @@ def coerce : A : type -> ...@@ -204,17 +204,18 @@ def coerce : A : type ->
select _ (coerce A B st a) select _ (coerce A B st a)
--> -->
(l : label => C : type => p : pos l C B => (l : label => C : type => p : pos l C B =>
select A a l C (dk_type.domain_subtype A B st l C p)). select A a l C (st l C p)).
[A,B,st,a] [A,B,st,a]
update _ (coerce A B st a) update _ (coerce A B st a)
--> -->
(l : label => C : type => p : pos l C B => m : (Expr B -> Expr C) => (l : label => C : type => p : pos l C B => m : (Expr B -> Expr C) =>
coerce A B st coerce A B st
(update A a l C (dk_type.domain_subtype A B st l C p) (update A a l C (st l C p)
(self : Expr A => (self : Expr A =>
m (coerce A B st self)))). m (coerce A B st self)))).
[A,B,C,stAB,stBC,a] [A,B,C,stAB,stBC,a]
coerce B C stBC (coerce A _ stAB a) coerce B C stBC (coerce A _ stAB a)
--> -->
coerce A C (dk_type.st_trans A B C stAB stBC) a. coerce A C (dk_type.sub_trans A B C stAB stBC) a.
...@@ -71,38 +71,57 @@ def st_cons_tail : A : type -> ...@@ -71,38 +71,57 @@ def st_cons_tail : A : type ->
[p] st_cons_pos _ _ _ _ (st_cons _ _ _ _ p _) --> p. [p] st_cons_pos _ _ _ _ (st_cons _ _ _ _ p _) --> p.
[Hst] st_cons_tail _ _ _ _ (st_cons _ _ _ _ _ Hst) --> Hst. [Hst] st_cons_tail _ _ _ _ (st_cons _ _ _ _ _ Hst) --> Hst.
def sub (A : type) (B : type) := l : label -> C : type -> pos l C B -> pos l C A.
def domain_subtype : A : type -> def domain_subtype : A : type ->
B : type -> B : type ->
Hst : st A B -> Hst : st A B ->
l : label -> sub A B.
C : type ->
pos l C B ->
pos l C A.
[A,l,A2,B2,Hst] [p]
domain_subtype A (tcons l A2 B2) Hst _ _ (at_head _ _ _) domain_subtype _ _ (st_cons _ _ _ _ p _) _ _ (at_head _ _ _)
--> -->
st_cons_pos A l A2 B2 Hst. p.
[A,l2,A2,B2,Hst,l,H,C] [A,B2,tl,l,H,C]
domain_subtype A (tcons l2 A2 B2) Hst l C (in_tail _ _ _ _ _ H) domain_subtype _ _ (st_cons A _ _ B2 _ tl) l C (in_tail _ _ _ _ _ H)
--> -->
domain_subtype A B2 (st_cons_tail A l2 A2 B2 Hst) l C H. domain_subtype A B2 tl l C H.
def st_trans : A : type -> def st_trans : A : type ->
B : type -> B : type ->
C : type -> C : type ->
stAB : st A B -> st A B ->
stBC : st B C -> st B C ->
st A C. st A C.
[A] st_trans A _ tnil _ _ --> st_nil A (; [A] st_trans A _ _ _ (st_nil _) --> st_nil A ;)
[A,B,stAB,lC,C1,C2,stBC] [A,B,stAB,lC,C1,C2,p,tl]
st_trans A B (tcons lC C1 C2) stAB stBC st_trans A _ _ stAB (st_cons B lC C1 C2 p tl)
--> -->
st_cons st_cons
A A
lC lC
C1 C1
C2 C2
(domain_subtype A B stAB lC C1 (st_cons_pos B lC C1 C2 stBC)) (domain_subtype A B stAB lC C1 p)
(st_trans A B C2 stAB (st_cons_tail B lC C1 C2 stBC)). (st_trans A B C2 stAB tl).
def sub_trans : A : type ->
B : type ->
C : type ->
sub A B ->
sub B C ->
sub A C.
[stAB,stBC,l,D,p,C]
sub_trans _ _ C stAB stBC -->
(l : label => (D : type => (p : pos l D C => stAB l D (stBC l D p)))).
(; [A,B,C,stAB,stBC,l,D,p] ;)
(; domain_subtype A C (st_trans _ B _ stAB stBC) l D p --> ;)
(; domain_subtype A B stAB l D (domain_subtype B C stBC l D p). ;)
(; [A,B,C,D,stAB,stBC,stCD] ;)
(; st_trans A B D stAB (st_trans _ C _ stBC stCD) --> st_trans A C D (st_trans A B C stAB stBC) stCD. ;)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment