Executable Specification

[View fsub.sig] [View fsub.mod]
sig fsub.

% Subtyping relation in Fsub

kind tp         type.
type top        tp.
type arr        tp -> tp -> tp.
type all        tp -> (tp -> tp) -> tp.

%type tp         tp -> o.
type sub        tp -> tp -> o.

module fsub.

% Subtyping relation in Fsub

sub T top.
sub (arr S1 S2) (arr T1 T2) :- sub T1 S1, sub S2 T2.
sub (all S1 S2) (all T1 T2) :- 
    sub T1 S1, 
    pi a\ 
      (pi U\ pi V\ sub a U => sub U V => sub a V) =>
      sub a T1 => 
      sub a a =>
        sub (S2 a) (T2 a).

Reasoning

[View fsub.thm]

Click on a command or tactic to see a detailed view of its use.

Specification "fsub".

% Proof of the transitivity of subtyping in Fsub

Define name : tp -> prop by
  nabla n, name n.

Define ctx : olist -> prop by
  ctx nil;
  nabla a, ctx ((sub a a) :: (sub a T) ::
       (pi U\ pi V\ sub a U => sub U V => sub a V) :: L) := ctx L.

Define tp : tp -> prop by
  tp top ;
  nabla x, tp x ;
  tp (arr T1 T2) := tp T1 /\ tp T2 ;
  tp (all T1 T2) := tp T1 /\ nabla x, tp (T2 x).

Theorem ctx_mem : forall L F,
  ctx L -> member F L -> exists A, name A /\
        ((F = sub A A) \/
         (exists T, F = sub A T) \/
         (F = pi U\ pi V\ sub A U => sub U V => sub A V)).

Theorem ctx_sync : forall A L T,
  ctx L -> member (sub A T) L -> 
    member (pi U\ pi V\ sub A U => sub U V => sub A V) L.
          
 
Theorem ctx_sub_name : forall L D G,
  ctx L -> member D L -> {L, [D] |- G} -> exists A T, G = sub A T /\ name A.

Theorem transitivity :
  forall L S Q T,
    ctx L -> tp Q -> {L |- sub S Q} -> {L |- sub Q T} -> {L |- sub S T}.