Alternative translate subtyping

Controled Splitting

If we propose an alternative subtyping rule on the translated system, which only allow one-layer of splits:

A << B1
A << B2
B1 <<| B |>> B2
--------------
A << B

Then for the recursive subtyping we must allow composition on the left:

C \subset A
mcod(C) << B
---------------
A << [ B ]

Then we are left to show

1. The new subtyping is equivalent to the current one
2. The rewriting is invertible (B1 <<| B |>> B2 is easier, but we need to reason with mcod(C) )

Theorem: (soundness of new translate subtyping)

If A ~~> A' and B ~~> B' and A' << B', then A <: B

Proof draft: by induction on B and invert on subtyping

Case: mu a. B' ~~> [B [a- |-> {a : B}]]

By inversion on A << [B [a- |-> {a : B}]]

1. A [a- |-> {a :A }] << B [a- |-> {a : B}] OK by nominal unfolding
2. (after the change): exists $C\subseteq A$, mcod(C) << B [a- |-> {a : B}]
   • mcod(C) is not invertible!
   • mcod(C) = (A1 [a- |-> {a : A1}] & A2 [a- |-> {a : A2}] ...
   • mcod(C) << (A1 & A2 & ... ) [a- |-> {a : A1 & A2 & ... }]
   • However, how can we ensure (A1 & A2 & ... ) [a- |-> {a : A1 & A2 & ... }] is still a subtype of B [a- |-> {a : B}]??

   We would like to prove a lemma like: exists invertible C, B << C, then we can case analysis on the weakly positiveness of Ai << T, if weakly positive, then Ai can be freely rewritten, otherwise, Ai itself can serve as the expected invertible C since B << Ai is obtained from negative subtyping

3. S-andl and S-andr : OK, since types are invertible
4. A << B1 [a- |-> {a : B}] and A << B2 [a- |-> {a : B}] … we look at the case where A << T [a- |-> {a : B}] where T is ordinary and part of B, what lemma are we looking for in this case?